diff --git a/changes-set.txt b/changes-set.txt index 1f837dcccf..563ea35cfc 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -78,12 +78,12 @@ proposed syl6eqss eqsstrdi compare to eqsstri or eqsstrd proposed syl6eqssr eqsstrrdi compare to eqsstrri or eqsstrrd proposed syl6eqbr eqbrtrdi compare to eqbrtri or eqbrtrd proposed syl6eqbrr eqbrtrrdi compare to eqbrtrri or eqbrtrrd -proposed syl6breq breqtrdi compare to breqtri or breqtrd (Please send any comments on these proposals to the mailing list or make a github issue.) DONE: Date Old New Notes +28-Dec-23 syl6breq breqtrdi compare to breqtri or breqtrd 26-Dec-23 syl6breqr breqtrrdi compare to breqtrri or breqtrrd 25-Dec-23 prth anim12 25-Dec-23 selpw velpw diff --git a/iset.mm b/iset.mm index 427361428c..d2235c6064 100644 --- a/iset.mm +++ b/iset.mm @@ -34340,11 +34340,11 @@ same disjoint variable group (meaning ` A ` cannot depend on ` x ` ) and $} ${ - syl6breq.1 $e |- ( ph -> A R B ) $. - syl6breq.2 $e |- B = C $. + breqtrdi.1 $e |- ( ph -> A R B ) $. + breqtrdi.2 $e |- B = C $. $( A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) $) - syl6breq $p |- ( ph -> A R C ) $= + breqtrdi $p |- ( ph -> A R C ) $= ( eqid 3brtr3g ) ABCBDEFBHGI $. $} @@ -34354,7 +34354,7 @@ same disjoint variable group (meaning ` A ` cannot depend on ` x ` ) and $( A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) $) breqtrrdi $p |- ( ph -> A R C ) $= - ( eqcomi syl6breq ) ABCDEFDCGHI $. + ( eqcomi breqtrdi ) ABCDEFDCGHI $. $} ${ @@ -69327,7 +69327,7 @@ elements or fails to hold (is equal to ` (/) ` ) for some element. and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.) $) en2eleq $p |- ( ( X e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } ) $= ( wcel c2o cen wbr csn cdif cuni wne cpr wceq c1o com csuc 1onn simpr df-2o - wa syl6breq simpl dif1en mp3an2i en1uniel syl sylib simprd necomd wi simpld + wa breqtrdi simpl dif1en mp3an2i en1uniel syl sylib simprd necomd wi simpld eldifsn en2eqpr syl3anc mpd ) BACZADEFZSZBABGHZIZJZABUSKLZUQUSBUQUSACZUSBJZ UQUSURCZVBVCSUQURMEFZVDMNCUQAMOZEFUOVEPUQADVFEUOUPQZRTUOUPUAZAMBUBUCURUDUEU SABUKUFZUGUHUQUPUOVBUTVAUIVGVHUQVBVCVIUJBUSAULUMUN $. @@ -69337,7 +69337,7 @@ elements or fails to hold (is equal to ` (/) ` ) for some element. en2other2 $p |- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = X ) $= ( wcel c2o cen wbr csn cdif cuni cpr en2eleq prcom syl6eq difeq1d difprsnss - wa syl6eqss wne simpl c1o com csuc 1onn simpr df-2o syl6breq dif1en syl3anc + wa syl6eqss wne simpl c1o com csuc 1onn simpr df-2o breqtrdi dif1en syl3anc a1i en1uniel eldifsni 3syl necomd eldifsn sylanbrc snssd unieqd wceq unisng eqssd adantr eqtrd ) BACZADEFZPZAABGZHZIZGZHZIVFIZBVEVJVFVEVJVFVEVJVHBJZVIH VFVEAVLVIVEABVHJVLABKBVHLMNVHBOQVEBVJVEVCBVHRBVJCVCVDSZVEVHBVEVGTEFZVHVGCVH @@ -69673,7 +69673,7 @@ Similar to the Axiom of Choice (first form) of [Enderton] p. 49. of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) $) dju0en $p |- ( A e. V -> ( A |_| (/) ) ~~ A ) $= - ( wcel cdju cun cen cvv cin wceq wbr 0ex in0 endjudisj mp3an23 un0 syl6breq + ( wcel cdju cun cen cvv cin wceq wbr 0ex in0 endjudisj mp3an23 un0 breqtrdi c0 ) ABCZAQDZAQEZAFRQGCAQHQISTFJKALAQBGMNAOP $. $( Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. @@ -113291,7 +113291,7 @@ A Cauchy sequence (as defined here, which has a rate of convergence $( The maximum of two reals is no smaller than the second real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.) $) maxle2 $p |- ( ( A e. RR /\ B e. RR ) -> B <_ sup ( { A , B } , RR , < ) ) $= - ( cr wcel wa cpr clt csup cle wbr maxle1 ancoms maxcom syl6breq ) ACDZBCDZE + ( cr wcel wa cpr clt csup cle wbr maxle1 ancoms maxcom breqtrdi ) ACDZBCDZE BBAFCGHZABFCGHIPOBQIJBAKLBAMN $. ${ @@ -113951,7 +113951,7 @@ A Cauchy sequence (as defined here, which has a rate of convergence 30-Apr-2023.) $) xrmax2sup $p |- ( ( A e. RR* /\ B e. RR* ) -> B <_ sup ( { A , B } , RR* , < ) ) $= - ( cxr wcel wa cpr clt csup cle wbr xrmax1sup ancoms prcom supeq1i syl6breq + ( cxr wcel wa cpr clt csup cle wbr xrmax1sup ancoms prcom supeq1i breqtrdi ) ACDZBCDZEBBAFZCGHZABFZCGHIQPBSIJBAKLCRTGBAMNO $. $( The maximum of two real numbers is the same when taken as extended reals @@ -120308,7 +120308,7 @@ Infinite sums (cont.) rexbidv elab2g mpbird letrd nn0ex mptex biimpri syl2an2 readdcl seq3feq 1nn0 recnd serf0 climi0 fveq2i oveq1i oveq2i breq2i ralbii sylib absidd cbvsumv sumeq2i rspccva nfv nfsum1 nfbr cbvral syl6bbr eqeltrrid biimpi - syl6breq csb nfcsb1v nfeq2 csbeq1a nfel1 eqeq2i abbii mertenslemi1 expr + breqtrdi csb nfcsb1v nfeq2 csbeq1a nfel1 eqeq2i abbii mertenslemi1 expr eqtri ex syl5bir expdimp ) AJULZUMNUNUOZUPZUQFIURZUSUTVAUPZLUUMVBUTZUQH ULZPUPZHURZVFUMUTZVBUTZVCVDZJQULZVGUPZVEZQVHVIUNUYIVJUTZEUYIUYOUSUTVFUM UTVGUPFIURVKUTHURVAUPLVCVDJCULZVGUPVECUQVIZAUYLUYKUYSQJUYJVFVHVLAVMZAUY @@ -120756,7 +120756,7 @@ Infinite sums (cont.) eqtr4i df-e breqtrrdi cn clt nnred nngt0d 1re 0le1 divge0 mpanl12 syl2anc breqtrrd climserle eqbrtrrd mptru cmin nnuz 1zzd recnd 0p1e1 seqeq1 ax-mp clim2ser oveq2i 3brtr3g cmul 2cnd halfre id reexpcld eqid reexpcl sylancr - oveq2 simpr cabs 1lt2 mp2an breqtrri 2m1e1 eqtri syl6breq sylan2 nnrpd + oveq2 simpr cabs 1lt2 mp2an breqtrri 2m1e1 eqtri breqtrdi sylan2 nnrpd 2re 0le2 absid georeclim 2cn halfcn exp0 eqeltri nnnn0 remulcld isermulc2 eqtr4d 2t1e2 remulcl faclbnd2 nnexpcl rphalfcld lerecd mpbid nncnd nnap0d 2nn divrecapd cap 2ap0 recdivapd exprecapd 3eqtr4rd 3brtr4d ere lesubaddi @@ -122139,7 +122139,7 @@ Infinite sums (cont.) cioc cexp cmin ccos cfv wceq cxr w3a 0xr elioc2 mp2an simp1bi resqcld recnd cap 2cn 3cn pm3.2i div12ap mp3an13 syl cz 2z expgt0 3adant3 sylbi 2lt3 3pos mp3an2 ltdiv1ii dividapi breqtri redivclapi mp3an12 syl2anc mulid1d breqtrd - mpbi ltmul2 mpbii eqbrtrd wi 0re ltle mpan imdistani le2sq2 mpanr1 syl6breq + mpbi ltmul2 mpbii eqbrtrd wi 0re ltle mpan imdistani le2sq2 mpanr1 breqtrdi stoic3 redivclap mp3an23 remulcl sylancr ltletr mp3an3 mp2and sylancl mpbid sq1 posdif cos01bnd simpld resubcl recoscld lttr mp3an2i ) ABCUADEZBCFAFUBD ZGHDZIDZUCDZJKZXLAUDUEZJKZBXNJKZXHXKCJKZXMXHXKXIJKZXICLKZXQXHXKXIFGHDZIDZXI @@ -122158,7 +122158,7 @@ Infinite sums (cont.) ( cc0 c2 cioc co wcel cmul csin cfv clt cr wbr cle wb 2re syl c1 wa 2pos cc cdiv ccos w3a cxr 0xr elioc2 mp2an rehalfcl 3ad2ant1 sylbi resincl remulcld recoscl divgt0 mpanr12 3adant3 pm3.2i lediv1 mp3an23 biimpa 2div2e1 3adant2 - syl6breq 3jca 1re 3imtr4i sin01gt0 cos01gt0 wi axmulgt0 syl2anc mp2and mpan + breqtrdi 3jca 1re 3imtr4i sin01gt0 cos01gt0 wi axmulgt0 syl2anc mp2and mpan mpani sylc wceq recnd sin2t breqtrrd simp1bi cap 2cn 2ap0 divcanap2 breqtrd fveq2d ) ABCDEFZBCACUAEZGEZHIZAHIJWGBCWHHIZWHUBIZGEZGEZWJJWGWMKFZBWMJLZBWNJ LZWGWHKFZWOWGAKFZBAJLZACMLZUCZWRBUDFZCKFZWGXBNUEOBCAUFUGZWSWTWRXAAUHUIZUJZW @@ -129234,7 +129234,7 @@ reduced fraction representation (no common factors, denominator ( vz cn cen wbr cin c0 wceq cun c2 wn crab ensymi entr mpan2 wa wo wcel cz w3a cv cdvds oddennn 3ad2ant1 evenennn 3ad2ant2 simp3 inrab wral ancom pm3.24 mtbi rgenw rabeq0 mpbir eqtri a1i syl22anc unrab rabid2 wdc nnz 2z - unen zdvdsdc mpan exmiddc 3syl orcomd mprgbir eqtr4i syl6breq ) ADEFZBDEF + unen zdvdsdc mpan exmiddc 3syl orcomd mprgbir eqtr4i breqtrdi ) ADEFZBDEF ZABGHIZUAZABJZKCUBZUCFZLZCDMZVTCDMZJZDEVQAWBEFZBWCEFZVPWBWCGZHIZVRWDEFVNV OWEVPVNDWBEFWEWBDCUDNADWBOPUEVOVNWFVPVODWCEFWFWCDCUFNBDWCOPUGVNVOVPUHWHVQ WGWAVTQZCDMZHWAVTCDUIWJHIWILZCDUJWKCDVTWAQWIVTULVTWAUKUMUNWICDUOUPUQURAWB @@ -148186,7 +148186,7 @@ Limited Principle of Omniscience (LPO) implies excluded middle, so we eqeltrd iserex mpbid isumrecl cvv wbr seqex ax-1cn geo2lim ax-mp adantr cle eqbrtrd wo elpri breqtrrd breldmg mp3an rpge0d mulid1d leidd fsumle mpjaodan rpgt0d leltaddd trilpolemisumle ltleaddd eqbrtrid ltned neneqd - geoihalfsum syl6breq pm2.65da ffvelrnda orcomd ecased ralrimiva ) ABUAZ + geoihalfsum breqtrdi pm2.65da ffvelrnda orcomd ecased ralrimiva ) ABUAZ EJZKUDZBLAUVBLMZVJZUVDUVCNUDZUVFUVGCKUDZAUVHUVEUVGHUBUVFUVGVJZCKUVICKAC OMUVEUVGACDEFGUCUBUVICLKPDUAZUEQZUFQZDRZKUGUVICKUVBUHQZUVLDRZUVBKSQZUIJ ZUVLDRZSQZUVMUGUVICKUVBUJQZUVBUKULZUVLDRZUVRSQZUVSUGUVICUVTUVLDRZKPUVBU diff --git a/set.mm b/set.mm index 95b616b3bc..b984701a86 100644 --- a/set.mm +++ b/set.mm @@ -46065,11 +46065,11 @@ proper class (see for example ~ iprc ). (Contributed by NM, $} ${ - syl6breq.1 $e |- ( ph -> A R B ) $. - syl6breq.2 $e |- B = C $. + breqtrdi.1 $e |- ( ph -> A R B ) $. + breqtrdi.2 $e |- B = C $. $( A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.) $) - syl6breq $p |- ( ph -> A R C ) $= + breqtrdi $p |- ( ph -> A R C ) $= ( eqid 3brtr3g ) ABCBDEFBHGI $. $} @@ -46079,7 +46079,7 @@ proper class (see for example ~ iprc ). (Contributed by NM, $( A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.) $) breqtrrdi $p |- ( ph -> A R C ) $= - ( eqcomi syl6breq ) ABCDEFDCGHI $. + ( eqcomi breqtrdi ) ABCDEFDCGHI $. $} ${ @@ -84492,7 +84492,7 @@ the first case of his notation (simple exponentiation) and subscript it difsnen $p |- ( ( X e. V /\ A e. X /\ B e. X ) -> ( X \ { A } ) ~~ ( X \ { B } ) ) $= ( wcel csn cdif cen wbr wceq cvv difexg enrefg syl wne cun c0 incom disjdif - cin w3a 3ad2ant1 sneq difeq2d breq2d syl5ibcom imp wa simpl1 dif32 syl6breq + cin w3a 3ad2ant1 sneq difeq2d breq2d syl5ibcom imp wa simpl1 dif32 breqtrdi 4syl simpl3 simpl2 en2sn syl2anc eqtri unen syl22anc simpr eldifsn sylanbrc a1i necomd difsnid 3brtr3d pm2.61dane ) DCEZADEZBDEZUAZDAFZGZDBFZGZHIZABVKA BJZVPVKVMVMHIZVQVPVHVIVRVJVHVMKEZVRDVLCLZVMKMNUBVQVMVOVMHVQVLVNDABUCUDUEUFU @@ -88846,7 +88846,7 @@ intersections of elements of the argument (see ~ elfi2 ). (Contributed sstri inex1 ad2antll spcv sylancr cop elimasn snssd ad2ant2lr f1osn eqtri sstrid f1oun wb snssi undif f1oeq2d f1of1 ssv f1ss ex expd syl5bi exanali cres simprll pssss sspwb simplrr ssralv resima2 eqcomd ralbiia ssres inxp - simplrl df-res xpss12 eqsstri resex imaundi undif2 syl6breq simp-4l ssfid + simplrl df-res xpss12 eqsstri resex imaundi undif2 breqtrdi simp-4l ssfid eqtr4i cen bren2 sylanbrc ensymd ssdifin0 domunfican syl6eq biimpar disj4 neeq1d bicomi necon1abii resss syl6sseqr mp2d sylan2br pm2.61dan ralrimiv df-ima imp exp32 exp31 a2d findcard3 ) CUIZUJFZEUIZDUIZVUCUBZGHZEUAUIZIZJ @@ -96909,7 +96909,7 @@ several of their earlier lemmas available (which would otherwise be and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.) $) en2eleq $p |- ( ( X e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } ) $= ( wcel c2o cen wbr wa csn cdif cuni cpr cfn wss wceq com adantl wne syl3anc - 2onn c1o nnfi ax-mp enfi mpbiri simpl csuc 1onn simpr df-2o syl6breq dif1en + 2onn c1o nnfi ax-mp enfi mpbiri simpl csuc 1onn simpr df-2o breqtrdi dif1en mp3an2i en1uniel syl eldifsn sylib simpld prssd simprd necomd pr2nelem entr ensym syl2anc fisseneq eqcomd ) BACZADEFZGZBABHIZJZKZAVIALCZVLAMVLAEFZVLANV HVMVGVHVMDLCZDOCVOSDUAUBADUCUDPVIBVKAVGVHUEZVIVKACZVKBQZVIVKVJCZVQVRGVIVJTE @@ -96922,7 +96922,7 @@ several of their earlier lemmas available (which would otherwise be en2other2 $p |- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = X ) $= ( wcel c2o cen wbr csn cdif cuni cpr en2eleq prcom syl6eq difeq1d difprsnss - wa syl6eqss wne simpl c1o com csuc 1onn simpr df-2o syl6breq dif1en mp3an2i + wa syl6eqss wne simpl c1o com csuc 1onn simpr df-2o breqtrdi dif1en mp3an2i en1uniel eldifsni 3syl necomd eldifsn snssd eqssd unieqd wceq unisng adantr sylanbrc eqtrd ) BACZADEFZPZAABGZHZIZGZHZIVEIZBVDVIVEVDVIVEVDVIVGBJZVHHVEVD AVKVHVDABVGJVKABKBVGLMNVGBOQVDBVIVDVBBVGRBVICVBVCSZVDVGBVDVFTEFZVGVFCVGBRTU @@ -99816,7 +99816,7 @@ Because we use a disjoint union for cardinal addition (as explained in the of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) $) dju0en $p |- ( A e. V -> ( A |_| (/) ) ~~ A ) $= - ( wcel cdju cun cen cvv cin wceq wbr 0ex in0 endjudisj mp3an23 un0 syl6breq + ( wcel cdju cun cen cvv cin wceq wbr 0ex in0 endjudisj mp3an23 un0 breqtrdi c0 ) ABCZAQDZAQEZAFRQGCAQHQISTFJKALAQBGMNAOP $. $( Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. @@ -99983,7 +99983,7 @@ Because we use a disjoint union for cardinal addition (as explained in the pwdju1 $p |- ( A e. V -> ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) ) $= ( wcel c1o cdju cpw cxp cen wbr con0 pwdjuen mpan2 pwexg 1oex pwex xpcomeng 1on cvv c2o c0 sylancl entr syl2anc csn cpr pwpw0 df1o2 pweqi df2o2 3eqtr4i - xpeq1i xp2dju eqtri syl6breq ensymd ) ABCZADEFZAFZUREZUPUQDFZURGZUSHUPUQURU + xpeq1i xp2dju eqtri breqtrdi ensymd ) ABCZADEFZAFZUREZUPUQDFZURGZUSHUPUQURU TGZHIZVBVAHIZUQVAHIUPDJCVCQADBJKLUPURRCUTRCVDABMDNOURUTRRPUAUQVBVAUBUCVASUR GUSUTSURTUDZFTVEUEUTSUFDVEUGUHUIUJUKURULUMUNUO $. @@ -100273,7 +100273,7 @@ Because we use a disjoint union for cardinal addition (as explained in the pwdjudom $p |- ( ~P ( A |_| A ) ~<_ ( A |_| B ) -> ~P A ~<_ B ) $= ( cdju cpw cdom wbr c1o csn cxp cen cwdom cvv wcel xpsnen2g sylancr syl2anc c0 wn syl con0 canthwdom wi 0ex reldom brrelex2i djuexb sylibr simpld endom - wa domwdom wdomtr expcom 4syl mtoi cun wo wb pwdjuen domen1 df-dju syl6breq + wa domwdom wdomtr expcom 4syl mtoi cun wo wb pwdjuen domen1 df-dju breqtrdi ibi unxpwdom ord mpd 1on simprd domentr ) AACDZABCZEFZADZGHBIZEFZVNBJFZVMBE FVLVMQHAIZKFZRVOVLVRVMAKFZAUAVLVQAJFZVQAEFVQAKFZVRVSUBVLQLMALMZVTUCVLWBBLMZ VLVKLMWBWCUJVJVKEUDUEABUFUGZUHZQALLNOVQAUIVQAUKVRWAVSVMVQAULUMUNUOVLVRVOVLV @@ -100381,7 +100381,7 @@ Because we use a disjoint union for cardinal addition (as explained in the ( com wcel cpw ccrd cfv cdju cen wbr wceq c2o cxp cmap pw2eng syl cvv a1i co entr syl2anc csuc coa peano2 csn cun df-suc oveq2i cin elex snex elexi c0 2onn word nnord orddisj mapunen syl31anc ovex enref con0 mapsnend xpen - 2on sylancr eqbrtrid xpcomen sylancl ensymd xp2dju syl6breq cfn nnfi pwfi + 2on sylancr eqbrtrid xpcomen sylancl ensymd xp2dju breqtrdi cfn nnfi pwfi id sylib ficardid djuen carden2b ficardom nnadju eqtrd ) ABCZAUAZDZEFZADZ EFZWHGZEFZWHWHUBRZWCWEWIHIZWFWJJWCWEWGWGGZHIWMWIHIWLWCWEKWGLZWMHWCWEKWDMR ZHIZWOWNHIZWEWNHIWCWDBCWPAUCWDBNOWCWOKKAMRZLZHIZWSWNHIWQWCWOWRKLZHIXAWSHI @@ -106756,7 +106756,7 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this fvex djuex cdm wfn alephfnon fndm eleq2i notbii csn c1o xpundir xp0 3eqtr2i df-dju ndmfv djueq12 syl2an adantr adantl uneq12d un0 syl6eq syl2anbr eqeng 3eqtr4a mpsyl ex wss alephgeom cdom wi ssdomg alephon onenon infdju mp3an12 - ccrd syl sylbi djucomen entr sylancr uncom syl6breq pm2.61ii ) ACDZBCDZAEFZ + ccrd syl sylbi djucomen entr sylancr uncom breqtrdi pm2.61ii ) ACDZBCDZAEFZ BEFZGZWGWHHZIJZWEKZWFKZWKWILDZWLWMMWIWJNZWKWGLDZWHLDZWNAETZBETZWGWHLLUAOWLA EUBZDZKZBWTDZKZWOWMXAWEWTCAECUCWTCNUDCEUEPZUFUGXCWFWTCBXEUFUGXBXDMZQQGZQWIW JXGQUHZQRUIUHZQRHXHXIHZQRQQQUMXHXIQUJXJUKULXBWGQNZWHQNZWIXGNXDAEUNZBEUNZWGQ @@ -113541,7 +113541,7 @@ divided by the argument (although we don't define full division since we n0 cfv simprl simpl2 recclnq mulclnq archnq sylan2 simpll2 simplrl simprr cop cnpi wb ltmnq vex fvex mulcomnq mulassnq caov12 breq12i syl6bb oveq2d recidnq mulidnq sylan9eq breq1d bitrd syl21anc pinq sylan simpll1 simplrr - biimpa elprnq ltaddnq addcomnq syl6breq ltsonq ltrelnq sotri simpll3 cpli + biimpa elprnq ltaddnq addcomnq breqtrdi ltsonq ltrelnq sotri simpll3 cpli opeq1 df-1nq syl6eqr oveq1d syl5eq oveq1 rspccva biimpar syl2an 1nq cplpq cerq cmi 1pi mpan2 mulidpi mpd 3impb 3simpa addassnq opex distrnq caovdir elexi addpqnq sylancl oveq2i addpipq mpanr12 oveq12d opeq12d eqtrd fveq2d @@ -113630,7 +113630,7 @@ divided by the argument (although we don't define full division since we NM, 3-Apr-1996.) (New usage is discouraged.) $) ltexprlem2 $p |- ( B e. P. -> C C. Q. ) $= ( cnp wcel cnq cv wn cplq co wa wex abeq2i elprnq cxp cltq wbr addnqf syl - fdmi 0nnq ndmovrcl ltaddnq ancoms addcomnq syl6breq prcdnq mpd ex adantld + fdmi 0nnq ndmovrcl ltaddnq ancoms addcomnq breqtrdi prcdnq mpd ex adantld syl5 exlimdv syl5bi ssrdv prpssnq sspsstrd ) DGHZEDIUTAEDAJZEHBJZCHKZVBVA LMZDHZNZBOZUTVADHZVGAEFPUTVFVHBUTVEVHVCUTVEVHUTVENZVBIHZVAIHZNZVHVIVDIHVL DVDQVBVAILIIRILUAUCUDUEUBVLVAVDSTVIVHVLVAVAVBLMZVDSVKVJVAVMSTVAVBUFUGVAVB @@ -123211,7 +123211,7 @@ Ordering on reals (cont.) recgt0ii $p |- 0 < ( 1 / A ) $= ( cc0 c1 cdiv co clt wbr wn recni 0re 1re ax-mp cneg cmul cr wb lt0neg1 wcel wceq ax-1cn ax-1ne0 gt0ne0ii divne0i nesymi 0lt1 rereccli renegcli - wo ltnsymi mulgt0i mpan2 mulneg1i recidi mulcomli negeqi eqtri syl6breq + wo ltnsymi mulgt0i mpan2 mulneg1i recidi mulcomli negeqi eqtri breqtrdi 3imtr4i mto pm3.2ni axlttri mp2an mpbir ) DEAFGZHIZDVFUAZVFDHIZUJJZVHVI VFDEAUBABKZUCABCUDZUEUFVIEDHIZDEHIVMJUGDELMUKNDVFOZHIZDEOZHIZVIVMVODVNA PGZVPHVODAHIDVRHICVNAVFABVLUHZUIBULUMVRVFAPGZOVPVFAVFVSKZVKUNVTEAVFEVKW @@ -144595,7 +144595,7 @@ notation is used by Donald Knuth for iterated exponentiation (_Science_ renegcld rspcdva sqneg sqdiv syl3anc sqval mul32d syl6eq 3eqtr2d divdiv1d wral 3eqtrd eqtr4d divcan2d mulneg2d negeqd negsubd addsubd breqtrd mpbid readdcld subge0d eqbrtrd leadd2d mpbird suble0d resubcld ledivmuld mul01d - 0red wn c1 peano2re ltnegd df-neg syl6breq ltaddsubd expr simprr redivcld + 0red wn c1 peano2re ltnegd df-neg breqtrdi ltaddsubd expr simprr redivcld ltp1d simprl sqcl mul02d addid2d wb 0re lenlt cif pm2.65d nne sylib sq0id mul01i 0m0e0 0le0 eqbrtri syl6eqbr wo eqid discr1 leloe mpjaodan ) AJCUFK ZDLUAMZNCEOMZOMZUBMZJPKJCUGZAUUOUCZUUSNCOMZJOMZJPUVAUUSUVBQMZJPKUUSUVCPKU @@ -145254,7 +145254,7 @@ notation is used by Donald Knuth for iterated exponentiation (_Science_ cz 1exp syl6eq oveq2 nn0cni exp1 oveq12d fveq2 fac1 oveq2d mulcli mulid1i recni breq12d sylbir adantr a1i faccl nn0mulcli nncni expm1t oveq12i mpbi expp1 elnnnn0 simpri mulassi eqtri nn0addcli w3a 3pm3.2i wb nnltp1le df-2 - breq1i bitr4i expubnd lemul1a mul4i oveq2i 3eqtr2i syl6breq ax-1cn eqtr3i + breq1i bitr4i expubnd lemul1a mul4i oveq2i 3eqtr2i breqtrdi ax-1cn eqtr3i mpan letrd eqtr4i nn0zi sqvali mp3an12 mul12i adantl mul32i facnn2 expadd sylancr addassi eqbrtrid ltp1i ltleii eqcomi adddii 3brtr4i eluz1i jaoian mpbir2an breqtrrdi ) CGHIZGCUAIZUCZCGUDJZAKJZBUVBKJZLJZMAMKJZKJZBBAUBJZKJ @@ -147105,7 +147105,7 @@ are used instead of sets because their representation is shorter (and more mp3an23 hashsng elv oveq2i syl6req breqtrd difsnid dmeqd 3ad2ant2 3brtr3d rexlimdv3a syl5bi imp gtned necon4bd wex 2nalexn df-ne anbi2i annim exbii exnal bitr2i 2exbii cpr 2re readdcl sylancr 1re opex undif sylbb syl5reqr - ex prss vex ad2antrl dmprop dfsn2 eqtr4i uneq1i hashun2 syl6breq mp3an12i + ex prss vex ad2antrl dmprop dfsn2 eqtr4i uneq1i hashun2 breqtrdi mp3an12i oveq1i 1lt2 ltadd1 mpbii leadd2 mp3an3 mpbid prfi mp3an13 simprbi necon3i opth hashprg mp2an sylib oveq1d ad2antll 3eqtr3rd ltletrd exlimdvv dffun4 exlimdv sylanbrc impbid2 ) AEFZAUAZAGHZAIZGHZTZUVMAUVOUBUVQAUCUVOAUDUEUVL @@ -157896,7 +157896,7 @@ reflection about the origin (under the map ` x |-> -u x ` ). (Contributed resqcld resubcld cc0 posdifd biimpa elrpd 3rp rpdivcl sylancl rpaddcld cc cmul recnd cn 3nn nndivre binom2 syl2anc remulcld remulcl sylancr addassd 2re eqtrd mulass mp3an2i eqcomd sqvald oveq12d adddird eqtr4d simprd 1red - 2cn 2rp a1i lemul2d mpbid 2t1e2 syl6breq sqge0d addge01d lesubaddd mpbird + 2cn 2rp a1i lemul2d mpbid 2t1e2 breqtrdi sqge0d addge01d lesubaddd mpbird simplr letrd 1le3 wi 1re 3re letr mp3an23 mpan2i mpd 3t1e3 breqtrrdi 3pos wb ledivmul mp3an2 mpanr12 le2add mp2and readdcld lemul1d divcan2 breqtrd df-3 3cn 3ne0 eqbrtrd leaddsub2d oveq1 breq1d crab cbvrabv eqtri sylanbrc @@ -157952,7 +157952,7 @@ reflection about the origin (under the map ` x |-> -u x ` ). (Contributed cv wrex wo wb leloe mpan elrp 01sqrex rprege0 anass sylib adantrl reximi2 anim1i syl sylanbr exp31 sq0 syl5eq 0le0 jctil breq2 oveq1 eqeq1d anbi12d id rspcev sylancr a1i13 jaod sylbid imp 0lt1 ltletr mp3an12 mpani biimpri - rpreccld simpr lerec mpanl12 mpbid 1div1e1 syl6breq syl2anc rpre 3ad2ant2 + rpreccld simpr lerec mpanl12 mpbid 1div1e1 breqtrdi syl2anc rpre 3ad2ant2 1re w3a rpgt0 wne gt0ne0 rereccl recgt0 ltle sylc cc adantr sqrecd simp3r recn oveq2d recrec syl2an2r 3ad2ant1 3eqtrd syl12anc rexlimdv3a mpd simpl ex letric sylancl mpjaod ) BDEZFBGHZIZBJGHZFAUAZGHZXSKLMZBNZIZADUBZJBGHZX @@ -159680,7 +159680,7 @@ the complex numbers (sorting by real part first, then by imaginary part as ( abs ` ( A - B ) ) < D ) $= ( cmin co cabs cfv c2 clt wbr caddc subcli abscli readdcli recni cdiv cle abs3difi rehalfcli lt2addi lelttri sylancr cmul 2timesi 2cn 2ne0 divcan2i - wa eqtr3i syl6breq ) ACIJZKLZDMUAJZNOCBIJZKLZURNOUMZABIJZKLZURURPJZDNVAVC + wa eqtr3i breqtrdi ) ACIJZKLZDMUAJZNOCBIJZKLZURNOUMZABIJZKLZURURPJZDNVAVC UQUTPJZUBOVEVDNOVCVDNOABCEFGUCUQUTURURUPACEGQRZUSCBGFQRZDHUDZVHUEVCVEVDVB ABEFQRUQUTVFVGSURURVHVHSUFUGMURUHJVDDURURVHTUIDMDHTUJUKULUNUO $. $} @@ -168002,7 +168002,7 @@ Infinite sums (cont.) ( cn wcel cr vk vz vm cv wf cfv cle wbr wral wa wex ccom cli wrex csup c1 clt cdiv cmin wceq weq oveq2 oveq2d ovex fvmpt adantl crp wne wfo fof syl co feq3 syl5ibcom f00 simprbi syl6 necon3d suprcld eqeltrid nnrp rpreccld - c0 mpd ltsubrp syl2an eqbrtrd syl6breq wss w3a 3jca nnrecre resubcl fmptd + c0 mpd ltsubrp syl2an eqbrtrd breqtrdi wss w3a 3jca nnrecre resubcl fmptd wb ffvelrnda suprlub syl2an2r mpbid wi adantr sselda reximdva crn rexeqdv ltle forn wfn breq2 rexrn 3syl bitr3d ralrimiva nnenom fveq2 breq2d axcc4 ffn cvv nnuz 1zzd cc0 csn cxp cmpt cc cz recnd 1z cuz eqimss2i climconst2 @@ -173034,7 +173034,7 @@ seq m ( x. , G ) ~~> z ) ) $. syl nnrecred eqeltrd clt nnred nngt0d 1re divge0 mpanl12 syl2anc breqtrrd 0le1 climserle eqbrtrrd mptru cmin nnuz recnd clim2ser 0p1e1 seqeq1 ax-mp 1zzd oveq2i 3brtr3g cmul 2cnd oveq2 eqid halfre reexpcl sylancr cabs 1lt2 - simpr 2re 0le2 absid mp2an breqtrri georeclim 2m1e1 eqtri syl6breq halfcn + simpr 2re 0le2 absid mp2an breqtrri georeclim 2m1e1 eqtri breqtrdi halfcn 2cn exp0 nnnn0 sylan2 eqtr4d isermulc2 2t1e2 remulcl nnrpd wne 2ne0 mpbid faclbnd2 2nn nnexpcl rphalfcld lerecd nncnd nnne0d divrecd recdiv mpanr12 exprecd 3eqtr4rd 3brtr4d iserle ere lesubaddi mpbi df-3 pm3.2i ) FGHIZGUC @@ -174512,7 +174512,7 @@ seq m ( x. , G ) ~~> z ) ) $. cioc cexp cmin ccos cfv wceq cxr w3a 0xr elioc2 mp2an simp1bi resqcld recnd wne 2cn 3cn pm3.2i div12 mp3an13 syl cz 2z expgt0 mp3an2 3adant3 sylbi 2lt3 3pos ltdiv1ii dividi breqtri redivcli mp3an12 mpbii syl2anc mulid1d breqtrd - mpbi ltmul2 eqbrtrd wi 0re ltle imdistani le2sq2 mpanr1 stoic3 sq1 syl6breq + mpbi ltmul2 eqbrtrd wi 0re ltle imdistani le2sq2 mpanr1 stoic3 sq1 breqtrdi redivcl mp3an23 remulcl sylancr ltletr mp3an3 mp2and sylancl mpbid cos01bnd mpan posdif simpld resubcl recoscld lttr mp3an2i ) ABCUADEZBCFAFUBDZGHDZIDZ UCDZJKZXLAUDUEZJKZBXNJKZXHXKCJKZXMXHXKXIJKZXICLKZXQXHXKXIFGHDZIDZXIJXHXIMEZ @@ -174531,7 +174531,7 @@ seq m ( x. , G ) ~~> z ) ) $. ( cc0 c2 cioc co wcel cmul csin cfv clt cr wbr cle wb 2re syl c1 wa 2pos cc cdiv ccos w3a cxr 0xr elioc2 mp2an rehalfcl 3ad2ant1 sylbi resincl remulcld recoscl divgt0 mpanr12 3adant3 pm3.2i lediv1 mp3an23 biimpa 2div2e1 3adant2 - syl6breq 3jca 1re 3imtr4i sin01gt0 cos01gt0 wi axmulgt0 syl2anc mp2and mpan + breqtrdi 3jca 1re 3imtr4i sin01gt0 cos01gt0 wi axmulgt0 syl2anc mp2and mpan mpani sylc wceq recnd sin2t breqtrrd simp1bi wne 2cn divcan2 fveq2d breqtrd 2ne0 ) ABCDEFZBCACUAEZGEZHIZAHIJWGBCWHHIZWHUBIZGEZGEZWJJWGWMKFZBWMJLZBWNJLZ WGWHKFZWOWGAKFZBAJLZACMLZUCZWRBUDFZCKFZWGXBNUEOBCAUFUGZWSWTWRXAAUHUIZUJZWRW @@ -178079,7 +178079,7 @@ equal to the half of the predecessor of the odd number (which is an even oveq2 elrab2 simprbi lelttrd ltexp2d elnnz sylanbrc nnm1nn0 nncnd mulid2d mpbird ltm1d ltnled mpbid wi infssuzle mpan eqbrtrid syl5bir mpand nltled syl mtod eqbrtrd 1red crp 2rp 1z zsubcld rpexpcld lemuldivd cc 2cn expm1t - breqtrd ltdivmuld df-2 syl6breq wb rerpdivcld sylancl mpbir2and syl2an2r + breqtrd ltdivmuld df-2 breqtrdi wb rerpdivcld sylancl mpbir2and syl2an2r flbi mtbiri bitsval2 sseldd elfzolt2 zlem1lt pm2.65da elfzo2 syl3anbrc ) AEJUBUCZKLDMNZUDKEUUJOPZEJUUJUGNKAEQUUIFUEUFAUUJALDLUHKZAUIRZGUJZUKAUUKUU JESPZULAUUOBDSPZAUUOVAZUUPBTUMNZDOPZUUQUURJDUGNZKUUSUUQEUNUCZUUTUURAUVAUU @@ -178162,7 +178162,7 @@ equal to the half of the predecessor of the odd number (which is an even wi mp2and nn0red dvdscmulr syl112anc pncan3d oveq1d divdird eqtr3d fveq2d ltled wceq fladdz eqtrd mvrladdd dvdssub2 syl31anc notbid z0even rpexpcld 3bitr3d 2rp modcld nn0ge0d divge0d rpred modlt 1le2 nltled leexp2ad rpcnd - ltletrd mulid1d ltdivmuld 1e0p1 syl6breq rerpdivcld bitr3d 3anass 3bitr4g + ltletrd mulid1d ltdivmuld 1e0p1 breqtrdi rerpdivcld bitr3d 3anass 3bitr4g 1red an12 flbi sylancl mpbir2and breqtrrid intnand 2thd con2bid pm2.61dan syl6bb pm5.32da elfzo2 elnn0uz 3anbi1i 3bitr2i anbi2i bitri bitsval eqrdv 0z elin ) BCDZAEDZFZUABGAUBRZUCRZUDHZBUDHZIAUERZUFZUVCUVECDZUAUGZEDZGUVEG @@ -187203,7 +187203,7 @@ given prime (or other positive integer) that divides the number. For wfn eqeq12d ralbiia bitri breq2 notbid ralbidv elrab2 simprbi syl2anr cin cun inundif raleqi ralunb bitr3i iffalse iftrue nnnn0d cfn ssrab2 pceq0 wss ssfi sylancr breq2d nnzd pcdvdsb syl3anc mtbid pccld nn0red - 2nn0 2re ltnle df-2 syl6breq nn0zd zleltp1 nn0uz elfz5 0z fzpr oveq2i + 2nn0 2re ltnle df-2 breqtrdi nn0zd zleltp1 nn0uz elfz5 0z fzpr oveq2i ax-mp preq2i 3eqtr4i prid1 ifclda fmpttd sylibr anbi12i eqfnfv eleq1w prex elmap simprll simprrl r19.26 fz1ssnn sstri anbi12d eqtr3 syl6bir eldifi ralimdva mp2and biantrud incom uneq1i eqtri eldifn eqtr4d rgen @@ -224424,7 +224424,7 @@ operation is a permutation group (group consisting of permutations), see ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> F = G ) $= ( vx vy wf1o wa cid cdif cdm c2o cen wbr wceq wfn f1ofn wcel c1o wb cvv - ad2antrr ad2antlr cv cfv csn wmo csuc 1onn simplrr simplrl df-2o syl6breq + ad2antrr ad2antlr cv cfv csn wmo csuc 1onn simplrr simplrl df-2o breqtrdi com eqbrtrd simpr dif1en mp3an2i weu euen1b eumo sylbi wi f1omvdmvd eleq2 syl ex ad2antll difeq1 eleq2d 3imtr4d imp ad4ant24 fvex pm3.2i moi mp3an1 eleq1 syl12anc adantlr wn fnelnfp sylan bitrd necon2bbid eqtr4d pm2.61dan @@ -224538,7 +224538,7 @@ operation is a permutation group (group consisting of permutations), see 16-Aug-2015.) $) pmtrf $p |- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) : D --> D ) $= ( vz wcel wss c2o cen wbr w3a cv csn cdif cuni cif cfv wa c1o pmtrval com - simpll2 csuc 1onn simpll3 df-2o syl6breq simpr dif1en mp3an2i eldifi 3syl + simpll2 csuc 1onn simpll3 df-2o breqtrdi simpr dif1en mp3an2i eldifi 3syl en1uniel sseldd wn simplr ifclda fmpt3d ) ADGZBAHZBIJKZLZFAFMZBGZBVDNZOZP ZVDQABCRFABCDEUAVCVDAGZSZVEVHVDAVJVESZBAVHUTVAVBVIVEUCVKVGTJKZVHVGGVHBGTU BGVKBTUDZJKVEVLUEVKBIVMJUTVAVBVIVEUFUGUHVJVEUIBTVDUJUKVGUNVHBVFULUMUOVCVI @@ -224550,7 +224550,7 @@ operation is a permutation group (group consisting of permutations), see dom ( ( T ` P ) \ _I ) = P ) $= ( vz wcel wss c2o cen wbr cfv cdif wne crab cin wceq 3syl wa c1o cv pmtrf w3a cid cdm wf wfn ffn fndifnfp csn cif pmtrfv neeq1d wb iffalse necon1ai - cuni iftrue adantl csuc 1onn simpl3 df-2o syl6breq simpr mp3an2i en1uniel + cuni iftrue adantl csuc 1onn simpl3 df-2o breqtrdi simpr mp3an2i en1uniel com dif1en eldifsni eqnetrd ex impbid2 bitrd rabbidva incom dfin5 syl6eqr adantr eqtri simp2 df-ss sylib 3eqtrd ) ADGZBAHZBIJKZUCZBCLZUDMUEZFUAZWIL ZWKNZFAOZBAPZBWHAAWIUFWIAUGWJWNQABCDEUBAAWIUHFAWIUIRWHWNWKBGZFAOZWOWHWMWP @@ -224631,7 +224631,7 @@ operation is a permutation group (group consisting of permutations), see ( vx wcel wf wfn cdif cfv cen wbr wceq syl wa c1o sylan eqtrd cid cdm cvv ccom cres wss c2o w3a pmtrfrn simpld pmtrf simprd feq1d mpbird fco anidms eqid ffn 3syl fnresi a1i cv csn cif pmtrffv iftrue sylan9eq fveq2d simpll - cuni simp2d ad2antrr csuc 1onn simp3d df-2o syl6breq simpr dif1en mp3an2i + cuni simp2d ad2antrr csuc 1onn simp3d df-2o breqtrdi simpr dif1en mp3an2i com en1uniel eldifad sseldd syl2anc adantr en2other2 ancoms wn wb fnelnfp wne ffnd necon2bbid biimpar fveq2 pm2.61dan fvresi adantl 3eqtr4d eqfnfvd id fvco2 ) DBHZGADDUDZUAAUEZXDAADIZAAXEIZXEAJXDXGAADUAKUBZCLZIZXDAUCHZXIA @@ -229187,7 +229187,7 @@ U C_ ( T .(+) U ) ) $= ( A splice <. N , N , <" <. J , (/) >. <. J , 1o >. "> >. ) ) $= ( wcel cc0 co c0 cop c1o cs2 cotp csplice c2o wtru wceq chash cfv cfz w3a cdif wbr wa cpr 0ex prid1 df2o3 eleqtrri efgi mpanr2 3impa tru eqidd dif0 - opeq2i a1i s2eqd oteq3 mp2b oveq2i syl6breq ) AFIZEJAUAUBUCKIZDCIZUDAAEED + opeq2i a1i s2eqd oteq3 mp2b oveq2i breqtrdi ) AFIZEJAUAUBUCKIZDCIZUDAAEED LMZDNLUEZMZOZPZQKZAEEVIDNMZOZPZQKBVFVGVHAVNBUFZVFVGUGVHLRIVRLLNUHRLNUIUJU KULABCDLEFGHUMUNUOVMVQAQSVLVPTVMVQTUPSVIVKVIVOSVIUQVKVOTSVJNDNURUSUTVAVLV PEEVBVCVDVE $. @@ -229198,7 +229198,7 @@ U C_ ( T .(+) U ) ) $= ( A splice <. N , N , <" <. J , 1o >. <. J , (/) >. "> >. ) ) $= ( wcel cc0 co c1o cop cs2 cotp csplice c0 c2o wtru wceq chash cfv cfz w3a cdif wbr cpr 1oex prid2 df2o3 eleqtrri efgi mpanr2 3impa tru eqidd opeq2i - wa difid a1i s2eqd oteq3 mp2b oveq2i syl6breq ) AFIZEJAUAUBUCKIZDCIZUDAAE + wa difid a1i s2eqd oteq3 mp2b oveq2i breqtrdi ) AFIZEJAUAUBUCKIZDCIZUDAAE EDLMZDLLUEZMZNZOZPKZAEEVIDQMZNZOZPKBVFVGVHAVNBUFZVFVGURVHLRIVRLQLUGRQLUHU IUJUKABCDLEFGHULUMUNVMVQAPSVLVPTVMVQTUOSVIVKVIVOSVIUPVKVOTSVJQDLUSUQUTVAV LVPEEVBVCVDVE $. @@ -235663,7 +235663,7 @@ mapping the (infinite, but finitely supported) cartesian product of ( G dom DProd ( S o. F ) /\ ( G DProd ( S o. F ) ) C_ ( G DProd S ) ) ) $= ( ccom cdprd cdm wbr co wss crn cres wceq simpld simprd wf1 f1f frn csubg 3syl dprdres cfv dprdf2 fssresd fdmd wf1o f1f1orn syl dprdf1o cores ax-mp - wf ssid syl6breq oveq2i syl5eqr eqsstrd jca ) ADBCJZKLZMDVDKNZDBKNZOADBCP + wf ssid breqtrdi oveq2i syl5eqr eqsstrd jca ) ADBCJZKLZMDVDKNZDBKNZOADBCP ZQZCJZVDVEADVJVEMZDVJKNZDVIKNZRZAVICDVHFADVIVEMZVMVGOZAVHBDEGHAFECUAZFECU QVHEOIFECUBFECUCUEZUFZSAVHDUDUGZVIAEVTVHBABDEGHUHVRUIUJAVQFVHCUKIFECULUMU NZSVHVHOVJVDRVHURBCVHUOUPZUSAVFVMVGAVFVLVMVJVDDKWBUTAVKVNWATVAAVOVPVSTVBV @@ -308422,7 +308422,7 @@ the half element (corresponding to half the distance) is also in this cdm rnss dmxp xpeq12d adantr sseqtrd sstrid ad3antrrr sselda opelxp sylib rnxp simpll simprl simprr w3a simplll simp1d jca simp2d simp3d 3jca ffund wfun simpld opelxpd fdmd eleqtrrd 0xr simprd wf ffvelrnd psmetge0 syl3anc - rpxrd cle df-ov syl6breq clt cxad eqeltrid caddc cr rpred rehalfcld rexrd + rpxrd cle df-ov breqtrdi clt cxad eqeltrid caddc cr rpred rehalfcld rexrd 0red df-br fvimacnv elico2 biimpa rexaddd readdcld eqeltrd sylibr wex vex ex r19.29a psmettri syl13anc lt2halvesd eqbrtrd xrlelttrd elicod syl22anc eqbrtrrid breqd mpbird simpr brco wi brelrn sseldd adantrr ancrd 3ad2ant1 @@ -310495,7 +310495,7 @@ distance function as the normed group (restricted to the base set). cr syl3anc mscl readdcld rpred cle wbr mstri syl13anc c1 cmul c2 cdiv cfv nlmngp2 nmcl syl2anc cc0 ge0p1rpd remulcld rehalfcld wceq nlmdsdi nmge0 cxms msxms xmsge0 lep1d lemul1ad eqbrtrrd clt ltmuldiv2d mpbird - syl6breq lelttrd crp rphalfcld rpdivcld eqeltrid nlmdsdir cmin nm2dif + breqtrdi lelttrd crp rphalfcld rpdivcld eqeltrid nlmdsdir cmin nm2dif resubcld csg ngpdsr breqtrrd ltled letrd lesubadd2d mpbid lemul2ad wb eqid 0red ltaddrpd ltmuldiv syl112anc lt2halvesd ) ACPHUPZDQHUPZEUPZY FCQHUPZEUPZYIYGEUPZUQUPZFAOURUSZYFNUSZYGNUSZYHVHUSAOUTUSZYMAOVAUSZYPU @@ -312518,7 +312518,7 @@ Normed space homomorphisms (bounded linear operators) sstrid simpld ne0d simprd brralrspcev suprcld eqeltrid ltaddrpd rpred rphalfcld readdcld ltnled mpbid cif ifcld breqtrrdi ltled letrd breq2 suprubd ifboth min2 eqbrtrid w3a wb elicc2 mpbir3and cmin ltsubrpd c0 - syl6breq wne resubcld suprlub syl31anc wa wi weq oveq2 sseq1d rexbidv + breqtrdi wne resubcld suprlub syl31anc wa wi weq oveq2 sseq1d rexbidv elrab2 unieq sseq2d cbvrexv csn cun simpr1 elin adantrr simprr sseldd syl adantr expr lelttrd cxr rexr syl5eq rexlimdv syl5bi crab vex snex sylib elpwid simpll snssd unssd unex elpw sylibr snfi sylancl simplr2 @@ -312863,7 +312863,7 @@ Normed space homomorphisms (bounded linear operators) c0 cc reseq2 syl6eq oveq2d elrnmpt1s supxrub sylancl breqtrrdi ctop letop wb ovex cioo simplrl simplrr simpr syl2anc simprrr adantr simprrl fssresd cr elind ssfid sstrd simprlr xrge0gsumle xrltletrd weq w3a mpbir3and expr - sseldd ralrimiva syl6breq ad3antrrr mpbid sylib reximddv eleq2 syl5ibrcom + sseldd ralrimiva breqtrdi ad3antrrr mpbid sylib reximddv eleq2 syl5ibrcom syl5bi mpd simprr ad2antrr ad2antrl ctps cha xrsbas ressbas2 cdif csubmnd cbs c0g xrge0subm difexi simpl eldifsn 3imtr4i ssriv ressabs eqtr4i xrs10 xrex subm0 xrge0cmn adantl fssres syl2an fmpttd frnd supxrcl eqeltrid 0ss @@ -314484,7 +314484,7 @@ Normed space homomorphisms (bounded linear operators) -> ( A x. B ) e. ( 0 [,] 1 ) ) $= ( cr wcel cc0 cle wbr c1 wa cmul co cicc remulcl 3ad2antr1 3ad2antl1 mulge0 w3a 3adantr3 1re elicc01 3adantl3 an6 wi lemul12a mpanr2 mpanl2 an4s 3impia - sylbi 1t1e1 syl6breq 3jca anbi12i 3imtr4i ) ACDZEAFGZAHFGZQZBCDZEBFGZBHFGZQ + sylbi 1t1e1 breqtrdi 3jca anbi12i 3imtr4i ) ACDZEAFGZAHFGZQZBCDZEBFGZBHFGZQ ZIZABJKZCDZEVDFGZVDHFGZQAEHLKZDZBVHDZIVDVHDVCVEVFVGUOUPVBVEUQUOUTUSVEVAABMN OUOUPVBVFUQUOUPIZUSUTVFVAABPRUAVCVDHHJKZHFVCUOUSIZUPUTIZUQVAIZQVDVLFGZUOUPU QUSUTVAUBVMVNVOVPUOUPUSUTVOVPUCZVKHCDZUSUTIZVQSVKVRIVSVRVQSAHBHUDUEUFUGUHUI @@ -316552,7 +316552,7 @@ a tuple of a topological space (a member of ` TopSp ` , not ` Top ` ) mulcom cn 4nn nnrecre mul02i recni 2timesi wne recdiv2 mp4an 2t2e4 eqtr3i oveq12i mulcomli adantlr simplll ad2antlr letric orcanai readdcl leadd1dd wo simplr eqbrtrrid simp3bi 2lt4 2pos ltrecii le2addd pco0 adddid syl5eqr - syl6breq pnpcan2d divcan1i subidi 1mhlfehlf iccshftli subdid recidi elii2 + breqtrdi pnpcan2d divcan1i subidi 1mhlfehlf iccshftli subdid recidi elii2 remulcl sseli div0i icccntri addid2i iccshftri 3syl 1cnd divdird peano2cn divcan2d eqtr3d mvrraddd mpteq2dva wral iitopon 0elunit cioo crn ctg 0red 1red addcomi breq1d recgt0ii 3eqtr4a 0xr rexri lbicc2 sstri retop restabs @@ -320218,7 +320218,7 @@ vector spaces which are also normed vector spaces (that is, normed groups cfv subcld abscld cngp cr cnlm cphnlm syl nlmngp nmcl syl2anc cc0 nmge0 cle wbr ge0p1rpd cms mscl remulcld rehalfcld csg wceq cphsubdi syl13anc ngpms eqid fveq2d cgrp ngpgrp grpsubcl ipcau ngpds oveq2d breqtrrd cxms - eqbrtrrd msxms xmsge0 lep1d lemul1ad syl6breq ltmuldiv2d mpbird lelttrd + eqbrtrrd msxms xmsge0 lep1d lemul1ad breqtrdi ltmuldiv2d mpbird lelttrd letrd clt crp rphalfcld rpdivcld eqeltrid readdcld oveq1d nm2dif ngpdsr cphsubdir resubcld ltled lesubadd2d mpbid lemul2ad wb ltaddrpd ltmuldiv 0red syl112anc abs3lemd ) ABCHUHZLMHUHZBMHUHZEAKUIUJZBJUJZCJUJZYHUKUJTU @@ -324692,7 +324692,7 @@ Hilbert space (in the algebraic sense, meaning that all algebraically cv simprd eqeltrid wn ivthlem2 wa cmin wi crp cc ccncf adantr suprubd cabs breqtrrdi wne w3a 3jca suprleub mpbird eqbrtrid elicc2 mpbir3and c0 wb sseldd fveq2 eleq1d ralrimiva rspcdva difrp biimpa cncfi ssralv - syl3anc ad2antrr ltsubrp sylancom syl6breq rpre adantl resubcld mpbid + syl3anc ad2antrr ltsubrp sylancom breqtrdi rpre adantl resubcld mpbid syl suprlub ad2antrl simplll simprl suprub abssuble0d simprr ltsub23d sseli eqbrtrd jca32 ex reximdv2 mpd r19.29 pm3.45 imp caddc absdifltd ad2antll recnd breq1d sylbid rexlimdva notbid necon2ad jctild sylibrd @@ -329170,7 +329170,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by ressxr csn cxp mpteq2dva fconstmpt syl6eqr seqeq3d fveq1d recnd ser1const cc ffnd fnfvelrn eqeltrrd supxrub wdisj vitalilem3 voliun eqtr3d breqtrrd wfn jca xrltletrd simp3d ovolss 2cn ax-1cn subnegi 2pos lttri ltleii df-3 - neg1lt0 3eqtr4i syl6breq xrlenlt pm2.65da wo ovolge0 0xr xrleloe ord mpd + neg1lt0 3eqtr4i breqtrdi xrlenlt pm2.65da wo ovolge0 0xr xrleloe ord mpd ) AHUBZUCUDZUEZUXKGUFZUGUFZJUHZUGUFZUPUXMUXOLUBZUXKKUFZUIUJZUXPUDZLTUKZUG UFUXQUXMUXNUYBUGUXLUXNUYBULAIUXKUXRIUBZKUFZUIUJZUXPUDZLTUKZUYBUCGUYCUXKUL ZUYFUYALTUYHUYEUXTUXPUYHUYDUXSUXRUIUYCUXKKUMUNUOUQRUYALTURUSUTVAVBUXMLUXP @@ -329250,7 +329250,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by pwex cxp cin weinxp wceq unipw weeq2 ax-mp bitr4i inex2 weeq1 spcev sylbi wb xpex dfac8c mpsyl cneg cicc wf1o cen cdom qex inex1 nnrecq cle nnrecre neg1rr a1i 0re neg1lt0 ltleii nnrp rpreccld rpge0d letrd nnge1 nnre nngt0 - clt 1re 0lt1 lerec mpanl12 syl2anc mpbid 1div1e1 syl6breq syl3anbrc elind + clt 1re 0lt1 lerec mpanl12 syl2anc mpbid 1div1e1 breqtrdi syl3anbrc elind elicc2i weq oveq2 nncn nnne0 recrecd eqeqan12d syl5ib impbid1 dom2 ssdomg inss1 mp2 qnnen domentr mp2an sbth bren mpbi cmpt crab eleq1w eleq1d eqid wn fvex fveq2 wtru sylibr copab cqs cdif bi2anan9 oveq12 anbi12d cbvopabv @@ -338200,7 +338200,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by 1cnd cop c0ex snid opelxpi mpan2 dvconst eleqtrrd df-br sylibr ccom oveq1 cofmpt eqid ovex fvmpt subid eqtrd dveflem syl6eqbr 1ex cr cpr cnelprrecn simpr dvmptid simpl id dvmptc dvmptsub 1m0e1 mpteq2i eqtr4i syl6eq dvcobr - 1t1e1 syl6breq breqdi dvmulbr mul02d fvex mulid2d oveq12d addid2d breqtrd + 1t1e1 breqtrdi breqdi dvmulbr mul02d fvex mulid2d oveq12d addid2d breqtrd ffvelrnd fvconst2 vex breldm ssriv eqssi feq2i mpbi wfun ffun ax-mp mpsyl funbrfv mpteq2ia eqtr4d mptru ) CDEFZDGHYQACAUAZDIZJZDHYQACYRYQIZJYTHACCY QCCYQKZHYQUBZCYQKZUUBDUCZUUCCCYQUUCCCDUDACUUCYRCLZYRYSYQUEZYRUUCLUUFCCYSU @@ -343858,7 +343858,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by ( F E G ) = ( A ` ( ( O ` F ) ` N ) ) ) $= ( co cc0 cco1 cfv cdg1 cle wbr wceq cn0 wcel csn c1 caddc clt crg cuc1p cmnf cnzr nzrring syl cmn1 ccnv c0g cima eqid ply1remlem simp1d syl2anc - mon1puc1p r1pdeglt syl3anc simp2d breqtrd 1e0p1 syl6breq 0nn0 nn0leltp1 + mon1puc1p r1pdeglt syl3anc simp2d breqtrd 1e0p1 breqtrdi 0nn0 nn0leltp1 wb mpan2 syl5ibrcom wi elsni cxr 0xr mnfle ax-mp syl6eqbr a1i cun r1pcl deg1cl elun sylib mpjaod deg1le0 mpbid cq1p cmulr cplusg cof cpws r1pid wo fveq2d cghm ccrg evl1rhm rhmghm ply1ring q1pcl mon1pcl ringcl ghmlin @@ -348246,7 +348246,7 @@ of all kernels (preimages of ` { 0 } ` ) of all polynomials in weq mulid1d eqtrd breqtrrd uzid oveq1 3brtr4d rpge0d simpl halfre halfgt0 nnz 3syl elrpii eluzelz zsubcl syl2anr rpmulcld adantr adantl zmulcld a1i jca31 simpr 1le2 nncnd zcnd mulneg1d nnmulcld nnge1d wb nnred leneg mpbid - 2re 1re eqbrtrd neg1z eluz sylancl mpbird leexp2a mp3an12i expn1 syl6breq + 2re 1re eqbrtrd neg1z eluz sylancl mpbird leexp2a mp3an12i expn1 breqtrdi 2cn lemul12a 3impia syl112anc ex cn0 facp1 ax-1cn addcom peano2cn 3eqtr3d 1cnd adddid oveq1d wne 2cnne0 expaddz mpan syl2anc addsubd uznn0sub expp1 mulassd eqtr4d sylibrd peano2uz 3imtr4d expcom a2d uzind4i impcom cxr w3a @@ -351348,7 +351348,7 @@ evaluate the derivatives (generally ` RR ` or ` CC ` ), ` F ` is the eqeltrd df-neg syl6eqr fveq2d abelthlem4 absnegd adantlr ad2ant2r fveq2 sylan9eqr abs00bd ad5ant15 simpllr rpgt0d eqbrtrd wne ad3antrrr simprll cdm simprr eldifsn sylanbrc simplrl 2fveq3 simplrr breq1d cbvralv sylib - weq simprlr cbvsumv oveq1i oveq2i syl6breq abelthlem7 rpcn adantl rpcnd + weq simprlr cbvsumv oveq1i oveq2i breqtrdi abelthlem7 rpcn adantl rpcnd rpne0d divcan2d breqtrd anassrs pm2.61dane expr ralrimiva breq2 syl2anc rspceaimv rexlimddv ) AGUEUFZUGZUAUHZUIFSUJZUKZULUKZGKTUIUMZUNUMZUOUPZU AUBUHZUQUKZURZTCUHZUSUMULUKZEUHZUOUPZTJUKZUVRJUKZUSUMZULUKZGUOUPZUTCHUR @@ -351388,7 +351388,7 @@ evaluate the derivatives (generally ` RR ` or ` CC ` ), ` F ` is the 0nn0 eqidd isumcl adantr subcld ifcld fmpttd caddc cli cdm 1e0p1 eqeltrri cseq cz 1z cuz nnuz fveq2i eqtri eleq2i nnnn0 adantl eqeq1 fveq2 ifbieq2d cn weq eqid ovex fvex ifex fvmpt syl nnne0 neneqd iffalsed eqtrd sylan2br - seqfeq isumclim2 clim2ser 0z seq1 ax-mp oveq2i syl6breq eqbrtrd clim2ser2 + seqfeq isumclim2 clim2ser 0z seq1 ax-mp oveq2i breqtrdi eqbrtrd clim2ser2 wne syl5eq breqtrd wss oveq1 nn0z sylan9eq oveq12d sumeq2dv sumex adantlr mulid1d oveq2d oveq1d cbvsumv breqtrrd isumclim oveq2 expcl sylan mulcld 1exp iftrue sylancl npncan2 syl2anc seqex c0ex breldm abelthlem8 csn cdif @@ -352764,7 +352764,7 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is wa subcl eqtr3d wne cz wn adantr pipos gt0ne0ii divcan1d zre adantl remulcl cmul sylancl eqeltrrd resubcl rered simplr caddc elioore eliooord simprd wb 0zd posdif mpbid divgt0d negcli negsubi pidiv2halves subaddrii eqtri simpld - eqbrtrid ltsub23d mulid1i breqtrrdi 1red ltdivmul syl112anc mpbird syl6breq + eqbrtrid ltsub23d mulid1i breqtrrdi 1red ltdivmul syl112anc mpbird breqtrdi 1e0p1 btwnnz syl3anc pm2.01da sineq0 necon3abid eqnetrd ) ABCZAUADZEUBUCQZU DZXDUEQZCZULZAFDZXDAGQZUFDZHXHXDXJGQZFDZXIXKXHXLAFXHXDBCZXBXLAIZXDJUGZXBXGU HZXDAUIKZUJXHXJBCZXMXKIXHXNXBXSXPXQXDAUMKZXJUKLUNXHXKHUOXJEUCQZUPCZUQZXHYBX @@ -352839,7 +352839,7 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is ( vx cpi co cicc wcel clt wbr cmin cfv cr neghalfpire halfpire sseli wceq wb cc0 cle syl c2 cdiv cneg wa ccos csin wss iccssre ltsub2 mp3an3 syl2an mp2an eleq1d resubcl sylancr elicc2i simp3bi subge0 mpbird simp2bi lesub2 - cv oveq2 mp3an13 mpbid caddc recni subnegi pidiv2halves syl6breq 0re pire + cv oveq2 mp3an13 mpbid caddc recni subnegi pidiv2halves breqtrdi 0re pire eqtri syl3anbrc vtoclga cosord syl2anr recnd coshalfpim breqan12d 3bitrd cc ) ADUAUBEZUCZWCFEZGZBWEGZUDABHIZWCBJEZWCAJEZHIZWJUEKZWIUEKZHIZAUFKZBUF KZHIWFALGZBLGZWHWKQZWGWELAWDLGZWCLGZWELUGMNWDWCUHULZOZWELBXBOZWQWRXAWSNAB @@ -353004,7 +353004,7 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 1re retanhcl resqcld resubcl tanrpcl adantl absresq tanhbnd eliooord abscld recld abslt absge0d 0le1 mulgt0d oveq1i remul2d ine0 divcan2d oveq2d 3eqtrd a1i syl5eq eqtr3d oveq12d eqtrd negeqd 3eqtr4d breqtrrd divrec2d lt2sqd sq1 - syl6breq eqbrtrrd posdif recjd negicn negne0i divcld imre divneg2d renegcld + breqtrdi eqbrtrrd posdif recjd negicn negne0i divcld imre divneg2d renegcld resub re1 eqeltrrd reim0d 3eqtr3rd mul01d 1m0e1 syl6eq crred mulcom mulassd imcjd imsub df-neg eqtr4i immul2d imval remulcld negnegd crimd sqvald sqcld im1 remuld subdid tanadd syl23anc recval oveq1d div23d ) ABCZADEZFUAGHIZUBI @@ -354004,7 +354004,7 @@ imaginary part lies in the interval (-pi, pi]. See crp divcld immul2d divcan2d fveq2d eqtr3d 3brtr4d a1i ltmul2d mpbird efiarg breqtrrd resinval resincld lt0neg2d mpbid caddc cicc readdcl sylancl df-neg wn cmin logimcl simpld wi renegcli ltle sylancr eqbrtrrid lesubaddd leadd1d - mpd biimpa picn addid2i syl6breq elicc2i syl3anbrc sinq12ge0 sinppi breqtrd + mpd biimpa picn addid2i breqtrdi elicc2i syl3anbrc sinq12ge0 sinppi breqtrd ex con3d renegcld ltnle 3imtr4d simprd negneg eleq1d syl5ib lognegb 3imtr3d rpre reim0b necon3d necomd leneltd cxr w3a 0xr rexri elioo2 mp2an ) AUABZCA DEZFGZUMZAUBEZDEZHBZCYPFGZYPIFGZYPCIUCRBZYNYOYKYMACUDZYOUABYNYLCUDZUUAYKYLH @@ -354652,7 +354652,7 @@ imaginary part lies in the interval (-pi, pi]. See rexri elioo2 syl3anbrc wfn imf elpreima mp2b sylanbrc mprgbir ce eliooord ffn simpl adantl imcl adantr ltle sylancl mpd ellogrn logef syl efcl picn recnd pipos gt0ne0ii cdiv caddc cmul mulid1i breqtrrdi ltdivmul syl112anc - 1re mpbird 1e0p1 syl6breq cz csin ccos ci recoscld resincld crimd sylancr + 1re mpbird 1e0p1 breqtrdi cz csin ccos ci recoscld resincld crimd sylancr ad2antrr redivcld eqeltrrd 0z efeul oveq1d ax-icn mulcl addcld recl efne0 cre divcan3d eqtrd simpr reefcld reim0d eqtr3d sineq0 zleltp1 cmin df-neg mulm1i eqbrtrid eqbrtrrid zlem1lt letri3 mpbir2and diveq0d reim0b rpefcld @@ -354965,7 +354965,7 @@ imaginary part lies in the interval (-pi, pi]. See wn ifclda expcl adantlr mulcld caddc cseq cmin cli cdm recnd absidm simpr eqbrtrd geolim seqex breldm syl 1red cuz cn elnnuz nnrecre sylan2 absmuld nnnn0 crp rpreccld rpge0d absidd simpl absexp eqtrd absge0d breqtrd nnge1 - nnrp 0lt1 nnre nngt0 lerec syl22anc mpbid 1div1e1 syl6breq lemul1ad nnne0 + nnrp 0lt1 nnre nngt0 lerec syl22anc mpbid 1div1e1 breqtrdi lemul1ad nnne0 wb neneqd iffalsed oveq1d fveq2d oveq2d 3brtr4d sylan2br cvgcmpce ) ACDZA EFZGHIZJZGUABKYCBUNZLMZUBZBKYFNOZNGYFPMZUCZAYFLMZQMZUBZNGKUDGKDYEUEUFYEUA UNZKDZJZYOYHFZYCYOLMZRYPYRYSOZYEBYOYGYSKYHYFYOYCLUGYHUHYCYOLUIUJSZYEYCRDZ @@ -356190,7 +356190,7 @@ the complex square root function (the branch cut is in the same place for sylan simp2r cdm cnvimass fdmi sseqtri eqsstri sseli syl abscxp syl2anc recld 3ad2ant1 simp1r simp1l simplbi rehalfcld 1re min1 2re 2pos lediv1 a1i syl112anc mpbid eqbrtrid caddc 2halvesd resubd subcld abscld simp3r - recnd releabsd syl6breq ltmin syl3anc lelttrd eqbrtrrd eqbrtrd rprege0d + recnd releabsd breqtrdi ltmin syl3anc lelttrd eqbrtrrd eqbrtrd rprege0d simpld mpbird lttrd wne rpcnd breq2 ltletrd ltsubadd2d ltadd1d rehalfcl absid simp3l mp1i min2 halflt1 cxplt3d cmul rpcnne0d recid oveq2d cxp1d cxpmuld 3eqtr3d simprd cxplt2 3expia anassrs sylan2br expr eleq2s fveq2 @@ -357399,7 +357399,7 @@ be obtained in Metamath (without the need for a new definition) by the curry breqtrd ltmuldiv gt0ne0ii redivcld ltaddsubd subid1i eqnetri negsub 1rp 2pos oveq12d addsub4d ax-icn ine0 biimpar syl22anc biimpa syldan eqcomd add20 lognegb rpaddcl rpreccld oveq1d div2negd rpdivcld readdcld reim0d - negsubdi2 oveq2d necon3d mpi ltlen mpbir2and ltdivmul2 divdiri syl6breq + negsubdi2 oveq2d necon3d mpi ltlen mpbir2and ltdivmul2 divdiri breqtrdi ex 2div2e1 ltsubaddd jca ) CUAJZCKUBZCLUBZUGZMUCZFNOFLNOUWHUWIDUDUEPZMQ UFPZUEPZLMUEPZUHPZFNUWHUWIUWMRPZUWLNOUWIUWNNOUWHUWOUIMUEPZUCZUWLNMUWMUH PZUCUWOUWQMUWMUJUWMLUKULZUMUNUWRUWPUOMUEPZUWMUHPZUWRUWPUWTMUWMUHUPUQUOL @@ -357457,7 +357457,7 @@ be obtained in Metamath (without the need for a new definition) by the curry T e. { -u ( _i x. _pi ) , ( _i x. _pi ) } ) $= ( cc wcel cc0 c1 ci cpi cmul co wceq c2 a1i wne w3a cneg wo cpr clt wbr cdiv 2cn picn mulcli 2ne0 divreci divcan3i eqtr3i cmin caddc ang180lem2 - wa cle simprd 1e0p1 syl6breq cz wb cr ang180lem1 simpld zleltp1 sylancl + wa cle simprd 1e0p1 breqtrdi cz wb cr ang180lem1 simpld zleltp1 sylancl 0z mpbird adantr zlem1lt sylancr df-neg breq1i syl6bbr biimpar zred 0re letri3 mpbir2and syl5eqr clog ax-1cn simp1 subcl simp3 necomd necon3bid subeq0 reccld recne0d logcld simp2 divcld divne0d addcld logcl eqeltrid @@ -360183,7 +360183,7 @@ already know is total (except at ` 0 ` ). There are branch points at ctan imi 3brtr4d tanarg argregt0 mpbird cxr rexri addsub4d subnegi resubcld 3eqtri readdcl renegcli renegcld simpld leneg ltleaddd negsubd breqtrd 0red simprd eqbrtrrid peano2rem peano2re ltm1d ltp1d lttrd ltdiv1 tanord addid2d - syl112anc ltadd1dd addid2i syl6breq elioo2 syl3anbrc eqeltrd ) AUAUBBZCADEZ + syl112anc ltadd1dd addid2i breqtrdi elioo2 syl3anbrc eqeltrd ) AUAUBBZCADEZ FGZUCZHIAUDJZKJZLEZHUVOMJZLEZMJNEZAIMJZLEZNEZAIKJZLEZNEZMJZOKJZOUEZOUFJZUVN UVTUVQNEZUVSNEZMJUWCOUGVRJZKJZUWFUWMUEZKJZMJZUWHUVNUVQUVSUVNUVPUVNHPBZUVOPB ZUVPPBUHUVNIPBZAPBZUWSSUVNUXAUVRCUIZUVPCUIZUVNUVKUXAUXBUXCUJUVKUVMUKAULUMZU @@ -360541,7 +360541,7 @@ already know is total (except at ` 0 ` ). There are branch points at bndatandm $p |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. dom arctan ) $= ( cc wcel cabs cfv c1 clt wbr wa c2 cexp cneg wne catan cdm adantr wceq cc0 co cle simpl sqcl abscld cn0 2nn0 absexp sylancl simpr cr abscl 1red absge0 - 0le1 a1i lt2sqd mpbid sq1 syl6breq eqbrtrd ltned fveq2 ax-1cn absnegi eqtri + 0le1 a1i lt2sqd mpbid sq1 breqtrdi eqbrtrd ltned fveq2 ax-1cn absnegi eqtri abs1 syl6eq necon3i syl atandm3 sylanbrc ) ABCZADEZFGHZIZVKAJKSZFLZMZANOCVK VMUAZVNVODEZFMVQVNVSFVNVOVKVOBCVMAUBPUCVNVSVLJKSZFGVNVKJUDCVSVTQVRUEAJUFUGV NVTFJKSZFGVNVMVTWAGHVKVMUHVNVLFVKVLUICVMAUJPVNUKVKRVLTHVMAULPRFTHVNUMUNUOUP @@ -360945,7 +360945,7 @@ already know is total (except at ` 0 ` ). There are branch points at cneg cdm nn0re 2re 2pos lemul2 leadd1dd ax-1cn divcnv nn0ex nnrecre nnnn0 sylan2 nn0addge1 2timesd letrd nnrpd climsqz2 neg1cn nncnd divrecd climdm iseralt fvex seqex breldm isumclim2 cicc nnrp rpred nnge1 ledivmul mpbird - abelth2 elicc01 syl3anbrc 1cnd nnex climsubc2 syl6breq sumeq2sdv adantllr + abelth2 elicc01 syl3anbrc 1cnd nnex climsubc2 breqtrdi sumeq2sdv adantllr iirev 1m0e1 resubcl ad2antrr simplr reexpcld nn0cn div12d mulcomd ifeq2da ad2antlr mul02d ifeq1d ovif syl6eqr simpr ralrimiva mulcld eqeltrrd 0p1e1 nfov 0nn0 seqeq1 cuz elnnuz nnne0 neneqd biorf bicomd ifbid rgen sylan2br @@ -362979,7 +362979,7 @@ group sum in the additive group (i.e. the sum of the elements). This is ax-mp eqeltrrd rpge0d subge0d mpbid fveq2 breq1d leidi simpld wi peano2nn 1re syl syl3anc mpand nnind letrd ralrimiva brralrspcev climsup eqbrtrrid letr climrel releldmi isumclim2 df-em 3brtr4g cfz cmpt nnex mptex eqeltri - emcllem4 eqeltrd pncan3d eqtr2d climadd cc climcl addid1i syl6breq pm3.2i + emcllem4 eqeltrd pncan3d eqtr2d climadd cc climcl addid1i breqtrdi pm3.2i mptru ) DUBUCLZEUBUCLZYTMDUBUDUENUBUCMUBUDKEFDOUFPUGMUHZMUEAOUIZPOKVBZUJN ZOUUEUENZUKQZULNZKUMEUBUCMUUHKAOPUGUUBUUDPRZUUDAQUUHUNMCUUDOCVBZUJNZOUUKU ENZUKQZULNUUHPACKUOZUUKUUEUUMUUGULUUJUUDOUJUPZUUNUULUUFUKUUNUUKUUEOUEUUOU @@ -363016,7 +363016,7 @@ group sum in the additive group (i.e. the sum of the elements). This is simpli df-neg climsubc2 adantr renegcld eqeltrd adantlr simpld syl lenegd peano2nn mpbid 3brtr4d eqbrtrrd breqtrrdi mptru leneg mpbird log1 elicc2i wb 1m0e1 syl3anbrc wfn ffn mp1i elfznn ffnfv sylanbrc breq2d cuz syl6eleq - monoord2 syl6breq monoord eqbrtrrid 3jca ) KLUDUEMZUFNZLUGNOZPKLUGNZDUHZP + monoord2 breqtrdi monoord eqbrtrrid 3jca ) KLUDUEMZUFNZLUGNOZPKLUGNZDUHZP UUJKUGNZEUHZUIQUUKUUMUUOQKROZUUJKSTZKLSTZUUKQKUAELPUJQUKZEKULTZQDKULTZUUT ABCDEFGHIJUMZUNZUOUAUPZPOZUVDEMZROZQPRUVDEPRDUHZPREUHZBCDEGHUQZUNZURZUSUT ZQLPOZUBUPZEMZKSTZUBPVBUUQVCQUVQUBPQUVOPOZVAZKUAELUVOPUJQUVRVDZUUTUVSUVCU @@ -363853,7 +363853,7 @@ group sum in the additive group (i.e. the sum of the elements). This is oveq1 fvmpt ovex simprbi simpld lemul1ad absrpcld abslogle syl2anc cneg relogdiv sylancr log1 oveq1i df-neg eqtr4i syl6req 0le1 lediv2ad simprd nnnn0d rspcdva lediv1dd recdiv2d divdird dividd 3eqtrrd rpreccld oveq2i - wne abstrid abs1 syl6breq absge0d nnge1d lediv12ad lemulge11d mpbir2and + wne abstrid abs1 breqtrdi absge0d nnge1d lediv12ad lemulge11d mpbir2and div1d absled le2addd ifbothda id mpteq2dv cnex rabex2 mptex fveq1d eqid oveq1d ifbieq12d ifex 3brtr4d ) AJUBZUCUDZCUBZGUDZUEZUEZUWMUWKPQRZUWKUF RZUGSZUHRZUWMUWKUFRZPQRZUGSZUIRZUJSZUKEUHRZUWKTUMZEUKEPQRZUHRZUWKUKULRZ @@ -364258,7 +364258,7 @@ group sum in the additive group (i.e. the sum of the elements). This is ccncf logcn dvlog2lem eluznn ad2antrl imp cnmetdval absdivd rpge0d absidd simplrr cle eluzle nnleltp1 lttrd mulid1d breqtrrd 1red ltdivmuld eqbrtrd ex cxmet cxr cnxmet rpxr elbl3 syl22anc fmpttd ssrdv divcnvshft climaddc1 - simpr syl6breq eqbrtrrd ellogdm mpbir2an climcncf csn wf1o logf1o logdmss + simpr breqtrdi eqbrtrrd ellogdm mpbir2an climcncf csn wf1o logf1o logdmss 0p1e1 f1of cofmpt wss frn cores 3syl log1 syl6eq 3brtr3d rexlimddv dmgmn0 fvres fvex climsubc2 subid1d rpdivcld fzfid eqeltrrd nncand sub4d pncan2d id subdird mulid2d subsubd addcomd subsub2d wne nnnn0d dmgmaddn0 nnncan2d @@ -365029,7 +365029,7 @@ sum notation (which we used for its unordered summing capabilities) into sumz 1cnd min1 syl31anc 3eqtrrd 3brtr4d fsumabs elfzelz rpexpcl absge0d exple1 subge0 leexp2rd lemul2ad fsumle fsummulc1 breqtrrd mulcomd nnssz expp1d sstri ne0d infssuzcl eqeltrid sseldi rpexpcld peano2re min2 0red - syl6breq fsumge0 lemuldiv2 syl112anc ltletrd ltsub2dd ltaddsubd 2fveq3 + breqtrdi fsumge0 lemuldiv2 syl112anc ltletrd ltsub2dd ltaddsubd 2fveq3 breq1d rspcev ) AELUBUCZUDUEZVUJIUFZUGUFZUHIUFZUGUFZUIUJZBUKZIUFUGUFZVU OUIUJZBUDULAELAEUDUEZFUMUEZLUMUEZAJUNUEZJCUFZUHUOZUPZVUTVVAVVBUQZACDEFG HIJKLMNOPQRSTUAUSZURZUTZALALAVUTVVAVVBVVIUUAZVAZVBZVCZAVUMVUOVUOLJVDUCZ @@ -365533,7 +365533,7 @@ sum notation (which we used for its unordered summing capabilities) into vk vx vy csn cxp cof 1zzd ax-1cn cuz eqimss2i nnex climconst2 basellem6 cz ovexd cv wf wss elexi fconst snssd fss ffvelrnda c2 cdiv 2nn nnmulcl wa sylan peano2nnd nnrecred recnd fmptd ffnd inidm eqidd climmul mul01i - ofval syl6breq 1ex mulcl adantl off climadd mptru 1p0e1 breqtri ) FGUEZ + ofval breqtrdi 1ex mulcl adantl off climadd mptru 1p0e1 breqtri ) FGUEZ UFZFAUEZUFZCHUGZIZJUGZIZGKJIZGLWQWRLMNGKUBWKWOWQGOFUANUHZNGPQZGUOQZWKGL MUIWSGGFFGUJRUAUKZULUMSNWKWOWPUPNWOAKHIKLNAKUBWMCWOGOFUAWSNAPQZXAWMALME WSAGFXBULUMSNWMCWNUPCKLMNBCDUNTNFPUBUQZWMNFWLWMURWLPUSFPWMURFAAPEUTVANA @@ -365684,7 +365684,7 @@ sum notation (which we used for its unordered summing capabilities) into 6re 6nn redivcli snssd fss sylancr resubcl 1ex 1red 2nn nnmulcl peano2nnd sylan nnrecred nnex inidm off readdcl negex ovexd feqmptd offval2 3eqtr4d nnne0i cc recn recni climconst2 ax-resscn sylancl basellem7 ffnd fnconstg - c3 wbr wfn syl offn eqidd ofval climmul syl6breq eqbrtrid 3cn mul01i ofc1 + c3 wbr wfn syl offn eqidd ofval climmul breqtrdi eqbrtrid 3cn mul01i ofc1 2cn eqbrtrrd cle npcand mpteq2dva w3a subdi syl3an caofdi oveq12i syl6eqr zrei cuz eqimss2i ofnegsub mp3an2i neg1cn syl6eqbrr mulid1i basellem6 3ex 3re mulid2d mulneg1 negeqd mulcl negnegd eqtr2d oveq12d eqtrd df-3 ax-1cn @@ -366667,7 +366667,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 ppieq0 $p |- ( A e. RR -> ( ( ppi ` A ) = 0 <-> A < 2 ) ) $= ( cr wcel cppi cfv cc0 wceq c2 clt wbr wn cle wne wb 2re wa ex c1 adantr cz lenlt mpan ppinncl nnne0d sylbird necon4bd cfl reflcl 1red caddc co 2z fllt - mpan2 biimpa df-2 syl6breq 1z zleltp1 sylancl mpbird ppiwordi syl3anc ppifl + mpan2 biimpa df-2 breqtrdi 1z zleltp1 sylancl mpbird ppiwordi syl3anc ppifl flcl ppi1 a1i 3brtr3d cn0 ppicl nn0le0eq0 syl mpbid impbid ) ABCZADEZFGZAHI JZVOVRVPFVOVRKZHALJZVPFMZHBCVOVTVSNOHAUAUBVOVTWAVOVTPVPAUCUDQUEUFVOVRVQVOVR PZVPFLJZVQWBAUGEZDEZRDEZVPFLWBWDBCZRBCWDRLJZWEWFLJVOWGVRAUHSWBUIWBWHWDRRUJU @@ -367481,7 +367481,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 5nn nnzi 3p2e5 pncan2 negeqi 3eqtr2i divneg lenegi ltnegi 1pneg1e0 neg1cn 0z neg0 renegcli neg1z 2timesd df-6 addsub4 mulcl divsubdir 3t2e6 mulcomi subneg 3ne0 2cnne0 divcan5 dividi divdir mp3an3 addassd 3brtr4d lesubaddd - npcan readdcl ppiwordi mp3an2 syl6breq 3pos divge0 addge02 lecasei ) ACDZ + npcan readdcl ppiwordi mp3an2 breqtrdi 3pos divge0 addge02 lecasei ) ACDZ EAFGZUAZAUBHZAIJKZLMKZFGZIAICDZVULUCNVUJVUKUDVUJIAFGZVUPVUKVUJVURUAZVUMLO KZVUNFGVUPVUSVUTBUEZPUFKZQTUGDZBUHAUIHZUJKZUKZULHZVUNVUSVUMCDZLCDZVUTCDVU JVVHVURVUJVUMAUMUNZUOZUPVUMLUQURVVGCDVUSVVGVVFUSDZVVGUUADVVEUSDZVVFVVEUTV @@ -367581,7 +367581,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 chpeq0 $p |- ( A e. RR -> ( ( psi ` A ) = 0 <-> A < 2 ) ) $= ( cr wcel cchp cfv cc0 wceq c2 clt wbr wn cle wne wb wa ex adantr sylancl c1 cz 2re lenlt mpan chprpcl rpne0d sylbird necon4bd reflcl 1red caddc co - cfl 2z fllt mpan2 biimpa df-2 syl6breq 1z zleltp1 mpbird chpwordi syl3anc + cfl 2z fllt mpan2 biimpa df-2 breqtrdi 1z zleltp1 mpbird chpwordi syl3anc flcl chpfl chp1 a1i 3brtr3d chpge0 chpcl 0re letri3 mpbir2and impbid ) AB CZADEZFGZAHIJZVOVRVPFVOVRKZHALJZVPFMZHBCVOVTVSNUAHAUBUCVOVTWAVOVTOVPAUDUE PUFUGVOVRVQVOVROZVQVPFLJZFVPLJZWBAULEZDEZSDEZVPFLWBWEBCZSBCWESLJZWFWGLJVO @@ -368100,7 +368100,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 cc wb sylancr simp3d logled eqbrtrd lemuldivd wn eldifn adantl elin rbaib df-3an syl6bb baibd bitrd mtbid ltnled lt2sqd eqbrtrrd nnsqcld syl2anc cz logltb sylancl breqtrd eqtrd flle letrd chash cn0 cfz relogexp ltdivmul2d - 2z 2re df-2 syl6breq 1z flbi mpbir2and oveq2d oveq1d subidd fsumss chtval + 2z 2re df-2 breqtrdi 1z flbi mpbir2and oveq2d oveq1d subidd fsumss chtval chpval2 oveq12d 3eqtr4rd lemuldiv2d fsumle fsumconst hashcl nn0red logge0 subge02d cdom fzfid ppisval inss1 2eluzge1 fzss1 mp1i sstrid eqsstrd sylc ssdomg hashdom flge0nn0 hashfz1 lemul1ad lesubadd2d ) ACDZEAFGZHZAUAIZAUB @@ -368260,7 +368260,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 ( crp cfv cdiv co cmin cmpt c1 crli wbr wtru cc0 wcel wa cc cr adantl cle cabs adantrr clog cfl cfa caddc 1red 1cnd wne wceq relogcl rpcnne0 divdir recnd syl3anc mpteq2dva simpr rerpdivcld rpreccl rpred ccxp simpld oveq2d - cxp1d 1rp cxploglim mp1i eqbrtrrd ax-1cn divrcnv rlimadd eqbrtrd syl6breq + cxp1d 1rp cxploglim mp1i eqbrtrrd ax-1cn divrcnv rlimadd eqbrtrd breqtrdi cv 00id peano2re syl cn0 cn rprege0 flge0nn0 faccl 3syl nnrpd subcld cmul logfacbnd3 clt ad2antrl subcl sylancl mulcld abscld rpregt0 lediv1 simprd wb mpbid divcan3d oveq1d divsubdir sub32d 3eqtr4rd fveq2d absdivd abssubd @@ -368300,7 +368300,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 cn 1z a1i cdv nnne0d eqtrd oveq2 fveq2d w3a rpdivcld log1 mulid2d eqbrtrd rpcnd rpred lemuldivd mpbid wb logleb sylancr eqbrtrrid 3ad2antr1 sumeq1d ad2antrl cvv syl6eq sumeq2dv ax-1cn cdif div0d ovexd fvmptd ax-mp 3brtr3d - syl 3eqtrd divsubdir syl3anc wss rpssre rlimconst breqtrd syl6breq simpld + syl 3eqtrd divsubdir syl3anc wss rpssre rlimconst breqtrd breqtrdi simpld cxp1d nn0cn cxploglim2 sylancl eqbrtrrd vtoclga rpcnne0 divcld cpnf ioorp csb cioo eqcomi nnuz cz 1re 1nn0 nn0addge1i 0red rpre simprl sylan sylan2 nnrp reelprrecn advlogexp syl2anc dvmptcmul divcan2d rpxrd simp1rl simp2r @@ -370014,7 +370014,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 syl nnne0d divassd recnd muls1d oveq12d wceq 2cn nncan breqtrd lelttrd 1z eqtrd breq2d nnred cuz nnrpd efexple syl3anc nnzd rplogcld rpge0d adantrr wn ltdivmul syl112anc bitrd impr 0p1e1 breqtrrdi 0z flbi mpbir2and syl6eq - eqcomd ce cn0 3brtr4d 3syl df-2 syl6breq zleltp1 iftrue syl5ibrcom nnge1d + eqcomd ce cn0 3brtr4d 3syl df-2 breqtrdi zleltp1 iftrue syl5ibrcom nnge1d biantrurd prmuz2 eluz2gt1 jca elfzelz 1lt2 2t1e2 nnre 0le2 nnge1 syl31anc lemul2a eqbrtrrid ltletrd rpdivcld 3bitr4rd notbid ltnled mulid1d biimprd elfz bitr4d nngt0d ltaddrp2d 2timesd breqtrrd wi lttr mpand sylibrd 2t0e0 @@ -370086,7 +370086,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 elfznn wa oveq2 prmnn syl nncnd exp1d sylan9eqr oveq2d fveq2d caddc 2t1e2 mulid2d eqbrtrd wb nnred nngt0d lemuldiv syl112anc mpbid nndivred 1re 2re 1red 2pos pm3.2i lemul2 mp3an13 eqbrtrrid nnne0d divassd breqtrrd nnmulcl - 2cnd 2nn sylancr 3pos ltdiv23 mp3an2 syl12anc df-3 syl6breq cz 2z sylancl + 2cnd 2nn sylancr 3pos ltdiv23 mp3an2 syl12anc df-3 breqtrdi cz 2z sylancl 3re flbi mpbir2and eqtrd c4 remulcl a1i 4re eqbrtrrd 3lt4 lttrd breqtrrdi 2t2e4 ltmul2 mp3an23 mpbird df-2 syl6eq oveq12d 2cn subidi crp eluzge2nn0 1z nnrpd nnexpcl syl2an rpdivcld rpge0d ltdivmul ltdivmuld 1e0p1 rpred 0z @@ -370767,7 +370767,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 lgslem3 $p |- ( ( A e. Z /\ B e. Z ) -> ( A x. B ) e. Z ) $= ( cz wcel cabs cfv c1 cle wbr wa cmul co wceq cr jca fveq2 breq1d zcn cc0 zmulcl ad2ant2r cc absmul syl2an wi abscl absge0 syl adantr 1red lemul12a - adantl syl22anc imp an4s 1t1e1 syl6breq eqbrtrd cv elrab2 anbi12i 3imtr4i + adantl syl22anc imp an4s 1t1e1 breqtrdi eqbrtrd cv elrab2 anbi12i 3imtr4i ) BFGZBHIZJKLZMZCFGZCHIZJKLZMZMZBCNOZFGZVOHIZJKLZMBDGZCDGZMVODGVNVPVRVFVJ VPVHVLBCUCUDVNVQVGVKNOZJKVFVJVQWAPZVHVLVFBUEGZCUEGZWBVJBUAZCUAZBCUFUGUDVN WAJJNOZJKVFVJVHVLWAWGKLZVFVJMZVHVLMZWHWIVGQGZUBVGKLZMZJQGZVKQGZUBVKKLZMZW @@ -372934,7 +372934,7 @@ multiple of the prime (in which case it is ` 0 ` , see ~ lgsne0 ) and resubcld fllt 3bitrd peano2rem 3bitr4d 2nn nnmulcl 2timesd mvrladdd ltm1d anbi2d ltdiv1 div32d peano2re elfzle1 ltletrd ltdivmul eqbrtrrid ledivmul ltled flltp1 zlem1lt lemuldiv div23d flge subled pm4.71rd bitr4d pm5.32da - letrd letr syl5bb syl6breq lemuldiv2 posdifd elnnz oveq12i pncan2d eqtr3d + letrd letr syl5bb breqtrdi lemuldiv2 posdifd elnnz oveq12i pncan2d eqtr3d sylanbrc ltsub23d biantrurd bitr3d anbi12d vex op1std eqeq1d opelxp velsn biancomi anbi1i 3bitr4g eqrelrdv xpsnen2g hasheni ltmul2 eqbrtrrd zltlem1 cen ltdivmul2 breqtrrd eluz2 syl3anbrc uznn0sub hashfz1 fsumsub fsumconst @@ -373175,7 +373175,7 @@ multiple of the prime (in which case it is ` 0 ` , see ~ lgsne0 ) and ( co cmul c1 wcel wa syl vw vz clgs cneg cfz clt wbr copab chash cfv cexp cv caddc necomd weq wb bi2anan9 biancomd oveq1 breqan12d anbi12d cbvopabv eleq1w ancoms lgsquadlem2 cen wceq ccnv cfn relopab cxp wss fzfid syl2anc - wrel xpfi opabssxp sylancl sylancr cnvopab syl6breq hasheni oveq2d eqtr4d + wrel xpfi opabssxp sylancl sylancr cnvopab breqtrdi hasheni oveq2d eqtr4d ssfi cnven oveq12d cc neg1cn a1i cn0 eqsstri hashcl expaddd cun wne cdvds wo wn cn cmin cprime c2 csn eldifad adantr prmnn cuz cz gausslemma2dlem0b cle nnzd prmz peano2zm nnred zred cdiv crp uz2m1nn nnrpd elfzelz ad2antll @@ -375359,7 +375359,7 @@ to the second component (see, for example, ~ 2sqreunnltb and 4re rpred 2nn nnmulcl nndivred remulcld syl 0red 8pos relogcld rerpdivcld elrpd syl2anc cexp elrpii rpexpcl nnrpd rpdivcld epr rerpdivcl c3 egt2lt3 4pos simpri 3lt4 3re lttri mp2an ltled oveq1i nngt0d mpbird recnd breqtrd - syl3anc cc recni rpcnd wceq wne lttrd leidi logdivlt loge syl6breq pm3.2i + syl3anc cc recni rpcnd wceq wne lttrd leidi logdivlt loge breqtrdi pm3.2i mpanl12 jca lt2mul2div syl22anc mulid2d ltmuldiv ltsub2dd subdird mulcomd 2z zmulcl relogexp 2cnd nnnn0d cn0 2nn0 expmuld sq2 syl6eq fveq2d 3eqtr2d divrec2d divcan5d eqtr3d oveq12d eqtrd relogdivd 3brtr4d cbc chebbnd1lem1 @@ -375543,7 +375543,7 @@ to the second component (see, for example, ~ 2sqreunnltb and adantl cpnf cico cv ccht cppi clog cdiv cmpt crli cmin cabs wral wrex cif wi csqrt cexp rpre resubcl sylancr ifcl 0red halfgt0 max2 sylancl ltletrd elrpd rpsqrtcld halflt1 ltsubrp mpan breq1 ifboth rpge0d 0le1 mpbid sqrt1 - sqrtltd syl6breq chtppilimlem2 wa adantr max1 wb 2re elicopnf ax-mp chtcl + sqrtltd breqtrdi chtppilimlem2 wa adantr max1 wb 2re elicopnf ax-mp chtcl simplbi syl ppinncl sylbi nnrpd 1lt2 simprbi rplogcld rpmulcld rerpdivcld cn lelttr syl3anc mpand wceq recnd sqsqrtd oveq1d rpregt0d ltmuldiv bitrd breq1d 2pos chtleppi mulid1d breqtrrd ledivmuld mpbird abssuble0d ltsub23 @@ -375646,7 +375646,7 @@ to the second component (see, for example, ~ 2sqreunnltb and ltletrd chtrpcl syl2anc rerpdivcld wss ssriv rlimconst sylancr ccxp cof cvv recnd ovexd cxpsqrt oveq2d wne rpsqrtcld rpcnne0d divcan5 syl3anc remsqsqrt eqidd 3eqtr2d mpteq2dva offval2 rpne0d syl211anc eqtrd co1 chto1lb rphalfcl - dmdcan 1rp cxploglim rlimres2 o1rlimmul eqbrtrrd rlimadd 1p0e1 syl6breq 1re + dmdcan 1rp cxploglim rlimres2 o1rlimmul eqbrtrrd rlimadd 1p0e1 breqtrdi 1re readdcl chpcl chtcl readdcld letrd chpub lediv1dd rpcnd divdir divid oveq1d breqtrd adantrr mulid2d chtlepsi eqbrtrd lemuldivd mpbid rlimsqz2 mptru 1le2 ) ABUAUBCZAUCZUDUEZYIUFUEZDCZEFGHIAYHFYIUGUEZYIUHUEZJCZYKDCZKCZYLFFIUI @@ -376938,7 +376938,7 @@ to the second component (see, for example, ~ 2sqreunnltb and fvmpt absidd 3eqtrd rpcnne0 div12 syl3anc 3brtr4d rspccva eqcomd nnrp syl6eleq pm2.61dane elfzelz 3rp nndivre remulcld cxr w3a rexri elico2 mp2an simp1bi 0lt1 simp2bi subcld abs2dif2d fsumabs absge0d wss flcld - 2z simp3bi 3z fllt df-3 syl6breq zleltp1 mpbird eluz2 syl3anbrc fzss2 + 2z simp3bi 3z fllt df-3 breqtrdi zleltp1 mpbird eluz2 syl3anbrc fzss2 rpre fsumless log1 elfzle1 breq2 ifboth 1rp logleb eqbrtrrid rpregt0d divge0 syl21anc eqeltrd nnred 2re elfzle2 2lt3 lelttrd breq1 wi rpred ltle mpd lediv1d eqbrtrd fsumle leadd1d ralrimiva dchrvmasumlem3 ) AB @@ -377569,7 +377569,7 @@ a multiplicative function (but not completely multiplicative). eldifsn znzrhfo fof nnz ffvelrn ffvelrnd nncn nnne0 cjdivd 3eqtr4d wrex wex dchrmusumlema simprrl simprrr dchrvmaeq0 breqtrd rexlimdvaa exlimdv eqtrd mpd seqex ovex serf simpl fsumcj cuz syl6eleq 3eqtr3rd climcj cj0 - simpr syl6breq isumclim sumeq2sdv eqeq1d elrab2 simplr nehash2 lemul2ad + simpr breqtrdi isumclim sumeq2sdv eqeq1d elrab2 simplr nehash2 lemul2ad suble0 df-2 oveq1i 1cnd addsubassd syl5eq adantrr adddid mulid1d 3eqtrd fveq1 mul01d 3brtr3d nn0ge0d clt vmage0 nngt0d syl22anc fsumge0 mulge0d divge0 leaddsub syl3anc 3brtr4d ex necon1bd mpi fveq1d eqtr3d ralrimiva @@ -378335,7 +378335,7 @@ a multiplicative function (but not completely multiplicative). recnd zcnd fsumcl rpne0 divcld ovexd eqidd offval2 wss adantr cc0 absdivd rpcn wne rprege0 absid oveq2d eqtrd abscld adantlr fsumabs fz1ssnn sselda fsumrecl absmuld absge0d simpl nnrpd rpdivcl sseldi flle abssubge0d mule1 - fracle1 eqbrtrd lemul12ad 1t1e1 syl6breq chash cfn 1cnd fsumconst syl2anc + fracle1 eqbrtrd lemul12ad 1t1e1 breqtrdi chash cfn 1cnd fsumconst syl2anc fsumle flge1nn sylan nnnn0d hashfz1 oveq1d mulid1d breqtrd letrd breqtrrd 3eqtrd ledivmuld mpbird elo1d crli ax-1cn divrcnv ax-mp rlimo1 mp1i o1add cn0 rpcnne0 w3a eqtr3d syl3anc 3eqtr3d sumeq2dv eqeltrrd nndivred fsumadd @@ -378590,7 +378590,7 @@ a multiplicative function (but not completely multiplicative). cz wceq sylan2 nncnd eqtrd sumeq2dv fsummulc2 cc0 wne jca div23 syl3anc rpcnne0 divdiv1 fveq2d oveq12d oveq2d oveq2 rpred ere clt c3 ltleii 1rp addge0d mulid2d letrd eqbrtrd mpbid wb logleb eqbrtrrid divge0 syl21anc - log1 ad3antrrr absidd syl6breq lediv1 ad5ant15 adantlr logfacrlim2 mucl + log1 ad3antrrr absidd breqtrdi lediv1 ad5ant15 adantlr logfacrlim2 mucl cmu simplr rerpdivcld rlimcl rlimo1 o1mul2 o1add2 sqcld ad2antrr addcld halfcld relogcl zcnd nnrp nnne0d div23d subdid fsumsub cdvds w3a divass crab eqtr3d mulcomd ssrab2 simprr sseldi ad2antrl remulcld dvdsflsumcom @@ -381470,7 +381470,7 @@ a multiplicative function (but not completely multiplicative). cc cmin c3 resubcld c4 rpdivcld lttrd cchp rpne0d oveq2d eqtrd rpcnne0d oveq1d oveq12d fveq2d addassd letrd fveq2 oveq2 rspcdva syl2anc breqtrd id wb rpcnd wrex nnrpd pntibndlem1 nnred cico wss relogcld pnfxr sseldd - icossre ltmul12ad 1t1e1 syl6breq ltadd2dd df-2 rpcnne0 div23 lemuldiv2d + icossre ltmul12ad 1t1e1 breqtrdi ltadd2dd df-2 rpcnne0 div23 lemuldiv2d ltmul1dd ltletrd pntibndlem2a simp1d simp2d pntrf nndivred abs2difd 3re rpgecld cn 4nn nnrp efgt1 ltaddrpd rplogcld peano2re chpcl cneg abstrid renegcld divsubdird dividd 1cnd subdird dmdcan 3eqtrd negeqd negsubdi2d @@ -381809,7 +381809,7 @@ a multiplicative function (but not completely multiplicative). ltled rerpdivcld 3jca relogcld nndivre relogexp recnd oveq2d oveq1d wne cc rpcnne0d 3eqtrd elico2 rpgecld rpsqrtcld 1lt2 simpli simpri 3lt4 3re pnfxr pntlemd cioo pntlemc rpdivcl ltmul1dd mulid2d 4pos ltmul2 mulid1i - jctir 4cn syl6breq resqcld 3nn0 2nn decnncl 3rp breqtrrdi resqrtth 0le1 + jctir 4cn breqtrdi resqcld 3nn0 2nn decnncl 3rp breqtrrdi resqrtth 0le1 rpefcld syl21anc sq1 ltmul2dd remsqsqrt rplogcld readdcl addcomd syl5eq logltb eqbrtrrd ltmuldiv2 ltdiv1dd relogmuld eqtrd 2cnd mulcld divcan4d divdir rpcnne0 divdiv32 remulcld divdiv2 mulcomd div23 reefcld reeflogd @@ -381917,7 +381917,7 @@ a multiplicative function (but not completely multiplicative). rerpdivcld cn cuz c4 pntlemg simp1d nnred elfzuz eluznn syl2an caddc cr cfl flltp1 breqtrrdi elfzle1 adantl ltletrd ltdivmul2d mpbid cz elfzelz syl wceq relogexp syl2anc breqtrrd wb rpexpcld logltb mpbird c2 sylancl - oveq2d 2z 2cnd recnd mulassd 3eqtr4d elfzle2 syl6breq ceu cdc rehalfcld + oveq2d 2z 2cnd recnd mulassd 3eqtr4d elfzle2 breqtrdi ceu cdc rehalfcld pntlemb flge 2re a1i 2pos lemuldiv2 syl112anc remulcl sylancr lemuldivd c3 eqbrtrd rprege0d rpexpcl logled resqrtth rpsqrtcld le2sq jca ) AJMNU QURUSZUTZPKJVAURZVBVCZUUIRVDVEZVFVCZUUHUUJPVGVEZUUIVGVEZVBVCZUUHUUMJKVG @@ -383537,7 +383537,7 @@ a multiplicative function (but not completely multiplicative). cle cgcd caddc nnexpcl nnzd mpd zq qmulcl rpred cvv qex ad2antrl wral ccnfld breq1d 1re rspcdva letrd eqbrtrd prmuz2 eluz2b2 simpld qrngbas sylib qrng0 relogcld nnred simprd rplogcld rerpdivcld renegcld logltb - cuz 1rp log1 syl6breq 0red ltdivmuld lt0neg1d padicabvcxp nncnd exp1d + cuz 1rp log1 breqtrdi 0red ltdivmuld lt0neg1d padicabvcxp nncnd exp1d mul01d pcid eqtr3d neg1z cxpexpzd eqtr4d mulm1d negeqi negnegd syl5eq nnrpd neg1rr cxpmuld cxpefd divcan1d reeflogd 3eqtr3d 3eqtrrd eqeq12d 1z syl5ibcom prmnn 1cxpd cdvds pceq0 dvdsprm sylan necon3bbid biimpar @@ -409683,7 +409683,7 @@ According to Wikipedia ("Cycle (graph theory)", cfz caddc csn cpr wss wif cfzo wral w3a ccsh ccrcts crctiswlk wlkf cshwcl 3syl syl eqeltrid adantr cmin cle cif wi wlkp simpll cn0 elfznn0 elfzonn0 nn0addcld elfz3nn0 eqeltrrid ad2antlr cr wb elfzelz zred elfzoelz elfzel2 - adantl leaddsub syl3anc biimpar syl6breq sylanl1 elfz2nn0 sylibr ffvelrnd + adantl leaddsub syl3anc biimpar breqtrdi sylanl1 elfz2nn0 sylibr ffvelrnd 3jca adantll elfzoel2 zaddcl adantrr simprr zsubcld clt zsubcl ancoms zre wn cz ltnle syl2anr ltsubadd syl2an23an posdifd 0red ltle syl2anc sylbird sylbid imp exp31 syl11 imp31 nn0re 3ad2ant1 3impia ex mpbird mpcom oveq2d @@ -440731,7 +440731,7 @@ negative of a vector from this axiom (see ~ hvsubid and ~ hvsubval ). ( normh ` ( A -h B ) ) < D ) $= ( cmv co cno cfv c2 clt wbr caddc hvsubcli normcli readdcli recni cdiv wa cle norm3difi rehalfcli lt2addi lelttri sylancr 2timesi 2cn divcan2i - cmul 2ne0 eqtr3i syl6breq ) ACIJZKLZDMUAJZNOCBIJZKLZURNOUBZABIJZKLZURUR + cmul 2ne0 eqtr3i breqtrdi ) ACIJZKLZDMUAJZNOCBIJZKLZURNOUBZABIJZKLZURUR PJZDNVAVCUQUTPJZUCOVEVDNOVCVDNOABCEFGUDUQUTURURUPACEGQRZUSCBGFQRZDHUEZV HUFVCVEVDVBABEFQRUQUTVFVGSURURVHVHSUGUHMURULJVDDURURVHTUIDMDHTUJUMUKUNU O $. @@ -451563,7 +451563,7 @@ problem in Remark (b) after Theorem 7.1 of [Mayet3] p. 1240. ( vy cfv cnop cle wbr cno c1 chba wf wcel bdopf mp2b wa cmul co cr adantr cbo cado cv wi wral wb adjbdln nmopxr nmopub mp2an ffvelrni normcl nmopre cxr syl ax-mp remulcl sylancr 1re remulcli a1i nmopadjlei nmopge0 lemul2a - cc0 pm3.2i mp3anl3 mpanl2 sylan letrd recni mulid1i syl6breq ex mprgbir ) + cc0 pm3.2i mp3anl3 mpanl2 sylan letrd recni mulid1i breqtrdi ex mprgbir ) AUADZEDAEDZFGZCUBZHDZIFGZVRVODZHDZVPFGZUCZCJJJVOKZVPUMLZVQWDCJUDUEATLZVOT LWEBAUFVOMNZWGJJAKZWFBAMZAUGNCVPVOUHUIVRJLZVTWCWKVTOZWBVPIPQZVPFWLWBVPVSP QZWMWKWBRLZVTWKWAJLWOJJVRVOWHUJWAUKUNSWKWNRLZVTWKVPRLZVSRLZWPWGWQBAULUOZV @@ -451755,7 +451755,7 @@ problem in Remark (b) after Theorem 7.1 of [Mayet3] p. 1240. mp2b cado ccom cnop c2 cexp cv wi wf cxr wral wb cbo adjbdlnb mpbi hocofi bdopf nmopre resqcli rexr nmopub mp2an hocoi fveq2d ffvelrni 3syl remulcl normcl sylancr remulcli a1i nmbdoplbi nmopge0 pm3.2i lemul2a mpanl2 sylan - 1re mp3anl3 recni mulid1i syl6breq letrd syl21anc eqbrtrd nmopadji oveq1i + 1re mp3anl3 recni mulid1i breqtrdi letrd syl21anc eqbrtrd nmopadji oveq1i sqvali eqtr4i ex mprgbir csqrt bdopcoi sqrtcli csp cabs cc mpancom abscld hicl remulcld bcs hococli normge0 jca simpr mp3anl2 recnd mulid1d breqtrd eqtr4d resqcl sqge0 absidd normsq cdm bdopadj mp3an1 adjadj fveq1i oveq2i @@ -453586,7 +453586,7 @@ A C_ ( _|_ ` B ) ) ) -> ( ( normh ` ( S ` ( A vH B ) ) ) ^ 2 ) = ( wcel cch wa cfv cno cle wbr c2 cexp co caddc adantlr syl sylan2 adantrr c1 cr chst wss cort wceq hstnmoc oveq2d hstcl normcl resqcld adantr recnd chba choccl add12d eqtr3d chj ococ sseq2d biimpar jca hstpyth cc0 anassrs - chjcl normge0 hstle1 le2sq2 mpanr1 syl21anc syl6breq eqbrtrrd wb readdcld + chjcl normge0 hstle1 le2sq2 mpanr1 syl21anc breqtrdi eqbrtrrd wb readdcld 1re sq1 leadd2 mp3an2 syl2anc mpbid eqbrtrd leadd1 mp3an3 mpbird le2sq ) CUADZAEDZFZBEDZABUBZFZFZACGZHGZBCGZHGZIJZWMKLMZWOKLMZIJZWKWSWQSNMZWRSNMZI JZWKWTWRWQBUCGZCGZHGZKLMZNMZNMZXAIWGWHWTXHUDWIWGWHFZWQWRXFNMZNMWTXHXIXJSW @@ -453784,7 +453784,7 @@ A C_ ( _|_ ` B ) ) ) -> ( ( normh ` ( S ` ( A vH B ) ) ) ^ 2 ) = cch stcl eqeq1d wn eqcom wne wi readdcld ltne ex syl necon2bd syl5bi wa readdcli a1i 1red le2addd leadd2dd adantr w3a ltadd1 biimpd syl3anc imp stle1 readdcl sylancl lelttr mp2and c2 df-3 df-2 oveq1i addassi 3eqtrri - ax-1cn syl6breq con3d wo wb leloe mpbid ord 3syld sylbid ) DUAHZADIZBDI + ax-1cn breqtrdi con3d wo wb leloe mpbid ord 3syld sylbid ) DUAHZADIZBDI ZJKCDIZJKZLMWKWLWMJKZJKZLMZWKNMZWJWNWPLWJWKWLWMWJWKWJAUDHZWKOHZEADUEPZU BWJWLWJBUDHZWLOHFBDUEPZUBWJWMWJCUDHZWMOHGCDUEPZUBUCUFWJWQWPLQRZUGZWKNQR ZUGWRWQLWPMWJXGWPLUHWJXFLWPWJWPOHZXFLWPUIZUJWJWKWOXAWJWLWMXCXEUKZUKZXIX @@ -453905,7 +453905,7 @@ A C_ ( _|_ ` B ) ) ) -> ( ( normh ` ( S ` ( A vH B ) ) ) ^ 2 ) = ( wcel cno cfv c1 wceq wa clt wbr c2 cexp cv cdif co cch strlem2 ax-mp wn cpjh eldif chba cheli pjnel biimpa sylan sylbi breq2 syl5ib impcom eldifi wb mpan cc0 cle pjhcli normcl syl normge0 0le1 lt2sq mpanr12 syl2anc 3syl - cr 1re adantr mpbid eqbrtrid sq1 syl6breq ) ACUAZDEUBKZVTLMZNOZPZEFMZNQRH + cr 1re adantr mpbid eqbrtrid sq1 breqtrdi ) ACUAZDEUBKZVTLMZNOZPZEFMZNQRH WDWENSTUCZNQWDWEVTEUHMMZLMZSTUCZWFQEUDKZWEWIOJBCEFGUEUFWDWHNQRZWIWFQRZWCW AWKWAWHWBQRZWCWKWAVTDKZVTEKUGZPWMVTDEUIWNVTUJKZWOWMVTDIUKZWPWOWMWJWPWOWMU TJVTEULVAUMUNUOWBNWHQUPUQURWAWKWLUTZWCWAWNWPWRVTDEUSWQWPWHVMKZVBWHVCRZWRW @@ -463444,7 +463444,7 @@ its graph has a given second element (that is, function value). -> W = ( ( W prefix ( N - 2 ) ) ++ <" ( W ` ( N - 2 ) ) ( W ` ( N - 1 ) ) "> ) ) $= ( wcel c2 cle wbr cfv c1 cmin co cpfx cconcat syl2anc syl cn0 syl3anc cc0 - wceq cword wa chash cs1 cs2 clsw c0 simpl syl6breq wrdlenge2n0 pfxlswccat + wceq cword wa chash cs1 cs2 clsw c0 simpl breqtrdi wrdlenge2n0 pfxlswccat wne simpr lsw oveq1i fveq2i syl6eqr s1eqd oveq2d eqtr3d pfxcl cn eqeltrid lencl nn0ge2m1nn eqeltrrid nn0red lem1d cfz ige2m1fz pfxlen oveq1d cz 0zd pfxn0 nn0ge2m1nn0 1zzd zsubcld 2nn0 a1i nn0sub biimpa syl21anc nn0ge0d cc @@ -467351,7 +467351,7 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a ( cgsu co wcel wceq oveq2d va ve vy vz vx cres cfn wbr wss ssid wa cv csn wi c0 cun sseq1 anbi2d reseq2 breq12d imbi12d cpo comnd ctos omndtos 3syl tospos c0g cfv res0 oveq2i eqid gsum0 eqtri cmnd omndmnd mndidcl eqeltrid - posref syl2anc eqtr4i syl6breq adantr wn ssun1 sstr2 anim2i imim1i simplr + posref syl2anc eqtr4i breqtrdi adantr wn ssun1 sstr2 anim2i imim1i simplr ax-mp simpllr simpr cplusg ad3antrrr wf ad2antrr ssun2 vex snss mpbir a1i sseldd ffvelrnd ccmn sstrid fssresd fvexd fdmfifsupp fsuppres gsumcl ssfi cvv cofr simpll ffnd inidm eqidd ofrval syl3anc omndadd2d elun1 adantl ex @@ -472845,7 +472845,7 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a impbida 3bitr4g dfiun3g 3eqtrd elrnmpt ssrexv sylc nfmpt1 nfrn nfcri rspa simp-5r sseqtrd ralrimi unissb sylibr exp31 reximdai rnex mptex mpbir2and eqsstrd rnexg isref ffun ad6antlr imafi simp3 cnvex fvmpt 3ad2ant2 fnmpti - wfo dffn4 mpbi rabfodom cbvrabv syl6breq rabex nfrab1 nfel1 nfrex ad5antr + wfo dffn4 mpbi rabfodom cbvrabv breqtrdi rabex nfrab1 nfel1 nfrex ad5antr rabid sylanbrc fveqeq2 uniinn0 adantl r19.29af2 ssdomg mpsyl domtr adantr ss2rabdv dffn3 ssrab2 fimarab mpan2 breqtrrd domfi imdistanda imp simplll 3syl simp3d r19.21bi syl3anbrc dmeq rneq 3anbi123d breq1d eleq1d syl32anc @@ -474346,7 +474346,7 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a mp3an csn wo cun uncom 1xr 0le1 snunioc eqtr3i eleq2i bitr3i pm2.53 sylbi wi elun elsni syl6 con1d imp crp cioo wss 0le0 ltpnf ax-mp iocssioo mp4an cr 1re ioorp sseqtri sseli relogcld renegcld rexrd w3a elioc1 simp3bi 1rp - mp2an logled mpbid log1 syl6breq le0neg1d syl elico1 sseldi ifclda adantl + mp2an logled mpbid log1 breqtrdi le0neg1d syl elico1 sseldi ifclda adantl syl3anbrc 0elunit iocssicc snunico rge0ssre reefcld simp2bi le0neg2d efle efgt0 0re sylancl eqeq2 bibi1d simpr iftrue eqeq2d syl5ibrcom ubico nelir ef0 neleq1 mpbiri syl5ibcom df-nel iffalse eqeltrd ex bibi2d syl2an recnd @@ -482024,7 +482024,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry sylib eqbrtrrd fssdm ffun difpreima fimacnv difeq1d uncom difun2 eqtr3i difeq1i eqsstri sspreima eqsstrrd fvimacnvi wf1o simpr3 fresf1o disjrdx difss fvres disjeq2dv bitr3d mpbid biimpa syl21anc 3eqtr3rd ciun uniiun - disjss3 elpwiuncl eqeltrid cfz cbvesum syl6breq fz1ssnn fzfi fnfi resss + disjss3 elpwiuncl eqeltrid cfz cbvesum breqtrdi fz1ssnn fzfi fnfi resss ffn fnssres rnfi rnss cbvdisj disjun0 sylbi sylc carsgclctunlem1 unissd pwidg uniun unisn uneq2i un0 3eqtri uniss unipw elpwid esumeq2d reseq1d resmpt syl6eq eqcomd adantlr syldan ad3antrrr 3eqtr2d carsgmon esumgect @@ -482279,7 +482279,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry sseldd elpwi omsmon syl6sseq nfv ralrimiva esumeq2d 3brtr4d csn cdif snex syl6eq adantr ffvelrnd elsni fveq2d sylan9eqr esumpad2 difss ssdomg domtr neldifsnd mpisyl ssdifssd simprr sylib disjss1 mpsyl cxr wb sseldi csiga - carsggect eqbrtrrd unidif0 syl6breq jca iccssxr xrletri3 sylan2b 3jca crn + carsggect eqbrtrrd unidif0 breqtrdi jca iccssxr xrletri3 sylan2b 3jca crn esumcl ex carsgsiga eqeltrid elrnsiga ismeas 3syl ) AEDUDZDUEOPZDUFUGUHUI ZUURUKZQUUROZUFRZUAULZUJUMSZMUVDMULZUNZUOZUVDUPZUUROZUVDUVFUUROZMUQZRZURZ UADUSZUTZVAZAUVAUVCUVPABUPZUSZUUTDEAUVSUUTEUKZCVBZUPZUSZUUTCVCOZUKZABFPZB @@ -487939,7 +487939,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry sselda ssrexv 3syl mpd c1 cmpt crli cvv cnex eqidd eqbrtrrd mpbid ax-mp rpssre imbi2d rexralbidv r19.29a wne c0p nn0zd coef2 ffvelrnda renegcld mpan2 simplbda negidd breqtrd ge0divd notbid 3bitr4d cicc iccssre ccncf - plycn negelrp biimpa sylancl mul2lt0rlt0 syl6breq coefv0 breqtrrd ivth2 + plycn negelrp biimpa sylancl mul2lt0rlt0 breqtrdi coefv0 breqtrrd ivth2 0nn0 0le0 ioossioo mpanl12 syl6sseq cico cof plyf ffnd ovex rgenw fnmpt wfn eqid mp1i sstri ssexi cin sseqin2 ovexd fvmptd offval oveq1 cbvmptv mpbi signsplypnf expcld divcld ralrimiva 1red rlim3 0lt1 icossioo mp4an @@ -488672,7 +488672,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry fveq2d cr cword csn cdif wcel wne signsvfn syl21anc eqtrd adantr 0red c0 cfzo wf eldifad signstf wrdf 3syl cn eldifsn sylib lennncl fzo0end signstlen oveq2d eleqtrrd ffvelrnd remulcld simpr oveq1i fveq2i eqtri - syl eqeltrid recnd mulcomd breqtrrd syl6breq ltnsymd iffalsed cn0 a1i + syl eqeltrid recnd mulcomd breqtrrd breqtrdi ltnsymd iffalsed cn0 a1i signsvvf nn0cnd addid1d 3eqtrd ) AUGBCUHUIZUJUKZULZKMUMZJMUMZJUNUMZUO UPUIZJEUMZUMZBUHUIZUGUJUKZUOUGUQZURUIZXMUGURUIXMAXLYAUSXJAXLJBUTVAUIZ MUMZYAAKYBMUCVBAJVCVDZVNVEZVFVGZUGJUMUGVHBVCVGZYCYAUSUAUBUDDEFGHIJBMN @@ -491721,7 +491721,7 @@ of the indicator function (Contributed by Thierry Arnoux, wral c4 c8 cexp cioo cvma cof cvts ci cpi cneg ce w3a cprime cin c3 crepr citg chash clt cpnf cico cmap wcel ad3antrrr cdc elmapi ad3antlr ad2antlr wa wf simpr1 wceq fveq2 breq1d cbvralv sylib simpr2 simpr3 oveq1d oveq12d - r19.21bi oveq2d fveq2d cbvitgv syl6breq tgoldbachgtda hgt749d r19.29vva + r19.21bi oveq2d fveq2d cbvitgv breqtrdi tgoldbachgtda hgt749d r19.29vva oveq2 ) AHJZUAJZKZLMUEUFUFUGUGNNNNNUHOZPQZHRUIZWSUBJZKZLUJLUJNNUHOZPQZHRU IZMMMMUJSSUJUKNNNNNNNUHOCSULOTOZUCMLUMOZUCJZUNXETUOZOCUPOZKZXLUNWTXMOCUPO ZKZSULOZTOZUQSURTOTOZCUSZXLTOZTOZUTKZTOZVFZPQZVAZMDVBVCCVDVEKOVGKVHQUBUAM @@ -511392,7 +511392,7 @@ Real and complex numbers (cont.) wi sqcn oveq1 cnmpt11 ctx subcn cnmpt12f mptru cncfcn1 3eltr4i cncfi wceq mp3an1 fvco3 syldan climcn1lem oveq1d syl6eq oveq2d fvmpt csin ovex eqtrd 0cn 1re eqeltrd fveq2 oveq12d resincld simprd cle cmul eqbrtrd cneg ltled - id sq0i div0i 1m0e1 1ex ax-mp syl6breq resqcld 3nn nndivre resubcl abscld + id sq0i div0i 1m0e1 1ex ax-mp breqtrdi resqcld 3nn nndivre resubcl abscld redivcld subdird mulid2d caddc df-3 oveq2i cn0 2nn0 absresq syl5eq div23d expp1 eqtr2d cioc absrpcld rpgt0d ltle mpd cxr w3a wb 0xr elioc2 sin01bnd syl3anbrc ltmuldivd mpbid sinneg div2negd eqeq1d syl5ibrcom absord mpjaod @@ -512619,7 +512619,7 @@ Real and complex numbers (cont.) syl nncn climconst mptru wa simpr nn0p1nn nnzd divcnvlin adantr cc nnnn0d nnexpcl sylan ancoms nnmulcld nnred nnnn0addcl nndivred ffvelrnda adantlr recnd fmpttd nnaddcld simpl expp1d mulassd eqtr4d nn0addcld facp1 addassd - nn0cnd 3eqtr3d divmuldivd 3eqtr4d climmul 1t1e1 syl6breq nn0ind eqbrtrid + nn0cnd 3eqtr3d divmuldivd 3eqtr4d climmul 1t1e1 breqtrdi nn0ind eqbrtrid ex ) CUDEBAFAUOZGHZXTIJKZCLKZMKZXTCJKZGHZNKZUEZIODAFYAYBUAUOZLKZMKZXTYIJK ZGHZNKZUEZIOUFAFYAYBTLKZMKZXTTJKZGHZNKZUEZIOUFZAFYAYBUBUOZLKZMKZXTUUCJKZG HZNKZUEZIOUFZAFYAYBUUCIJKZLKZMKZXTUUKJKZGHZNKZUEZIOUFZYHIOUFUAUBCYITPZYOU @@ -543840,7 +543840,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= sylanb syl12anc syl13anc elfzelz zleltp1 biimpac sylan elfzle2 breqtrrd breq1d jaodan elfz2nn0 syl3anbrc fzss2 sselda 3ad2antr1 ad2antll simprl nfbr fvun1 adantlrr 3adantr3 simpr3 simp1 sylanr2 simp2 adantrlr neeq1d - poimirlem27 poimirlem26 zsubcl dvds2sub mp3an nnncan1 syl6breq dvdssub2 + poimirlem27 poimirlem26 zsubcl dvds2sub mp3an nnncan1 breqtrdi dvdssub2 nfne nn0cni sylancr nn0cn pncan1 rexeqdv 3anbi1d rabbidv cen poimirlem4 simprr hashen eqtr4d con3d expcom a2d 3adant1 fnn0ind mpcom dvds0 hash0 breqtrri fveq2 breqtrrid fzn csbie rexbidv ralbidv syl5ibr necon3bd mpd @@ -545473,7 +545473,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= frn syl6ss supxrcl 3syl pnfge nltpnft necon2abii ovolge0 0re mpanl12 mpan xrre3 sylbir dfss4 rembl cldopn opnmbl eqeltrrd sstr ctop 0cld 0mbl ovol0 difmbl eqtr2i difss2 ssrin ssdif dfin4 fveq2i oveq1i sseq2i anbi1i rexbii - le2addd syl6breq jctl jctil wor ltso xrlenlt notbid bitr4d sylbi retopbas + le2addd breqtrdi jctl jctil wor ltso xrlenlt notbid bitr4d sylbi retopbas adantrl bastg uniopn mblfinlem2 eqcomd anim1i anim2d spcev anasss reximia fvex syl6 r19.41v exbii rexcom4 rexab 3bitr4i eqsupd syl6eq syl6bb cbvabv eqeq2i biimpi mblfinlem3 syl112anc syl5reqr syl5eq ne0i supadd wal reeanv @@ -627044,7 +627044,7 @@ standardize vectors to a length (norm) of one, but such definitions require 2nn sylancl oexpneg syl3anc expcld negcld addcomd negsubd 3eqtrd addcanad eqtrd ad8antr iffalse pm2.61dan eqtr4d negeqd negdid rexlimdva nne bicomi expclzd rexbii rexnal bitri wss ax-mp weq neeq1d addgt0d breqtrd readdcld - 0red expeq0 eluzelz expne0d lt2addd 00id syl6breq breq2d eqeq2d cmul 2nn0 + 0red expeq0 eluzelz expne0d lt2addd 00id breqtrdi breq2d eqeq2d cmul 2nn0 ltnsymd simp-5l nncn 2cnd 2ne0 divcan2d cdvds nndivdvds mvrraddd mvlraddd nnnn0 subcld pncan3d addcld negidd addassd addid2d 3eqtr3d pncand negnegd eqtr3d 3rspcedvd rexlimdva2 reximia 3imtr3i con4i wi c0 0nnn disjsn mpbir @@ -630043,7 +630043,7 @@ to be empty ( ` ( 1 ... 0 ) ` ). (Contributed by Stefan O'Rear, cn cv cfl cdiv irrapxlem1 caddc nnre ad3antlr rpre ad3antrrr elfzelz zred cfz ad2antlr remulcld 1rp a1i modcld intfrac adantl oveq12d fveq2d adantr simpr oveq1d flcld zcnd pnpcand cico 0red 1red modelico sylancl icodiamlt - syl syl22anc 1m0e1 syl6breq eqbrtrd ex wb resubcld nngt0 gt0ne0d rereccld + syl syl22anc 1m0e1 breqtrdi eqbrtrd ex wb resubcld nngt0 gt0ne0d rereccld abscld ltmul2 syl112anc nnnn0 nn0ge0d absidd eqcomd absmuld subdid recidd cle 3eqtr2d breq12d bitrd sylibrd anim2d reximdva mpd ) CUAEZDUBEZFZAUCZB UCZGHZDCXHIJZKLJZIJZUDMZDCXIIJZKLJZIJZUDMZNZFZBODUNJZPZAYAPXJXLXPQJZRMZKD @@ -630263,7 +630263,7 @@ to be empty ( ` ( 1 ... 0 ) ` ). (Contributed by Stefan O'Rear, nngt0d gt0ne0d absgt0 biimpa ltmul1 syl112anc mpbid sqgt0d ltmul2 expclzd mulass syl3anc expneg sylancl recidd oveq1d mulid2d addcomd ppncan 2times cn0 syl abstrid 0le2 sqrtge0d mulge0d nnsqcld 0lt1 lerec syl22anc 1div1e1 - nnge1d syl6breq eqbrtrd ltletrd ltled leadd1dd letrd ) CUADZAUADZBUADZUBZ + nnge1d breqtrdi eqbrtrd ltletrd ltled leadd1dd letrd ) CUADZAUADZBUADZUBZ ABEFZCUCGZUDFZHGZBIUEZUFFZJKZVDZAIUFFZCBIUFFZLFZUDFZHGZUUPUUIUUGUUHMFZLFZ HGZLFZNIUUHLFZMFZJUUNUUPUUSUUPEFZLFUUPUURUUPEFZHGZLFUUSUVCUUNUVFUVHUUPLUU NUVFUUSUUPHGZEFUVHUUNUUPUVIUUSEUUNUVIUUPUUNUUPUUNBUUNBUUCUUDUUEUUMUGZUMZU @@ -638879,7 +638879,7 @@ is in the span of P(i)(X), so there is an R-linear combination of recn redivcld sselda jca ssopab2i df-xp 3sstr4i cif iftrue nfopab2 nfcxfr 1cnd nfv nfima cop elimasn eleq2i opabid 3bitri baib fveq2d iccmbl subidd vex eqrd cxr rexri iccleub mp3an12 sylancl subidi ltsub1d mpbii eqbrtrrid - wb lediv1 syl112anc mpbid dividi syl6breq eqbrtrrd lemul1ad elrpd iccgelb + wb lediv1 syl112anc mpbid dividi breqtrdi eqbrtrrd lemul1ad elrpd iccgelb divge0d le2addd 3brtr4d ovolicc syl3anc iffalse simplbi noel pm2.21i 0mbl wn pm5.21ni ovol0 pm2.61i eqcomi 0re ifcl wfun cpnf wf volf ffun fvimacnv ifcld sylancr rgen rembl cdif eldifn mpteq2ia ccncf ccnfld ctopn eqid ctx @@ -652031,7 +652031,7 @@ elements and the subgroup containing only the identity ( ~ simpgnsgbid ). cz cuz eluzelz syl uzid syl6eleqr cv wceq wa eleq1d fveq2d breq2d imbi12d simpr wne cc wb eleq2i uztrn2 sylan2b sylan syldan absgt0 mpbid ex vtocld mpd 0red abscld ltnled cmpt adantr cvv fvexi mptex a1i adantlr eqidd fvex - cr fvmptd climabs syl6breq eqeltrd c1 2fveq3 imbi2d leidd expcom ad2antrr + cr fvmptd climabs breqtrdi eqeltrd c1 2fveq3 imbi2d leidd expcom ad2antrr abs0 peano2uzs ovex eleq1 anbi2d fveq2 chvarv vtocl sylan2 letrd sylan2br co a2d uzind4 impcom breqtrrd climlec2 mtand eluzel2 serf0 df-nel sylibr ) AUBCDUCZUDUEZPZUFYDYEUGAYFCQUDUHZAYGECRZSRZQUIUHZAQYIUJUHZYJUFAEGPZYKAE @@ -653160,7 +653160,7 @@ elements and the subgroup containing only the identity ( ~ simpgnsgbid ). cz 0z mp2an eqbrtri adantr nn0cnd wne adantl divcld eqeltrd oveq12d wfn ovex eqid fnmpti inidm ofval climsub offval2 divsubdird pnpcan2d eqtr3d mpteq2dva eqtrd df-neg eqcomi 3brtr3d oveq2 oveq1 subcld fveq2d climabs - fvexd eqtr4d absnegi abs1 eqtri syl6breq ) AEJDEUFZKLZXSMUBLZNLZOPZUCZM + fvexd eqtr4d absnegi abs1 eqtri breqtrdi ) AEJDEUFZKLZXSMUBLZNLZOPZUCZM UDZOPZMUGAYEUAEJYBUCZYDQRJUEAEJDMUBLZYANLZUCZEJYAYANLZUCZKUHZLZQMKLZYGY EUGAQMUAYJYLYNQRJUEAUIZAYHMUAYJQRJUEYPADSTZYHSTZIDUJUKZAULYJRTAEJYIUMUN UTAUAUFZJTZUOZEYTYIYHYTMUBLZNLZJYJRUUBYJUPUUBXSYTUQZUOZYAUUCYHNUUFXSYTM @@ -672156,7 +672156,7 @@ not even needed (it can be any class). (Contributed by Glauco mpbid syl3anc mpbir2and ancli nfv nfan nfcv nffv nfbr nfim anbi2d imbi12d eleq1 vtoclg1f sylc cmul cseq fveq1i seq1 syl5eq breqtrrd eqbrtrd jca a1i cfzo w3a cr elfzouz 3ad2ant1 simpl3 wss elfzouz2 fzss2 sselda nfel1 chvar - eleq1d remulcl adantl seqcl simp3 fzofzp1 anabsi7 pm3.35 3adant1 syl6breq + eleq1d remulcl adantl seqcl simp3 fzofzp1 anabsi7 pm3.35 3adant1 breqtrdi ancoms simpl simp1 mulge0d seqp1 breqtrrdi remulcld 1red lemul2ad mulid1d recnd breqtrd simp2 simprd eqbrtrrid letrd eqbrtrid 3exp fzind2 mpcom ) E FGUDUEZQAREBUFZSUGZYOTSUGZUHZMARUAUIZBUFZSUGZYTTSUGZUHZUNARFBUFZSUGZUUDTS @@ -672855,7 +672855,7 @@ closed under the multiplication ( ' X ' ) of a finite number of nncn wne nnne0 divdiv1d mpteq2dva wbr divcld divcnv syl eqbrtrrd wf fmpti eqid mulcld mulne0d fmpttd oveq2 oveq1d oveq12d simpr nncnd addcld nnne0d ffvelrnda fvmptd3 divdird dividd eqtrd eqcomd oveq2d 3eqtrd climadd 1p0e1 - syl6breq ) AEJKLMJUAAJKUFDNJOZDNCBDUGZUBMZPMZOZEJQNUCAUDZAJUFWNJQNUCWSWNQ + breqtrdi ) AEJKLMJUAAJKUFDNJOZDNCBDUGZUBMZPMZOZEJQNUCAUDZAJUFWNJQNUCWSWNQ RADNJUEUHUIAUJUFUGZNRZWTWNUKZJULAXADWTJJNWNSXAWNUMXAWOWTULZUNJUMXAUOXAUJU PUQZUREQRAEDNWPCLMZWPPMZOQFDNXFUEUHUSUIADNCBPMZWOPMZOZWRKUAADNXHWQAWONRZU NZCBWOACSRZXJITZABSRZXJGTZXJWOSRAWOUTUQZABKVAZXJHTZXJWOKVAAWOVBUQZVCVDAXG @@ -679503,7 +679503,7 @@ distinct definitions for the same symbol (limit of a sequence). ( cc0 c2 cpi cmul co wcel cdiv cz cc a1i wne pire pipos clt wbr 2re syl3anc c1 cxr cioo csin cfv wceq elioore recnd 2cnd picn 2ne0 gt0ne0ii divdiv1d wn caddc 0zd cr remulcli 0xr rexrd ioogtlb 2pos mulgt0ii divgt0d crp 1rp elrpd - id div1d iooltub eqbrtrd ltdiv23d 1e0p1 syl6breq btwnnz eqneltrd wb halfcld + id div1d iooltub eqbrtrd ltdiv23d 1e0p1 breqtrdi btwnnz eqneltrd wb halfcld sineq0 syl mtbird neqned ) ABCDEFZUAFGZACHFZUBUCZBWBWDBUDZWCDHFZIGZWBWFAWAH FZIWBACDWBAABWAUEZUFZWBUGDJGWBUHKCBLWBUIKDBLWBDMNUJKUKWBBIGBWHOPWHBSUMFZOPW HIGULWBUNWBAWAWIWAUOGWBCDQMUPKZWBBTGZWATGZWBBAOPWMWBUQKZWBWAWLURZWBVFZBWAAU @@ -685146,7 +685146,7 @@ distinct definitions for the same symbol (limit of a sequence). 2re syl112anc halflt1 lttrd eqbrtrd adantlr cuz cmin simpll simplrl neqne cfv syl eluz2b3 sylanbrc peano2rem ad2antrr rpne0d rereccld cz 1zzd caddc w3a df-2 fveq2i eleq2i eluzsub wi ex sylibr mpd 3adant3 3ad2ant1 resubcld - 1cnd syl6breq syl3an3b wo ltm1d ltnle notbid rspcev rexnal imnan ad2antlr + 1cnd breqtrdi syl3an3b wo ltm1d ltnle notbid rspcev rexnal imnan ad2antlr nnuz con2i sylnib ianor nltled eluzelre remulcld readdcld eluzelcn mulcld imor npcand simp3 3ad2ant2 lemul1 subdird oveq2d divcan1 3brtr3d leadd1dd 3jca eqbrtrrd pm3.2i lediv1 ltadd2dd 1p1e2 2div2e1 pm2.61dan jca32 eximdv @@ -685234,7 +685234,7 @@ distinct definitions for the same symbol (limit of a sequence). elrab2 nfra1 nfrab nfcxfr nfcri nf3an cr wf jca adantr syl simpr ffvelrnd nfcv wi eleq1w anbi2d feq1 imbi12d vtoclg sylc ffvelrnda simprbi r19.21bi simpld mulge0d wceq remulcld fvmpt2 syl2anc breqtrrd 1red lemul12ad 1t1e1 - simprd syl6breq eqbrtrd ex ralrimi nfmpt1 nfeq2 ralbid sylanbrc syl6eleqr + simprd breqtrdi eqbrtrd ex ralrimi nfmpt1 nfeq2 ralbid sylanbrc syl6eleqr elrab ) AEUAZIOZFUAZIOZUBZHPBUAZGUAZUKZQRZXMSQRZTZBDUCZGCUDZIXJHCOPXKHUKZ QRZXSSQRZTZBDUCZHXROXJHBDXKXFUKZXKXHUKZUEUFZUGZCLXJAXFCOZXHCOZYGCOAXGXIUH ZXGAYHXIXGYHPYDQRZYDSQRZTZBDUCZXQYNGXFCIGEULZXPYMBDYOXNYKXOYLYOXMYDPQXKXL @@ -685722,7 +685722,7 @@ functions with (possibly) negative values. (Contributed by Glauco 3pos mpbi rpgt0d mulltgt0 syl22anc chash cfn 0cn fsumconst sylancl hashcl cn0 nn0cn 3syl mul01d rpge0d nfan nfim imbi2d 3expia com12 vtoclgaf mpcom mulge0d fsumle ltletrd zre nndivred 2z nnzd nnred 0le2 lesub2d zcnd eluz2 - wss fzss2 sselda ltadd2dd 3p1e4 3eqtr3ri syl6breq rpcnd subsub4d ltmul1dd + wss fzss2 sselda ltadd2dd 3p1e4 3eqtr3ri breqtrdi rpcnd subsub4d ltmul1dd divdiri mulcomd subdid eqtr3d 1zzd zlem1lt nngt0d ltdiv1 syl112anc nnne0d nncnd dividd mulgt0d ltmul2 mulid1d divcld subdird mulid2d div32d mulassd eqtr4d cn elnnuz elfzp12 orcanai 1p1e2 elfzle1 subge0d mpbird hashfz cneg @@ -686770,7 +686770,7 @@ the final h is a normalized version of G ( divided by its norm, see the co fvmpt2 mpan2 adantl oveq1d mpteq2da stoweidlem4 eqeltrid nfmpt1 nfcxfr cr syl6eqr nfcv stoweidlem33 mpd3an23 eqeltrrd ffvelrnda 1red 0red simprd r19.21bi 1m0e1 breqtrrdi lesubd resubcld syl2anc breqtrrd simpld lesub2dd - simpr syl6breq eqbrtrd jca ex ralrimi sseli sylan2 adantr ltsub23d eldifi + simpr breqtrdi eqbrtrd jca ex ralrimi sseli sylan2 adantr ltsub23d eldifi rpred ltsub2dd nfeq2 fveq1 breq2d breq1d ralbid 3anbi123d rspcev syl13anc anbi12d ) ANFUIUJEUKZNULZUMUNZXRUOUMUNZUPZEGUQZXRKURUNZEMUQZUOKUSVFZXRURU NZEGHUTZUQZUJXQBUKZULZUMUNZYJUOUMUNZUPZEGUQZYJKURUNZEMUQZYEYJURUNZEYGUQZV @@ -686828,7 +686828,7 @@ the final h is a normalized version of G ( divided by its norm, see the wf chvar seqcl cle cneg caddc rpcnd nncnd nnne0d eqcomd oveq2d negsubd c3 a1i cc0 wne wb mpbid lediv2 breqtrd eqbrtrd eqid breqtrrd lelttrd 3eqtr2d divcan1d 1cnd divcld mulcld mulneg1d renegcld 3re 3ne0 rereccld 1lt3 0lt1 - nnred 3pos ltdiv2 syl222anc 1div1e1 syl6breq lttrd ltletrd ltled rpregt0d + nnred 3pos ltdiv2 syl222anc 1div1e1 breqtrdi lttrd ltletrd ltled rpregt0d nnge1d nngt0d syl121anc rpcnne0d syl lenegd bernneq syl3anc oveq1d fmptdf cc divid feq1d mpbird r19.21bi an32s crp addid2d syl221anc 0red ltaddsubd div1d elrpd stoweidlem3 fmuldfeq ex ralrimi ) AUNJUOUPZBUQZMURZUSUTZBCQAU @@ -687047,7 +687047,7 @@ the final h is a normalized version of G ( divided by its norm, see the ( wcel cc0 cv cfv cle wbr c1 wa wral cmin co clt cdif wrex cexp cmpt eqid w3a nnnn0d nnexpcld stoweidlem40 1red cr ffvelrnda cn0 reexpcld nn0expcld adantr resubcld r19.21bi simpld simprd exple1 syl31anc lesub2dd eqbrtrrid - 1m1e0 expge0d stoweidlem12 breqtrrd 1m0e1 syl6breq eqbrtrd jca ex ralrimi + 1m1e0 expge0d stoweidlem12 breqtrrd 1m0e1 breqtrdi eqbrtrd jca ex ralrimi stoweidlem24 stoweidlem25 nfmpt1 nfcxfr nfeq2 fveq1 breq2d breq1d anbi12d 0red wceq ralbid 3anbi123d rspcev syl13anc ) AHEUPUQDURZHUSZUTVAZXRVBUTVA ZVCZDIVDZVBMVEVFZXRVGVAZDPVDZXRMVGVAZDIJVHZVDZUQXQCURZUSZUTVAZYJVBUTVAZVC @@ -688670,7 +688670,7 @@ approximated is nonnegative (this assumption is removed in a later elrpd nnred rpge0d mulge0d ge0p1rpd eqeltrd adantl wa rpmulcl seqcl rpcnd rpne0d reccld fmpti ffvelrnda wceq fveq2 eqidd oveq2d fvmptd 2cn 2ne0 csn eleq1d vtoclga divrecd divcan6d eqcomd mulassd 3eqtrd id rpreccld 3eqtr4d - climmulc2 divcli mulid1i syl6breq divne0i wn recne0d eqnetrd nelsn eldifd + climmulc2 divcli mulid1i breqtrdi divne0i wn recne0d eqnetrd nelsn eldifd cdif recrecd fvmpt3 3eqtr4rd eqeltri climrec mptru recdiv mp4an breqtri ) DGHIJKZJKZIHJKZUDDUVMUDUELUVLUABMGBUFZNCGUGZOZJKZUHZDGUIMUJLUKZLUVSUVLGNK UVLUDLGUVLUABMUVNUVRNKZUHZUVSGUIMUJUVTUWBGUDUELUBABCBMHUVONKZBULUBPIUMKUB @@ -688908,7 +688908,7 @@ approximated is nonnegative (this assumption is removed in a later 2re nnre remulcld cle 0le2 rpge0d mulge0d ge0p1rpd 1red 0le1 readdcld clt rpred nncn mulid2d 1lt2 ltmul1dd eqbrtrrd ltp1d lediv2ad 3brtr4d breqtrrd lttrd ltled climsqz2 1cnd recnd mulcld addcld rpne0d reccld subcld eqcomd - eqtrd climsubc2 1m0e1 syl6breq halfcld sqcld adddid mul12d sqvald mulid1d + eqtrd climsubc2 1m0e1 breqtrdi halfcld sqcld adddid mul12d sqvald mulid1d 2cnd cexp oveq12d wne 2ne0 divcan2d eqtr4d 3eqtrd cz 2z rpexpcld rpaddcld rphalfcld divmuldivd pncand dividd nnne0 divcld divne0d divcan5rd adddird divsubdird divcan6d div12d 1e2m1 oveq2i exp1d expm1d 3eqtr3a eqtr3d eqtri @@ -689623,7 +689623,7 @@ approximated is nonnegative (this assumption is removed in a later cli climrel releldmi mp1i adantr eqcomd nnuz eqbrtrd reccld wtru nnre cdm nnne0 fvmptd seqeq1 trireciplem wn simpl wo elnn1uz2 sylib ord mpd npcand uz2m1nn seqeq1d clim2ser pm2.61dan isumrecl nnrpd rpge0d ge0p1rpd isumge0 - rpmulcld leadd2dd addid1d mulcld isumsplit 3brtr4d 1zzd isumclim syl6breq + rpmulcld leadd2dd addid1d mulcld isumsplit 3brtr4d 1zzd isumclim breqtrdi mptru lemul2ad 4cn gt0ne0d fsummulc2 mulid1d 3brtr3d letrd subled ) EJKZL BMZEBMZLUGUBNZUWCOKUWBUWCLAMZPMZOLJKZUWGOKZUWCUWGUCUDUWHUWFUEKUWIUDACLFUH UWFUIUJZCLCUKZAMPMZUWGJBOCLULZCUWFPCPULZCLACACJUWKUMMUNUWKQNUOMUWKUPUBNUW @@ -691742,7 +691742,7 @@ approximated is nonnegative (this assumption is removed in a later ( cpi cneg co cc0 wcel c2 cdiv cz clt wbr wa c1 caddc pire adantr a1i simpr cr syl3anc cicc csn cdif cmul cmo wceq wn 0zd renegcli iccssre mp2an eldifi wss sseldi 2re remulcli 2pos pipos mulgt0ii divgt0d elrpd cxr rexri iccleub - cle rexrd crp pirp 2timesgt lelttrd ltdiv1dd recni gt0ne0ii dividi syl6breq + cle rexrd crp pirp 2timesgt lelttrd ltdiv1dd recni gt0ne0ii dividi breqtrdi mp1i 0p1e1 breqtrrdi btwnnz simpl 0red nltled eldifsni necomd leneltd neg1z wne redivcld 1red recnd divnegd renegcld rpmulcl iccgelb lenegcon1d eqbrtrd cc 2rp ltnegcon1d divlt0gt0d neg1cn ax-1cn addcomi eqtr2i syl2anc pm2.61dan @@ -700787,7 +700787,7 @@ u C_ ( -u _pi [,] _pi ) /\ ( vol ` u ) <_ d ) -> A. k e. NN ( abs ` S. u wiso syldan ccncf fourierdlem90 fourierdlem89 fourierdlem91 fourierdlem92 cbvmptv fourierdlem11 simp3d lesub1d ltsub23d ltsub1dd subid1d negsubdi2d eqbrtrrid subcld syl5eqr iccssred feqresmpt fssresd ioossicc fourierdlem8 - fourierdlem15 sstrid resabs1d eqeltrd syl6eqr negsubd subsubd id syl6breq + fourierdlem15 sstrid resabs1d eqeltrd syl6eqr negsubd subsubd id breqtrdi fourierdlem69 adantl lesubd rpge0d subge02d iccss syl22anc iccmbl syl2anc cvol cdm iblss 3eqtrrd eqtr4d pncand ltlecasei ) ABDUCVFVGZEUCVFVGZVHVGZB VIZPVJZVKZBDEVHVGZUXJVKZWAJUCAJUCVLVMZVNZUXKBUXFDVHVGZUXJVKZBUXGDVHVGZUXJ @@ -702556,7 +702556,7 @@ its Fourier expansion has only sine terms (coefficients for cosine terms ctopn iooretop tgioo2 1cnd dvmptconst ssid ax-resscn fss dvresioo 3eqtr3i dmeqi dmmpti eqtr3i ssdmres mpbir elind dmres syl6eleqr ad2antrr ad2antlr adantlr lttri5d iooss2 2timesi negpicn addassi addcomli ltadd1dd readdcli - modcld negidi addid2i syl6breq addcomd ltaddneg jca modid2 eqtr3d lensymd + modcld negidi addid2i breqtrdi addcomd ltaddneg jca modid2 eqtr3d lensymd neqne negcld sylan eldifn condan velsn sylibr ssriv ccncf eqsstri ioosscn ssfi inss1 sstri dvf fresin ffdm simpli cuni cun sseldi elun1 nltled ccnp clp mnfltd lptioo2 incom df-ss fveq2i ltpnfd lptioo1 mnfle syl6ss resabs1 @@ -709853,7 +709853,7 @@ sequence of nondecreasing measurable sets (with bounded measure) then ( vk cfv nfcv vy cv ciun cli wcel wa c1 caddc wss nfv nfan nffv nfss nfim co wi wceq eleq1w anbi2d fveq2 fvoveq1 sseq12d imbi12d chvar cle wbr wral cr wrex breq2 ralbidv wb nfbr 2fveq3 breq1d cbvral a1i bitrd cbvrex sylib - cmpt cbvmpt eqtri meaiuninc cbviun fveq2i syl6breq ) ACRHRUBZESZUCZFSDHDU + cmpt cbvmpt eqtri meaiuninc cbviun fveq2i breqtrdi ) ACRHRUBZESZUCZFSDHDU BZESZUCZFSUDAUACREFGHKLMNAWKHUEZUFZWLWKUGUHUOESZUIZUPAWHHUEZUFZWIWHUGUHUO ZESZUIZUPDRWSXBDAWRDIWRDUJUKDWIXADWHEJDWHTULZDWTEJDWTTULUMUNWKWHUQZWOWSWQ XBXDWNWRADRHURUSXDWLWIWPXAWKWHEUTWKWHUGEUHVAVBVCOVDAWLFSZBUBZVEVFZDHVGZBV @@ -709941,7 +709941,7 @@ nondecreasing measurable sets (with bounded measure) then the measure of meaiuninc3 $p |- ( ph -> S ~~>* ( M ` U_ n e. Z ( E ` n ) ) ) $= ( vk cfv c1 nfcv nffv cv ciun clsxlim wcel wa caddc co wss nfan nfss nfim wi nfv wceq eleq1w anbi2d fveq2 fvoveq1 sseq12d imbi12d chvar cmpt 2fveq3 - cbvmpt eqtri meaiuninc3v cbviun fveq2i syl6breq ) ABPGPUAZDQZUBZEQCGCUAZD + cbvmpt eqtri meaiuninc3v cbviun fveq2i breqtrdi ) ABPGPUAZDQZUBZEQCGCUAZD QZUBZEQUCABPDEFGJKLMAVMGUDZUEZVNVMRUFUGDQZUHZULAVJGUDZUEZVKVJRUFUGZDQZUHZ ULCPWAWDCAVTCHVTCUMUICVKWCCVJDICVJSTZCWBDICWBSTUJUKVMVJUNZVQWAVSWDWFVPVTA CPGUOUPWFVNVKVRWCVMVJDUQVMVJRDUFURUSUTNVABCGVNEQZVBPGVKEQZVBOCPGWGWHPVNEP @@ -741991,7 +741991,7 @@ combinations of elements (vectors) of S". Whereas spans are defined according cgsu csca cpw wceq simp1 fveq2i eqtri oveq1i eleq2i biimpi 3ad2ant3 elpwg adantr a1i eqcomd sseq2d bitr2d biimpa 3ad2ant2 lincval syl3anc eqid ccmn c0g lmodcmn 3ad2ant1 simpl wi elmapi ffvelrn syl imp ssel adantl lmodvscl - wf ex fmpttd simp3r syl6breq scmfsupp syl211anc gsumcl eqeltrd ) EUANZFGN + wf ex fmpttd simp3r breqtrdi scmfsupp syl211anc gsumcl eqeltrd ) EUANZFGN ZFAUBZOZDCFPQZNZDHRUCZOZUDZDFEUESQZEMFMUFZDSZXCEUGSZQZUHZUIQZAXAWMDEUJSZT SZFPQZNZFETSZUKNZXBXHULWMWPWTUMZWTWMXLWPWRXLWSWRXLWQXKDCXJFPCBTSXJKBXITJU NUOUPUQURVAUSWPWMXNWTWNWOXNWNXNFXMUBWOFXMGUTWNXMAFWNAXMAXMULWNIVBVCVDVEVF @@ -743504,7 +743504,7 @@ there exists a regular element r of the ring (an element that is neither pweqi simpll simpr fvres eqcomd oveq1d eqtrd mpteq2dva oveq2d cplusg eqid syl13anc cgrp lmodfgrp 3ad2ant2 wf elmapi ffvelrn expcom 3ad2ant3 syl5com wi impcom grpinvcl 3ad2antr1 lincresunit1 3adantr3 ex imp eldifi lmodvscl - ssel2 c0g jca lincresunit2 syl6breq scmfsupp breqtrrdi gsumvsmul 3eqtr2rd + ssel2 c0g jca lincresunit2 breqtrdi scmfsupp breqtrrdi gsumvsmul 3eqtr2rd 3syl simp2 ) DBUGZUHZKUIUHZMDUHZUJZHGDUKULZUHZMHUMZFUHZHNUNUOZUJZUPZHDMVB ZUQZURZUUJKUSUMULZKAUUJAVCZUUKUMZUUMKUTUMZULZVAZVDULZKAUUJUUDLUMZUUMIUMZU UMUUOULZUUOULZVAZVDULUUSKAUUJUVAVAZVDULUUOULUUHYSUUKKVEUMZVFUMZUUJUKULUHZ @@ -743542,7 +743542,7 @@ there exists a regular element r of the ring (an element that is neither eqidd eqid lincdifsn eqeq1d fveq2 oveq12d cbvmptv oveq2d lincresunit3lem2 eqtr2d oveq1d cminusg cgrp lmodgrp elmapi ffvelrn syl2anr sselda lmodvscl lmodfgrp grpinvcl syl2an2r ccmn lmodcmn simpll2 lincresunit1 3adantr3 syl - id ffvelrnda c0g sylbid ssel2 fmpttd syl6sseq syl6breq scmfsupp breqtrrdi + id ffvelrnda c0g sylbid ssel2 fmpttd syl6sseq breqtrdi scmfsupp breqtrrdi syl2imc lincresunit2 gsumcl grpinvid2 lmodvsneg lincresunit3lem3 syl31anc simpr2 eqcom syl6bb biimpd sylbird 3impia eqtrd ) CAUGZUHZJUIUHZLCUHZUJZG FCUKULUHZLGUMZEUHZGMUNUOZUJZGCJUPUMZULZNUQZUJZHCLVAZURZUVKULZJOUVPOVBZHUM