Add divcnap to iset.mm

This is divcn from set.mm with a change in notation for the topology on
the complex numbers, and replacing not equal with apart.

Author: jkingdon

iset.mm

@@ -139341,6 +139341,43 @@ S C_ ( P ( ball ` D ) T ) ) $=
     mulcncntop $p |- x. e. ( ( J tX J ) Cn J ) $=
       ( vy vz vv vu va vb vc cmul ax-mulf cv mulcn2 addcncntoplem ) CDEFJAGHIBK
       CDEFGLHLILMN $.
+
+    $d .+ a b c u v x y z $.  $d J a b c u v w x y z $.
+    $d J a b q u w x y z $.  $d K a b q u w x y z $.
+    divcnap.k $e |- K = ( J |`t { x e. CC | x =//= 0 } ) $.
+    $( Complex number division is a continuous function, when the second
+       argument is apart from zero.  (Contributed by Mario Carneiro,
+       12-Aug-2014.)  (Revised by Jim Kingdon, 25-Oct-2023.) $)
+    divcnap $p |- ( y e. CC , z e. { x e. CC | x =//= 0 } |-> ( y / z ) )
+        e. ( ( J tX K ) Cn J ) $=
+      ( cc cv cc0 cap wbr cdiv co c1 wcel wa wtru cfv clt vq va vw vu crab cmpo
+      vb cmul ctx ccn wceq breq1 elrab divrecap 3expb sylan2b ctopon cntoptopon
+      mpoeq3ia a1i wss ssrab2 resttopon sylancl syl5eqel cnmpt1st cnmpt2nd cmpt
+      crest wf cabs cmin ccom cxp cres wi wral crp wrex recclap sylbi fmpti cpr
+      eqid cr cinf c2 reccn2ap 3expa sylanb ovres elrabi cnmetdval abssub eqtrd
+      wb syl2an breq1d simprbi recclapd oveq2 fvmptg oveqan12d imbi12d ralbidva
+      mpdan rexbidv adantr mpbird rgen2 cxmet cnxmet xmetres2 mp2an cmopn eqtri
+      metrest metcn mpbir2an cnmpt21 mulcncntop cnmpt22f mptru eqeltri ) BCHAIZ
+      JKLZAHUEZBIZCIZMNZUFBCHYGYHOYIMNZUHNZUFZDEUINDUJNZBCHYGYJYLYIYGPYHHPZYIHP
+      ZYIJKLZQYJYLUKZYFYQAYIHYEYIJKULUMYOYPYQYRYHYIUNUOUPUSYMYNPRBCYHYKUHDEDDDH
+      YGDHUQSPZRDFURUTZREDYGVINZYGUQSZGRYSYGHVAZUUAUUBPYTYFAHVBZYGDHVCVDVEZRBCD
+      EHYGYTUUEVFRBCUAYIOUAIZMNZYKDEEDHYGYGYTUUERBCDEHYGYTUUEVGUUEUAYGUUGVHZEDU
+      JNPZRUUIYGHUUHVJZUBIZUCIZVKVLVMZYGYGVNVOZNZUDIZTLZUUKUUHSZUULUUHSZUUMNZUG
+      IZTLZVPZUCYGVQZUDVRVSZUGVRVQUBYGVQZUAYGHUUGUUHUUHWDZUUFYGPUUFHPUUFJKLZQUU
+      GHPYFUVHAUUFHYEUUFJKULUMUUFVTWAWBUVEUBUGYGVRUUKYGPZUVAVRPZQUVEUULUUKVLNVK
+      SZUUPTLZOUULMNZOUUKMNZVLNVKSZUVATLZVPZUCYGVQZUDVRVSZUVIUUKHPZUUKJKLZQUVJU
+      VSYFUWAAUUKHYEUUKJKULUMZUVTUWAUVJUVSUDUCAUUKUVAOUUKVKSZUVAUHNWCWETWFUWCWG
+      MNUHNZUWDWDWHWIWJUVIUVEUVSWPUVJUVIUVDUVRUDVRUVIUVCUVQUCYGUVIUULYGPZQZUUQU
+      VLUVBUVPUWFUUOUVKUUPTUWFUUOUUKUULUUMNZUVKUUKUULYGYGUUMWKUVIUVTUULHPZUWGUV
+      KUKUWEYFAUUKHWLZYFAUULHWLZUVTUWHQUWGUUKUULVLNVKSUVKUUKUULUUMUUMWDZWMUUKUU
+      LWNWOWQWOWRUWFUUTUVOUVATUWFUUTUVNUVMUUMNZUVOUVIUWEUURUVNUUSUVMUUMUVIUVNHP
+      ZUURUVNUKUVIUUKUWIUVIUVTUWAUWBWSWTZUAUUKUUGUVNYGHUUHUUFUUKOMXAUVGXBXFUWEU
+      VMHPZUUSUVMUKUWEUULUWJUWEUWHUULJKLZYFUWPAUULHYEUULJKULUMWSWTZUAUULUUGUVMY
+      GHUUHUUFUULOMXAUVGXBXFXCUVIUWMUWOUWLUVOUKUWEUWNUWQUWMUWOQUWLUVNUVMVLNVKSU
+      VOUVNUVMUUMUWKWMUVNUVMWNWOWQWOWRXDXEXGXHXIXJUUNYGXKSPZUUMHXKSPZUUIUUJUVFQ
+      WPUWSUUCUWRXLUUDUUMYGHXMXNXLUBUGUDUCUUNUUMUUHEDYGHEUUAUUNXOSZGUWSUUCUUAUW
+      TUKXLUUDUUMUUNDUWTHYGUUNWDFUWTWDXQXNXPFXRXNXSUTUUFYIOMXAXTUHDDUINDUJNPRDF
+      YAUTYBYCYD $.
   $}
 
 

mmil.raw.html

@@ -10719,8 +10719,7 @@
 
 <tr>
   <td>divcn</td>
-  <td><i>none</i></td>
-  <td>the set.mm proof uses mulcn</td>
+  <td>~ divcnap</td>
 </tr>
 
 <tr>