From de462036acd8c03f551b15a6f16ec35810a4fa7b Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 7 Jan 2024 10:50:32 -0800 Subject: [PATCH] The exponential function is continuous (iset.mm) (#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 | 73 +++++++++++++++++++++++++++++++++++++++++++++++++++ mmil.raw.html | 71 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 144 insertions(+) diff --git a/iset.mm b/iset.mm index b8f0d204f6..22e93c6e6c 100644 --- a/iset.mm +++ b/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 diff --git a/mmil.raw.html b/mmil.raw.html index 79c4cdf7f5..d6f5aef5be 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11186,6 +11186,77 @@ ~ dvmptsubcn + + reeff1olem + none + 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. + + + + reeff1o + none + the set.mm proof uses reeff1olem + + + + reefiso + none + the set.mm proof uses reeff1o and the converse of + ~ efltim + + + + efcvx + none + the set.mm proof uses reeff1o , reefiso , dvres , dvres3 , + iccntr , and dvcvx + + + + reefgim + none + + + + pilem2 + none + 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 + + + + pilem3 + none + 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 . + + + + pigt2lt4 + none + the set.mm proof uses pilem3 + + + + sinpi + none + the set.mm proof uses pilem3 + + + + pire + none + the set.mm proof uses pilem3 + +