The exponential function is continuous (iset.mm) (metamath#3746)

* Add efcn to iset.mm

Copied without change from set.mm

* Add sincn to iset.mm

The proof needs minor intuitionizing in a number of steps but is
basically the set.mm proof.

* Add coscn to iset.mm

Stated as in set.mm.  The proof needs intuitionizing in a number of
places but is basically the set.mm proof.

* Add reeff1olem and reeff1o to mmil.html

* Add reefiso , efcvx , and reefgim to mmil.html

* Add pilem1 to iset.mm

Copied from set.mm with the only change being to not have the comment
link to theorems we don't have yet.

* add pilem2 and pilem3 to mmil.html

* add pigt2lt4 , sinpi , and pire to mmil.html

iset.mm

@@ -142684,6 +142684,79 @@ S C_ ( P ( ball ` D ) T ) ) $=
   $}
 
 
+$(
+###############################################################################
+  BASIC REAL AND COMPLEX FUNCTIONS
+###############################################################################
+$)
+
+
+$(
+#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
+  Basic trigonometry
+#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
+$)
+
+
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  The exponential, sine, and cosine functions (cont.)
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  $( The exponential function is continuous.  (Contributed by Paul Chapman,
+     15-Sep-2007.)  (Revised by Mario Carneiro, 20-Jun-2015.) $)
+  efcn $p |- exp e. ( CC -cn-> CC ) $=
+    ( cc wss ce wf ccncf co wcel ssid eff w3a cdv cdm wceq dvef feq1i fdmi dvcn
+    mpbir mpan2 mp3an ) AABZAACDZUACAAEFGZAHZIUDUAUBUAJACKFZLAMUCAAUEAAUEDUBIAA
+    UECNORPAACQST $.
+
+  ${
+    $d x y $.
+    $( Sine is continuous.  (Contributed by Paul Chapman, 28-Nov-2007.)
+       (Revised by Mario Carneiro, 3-Sep-2014.) $)
+    sincn $p |- sin e. ( CC -cn-> CC ) $=
+      ( vx vy cc ci cv cmul co cfv cmin cdiv cmpt wcel wtru ccom eqid mulc1cncf
+      ce a1i mp1i cncfmpt1f csin cneg c2 ccncf df-sin wral cmopn ctx subcncntop
+      wf cabs ccn efcn ax-icn negicn cncfmpt2fcntop cncff syl fmpt sylibr eqidd
+      oveq1 fmptcof cc0 cap wbr 2muliap0 divccncfap mp2an cncfco eqeltrrd mptru
+      2mulicn eqeltri ) UAACDAEZFGZQHZDUBZVOFGZQHZIGZUCDFGZJGZKZCCUDGZAUEWDWELM
+      BCBEZWBJGZKZACWAKZNWDWEMABCCWAWGWCWIWHMCCWIUJZWACLACUFMWIWELWJMAVQVTIUKIN
+      UGHZCWKOZIWKWKUHGWKULGLMWKWLUIRMAVPQCQWELMUMRZDCLACVPKZWELMUNADWNWNOPSTMA
+      VSQCWMVRCLACVSKZWELMUOAVRWOWOOPSTUPZCCWIUQURACCWAWIWIOUSUTMWIVAMWHVAWFWAW
+      BJVBVCMCCCWIWHWPWHWELZMWBCLWBVDVEVFWQVMVGBWBWHWHOVHVIRVJVKVLVN $.
+
+    $( Cosine is continuous.  (Contributed by Paul Chapman, 28-Nov-2007.)
+       (Revised by Mario Carneiro, 3-Sep-2014.) $)
+    coscn $p |- cos e. ( CC -cn-> CC ) $=
+      ( vx vy cc ci cv cmul co ce caddc cdiv cmpt wcel wtru ccom eqid mulc1cncf
+      cfv c2 a1i mp1i ccos cneg ccncf df-cos wf wral cabs cmin cmopn addcncntop
+      ctx ccn efcn ax-icn cncfmpt1f negicn cncfmpt2fcntop cncff syl fmpt sylibr
+      eqidd oveq1 fmptcof cc0 cap wbr 2cn 2ap0 divccncfap mp2an cncfco eqeltrrd
+      mptru eqeltri ) UAACDAEZFGZHQZDUBZVPFGZHQZIGZRJGZKZCCUCGZAUDWDWELMBCBEZRJ
+      GZKZACWBKZNWDWEMABCCWBWGWCWIWHMCCWIUEZWBCLACUFMWIWELWJMAVRWAIUGUHNUIQZCWK
+      OZIWKWKUKGWKULGLMWKWLUJSMAVQHCHWELMUMSZDCLACVQKZWELMUNADWNWNOPTUOMAVTHCWM
+      VSCLACVTKZWELMUPAVSWOWOOPTUOUQZCCWIURUSACCWBWIWIOUTVAMWIVBMWHVBWFWBRJVCVD
+      MCCCWIWHWPWHWELZMRCLRVEVFVGWQVHVIBRWHWHOVJVKSVLVMVNVO $.
+  $}
+
+
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Properties of pi = 3.14159...
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  $( Lemma for pire , pigt2lt4 and sinpi .  (Contributed by Mario Carneiro,
+     9-May-2014.) $)
+  pilem1 $p |- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <->
+                 ( A e. RR+ /\ ( sin ` A ) = 0 ) ) $=
+    ( crp csin ccnv cc0 csn cima cin wcel wa cfv wceq elin cc rpcn biantrurd wf
+    wfn wb sinf ffn fniniseg mp2b syl6rbbr pm5.32i bitri ) ABCDEFGZHIABIZAUGIZJ
+    UHACKELZJABUGMUHUIUJUHUJANIZUJJZUIUHUKUJAOPNNCQCNRUIULSTNNCUANEACUBUCUDUEUF
+    $.
+
+
 $(
 ###############################################################################
   GUIDES AND MISCELLANEA

mmil.raw.html

@@ -11186,6 +11186,77 @@
   <td>~ dvmptsubcn</td>
 </tr>
 
+<tr>
+  <td>reeff1olem</td>
+  <td><i>none</i></td>
+  <td>The set.mm proof depends on ivth (the Intermediate
+  Value Theorem).  Apparently, the Monotonic Intermediate
+  Value Theorem (Theorem 5.5 of [Bauer], p. 494) would
+  suffice if we can prove that.</td>
+</tr>
+
+<tr>
+  <td>reeff1o</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses reeff1olem</td>
+</tr>
+
+<tr>
+  <td>reefiso</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses reeff1o and the converse of
+  ~ efltim</td>
+</tr>
+
+<tr>
+  <td>efcvx</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses reeff1o , reefiso , dvres , dvres3 ,
+  iccntr , and dvcvx</td>
+</tr>
+
+<tr>
+  <td>reefgim</td>
+  <td><i>none</i></td>
+</tr>
+
+<tr>
+  <td>pilem2</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof needs some obvious intuitionizing around not
+  equal to zero versus apart from zero, and nonempty versus
+  inhabited, but more seriously it depends on infrecl , infregelb ,
+  and infrelb</td>
+</tr>
+
+<tr>
+  <td>pilem3</td>
+  <td><i>none</i></td>
+  <td>The set.mm proof depends on ivth2 (the Intermediate
+  Value Theorem).  Apparently, the Monotonic Intermediate
+  Value Theorem (Theorem 5.5 of [Bauer], p. 494) could
+  replace it if we can prove that.  Additionally, the set.mm
+  proof uses infrelb , infrecl , pilem2 , and infregelb .</td>
+</tr>
+
+<tr>
+  <td>pigt2lt4</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses pilem3</td>
+</tr>
+
+<tr>
+  <td>sinpi</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses pilem3</td>
+</tr>
+
+<tr>
+  <td>pire</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses pilem3</td>
+</tr>
+
 </TABLE>
 
 <HR NOSHADE SIZE=1><A NAME="bib"></A><B><FONT