From cdac5eea120be9d05b4609985a3f9f1f8d265f3e Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 5 Dec 2024 15:31:41 -0800 Subject: [PATCH] next 150 syl5bb to bitrid renames in set.mm --- set.mm | 300 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 150 insertions(+), 150 deletions(-) diff --git a/set.mm b/set.mm index 391a795995..5c2b62b1b6 100644 --- a/set.mm +++ b/set.mm @@ -108960,7 +108960,7 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). The cofinality cfslb $p |- ( ( Lim A /\ B C_ A /\ U. B = A ) -> ( cf ` A ) ~<_ B ) $= ( vx wlim wss cuni wceq cfv ccrd cdom wbr cvv wcel wex anbi12d sseq1d syl wa con0 w3a ccf cen fvex cv crab ciin wrex ssid ssex ad2antrr velpw sseq1 - cpw syl5bb unieq eqeq1d fveq2 spcegv mpcom df-rex rabid exbii bitri mpan2 + cpw bitrid unieq eqeq1d fveq2 spcegv mpcom df-rex rabid exbii bitri mpan2 anbi1i sylibr iinss cflim3 syl5ibr 3impib ssdomg mpsyl cdm limord ordsson word sstr2 mpan9 onssnum syl2an2 cardid2 3adant3 domentr syl2anc ) AEZBAF ZBGZAHZUAZAUBIZBJIZKLZWLBUCLZWKBKLWLMNWJWKWLFZWMBJUDWFWGWIWOWGWISZWOWFDDU @@ -109035,7 +109035,7 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). The cofinality syl smoiso2 syl2an biimpar simprd syl21anc smorndom syl3anc onsssuc mpbid wb adantrr ccom vex oiexg coexg sylancr fcod simpr ordsson ad2antrr simpl simprl ffvelrn wfn ffn jca smoel2 sylan wceq fveq2 eleq2d raleqbi1dv crab - wi eleq1d cbvralvw syl5bb cbvrabv eqtri elrab2 simprbi rspccv sylc ordtr1 + wi eleq1d cbvralvw bitrid cbvrabv eqtri elrab2 simprbi rspccv sylc ordtr1 weq ancomsd imp fvco3 syl2an2r 3eltr4d ralrimivva issmo2 syl13anc c0 cint sseq2d ex wn ffvelrnd mpd ralbidv wne rabn0 onint eqeltrid sylan2br elrab ssrab2 inteqi sylib adantl simpr2 eleq2i simp21 simp1l fssd simp22 simp1r @@ -109819,7 +109819,7 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). The cofinality cab imauni vex imaex dfiun2 eqtri weq rexrab eleq1 biimparc rexlimivw cdm ccnv cnvimass f1odm ad3antrrr sseqtrid cnvex elpw sylibr wfo f1ofo simprl sselda elpwid foimacnv syl2anc eqcomd simpr eqeq2d anbi12d rspcev impbid2 - eqeltrrd ex syl5bb abbi1dv unieqd eqtrid simplr ssrab2 a1i sylib exlimddv + eqeltrrd ex bitrid abbi1dv unieqd eqtrid simplr ssrab2 a1i sylib exlimddv simprrl n0 rabn0 wo elrab anbi12i simprrr adantr simprlr sorpssi wb f1of1 wf1 simprll f1imass orbi12d mpbid sylan2b ralrimivva sorpss fin2i cbvrabv syl22anc elrab2 simprbi syl expr sylan2 ralrimiva exlimiv sylbi cvv relen @@ -109996,7 +109996,7 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). The cofinality isfin3ds $p |- ( A e. V -> ( A e. F <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) ) $= ( cv csuc cfv wss com wral crn cint wcel cmap wceq wi cpw co suceq fveq2d - fveq2 sseq12d cbvralvw fveq1 ralbidv syl5bb inteqd eleq12d imbi12d oveq1d + fveq2 sseq12d cbvralvw fveq1 ralbidv bitrid inteqd eleq12d imbi12d oveq1d rneq pweq raleqdv elab2g ) HJZKZGJZLZUTVBLZMZHNOZVBPZQZVGRZUAZGDJZUBZNSUC ZOZAJZKZCJZLZVOVQLZMZANOZVQPZQZWBRZUAZCBUBZNSUCZOZDBEFVNWECVMOVKBTZWHVJWE GCVMVBVQTZVFWAVIWDVFVPVBLZVOVBLZMZANOWJWAVEWMHANUTVOTZVCWKVDWLWNVAVPVBUTV @@ -110645,7 +110645,7 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). The cofinality ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) } $= ( vf vy vb cfin3 cv cfv wss com wral crn cint wcel wi cpw cmap co weq cab csuc cwdom wbr isfin32i fveq1 sseq12d ralbidv rneq inteqd eleq12d imbi12d - wn cbvralvw pweq oveq1d raleqdv syl5bb cbvabv isf32lem12 abbii fin23lem41 + wn cbvralvw pweq oveq1d raleqdv bitrid cbvabv isf32lem12 abbii fin23lem41 mpd impbii eqriv ) DGAHZUBZCHZIZVFVHIZJZAKLZVHMZNZVMOZPZCBHZQZKRSZLZBUAZD HZGOZWBWAOZWCKWBUCUDUMWDWBUEAEWAWBGFVTVGFHZIZVFWEIZJZAKLZWEMZNZWJOZPZFEHZ QZKRSZLZBEVTWMFVSLZBETZWQVPWMCFVSCFTZVLWIVOWLWTVKWHAKWTVIWFVJWGVGVHWEUFVF @@ -111115,7 +111115,7 @@ version of the pigeonhole principle (for aleph-null pigeons and 2 holes) $( Lemma for ~ fin1a2 . (Contributed by Stefan O'Rear, 7-Nov-2014.) $) fin1a2lem5 $p |- ( A e. _om -> ( A e. ran E <-> -. suc A e. ran E ) ) $= - ( va com wcel c2o cv wceq wn wb ax-mp fvelrnb eqcom eqeq2d syl5bb rexbiia + ( va com wcel c2o cv wceq wn wb ax-mp fvelrnb eqcom eqeq2d bitrid rexbiia wrex bitri comu co csuc crn cfv wfn wf1 fin1a2lem4 f1fn fin1a2lem3 notbii nneob 3bitr4g ) BFGBHEIZUAUBZJZEFSZBUCZUOJZEFSZKBCUDZGZURVAGZKEBULVBUNCUE ZBJZEFSZUQCFUFZVBVFLFFCUGVGACDUHFFCUIMZEFBCNMVEUPEFVEBVDJUNFGZUPVDBOVIVDU @@ -112067,7 +112067,7 @@ that every (nonempty) pruned tree has a branch. This axiom is redundant syl wi wal eldifi elelpwi expcom 3syl expimpd exlimdv rneqi rnopab sseq1i alrimiv abss bitri sseqtrrd adantl cun cuni cxp fvrn0 elssuni ax-mp sseli anim2i ssopab2i df-xp 3sstr4i pwex difexi ssex unexg sylancl uniexd xpexg - frn p0ex sylancr ssexg eldm exbii bitr2i dmeq syl5bb rneq sseq12d anbi12d + frn p0ex sylancr ssexg eldm exbii bitr2i dmeq bitrid rneq sseq12d anbi12d breq ralbidv exbidv imbi12d ax-dc vtoclg mp2and simpr fveq2 suceq breq12d vex fveq2d rspccv fvex breldm syl6 ex eleq1 fveq1 imp adantll wb ad2antrr eleq2 mpbid fmptd impcom peano2 fvmptg eleq2d anbi2d brab simprbi syl6bir @@ -113312,7 +113312,7 @@ proved by Ernst Zermelo (the "Z" in ZFC) in 1904. (Contributed by Mario -> E. x e. A A. y e. A -. x R y ) $= ( vr vq vm vk vv vd vs vh vg vn cv wbr wral crab vu vt crn cvv crio crecs wn cmpt cima wceq weq breq1 notbid cbvralvw breq2 ralbidv cbvriotavw rneq - syl5bb raleqdv rabbidv riotaeqbidv eqtrid cbvmptv ax-mp cbvrabv zorn2lem7 + bitrid raleqdv rabbidv riotaeqbidv eqtrid cbvmptv ax-mp cbvrabv zorn2lem7 recseq eqid ) UAUBGHIJEHQZKQZFRZHLQZUCZSZKETZMQZGQZFRZMNUDOQZPQZVJRZUGZOV LHNQZUCZSZKETZSZPWGUEZUHZUFZUAQUISGETZFLMWKVSMWKUBQUISGETZDCABWJLUDJQZIQZ VJRZUGZJVPSZIVPUEZUHZUJWKWTUFUJNLUDWIWSNLUKZWIWQJWGSZIWGUEWSWHXBPIWGWHWNW @@ -113744,7 +113744,7 @@ proved by Ernst Zermelo (the "Z" in ZFC) in 1904. (Contributed by Mario fodomb $p |- ( ( A =/= (/) /\ E. f f : A -onto-> B ) <-> ( (/) ~< B /\ B ~<_ A ) ) $= ( c0 wne cv wfo wa csdm wbr cdom wceq eqeq1d wb cvv wcel mpcom 0sdomg syl - adantl wex cdm fof fdmd crn dm0rn0 forn syl5bb necon3bid biimpac vex dmex + adantl wex cdm fof fdmd crn dm0rn0 forn bitrid necon3bid biimpac vex dmex bitr3d eqeltrrdi fornex mpbird ex fodomg jca2 exlimdv sdomdomtr brrelex2i imp reldom mpbid fodomr jca impbii ) ADEZABCFZGZCUAZHDBIJZBAKJZHZVIVLVOVI VKVOCVIVKVMVNVIVKVMVIVKHVMBDEZVKVIVPVKADBDVKVJUBZDLZADLBDLZVKVQADVKABVJAB @@ -113831,7 +113831,7 @@ proved by Ernst Zermelo (the "Z" in ZFC) in 1904. (Contributed by Mario vg weq wb wne cin incom eqtri disjne mp3an1 vex opthpr syl equcom anbi12i c0 bitr2di df-br a1i anbi12d rexbidva rexbidv rexcom zfpair2 eqeq1 anbi1d 2rexbidv elab bitr4i adantr breq1 breq2 ceqsrex2v rmobidva ralbiia ancoms - bitrd eqcom ancom 3bitr4g bicomi syl5bb csn snex simpl ss2abi df-sn ssexi + bitrd eqcom ancom 3bitr4g bicomi bitrid csn snex simpl ss2abi df-sn ssexi sseqtrri ab2rexex2 eleq2 rmobidv ralbidv spcev exlimiv copab preq1 eleq1d syl2anbr preq2 eqid brab rmobii ralbii rexbii df-opab vuniex prid1 elunii cvv cuni mpan adantl prid2 eqeltrri abexex eqeltri breq impbii bitri ) CD @@ -113870,7 +113870,7 @@ proved by Ernst Zermelo (the "Z" in ZFC) in 1904. (Contributed by Mario vg brdom5 eqeq1 anbi1d df-br anbi2i bitr4di 2rexbidv wi weq wne wb cin c0 elab incom eqtri disjne mp3an1 vex opthpr syl breq12 biimprd impd adantrd syl6bi ex rexlimdvv syl5bi moimdv ralimia ancoms eqcom 3bitr4g bicomi a1i - ancom anbi12d rexbidva rexbidv syl5bb breq2 breq1 ceqsrex2v bitrd ralbiia + ancom anbi12d rexbidva rexbidv bitrid breq2 breq1 ceqsrex2v bitrd ralbiia adantr biimpri csn snex simpl ss2abi df-sn sseqtrri ssexi ab2rexex2 eleq2 mobidv ralbidv spcev syl2an exlimiv copab preq1 eleq1d preq2 mobii ralbii eqid brab rexbii cvv df-opab cuni vuniex prid1 elunii mpan prid2 eqeltrri @@ -113989,7 +113989,7 @@ proved by Ernst Zermelo (the "Z" in ZFC) in 1904. (Contributed by Mario eqeltrd fveq2d fveq1d ad2antrl xp2nd ffvelrnd opelxpd rexlimiva ex syl5bi fvex opth simpr eqeq2d djussxp eqsstri simprl sselid simpll csbeq1d nfel2 rspc sylc eqcomd eleqtrd rexlimi adantrr ralrimiv eleq12d rspccva adantrl - sylan eleqtrrd f1fveq syl12anc bitr3d pm5.32da simprr xpopth syl5bb dom2d + sylan eleqtrrd f1fveq syl12anc bitr3d pm5.32da simprr xpopth bitrid dom2d imp syl5com adantld exlimdv ) ACBCEDUCUDZUEZUAUFZUGZBJUFZDUHZEUVJUVHLZMZJ CNZOZUAUIZFCEUJZUKULZAUVGCUMPZUVKEKUFZMZKUVGVAZJCNZUVPHADEUVTMZKUVGVAZBCN ZUWCADEUKULZBCNZUWFIUWGUWEBCBUFZCPZUWGOZUVTUVGPZUWDOZKUIZUWEUWKUWDKUIZUWN @@ -114703,7 +114703,7 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this expcom con2d cun wo iscard3 elun df-or 3bitri syl56 wfn alephfnon fvelrnb mpbi syl6ib char cmpt eqid pwcfsdom fveq2 oveq12d breq12d mpbii rexlimivw syl6 imp ensdomtr enref mapen mapxpen mp3an sylancl xpdom2 biimpi infxpen - entri domentr csuc nsuceq0 dom0 nemtbir df-2o breq1i breq2 syl5bb biimpcd + entri domentr csuc nsuceq0 dom0 nemtbir df-2o breq1i breq2 bitrid biimpcd adantld mtoi mapdom2 expl com12 mt2d domtri biimpri nsyl2 cdm fndm eleq2i id ex eqtrdi fveq2d ndmfv sylnbir wne 1oex 0sdom mpbir oveq2 map0e cardnn 1n0 1onn df-1o fveq2i 0elon cfsuc eqtri mpbiri a1d pm2.61i ) ADEZUDBFGZAH @@ -115427,7 +115427,7 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this elgch $p |- ( A e. V -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) ) $= ( vy cgch wcel cfn cv csdm wbr cpw wa wn wal cab cun df-gch eleq2i elun - wo bitri wceq breq1 pweq breq2d anbi12d notbid albidv elabg orbi2d syl5bb + wo bitri wceq breq1 pweq breq2d anbi12d notbid albidv elabg orbi2d bitrid ) BEFZBGFZBDHZAHZIJZUOUNKZIJZLZMZANZDOZFZTZBCFZUMBUOIJZUOBKZIJZLZMZANZTUL BGVBPZFVDEVLBDAQRBGVBSUAVEVCVKUMVAVKDBCUNBUBZUTVJAVMUSVIVMUPVFURVHUNBUOIU CVMUQVGUOIUNBUDUEUFUGUHUIUJUK $. @@ -115516,7 +115516,7 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this ( v F ( s i^i ( v X. v ) ) ) = z ) ) } $= ( cv wss cxp wa wwe wceq wsbc weq cin co ccnv csn cima copab simpl sseq1d wral simpr sqxpeqd sseq12d anbi12d weeq2 weeq1 sylan9bb id ineq2d oveq12d - eqeq1d cbvsbcvw sneq imaeq2d eqeq2 sbceqbid syl5bb cbvralvw cnveqd ineq1d + eqeq1d cbvsbcvw sneq imaeq2d eqeq2 sbceqbid bitrid cbvralvw cnveqd ineq1d imaeq1d oveq2d raleqbidv cbvopabv eqtri ) HAMZFNZJMZVOVOOZNZPZVOVQQZEMZVQ WBWBOZUAZGUBZBMZRZEVQUCZWFUDZUEZSZBVOUIZPZPZAJUFKMZFNZIMZWOWOOZNZPZWOWQQZ DMZWQXBXBOZUAZGUBZCMZRZDWQUCZXFUDZUEZSZCWOUIZPZPZKIUFLWNXNAJKIAKTZJITZPZV @@ -116050,7 +116050,7 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this ( s We a /\ A. z e. a ( F ` ( `' s " { z } ) ) = z ) ) } $= ( cv wss wa wwe cima cfv wceq wral weq anbi12d cxp csn copab simpl sseq1d ccnv simpr sqxpeqd sseq12d weeq2 weeq1 sylan9bb imaeq2d fveq2d id eqeq12d - sneq cbvralvw cnveqd imaeq1d fveqeq2d raleqbidv syl5bb cbvopabv eqtri ) F + sneq cbvralvw cnveqd imaeq1d fveqeq2d raleqbidv bitrid cbvopabv eqtri ) F AKZDLZHKZVFVFUAZLZMZVFVHNZVHUFZBKZUBZOZEPZVNQZBVFRZMZMZAHUCIKZDLZGKZWBWBU AZLZMZWBWDNZWDUFZCKZUBZOZEPWJQZCWBRZMZMZIGUCJWAWPAHIGAISZHGSZMZVKWGVTWOWS VGWCVJWFWSVFWBDWQWRUDZUEWSVHWDVIWEWQWRUGZWSVFWBWTUHUITWSVLWHVSWNWQVLWBVHN @@ -116443,7 +116443,7 @@ set maps to an element of the set (so that it cannot be extended without wn vex ovmpt4g mp3an csdm wbr cdom wss cxp wwe w3a simprbi adantl domnsym syl isfinite iffalsed eqtrid cmap ciun wrex pwfseqlem1 eldif sylib simpld sylnibr eliun wf elmapi ad2antll wral ssiun2 ad2antrl simprd adantr elmap - ssneldd wfn wb ffnfv baib 3syl syl5bb mtbid con0 nnon ssrab2 omsson sstri + ssneldd wfn wb ffnfv baib 3syl bitrid mtbid con0 nnon ssrab2 omsson sstri ffn wne word ordom simprl ordelss sylancr rexnal sylibr ssrexv sylc rabn0 c0 onint sselid ontri1 syl2anc wi ssintrab syl2an imbi2d bitr4di pm5.74da con34b bi2.04 bitrdi elnn pm2.27 expcom a2d fveq2 eleq1d notbid rexlimddv @@ -116479,7 +116479,7 @@ set maps to an element of the set (so that it cannot be extended without simpr eqeltrd ex adantr syl5bir wn cdom cdm wb omelon onenon ax-mp simpr3 con0 wex 19.8ad ween sylibr domtri2 sylancr cdif nfv nfcv crab cif nfmpo2 cint cmpo nfcxfr nfov nfel1 nfim sseq1 weeq1 3anbi23d anbi1d anbi2d oveq2 - eleq1d imbi12d nfmpo1 xpeq12 anidms sseq2d weeq2 3anbi123d anbi12d syl5bb + eleq1d imbi12d nfmpo1 xpeq12 anidms sseq2d weeq2 3anbi123d anbi12d bitrid weq breq2 oveq1 difeq2 eleq12d pwfseqlem3 chvarfv eldifad sylbird pm2.61d expr ) APUDZFUEZNUDZYLYLUFZUEZYLYNUGZUHZUIZYLUJUKULZYLYNIUMZFUNZYTYLUOUNZ YSUUBYLUPAUUCUUBUQYRAUUCUUBAUUCUIZUUAYLURUSZKUSZFUUDUUCYNUTUNUUAUUFVAAUUC @@ -116519,7 +116519,7 @@ set maps to an element of the set (so that it cannot be extended without eleq1d imbi1d wn cdom cdm con0 omelon onenon ax-mp wex simpr3 19.8ad ween wb cdif nfv nfcv nfcxfr nfov nfel1 nfim chvarfv sylbird pwfseqlem2 finnum ficardom syl2anc domtri2 crab cint cif nfmpo2 anbi1d nfmpo1 xpeq12 anidms - sylancr breq2 anbi12d syl5bb difeq2 pwfseqlem3 eldifbd con4d vtocl vtoclg + sylancr breq2 anbi12d bitrid difeq2 pwfseqlem3 eldifbd con4d vtocl vtoclg cmpo expr mpcom mpd isfinite eqeltrrd cen fpwwe2lem3 cnvimass dmss dmxpss mpdan sstrdi sstrid ssfid inex1 eqtr3d wf1o f1of1 f1fveq syl12anc carden2 eqcomd wpss dfpss2 baib php3 sdomnen ex mt4d eleqtrrd eliniseg sylib weso @@ -119303,7 +119303,7 @@ construct and axiomatize real and complex numbers (e.g., ~ ax-resscn ). (New usage is discouraged.) $) ltpiord $p |- ( ( A e. N. /\ B e. N. ) -> ( A A e. B ) ) $= ( clti wbr cep cnpi cxp cin wcel wa df-lti breqi brinxp epelg adantl bitr3d - wb syl5bb ) ABCDABEFFGHZDZAFIZBFIZJZABIZABCSKLUCABEDZTUDABFFEMUBUEUDQUAABFN + wb bitrid ) ABCDABEFFGHZDZAFIZBFIZJZABIZABCSKLUCABEDZTUDABFFEMUBUEUDQUAABFN OPR $. $( Positive integer 'less than' is a strict ordering. (Contributed by NM, @@ -119486,7 +119486,7 @@ construct and axiomatize real and complex numbers (e.g., ~ ax-resscn ). (New usage is discouraged.) $) nlt1pi $p |- -. A ( x ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A ) ) $= ( vy vz vw wcel cv wa cnq co cltq wbr crq cfv cmq ltmnq ovex c1q cnp cplq - wb elprnq ltrnq mulcomnq caovord2 sylan9bbr syl5bb recidnq oveq1d mulidnq + wb elprnq ltrnq mulcomnq caovord2 sylan9bbr bitrid recidnq oveq1d mulidnq vex eqtrid sylan9eqr breq2d bitrd sylan wi prcdnq adantr sylbid ) BUAHCIZ BHJZAIZKHZJVEVCDIUBLZMNZVEVGOPZQLZVCQLZVCMNZVKBHZVDVCKHZVFVHVLUCBVCUDVNVF JZVHVKVEVEOPZQLZVCQLZMNZVLVHVIVPMNZVOVSVEVGUEVFVTVJVQMNVNVSVIVPVEREFGVJVQ @@ -121270,7 +121270,7 @@ divided by the argument (although we don't define full division since we 1idpr $p |- ( A e. P. -> ( A .P. 1P ) = A ) $= ( vx vf vg vw vu vv vy vz wcel c1p co cv cmq wrex cltq wbr wa cnq c1q cnp cmp wceq df-rex wb elprnq breq1 df-1p abeq2i ltmnq mulidnq breq2d bitr2id - wex bitrd sylan9bbr ex pm5.32rd exbidv 19.42v bitr3di syl5bb rexbidva 1pr + wex bitrd sylan9bbr ex pm5.32rd exbidv 19.42v bitr3di bitrid rexbidva 1pr sylan df-mp mulclnq genpelv mpan2 prnmax wi crq cfv ltrelnq brel vex fvex mulcomnq mulassnq caov12 oveq2d eqtrid sylan9eqr eqcomd ovex oveq2 eqeq2d recidnq spcev 3syl a1i ancld reximia syl prcdnq adantrd rexlimdva 3bitr4d @@ -121674,7 +121674,7 @@ B C_ ( A +P. C ) ) $= vf vg df-1p abeq2i wrex ltrnq mulcomnq recclnq mulidnq mp2b recidnq ax-mp wn 1nq 3eqtr3i breq1i prlem936 sylan2b prnmax ad2ant2r w3a elprnq 3adant3 bitri simp1r ltrelnq brel simpld syl simp3 simp2r fvex ltmnq vex caovord2 - wb syl5bb adantl biimpd eqtr3id oveqan12d mulassnq caov4 3eqtr3g recmulnq + wb bitrid adantl biimpd eqtr3id oveqan12d mulassnq caov4 3eqtr3g recmulnq mulclnq sylan mpbird eleq1d notbid biimprd anim12d wex ovex breq2 anbi12d fveq2 spcev breq1 anbi1d exbidv elab2 sylibr imp syl22anc simprd 3ad2ant3 syl6 eqtr3di oveq1d sylan9eqr syl2anc oveq2 rspceeqv 3expia reximdv df-mp @@ -122335,7 +122335,7 @@ B C_ ( A +P. C ) ) $= ( vf vg vh vx vy vw cltr cv cer wbr wceq wo wb cnp cpp co cltp wcel vex wa vz vv vu cnr cop cec wn df-nr breq1 eqeq1 breq2 orbi12d notbid bibi12d eqeq2 ltsrpr addclpr wor ltsopr sotric mpan syl2an an42s enreceq addcompr - breq12i bitri a1i bitr4d syl5bb 2ecoptocl wi anbi1d imbi12d imbi1d anbi2d + breq12i bitri a1i bitr4d bitrid 2ecoptocl wi anbi1d imbi12d imbi1d anbi2d anbi12d ovex ltapr caovord2 addasspr bitrdi bi2anan9r ltrelpr sotri dmplp 0npr ndmovordi caov12 3imtr4i syl6bi ad2ant2l 3adant2 3ecoptocl isso2i syl ) ABCUDGDHZEHZUEIUFZUAHZFHZUEIUFZGJZWSXBKZXBWSGJZLZUGZMAHZXBGJZXHXBKZ @@ -122604,7 +122604,7 @@ B C_ ( A +P. C ) ) $= E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A ) $= ( cm1r cplr co cltr wbr c1p cer wceq cnp wrex cnr wcel wb c0r cpp cltp vy vz cv cop cec ltrelsr brel simprd cmr ltasr ax-mp pn0sr addasssr addcomsr - oveq1i 3eqtr3i 0idsr eqtrid breq2d syl5bb m1r mulclsr mp2an addclsr df-nr + oveq1i 3eqtr3i 0idsr eqtrid breq2d bitrid m1r mulclsr mp2an addclsr df-nr mpan breq2 eqeq2 rexbidv imbi12d df-m1r breq1i addasspr breq2i ltsrpr 1pr wi ltapr 3bitr4i bitri ltexpri sylbi enreceq mpanl2 eqeq1i bitr4di ancoms wa addcompr rexbidva syl5ibr ecoptocl syl oveq2 sylan9eqr ex reximdv syld @@ -122636,7 +122636,7 @@ B C_ ( A +P. C ) ) $= ne0d ltasr ax-mp mpbi m1p1sr 3brtr3i breqtri ltrelsr sotri mpan map2psrpr ltsosr sylib breq2 ralbidv abeq2i ltpsrpr syl6ib ralrimiv syl6bir reximdv syl6 syl5bi com12 rexlimivw impcom supexpr syl2anc mappsrpr sylbir simprd - syld brel adantl wex sylanbr rexex wal df-ral 19.29 syl5bb bitr3id notbid + syld brel adantl wex sylanbr rexex wal df-ral 19.29 bitrid bitr3id notbid imbi12d biimpac exlimiv syl sylanb expcom 3syl impd impancom pm2.01d expr ex r19.29 biimprd vex bitrdi rspcev rexlimiva rexbidv syl5ib imim12d a1dd eleq1 sylan2b sotri2 mp3an3 syl5 expcomd ad2antrr pm2.61d adantlr anim12d @@ -123224,7 +123224,7 @@ of the other axioms (see ~ cnexALT ), but the proof requires the axiom of axrrecex $p |- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 ) $= ( vy vz cr wcel cc0 wne cv cmul co c1 wceq wrex c0r cop cnr bitri eqeq1d wa wi wex elreal df-rex neeq1 oveq1 rexbidv imbi12d df-0 eqeq2i necon3bii - vex eqresr cmr recexsr ex opelreal anbi1i mulresr df-1 ovex bitrdi syl5bb + vex eqresr cmr recexsr ex opelreal anbi1i mulresr df-1 ovex bitrdi bitrid c1r pm5.32da oveq2 rspcev syl6bir expd rexlimdv syld syl5bi gencl imp ) B EFZBGHZBAIZJKZLMZAENZCIZOPZGHZWBVQJKZLMZAENZUAVPVTUAWAQFZVOCWBBVOWBBMZCQN WGWHTCUBCBUCWHCQUDRWHWCVPWFVTWBBGUEWHWEVSAEWHWDVRLWBBVQJUFSUGUHWCWAOHZWGW @@ -124195,7 +124195,7 @@ this axiom (with the defined operation in place of ` x. ` ) follows as a reals. (Contributed by NM, 14-Oct-2005.) $) xrlenlt $p |- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) ) $= ( cxr wcel wa cle wbr cop clt ccnv wn df-br cxp wb opelxpi cdif df-le eldif - eleq2i bitri baib syl syl5bb opelcnvg bitr4id notbid bitr4d ) ACDBCDEZABFGZ + eleq2i bitri baib syl bitrid opelcnvg bitr4id notbid bitr4d ) ACDBCDEZABFGZ ABHZIJZDZKZBAIGZKUIUJFDZUHUMABFLUHUJCCMZDZUOUMNABCCOUOUQUMUOUJUPUKPZDUQUMEF URUJQSUJUPUKRTUAUBUCUHUNULUHUNBAHIDULBAILABCCIUDUEUFUG $. @@ -124572,7 +124572,7 @@ this axiom (with the defined operation in place of ` x. ` ) follows as a $( Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) $) eqlei2 $p |- ( B = A -> B <_ A ) $= - ( cr wcel wceq cle wbr wi eleq1a ax-mp wa eqcom letri3 mpan syl5bb syl6bi + ( cr wcel wceq cle wbr wi eleq1a ax-mp wa eqcom letri3 mpan bitrid syl6bi wb simpr mpcom ) BDEZBAFZBAGHZADEZUBUAICADBJKUAUBABGHZUCLZUCUBABFZUAUFBAM UDUAUGUFRCABNOPUEUCSQT $. @@ -125843,7 +125843,7 @@ it could represent the (meaningless) operation of 17-Jun-2010.) $) addsubeq4 $p |- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) = ( C + D ) <-> ( C - A ) = ( B - D ) ) ) $= - ( cc wcel wa cmin co wceq caddc eqcom subcl ancoms subadd 3expa an4s syl5bb + ( cc wcel wa cmin co wceq caddc eqcom subcl ancoms subadd 3expa an4s bitrid wb sylan addcom adantl oveq1d addsubass 3com12 eqtrd adantlr addcl 3bitr2rd eqeq1d 3expb sylan2 ) AEFZBEFZGZCEFZDEFZGZGZCAHIZBDHIZJZDUTKIZBJZCDKIZAHIZB JZABKIVEJZVBVAUTJZUSVDUTVALUMUPUNUQVIVDSZUMUPGUTEFZUNUQGZVJUPUMVKCAMNVLVKVJ @@ -126193,7 +126193,7 @@ it could represent the (meaningless) operation of 17-Jan-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) $) renegcli $p |- -u A e. RR $= ( vx cr wcel cv caddc co cc0 wceq wrex cneg ax-rnegex cc recn cmin df-neg - wb eqeq1i 0cn recni subadd mp3an12 syl5bb eleq1a sylbird rexlimiv mp2b + wb eqeq1i 0cn recni subadd mp3an12 bitrid eleq1a sylbird rexlimiv mp2b syl ) ADEACFZGHIJZCDKALZDEZBCAMUKUMCDUJDEZUKULUJJZUMUNUJNEZUOUKRUJOUOIAPH ZUJJZUPUKULUQUJAQSINEANEUPURUKRTABUAIAUJUBUCUDUIUJDULUEUFUGUH $. @@ -127730,7 +127730,7 @@ Ordering on reals (cont.) lesub0 $p |- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 ) ) $= ( cr wcel wa cc0 wceq cle wbr cmin co 0red letri3 sylan2 ancom simpr lesub2 - wb simpl syl3anc recnd subid1d breq1d bitrd ancoms anbi2d syl5bb bitr2d ) A + wb simpl syl3anc recnd subid1d breq1d bitrd ancoms anbi2d bitrid bitr2d ) A CDZBCDZEZAFGZAFHIZFAHIZEZUNBBAJKZHIZEZUJUIFCDZULUORUJLAFMNUOUNUMEUKURUMUNOU KUMUQUNUJUIUMUQRUJUIEZUMBFJKZUPHIZUQUTUIUSUJUMVBRUJUIPUTLUJUISZAFBQTUTVABUP HUTBUTBVCUAUBUCUDUEUFUGUH $. @@ -127893,7 +127893,7 @@ Ordering on reals (cont.) Mario Carneiro, 9-Mar-2015.) $) wloglei $p |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ch ) $= ( cv wcel wa cle vex weq cr wss adantr simprr sseldd simprl wi bi2anan9 - wbr eleq1w anbi2d wb breq12 ancoms anbi12d imbi12d ancom syl5bb syl2anb + wbr eleq1w anbi2d wb breq12 ancoms anbi12d imbi12d ancom bitrid syl2anb equcom bicomd w3a df-3an sylan2br anassrs vtocl2 lecasei ) AEOZIPZFOZIP ZQZQZCVJVHVMIUAVJAIUAUBVLLUCZAVIVKUDUEVMIUAVHVNAVIVKUFUEAGOZIPZHOZIPZQZ QZVQVORUIZQZBUGZVMVJVHRUIZQZCUGGHVHVJESFSGETZHFTZQZWBWEBCWHVTVMWAWDWHVS @@ -129423,7 +129423,7 @@ Ordering on reals (cont.) ( cc wcel cc0 wne wa cmul co cdiv caddc wceq cmin reccl adantr recid 3eqtrd c1 adantl ad2ant2r simpll simprl mul32d oveq1d mulid2 mulassd oveq2d mulid1 ad2antrl ad2antrr oveq12d mulcl adddid addcom 3eqtr4d mulid1d eqeq12d addcl - syl2an mulne0 ax-1cn mulcan mp3an2 syl12anc eqcom muleqadd syl5bb 3bitr3d + syl2an mulne0 ax-1cn mulcan mp3an2 syl12anc eqcom muleqadd bitrid 3bitr3d wb ) ACDZAEFZGZBCDZBEFZGZGZABHIZRAJIZRBJIZKIZHIZVQRHIZLZABKIZVQLZVTRLZARMIB RMIHIRLZVPWAWDWBVQVPVQVRHIZVQVSHIZKIBAKIZWAWDVPWHBWIAKVPWHAVRHIZBHIZRBHIZBV PABVRVJVKVOUAZVLVMVNUBZVLVRCDZVOANZOZUCVLWLWMLVOVLWKRBHAPUDOVMWMBLVLVNBUEUI @@ -129438,7 +129438,7 @@ Ordering on reals (cont.) by Mario Carneiro, 27-May-2016.) $) rereccl $p |- ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR ) $= ( vx cr wcel cc0 wne wa cv c1 cdiv co wceq wrex cmul ax-rrecex eqcom 1cnd - cc wb recnd simpll simplr divmul syl112anc syl5bb rexbidva mpbird risset + cc wb recnd simpll simplr divmul syl112anc bitrid rexbidva mpbird risset simpr sylibr ) ACDZAEFZGZBHZIAJKZLZBCMZUOCDUMUQAUNNKILZBCMBAOUMUPURBCUPUO UNLZUMUNCDZGZURUNUOPVAIRDUNRDARDULUSURSVAQVAUNUMUTUITVAAUKULUTUATUKULUTUB IUNAUCUDUEUFUGBUOCUHUJ $. @@ -131536,7 +131536,7 @@ of completeness axiom (it has a slightly weaker antecedent). infm3lem bitrdi n0 rabn0 3bitr4g imbi1d impexp albidv wceq imbi12d ralxfr breq2 rexbidv breq1 imbi2d negeq eleq1d elrab imbi1i bitri albii 3bitr4ri ralbidv wb leneg ancoms bitr3id rexbiia bitr4i anbi12d ssrab2 sup3 mp3an1 - ralbidva syl6bi notbid adantrd syl5bb ltneg rexrab anbi2d rexbidva adantl + ralbidva syl6bi notbid adantrd bitrid ltneg rexrab anbi2d rexbidva adantl sylibrd 3impib ) DIUAZDUBUDZAJZBJZKLZBDMZAINZXDXCOLZUCZBDMZXCXDOLZCJZXDOL ZCDNZPZBIMZQZAINZXAXBXGQZEJZFJZOLZUCZFGJZUEZDRZGIUFZMZYAXTOLZYAHJZOLZHYGN ZPZFIMZQZEINZXRXAXSYGUBUDZYAXTKLZFYGMZEINZQYPXAXBYQXGYTXAYADRZFUGZYFGINZX @@ -131657,7 +131657,7 @@ of completeness axiom (it has a slightly weaker antecedent). supaddc $p |- ( ph -> ( sup ( A , RR , < ) + B ) = sup ( C , RR , < ) ) $= ( vw va cr cle wbr wcel wrex clt csup caddc co wceq wn cv vex weq oveq1 - eqeq2d cbvrexvw eqeq1 rexbidv syl5bb elab2 wa sselda suprcld adantr wss + eqeq2d cbvrexvw eqeq1 rexbidv bitrid elab2 wa sselda suprcld adantr wss wral c0 wne w3a suprub sylan leadd1dd breq1 syl5ibrcom rexlimdva syl5bi 3jca ralrimiv wb readdcld eleq1a syl ssrdv wex ovex isseti rgenw r19.2z wi sylancl exbii n0 rexcom4 3bitr4i sylibr brralrspcev syl2anc suprleub @@ -131691,7 +131691,7 @@ of completeness axiom (it has a slightly weaker antecedent). ( va vw cr cle clt csup caddc wceq wbr wrex cab suprcld eqid supaddc wcel co cv wa sselda recnd adantr addcomd eqeq2d rexbidva abbidv supeq1d eqtrd wral vex weq eqeq1 rexbidv elab wss c0 wne adantlr rspe cbvrexvw 2rexbidv - oveq1 syl5bb elab2 sylibr ex anim12d readdcl syl6 eleq1a rexlimdvv syl5bi + oveq1 bitrid elab2 sylibr ex anim12d readdcl syl6 eleq1a rexlimdvv syl5bi wi sseld ssrdv wex ovex isseti rgenw r19.2z sylancl rexcom4 sylib syl2anc ralrimivw n0 exbii bitri readdcld adantrr adantrl w3a 3jca suprub le2addd sylan breq1 biimprcd ralrimiv brralrspcev syl3anc wb syl rexlimdva abssdv @@ -131744,7 +131744,7 @@ of completeness axiom (it has a slightly weaker antecedent). supmul1 $p |- ( ph -> ( A x. sup ( B , RR , < ) ) = sup ( C , RR , < ) ) $= ( vw vb cr clt cle wbr wa wcel cc0 adantr csup cmul co wceq wral wrex vex - wn cv oveq2 eqeq2d cbvrexvw eqeq1 rexbidv syl5bb elab2 wss c0 simpr sylbi + wn cv oveq2 eqeq2d cbvrexvw eqeq1 rexbidv bitrid elab2 wss c0 simpr sylbi wne w3a simp1d sselda suprcl syl simpl1 simpl2 jca sylan lemul2a syl31anc suprub breq1 rexlimdva syl5bi ralrimiv wb wi remulcld eleq1a ssrdv simpr2 syl5ibrcom wex ovex isseti rgenw r19.2z sylancl n0 rexcom4 3bitr4i sylibr @@ -131792,7 +131792,7 @@ of completeness axiom (it has a slightly weaker antecedent). supmullem1 $p |- ( ph -> A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) $= ( va cv cr cle wbr wcel wrex cc0 clt csup cmul wceq vex weq oveq1 rexbidv - co eqeq2d cbvrexvw eqeq1 2rexbidv syl5bb elab2 wa wi wss wne wral simp2bi + co eqeq2d cbvrexvw eqeq1 2rexbidv bitrid elab2 wa wi wss wne wral simp2bi c0 w3a simp1d sselda adantrr suprcl syl adantr simp3bi simp1l sylbi breq2 adantrl rspccv imp simp1r suprub sylan lemul12ad breq1 biimprcd rexlimdvv ex syl6 syl5bi ralrimiv ) AENZGOUAUBZHOUAUBZUCUIZPQZEIWHIRWHMNZJNZUCUIZUD @@ -131810,7 +131810,7 @@ of completeness axiom (it has a slightly weaker antecedent). supmullem2 $p |- ( ph -> ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) ) $= ( va cr cv cle wral wrex wcel cmul wss c0 wne wbr wceq vex eqeq2d rexbidv - co oveq1 cbvrexvw eqeq1 2rexbidv syl5bb elab2 wa wi cc0 w3a simp2bi sseld + co oveq1 cbvrexvw eqeq1 2rexbidv bitrid elab2 wa wi cc0 w3a simp2bi sseld simp1d simp3bi anim12d syl6 eleq1a rexlimdvv syl5bi ssrdv wex simp2d ovex remulcl isseti rgenw r19.2z sylancl rexcom4 sylib ralrimivw syl2anc exbii n0 bitri sylibr clt csup suprcl syl remulcld supmullem1 brralrspcev 3jca @@ -131838,7 +131838,7 @@ Dedekind cut construction of the reals (see ~ df-mp ). (Contributed by w3a cc0 wa simp2bi suprcl syl simp3bi cc mulcom syl2an syl2anc wex simp2d recn n0 sylib 0red simp1d sselda adantr wi simp1r sylbi rspccv imp suprub breq2 sylan letrd exlimddv simp1l eqid supmul1 syl31anc eqtrd vex rexbidv - biid eqeq1 elab rspe oveq1 eqeq2d cbvrexvw syl5bb elab2 sylibr supmullem2 + biid eqeq1 elab rspe oveq1 eqeq2d cbvrexvw bitrid elab2 sylibr supmullem2 2rexbidv sylan9r syl5bi ralrimiv adantlr remulcld eleq1a rexlimdva abssdv ex wb ovex isseti rgenw sylancl rexcom4 cbvexvw abn0 brralrspcev suprleub r19.2z mpbird eqbrtrd breq1 syl5ibrcom supmullem1 letri3d mpbir2and ) AFN @@ -132125,7 +132125,7 @@ Dedekind cut construction of the reals (see ~ df-mp ). (Contributed by Mario Carneiro, 27-May-2016.) $) creui $p |- ( A e. CC -> E! y e. RR E. x e. RR A = ( x + ( _i x. y ) ) ) $= ( vz vw cc wcel cv ci cmul co caddc wceq cr wrex wreu cnre wa wb wral cru - simpr eqcom ancoms syl5bb anass1rs rexbidva biidd ceqsrexv ad2antrr bitrd + simpr eqcom ancoms bitrid anass1rs rexbidva biidd ceqsrexv ad2antrr bitrd ralrimiva reu6i syl2anc eqeq1 rexbidv reubidv syl5ibrcom rexlimivv syl ) CFGCDHZIEHZJKLKZMZENODNOCAHZIBHZJKLKZMZANOZBNPZDECQVDVJDENNVANGZVBNGZRZVJ VDVCVGMZANOZBNPZVMVLVOVFVBMZSZBNTVPVKVLUBVMVRBNVMVFNGZRZVOVEVAMZVQRZANOZV @@ -132728,7 +132728,7 @@ subset of complex numbers ( ~ nnsscn ), in contrast to the more elementary nndiv $p |- ( ( A e. NN /\ B e. NN ) -> ( E. x e. NN ( A x. x ) = B <-> ( B / A ) e. NN ) ) $= ( cdiv co cn wcel cv wceq wrex cmul risset eqcom ad2antlr ad2antrr adantl - wa cc nncn cc0 wne nnne0 divmuld syl5bb rexbidva bitr2id ) CBDEZFGAHZUGIZ + wa cc nncn cc0 wne nnne0 divmuld bitrid rexbidva bitr2id ) CBDEZFGAHZUGIZ AFJBFGZCFGZQZBUHKECIZAFJAUGFLULUIUMAFUIUGUHIULUHFGZQZUMUHUGMUOCBUHUKCRGUJ UNCSNUJBRGUKUNBSOUNUHRGULUHSPUJBTUAUKUNBUBOUCUDUEUF $. $} @@ -134704,7 +134704,7 @@ distinguish between finite and infinite sets (and therefore if the set size by NM, 9-May-2004.) $) elznn0 $p |- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) ) $= ( cz wcel cr cc0 wceq cn cneg w3o wa cn0 wo elz wb elnn0 a1i recn 0cn bitri - cc negcon1 sylancl eqeq1i eqcom bitrdi orbi2d syl5bb orbi12d 3orass orordir + cc negcon1 sylancl eqeq1i eqcom bitrdi orbi2d bitrid orbi12d 3orass orordir neg0 orcom 3bitrri bitr2di pm5.32i ) ABCADCZAEFZAGCZAHZGCZIZJUPAKCZUSKCZLZJ AMUPVAVDUPVDURUQLZUTUQLZLZVAUPVBVEVCVFVBVENUPAOPVCUTUSEFZLUPVFUSOUPVHUQUTUP VHEHZAFZUQUPATCETCVHVJNAQRAEUAUBVJEAFUQVIEAUKUCEAUDSUEUFUGUHVAUQURUTLZLVKUQ @@ -135245,7 +135245,7 @@ nonnegative integers (cont.)". $) ( cn wcel cv cdiv co c1 wceq wo wi clt wbr cle w3a wa wb wn cr nnre sylan wne bi2.04 impexp imbi2i 3bitr4ri nngt1ne1 adantl anbi1d cz gtndiv 3expia neor nnz con2d lenlt syl2an sylibrd ancoms pm4.71rd anbi2d 3anass bitr4di - syl5 bitr3d imbi1d syl5bb ralbidva ) BCDZBAEZFGZCDZVJHIVJBIZJZKZHVJLMZVJB + syl5 bitr3d imbi1d bitrid ralbidva ) BCDZBAEZFGZCDZVJHIVJBIZJZKZHVJLMZVJB NMZVLOZVMKZACVOVJHUBZVLPZVMKZVIVJCDZPZVSVTVLVMKKVLVTVMKZKWBVOVTVLVMUCVTVL VMUDVNWEVLVMVJHUMUEUFWDWAVRVMWDVPVLPZWAVRWDVPVTVLWCVPVTQVIVJUGUHUIWDWFVPV QVLPZPVRWDVLWGVPWDVLVQVLVKUJDZWDVQVKUNWCVIWHVQKWCVIPZWHBVJLMZRZVQWIWJWHWC @@ -137808,7 +137808,7 @@ least element (schema form). (Contributed by NM, 17-Aug-2001.) $) eqreznegel $p |- ( A C_ ZZ -> { z e. RR | -u z e. A } = { z e. ZZ | -u z e. A } ) $= ( vw cz wss cv cneg wcel cr crab wa wi ssel cc recn caddc cc0 negid elrab - co eqeltrdi pm4.71i zrevaddcl syl5bb syl5ib syl6 impcomd simpr zre anim1i + co eqeltrdi pm4.71i zrevaddcl bitrid syl5ib syl6 impcomd simpr zre anim1i 0z jca2 impbid1 weq negeq eleq1d 3bitr4g eqrdv ) BDEZCAFZGZBHZAIJZVBADJZU SCFZIHZVEGZBHZKZVEDHZVHKZVEVCHVEVDHUSVIVKUSVIVJVHUSVHVFVJUSVHVGDHZVFVJLBD VGMVFVENHZVLVJVEOVMVMVEVGPTZDHZKVLVJVMVOVMVNQDVERUKUAUBVEVGUCUDUEUFUGVFVH @@ -137860,7 +137860,7 @@ least element (schema form). (Contributed by NM, 17-Aug-2001.) $) E. x e. A ( A. y e. A -. x < y /\ A. y e. B ( y < x -> E. z e. A y < z ) ) ) $= ( vm vn vw cz cv cle wbr wral wrex clt wa wceq wcel cneg zred c0 wn breq1 - wss wne wi cbvralvw breq2 ralbidv syl5bb cbvrexvw crab cr cuz cfv simp1rl + wss wne wi cbvralvw breq2 ralbidv bitrid cbvrexvw crab cr cuz cfv simp1rl cinf w3a znegcld simp2 simp1rr simp3 rspcdva lenegcon1d syl3anbrc rabssdv eluz2 wex n0 ssel2 zcnd negnegd simpr eqeltrd negeq eleq1d rspcev syl2anc ex exlimdv imp sylan2b adantr sylibr infssuzcl cbvrabv elrab2 simprbi syl @@ -138057,7 +138057,7 @@ least element (schema form). (Contributed by NM, 17-Aug-2001.) $) ( vy cr wcel cneg cv cle wbr c1 caddc co clt wa cz wreu znegcl cc wceq wb renegcl zbtwnre syl zcn negcon2 syl2an reuhyp breq2 breq1 anbi12d reuxfr1 zre leneg ancoms cmin peano2rem ltneg sylan ltsubadd mp3an2 recn negsubdi - ax-1cn sylancl adantr breq2d 3bitr3d sylan2 bicomd reubidva syl5bb mpbid + ax-1cn sylancl adantr breq2d 3bitr3d sylan2 bicomd reubidva bitrid mpbid 1re ) BDEZBFZCGZHIZVPVOJKLZMIZNZCOPZAGZBHIZBWBJKLMIZNZAOPZVNVODEWABUACVOU BUCWAVOWBFZHIZWGVRMIZNZAOPVNWFVTWJCAWGOOWBQCAWGVPFZOVPQVPOEVPREWBREVPWGSZ WBWKSTWBOEZVPUDWBUDVPWBUEUFUGWLVQWHVSWIVPWGVOHUHVPWGVRMUIUJUKVNWJWEAOVNWM @@ -138782,7 +138782,7 @@ Positive reals (as a subset of complex numbers) $( Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018.) $) negelrp $p |- ( A e. RR -> ( -u A e. RR+ <-> A < 0 ) ) $= - ( cneg crp wcel cr cc0 clt wbr elrp lt0neg1 renegcl biantrurd bitr2d syl5bb + ( cneg crp wcel cr cc0 clt wbr elrp lt0neg1 renegcl biantrurd bitr2d bitrid wa ) ABZCDPEDZFPGHZOZAEDZAFGHZPITUARSAJTQRAKLMN $. ${ @@ -139452,7 +139452,7 @@ Infinity and the extended real number system (cont.) ( ( ( ( A e. RR /\ B e. RR ) /\ A ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A R C /\ C S B ) ) ) $= ( cxr wcel wa wbr w3a co anass df-3an bitrd c0 anbi1i wb elixx1 3anass wn - ibar syl5bb cxp cpw ixxf fdmi ndmov eleq2d pm2.21i simpl pm5.21ni pm2.61i + ibar bitrid cxp cpw ixxf fdmi ndmov eleq2d pm2.21i simpl pm5.21ni pm2.61i noel 3bitr4ri ) DKLZEKLZMZFKLZMZDFGNZFEHNZMZMVBVCVGMZMZUTVAVCOZVGMFDEIPZL ZVBVCVGQVJVDVGUTVAVCRUAVBVLVIUBVBVLVCVEVFOZVIABCDEFGHIJUCVMVHVBVIVCVEVFUD VBVHUFUGSVBUEZVLFTLZVIVNVKTFDEKIKKUHKUIIABCGHIJUJUKULUMVOVBVIVOVBFURUNVBV @@ -142202,7 +142202,7 @@ the expression make the whole thing evaluate to zero (on both sides), ( cxr wcel w3a wbr wa co cun cv wo elun wb simpl1 simpl2 elixx1 syl2anc biimpa simp1d simp2d simp3d simplrr adantr simpl3 syl3anc mp2and jaodan wi 3jca simplrl biimpar syldan exmid jca df-3an bitrdi mpbirand 3anan12 - wn biantrud 3bitr2d orbi12d mpbiri impbida syl5bb eqrdv ) EUCUDZFUCUDZG + wn biantrud 3bitr2d orbi12d mpbiri impbida bitrid eqrdv ) EUCUDZFUCUDZG UCUDZUEZEFOUFZFGPUFZUGZUGZDEFNUHZFGHUHZUIZEGIUHZDUJZWQUDWSWOUDZWSWPUDZU KZWNWSWRUDZWSWOWPULWNXBXCWNXBWSUCUDZEWSJUFZWSGMUFZUEZXCWNWTXGXAWNWTUGZX DXEXFXHXDXEWSFKUFZWNWTXDXEXIUEZWNWGWHWTXJUMWGWHWIWMUNZWGWHWIWMUOZABCEFW @@ -142365,7 +142365,7 @@ the expression make the whole thing evaluate to zero (on both sides), B <_ A ) ) $= ( vx cxr wcel wa cioo co c0 wceq cv clt wbr crab cle iooval wn wrex bitrd cq eqeq1d wne df-ne rabn0 bitr3i wi xrlttr 3com23 3expa rexlimdva qbtwnxr - w3a qre rexrd anim1i reximi2 syl 3expia impbid syl5bb xrltnle con4bid ) A + w3a qre rexrd anim1i reximi2 syl 3expia impbid bitrid xrltnle con4bid ) A DEZBDEZFZABGHZIJACKZLMVGBLMFZCDNZIJZBAOMZVEVFVIICABPUAVEVJVKVEVJQZABLMZVK QVLVHCDRZVEVMVLVIIUBVNVIIUCVHCDUDUEVEVNVMVEVHVMCDVCVDVGDEZVHVMUFZVCVOVDVP AVGBUGUHUIUJVCVDVMVNVCVDVMULVHCTRVNCABUKVHVHCTDVGTEZVOVHVQVGVGUMUNUOUPUQU @@ -142523,7 +142523,7 @@ the expression make the whole thing evaluate to zero (on both sides), ( vx cxr wcel wa cico co c0 wceq cv cle wbr clt crab wn wrex wi cq bitrd icoval eqeq1d wne df-ne rabn0 bitr3i xrlelttr 3expa rexlimdva w3a qbtwnxr 3com23 qre rexrd a1i simpr1 simpl xrltle syl2anc anim1d anim12d ex adantr - syl pm2.43b reximdv2 mpd 3expia impbid syl5bb xrltnle con4bid ) ADEZBDEZF + syl pm2.43b reximdv2 mpd 3expia impbid bitrid xrltnle con4bid ) ADEZBDEZF ZABGHZIJACKZLMZVQBNMZFZCDOZIJZBALMZVOVPWAICABUAUBVOWBWCVOWBPZABNMZWCPWDVT CDQZVOWEWDWAIUCWFWAIUDVTCDUEUFVOWFWEVOVTWECDVMVNVQDEZVTWERZVMWGVNWHAVQBUG ULUHUIVMVNWEWFVMVNWEUJZAVQNMZVSFZCSQWFCABUKWIWKVTCSDWIVQSEZWKFZWGVTFZWLWI @@ -142537,7 +142537,7 @@ the expression make the whole thing evaluate to zero (on both sides), ( vx cxr wcel wa cioc co c0 wceq cv clt wbr cle crab wn wrex wi cq bitrd iocval eqeq1d wne df-ne rabn0 bitr3i xrltletr 3expa rexlimdva w3a qbtwnxr 3com23 qre rexrd a1i xrltle 3ad2antr2 anim2d anim12d syl pm2.43b reximdv2 - ex adantr mpd 3expia impbid syl5bb xrltnle con4bid ) ADEZBDEZFZABGHZIJACK + ex adantr mpd 3expia impbid bitrid xrltnle con4bid ) ADEZBDEZFZABGHZIJACK ZLMZVOBNMZFZCDOZIJZBANMZVMVNVSICABUAUBVMVTWAVMVTPZABLMZWAPWBVRCDQZVMWCWBV SIUCWDVSIUDVRCDUEUFVMWDWCVMVRWCCDVKVLVODEZVRWCRZVKWEVLWFAVOBUGULUHUIVKVLW CWDVKVLWCUJZVPVOBLMZFZCSQWDCABUKWGWIVRCSDWGVOSEZWIFZWEVRFZWJWGWKWLRZRZWIW @@ -142550,7 +142550,7 @@ the expression make the whole thing evaluate to zero (on both sides), B < A ) ) $= ( vx cxr wcel wa cicc co c0 wceq cv cle wbr crab iccval eqeq1d wrex bitrd clt wn wne df-ne rabn0 bitr3i wi xrletr 3com23 3expa rexlimdva w3a xrleid - simp2 simp3 3ad2ant2 anbi12d rspcev syl12anc 3expia impbid syl5bb xrlenlt + simp2 simp3 3ad2ant2 anbi12d rspcev syl12anc 3expia impbid bitrid xrlenlt breq2 breq1 con4bid ) ADEZBDEZFZABGHZIJACKZLMZVIBLMZFZCDNZIJZBASMZVGVHVMI CABOPVGVNVOVGVNTZABLMZVOTVPVLCDQZVGVQVPVMIUAVRVMIUBVLCDUCUDVGVRVQVGVLVQCD VEVFVIDEZVLVQUEZVEVSVFVTAVIBUFUGUHUIVEVFVQVRVEVFVQUJVFVQBBLMZVRVEVFVQULVE @@ -143325,7 +143325,7 @@ the existence of its supremum (see ~ suprcl ). (Contributed by Paul biimpa ad3antrrr sylancr mpbir3and adantll ltpnf ad3antlr sylancl sylbird elioo1 pnfxr orim12d jaod sylbid expimpd elun syl6ibr ioossre unssi sseli elioo2 biimpd a1i com13 3impd xrltnle a1ddd syl imp sylibr intnand mpbird - sylnibr anim12i jca impbid syl5bb eqrdv ) ACDZBCDZEZUACABUBFZUCZGAUDFZBHU + sylnibr anim12i jca impbid bitrid eqrdv ) ACDZBCDZEZUACABUBFZUCZGAUDFZBHU DFZUEZUAUFZXGDXKCDZXKXFDZIZEZXEXKXJDZXKCXFUGXEXOXPXEXOXKXHDZXKXIDZUHZXPXE XLXNXSXEXLEZXNXKJDZAXKUIKZXKBUIKZLZIZXSXTXMYDXEXMYDMZXLXCAJDZBJDZYFXDAUJZ BUJZABXKUKZULNUMYEYAYBYCEZEZIZXTXSYDYMYAYBYCUNZUOYNYAIZYLIZUHXTXSYAYLUPXT @@ -143499,7 +143499,7 @@ the existence of its supremum (see ~ suprcl ). (Contributed by Paul ( ( A / B ) e. ( 0 [,] 1 ) <-> A <_ B ) ) $= ( cdiv co cc0 c1 cicc wcel cr cle wbr clt w3a elicc01 df-3an bitri cmul 1re wa wb ledivmul mp3an2 simpll simprl gt0ne0 adantl redivcld divge0 biantrurd - adantlr wne jca cc recn ad2antrl mulid1d breq2d 3bitr3d syl5bb ) ABCDZEFGDH + adantlr wne jca cc recn ad2antrl mulid1d breq2d 3bitr3d bitrid ) ABCDZEFGDH ZUTIHZEUTJKZSZUTFJKZSZAIHZEAJKZSZBIHZEBLKZSZSZABJKZVAVBVCVEMVFUTNVBVCVEOPVM VEABFQDZJKZVFVNVGVLVEVPTZVHVGFIHVLVQRAFBUAUBUJVMVDVEVMVBVCVMABVGVHVLUCVIVJV KUDVLBEUKVIBUEUFUGABUHULUIVMVOBAJVMBVJBUMHVIVKBUNUOUPUQURUS $. @@ -143538,7 +143538,7 @@ the existence of its supremum (see ~ suprcl ). (Contributed by Paul simpl1 addcomd lincmb01cmp eqeltrd simpr wb elicc2 biimpa simp1d iccshftl 3adant3 eqid syl22anc mpbid resubcld difrp biimp3a adantr rpne0d divcan1d rpcnd mul02d subidd eqtr4d mulid2d oveq12d 3eltr4d 0red rerpdivcld iccdil - crp 1red mpbird eqcom adantrr divmul3d syl5bb remulcld subadd2d subadd23d + crp 1red mpbird eqcom adantrr divmul3d bitrid remulcld subadd2d subadd23d wne bitrdi subdid oveq1d 1cnd subdird eqtrd oveq2d eqeq2d 3bitrd f1ocnv2d 3eqtr4d ) CGHZDGHZCDUAIZUCZABJKLMZCDLMZAUBZDNMZKXMOMZCNMZPMZBUBZCOMZDCOMZ UDMZEFXJXMXKHZUEZXQXPXNPMXLYCXNXPYCXMDYCXMYBXMGHZXJYBYDJXMUFIXMKUFIXMUGUH @@ -143774,7 +143774,7 @@ the existence of its supremum (see ~ suprcl ). (Contributed by Paul elfz2 $p |- ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) ) $= ( cz wcel wa cle wbr w3a cfz co anass df-3an anbi1i elfz1 3anass ibar bitrd - wb c0 syl5bb wn cxp cpw fzf fdmi ndmov eleq2d noel pm2.21i pm5.21ni pm2.61i + wb c0 bitrid wn cxp cpw fzf fdmi ndmov eleq2d noel pm2.21i pm5.21ni pm2.61i simpl 3bitr4ri ) BDEZCDEZFZADEZFZBAGHZACGHZFZFUQURVBFZFZUOUPURIZVBFABCJKZEZ UQURVBLVEUSVBUOUPURMNUQVGVDSUQVGURUTVAIZVDABCOVHVCUQVDURUTVAPUQVCQUARUQUBZV GATEZVDVIVFTABCDJDDUCDUDJUEUFUGUHVJUQVDVJUQAUIUJUQVCUMUKRULUN $. @@ -143965,7 +143965,7 @@ the existence of its supremum (see ~ suprcl ). (Contributed by Paul $( A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.) $) fzn $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( N < M <-> ( M ... N ) = (/) ) ) $= - ( cz wcel wa clt wbr cfz co c0 wne cle wn cuz cfv fzn0 eluz syl5bb cr zre + ( cz wcel wa clt wbr cfz co c0 wne cle wn cuz cfv fzn0 eluz bitrid cr zre wb lenlt syl2an bitr2d necon4bbid ) ACDZBCDZEZBAFGZABHIZJUHUJJKZABLGZUIMZ UKBANODUHULABPABQRUFASDBSDULUMUAUGATBTABUBUCUDUE $. @@ -144521,7 +144521,7 @@ subset of a (possibly extended) finite sequence of integers. (Contributed fznn $p |- ( N e. ZZ -> ( K e. ( 1 ... N ) <-> ( K e. NN /\ K <_ N ) ) ) $= ( c1 cfz co wcel cn cuz cfv wa cz cle wbr elfzuzb elnnuz anbi1i bitr4i eluz - wb nnz sylan ancoms pm5.32da syl5bb ) ACBDEFZAGFZBAHIFZJZBKFZUFABLMZJUEACHI + wb nnz sylan ancoms pm5.32da bitrid ) ACBDEFZAGFZBAHIFZJZBKFZUFABLMZJUEACHI FZUGJUHACBNUFUKUGAOPQUIUFUGUJUFUIUGUJSZUFAKFUIULATABRUAUBUCUD $. $( Membership in a 1-based finite set of sequential integers. (Contributed @@ -144778,7 +144778,7 @@ subset of a (possibly extended) finite sequence of integers. (Contributed w3a mp3an3 3adant3 zsubcl mpan id syl3an 3com12 ovex oveq2 sbcco3gw ax-mp cvv ralbii cneg df-neg oveq2i subneg addcom eqtrd eqtr3id 3adant2 oveq12d zcn 3coml raleqdv elfzelz zcnd negsubdi2 syl2an sbceq1d ralbidva 3ad2ant3 - bitrd syl5bb 3bitrd ) EHIZFHIZDHIZUDZABEFJKLZABMGUAZNKZOZGMFNKZMENKZJKLZW + bitrd bitrid 3bitrd ) EHIZFHIZDHIZUDZABEFJKLZABMGUAZNKZOZGMFNKZMENKZJKLZW GGDCUAZNKZOZCDWINKZDWHNKZJKZLZABWKDNKZOZCEDPKZFDPKZJKZLZVTWAWDWJQZWBVTWAM HIZXDUBABGMEFUCUEUFWAVTWBWJWQQZWAWHHIZVTWIHIZWBWBXFXEWAXGUBMFUGUHXEVTXHUB MEUGUHWBUIWGGCDWHWIUCUJUKWQABMWLNKZOZCWPLZWCXCWMXJCWPWLUPIWMXJQDWKNULAGBW @@ -145309,7 +145309,7 @@ Finite intervals of nonnegative integers (or "finite sets of sequential nelfzo $p |- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e/ ( M ..^ N ) <-> ( K < M \/ N <_ K ) ) ) $= ( cfzo co wnel wcel wn cz w3a clt wbr cle wo df-nel wa wb cr zre syl notbid - ianor a1i elfzo anim12i 3adant3 ltnle anim12ci 3adant2 lenlt orbi12d syl5bb + ianor a1i elfzo anim12i 3adant3 ltnle anim12ci 3adant2 lenlt orbi12d bitrid 3bitr4d ) ABCDEZFAUNGZHZAIGZBIGZCIGZJZABKLZCAMLZNZAUNOUTBAMLZACKLZPZHZVDHZV EHZNZUPVCVGVJQUTVDVEUBUCUTUOVFABCUDUAUTVAVHVBVIUTARGZBRGZPZVAVHQUQURVMUSUQV KURVLASZBSUEUFABUGTUTCRGZVKPZVBVIQUQUSVPURUQVKUSVOVNCSUHUICAUJTUKUMUL $. @@ -146326,7 +146326,7 @@ Finite intervals of nonnegative integers (or "finite sets of sequential fzosplitsni $p |- ( B e. ( ZZ>= ` A ) -> ( C e. ( A ..^ ( B + 1 ) ) <-> ( C e. ( A ..^ B ) \/ C = B ) ) ) $= ( cuz cfv wcel c1 caddc co cfzo csn wceq wo fzosplitsn eleq2d elsn2g orbi2d - cun elun syl5bb bitrd ) BADEZFZCABGHIJIZFCABJIZBKZRZFZCUEFZCBLZMZUCUDUGCABN + cun elun bitrid bitrd ) BADEZFZCABGHIJIZFCABJIZBKZRZFZCUEFZCBLZMZUCUDUGCABN OUHUICUFFZMUCUKCUEUFSUCULUJUICBUBPQTUA $. $( A finite interval of integers as union of a half-open integer range and a @@ -148463,7 +148463,7 @@ The modulo (remainder) operation 13-Sep-2013.) $) om2uzisoi $p |- G Isom _E , < ( _om , ( ZZ>= ` C ) ) $= ( vy vz com cuz cfv cep clt wiso wf1o cv wbr wb wral om2uzf1oi wcel rgen2 - wa epel om2uzlt2i syl5bb df-isom mpbir2an ) HBIJZKLCMHUHCNFOZGOZKPZUICJUJ + wa epel om2uzlt2i bitrid df-isom mpbir2an ) HBIJZKLCMHUHCNFOZGOZKPZUICJUJ CJLPZQZGHRFHRABCDESUMFGHHUKUIUJTUIHTUJHTUBULGUIUCAUIUJBCDEUDUEUAFGHUHKLCU FUG $. @@ -148941,7 +148941,7 @@ equinumerous to omega (the set of finite ordinal numbers). (Contributed <-> E. s e. NN0 A. x e. NN0 ( s < x -> -. ph ) ) $= ( vy cn0 crab wss cfn wcel cv clt wbr wn wi wral wrex wb nfcv weq nfv nfn ssrab2 wnel ssnn0fi wsbc nnel nfsbc1v sbceq2a equcoms con2bid elrabf baib - wa syl5bb con4bid imbi2d ralbiia breq2 imbi12d cbvralw bitri a1i rexbidva + wa bitrid con4bid imbi2d ralbiia breq2 imbi12d cbvralw bitri a1i rexbidva nfim bitrd ax-mp ) ABEFZEGZVGHIZCJZBJZKLZAMZNZBEOZCEPZQABEUBVHVIVJDJZKLZV QVGUCZNZDEOZCEPVPDVGCUDVHWAVOCEWAVOQVHVJEIUMWAVRVMBVQUEZNZDEOVOVTWCDEVQEI ZVSWBVRWDVSWBVSMVQVGIZWDWBMZVQVGUFWEWDWFAWFBVQEBVQRBERWBBVMBVQUGZUABDSWBA @@ -149166,7 +149166,7 @@ equinumerous to omega (the set of finite ordinal numbers). (Contributed mptnn0fsupp $p |- ( ph -> ( k e. NN0 |-> C ) finSupp .0. ) $= ( cn0 wbr cfn wcel cv cvv wceq wral nn0ex cmpt cfsupp csupp co cfv crab wne wfn ralrimiva eqid fnmpt syl a1i elexd suppvalfn syl3anc wn wi wrex - clt csb wa simpr ad2antrr rspcsbela syl2anc fvmpts eqeq1d syl5bb imbi2d + clt csb wa simpr ad2antrr rspcsbela syl2anc fvmpts eqeq1d bitrid imbi2d ralbidva rexbidva mpbird rabssnn0fi sylibr eqeltrd wfun wb funmpt mptex nne funisfsupp mp3an12i ) AELDUAZGUBMZWDGUCUDZNOZAWFBPZWDUEZGUGZBLUFZNA WDLUHZLQOZGQOZWFWKRADCOZELSZWLAWOELJUIZELDWDCWDUJZUKULWMATUMAGFIUNZBWDQ @@ -151858,7 +151858,7 @@ notation is used by Donald Knuth for iterated exponentiation (_Science_ by NM, 27-Oct-1999.) $) sq11i $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> A = B ) ) $= - ( c2 cexp co wceq cmul cc0 cle wbr wa recni sqvali eqeq12i msq11i syl5bb + ( c2 cexp co wceq cmul cc0 cle wbr wa recni sqvali eqeq12i msq11i bitrid ) AEFGZBEFGZHAAIGZBBIGZHJAKLJBKLMABHSUATUBAACNOBBDNOPABCDQR $. $} @@ -154388,7 +154388,7 @@ notation is used by Donald Knuth for iterated exponentiation (_Science_ hashsdom $p |- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) < ( # ` B ) <-> A ~< B ) ) $= ( cfn wcel wa chash cfv clt wbr cdom cen wn csdm cle hashcl cr nn0re syl2an - cn0 wceq wne wb ltlen hashdom eqcom hashen syl5bb necon3abid anbi12d brsdom + cn0 wceq wne wb ltlen hashdom eqcom hashen bitrid necon3abid anbi12d brsdom bitrd bitr4di ) ACDZBCDZEZAFGZBFGZHIZABJIZABKIZLZEZABMIUOURUPUQNIZUQUPUAZEZ VBUMUPSDZUQSDZURVEUBZUNAOBOVFUPPDUQPDVHVGUPQUQQUPUQUCRRUOVCUSVDVAABCUDUOUTU QUPUQUPTUPUQTUOUTUQUPUEABUFUGUHUIUKABUJUL $. @@ -156358,7 +156358,7 @@ Proper unordered pairs and triples (sets of size 2 and 3) cr syl3anc 0nn0 pm3.22 0z eluz1 mpbird eluznn0 sylancr ex syl6com pm2.43a cuz com14 com12 3adant1 clt nn0p1gt0 breqtrrd adantrl cvv hashgt0elex csn mp2b vex hashdifsnp1 syl5bi peano2nn0 ad2antrr simplrr simprlr jca spc2gv - cdif com15 com23 mpcom mpd exlimiv sbcex sylbi 3jca difexi fveqeq2 syl5bb + cdif com15 com23 mpcom mpd exlimiv sbcex sylbi 3jca difexi fveqeq2 bitrid mp2an expdimp 3anbi2i anbi2i sylanb syl6an exp41 com4l com25 impcom sylan syl elv impancom alrimivv uzind sbccom syl5com exp31 expcom com24 pm2.43i expd hashcl syl11 3imp ) EQLUGZPOUGZOUHUIZNOUJUKZULUMZAUVNUNUIZUVLUVOAUOZ @@ -156711,7 +156711,7 @@ as finite sequences of _symbols_ (or _characters_) being elements of the 10-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) $) wrdval $p |- ( S e. V -> Word S = U_ l e. NN0 ( S ^m ( 0 ..^ l ) ) ) $= ( vw wcel cword cc0 cv cfzo co wf cn0 wrex cab cmap ciun df-word eliun wb - cvv ovex elmapg mpan2 rexbidv syl5bb abbi2dv eqtr4id ) ABEZAFGCHZIJZADHZK + cvv ovex elmapg mpan2 rexbidv bitrid abbi2dv eqtr4id ) ABEZAFGCHZIJZADHZK ZCLMZDNCLAUJOJZPZDACQUHUMDUOUKUOEUKUNEZCLMUHUMCUKLUNRUHUPULCLUHUJTEUPULSG UIIUAAUJUKBTUBUCUDUEUFUG $. $} @@ -156919,7 +156919,7 @@ of an open range of nonnegative integers (of length equal to the length of van der Vekens, 15-Jul-2018.) $) csbwrdg $p |- ( S e. V -> [_ S / x ]_ Word x = Word S ) $= ( vl vw wcel cv cword csb cc0 cfzo cn0 wrex cab df-word csbeq2i csbconstg - co wf wsbc sbcrex sbcfg csbvarg feq123d bitrd rexbidv syl5bb abbidv csbab + co wf wsbc sbcrex sbcfg csbvarg feq123d bitrd rexbidv bitrid abbidv csbab 3eqtr4g eqtrid ) BCFZABAGZHZIABJDGKRZUMEGZSZDLMZENZIZBHZABUNUSEUMDOPULURA BTZENUOBUPSZDLMZENUTVAULVBVDEVBUQABTZDLMULVDUQADBLUAULVEVCDLULVEABUOIZABU MIZABUPIZSVCAUOUMUPCBUBULVFUOVGBVHUPABUPCQABUOCQABCUCUDUEUFUGUHURAEBUIEBD @@ -159423,7 +159423,7 @@ computer programs (as last() or lastChar()), the terminology used for wrd2ind $p |- ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> ta ) $= ( vn vm cword wcel chash cfv wceq w3a cv wa wi wral cn0 lencl c1 caddc co - cc0 eqeq2 anbi2d imbi1d 2ralbidv weq wb eqeq1 adantl eqcom hasheq0 syl5bb + cc0 eqeq2 anbi2d imbi1d 2ralbidv weq wb eqeq1 adantl eqcom hasheq0 bitrid c0 mpbiri ex syl6bi com13 impcomd fveq2 eqeqan12d fveqeq2 anbi12d imbi12d adantr cmin cpfx clsw cs1 cconcat wsbc pfxcl ad2antrl wne simprll cle wbr ancoms cn eleq1 eqcoms syl5ibr impcom nnge1d wrdlenge1n0 syl mpbird lswcl @@ -162319,7 +162319,7 @@ the symbol at any position is repeated at multiples of L (modulo the s2f1o $p |- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( E = <" A B "> -> E : { 0 , 1 } -1-1-onto-> { A , B } ) ) $= ( wcel wne w3a cs2 wceq cc0 c1 cpr wf1o wa cop cz simpl1 0z jctil simpl2 1z - jca simpl3 0ne1 f1oprg sylc eqcom s2prop 3adant3 eqeq1d syl5bb biimpa mpbid + jca simpl3 0ne1 f1oprg sylc eqcom s2prop 3adant3 eqeq1d bitrid biimpa mpbid f1oeq1d ex ) ACEZBCEZABFZGZDABHZIZJKLZABLZDMZUSVANZVBVCJAOKBOLZMZVDVEJPEZUP NZKPEZUQNZNJKFZURNVGVEVIVKVEUPVHUPUQURVAQRSVEUQVJUPUQURVATUASUBVEURVLUPUQUR VAUCUDSJAKBPCPCUEUFVEVBVCVFDUSVAVFDIZVAUTDIUSVMDUTUGUSUTVFDUPUQUTVFIURABCUH @@ -164966,7 +164966,7 @@ a function (ordinarily on a subset of ` CC ` ) and produces a new cjreb $p |- ( A e. CC -> ( A e. RR <-> ( * ` A ) = A ) ) $= ( cc wcel ccj cfv wceq cre ci cneg cmul co caddc cr cmin recnd ax-icn mulcl cim sylancr cc0 negsubd mulneg2 oveq2d remim 3eqtr4rd replim eqeq12d negcld - recl imcl addcand eqcom eqnegd syl5bb wne wa ine0 pm3.2i a1i mulcan syl3anc + recl imcl addcand eqcom eqnegd bitrid wne wa ine0 pm3.2i a1i mulcan syl3anc wb reim0b 3bitr4d 3bitrrd ) ABCZADEZAFAGEZHAREZIZJKZLKZVHHVIJKZLKZFVKVMFZAM CZVFVGVLAVNVFVHVMIZLKVHVMNKVLVGVFVHVMVFVHAUIOZVFHBCZVIBCZVMBCPVFVIAUJOZHVIQ SZUAVFVKVQVHLVFVSVTVKVQFPWAHVIUBSUCAUDUEAUFUGVFVHVKVMVRVFVSVJBCZVKBCPVFVIWA @@ -167079,7 +167079,7 @@ reflection about the origin (under the map ` x |-> -u x ` ). (Contributed A. n e. A E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) ) $= ( vx vy vz cv wral cz wrex wb c0 wceq raleq rexralbidv bibi12d wa cvv cuz cfv csn cun weq wne cc0 0z ne0ii ral0 rgen2w r19.2z mp2an 2th wi cfn wcel - rexanuz ralunb ralbii rexbii ralsnsg sbcrex ralcom syl5bb rexbidv bitr4id + rexanuz ralunb ralbii rexbii ralsnsg sbcrex ralcom bitrid rexbidv bitr4id anbi1 wsbc bitrd elv anbi2i 3bitr4i 3bitr4g a1i findcard2 ) AEFIZJZDCIUAU BZJCKLZADVSJZCKLZEVQJZMAENJZDVSJZCKLZWBENJZMAEGIZJZDVSJCKLZWBEWHJZMZAEWHH IZUCZUDZJZDVSJZCKLZWBEWOJZMZAEBJZDVSJCKLZWBEBJZMFGHBVQNOZVTWFWCWGXDVRWDCD @@ -167208,7 +167208,7 @@ reflection about the origin (under the map ` x |-> -u x ` ). (Contributed cr syl122anc sylbid expd impr an32s anassrs expimpd ralimdv expr wss uzss ssralv sylan9 ralimdva ex com23 adantr sylan2 imdistanda 3imtr4g reximdva mpdd syld ralrimdva syl5bi raleqbidv ad2antlr oveq2d fveq2d anim2i 3expia - w3a sylc ralbi syl5bb sylibd impbid ) AEIUBZKUCZHUBZKUCZGUDLUCZFUBZUEUFZU + w3a sylc ralbi bitrid sylibd impbid ) AEIUBZKUCZHUBZKUCZGUDLUCZFUBZUEUFZU GZIYKUHUCZUIZHMUJZFUKUIZEYJJUBZKUCZGUDLUCZYNUEUFZJYIUHUCZUIZUGIYQUIZHMUJZ FUKUIZYTEYMUAUBZUEUFZUGZIYQUIHMUJZUAUKUIZAUUIYSUUMFUAUKFUAULZYPUULHIMYQUU OYOUUKEYNUUJYMUEUMUPUNUOAUUNUUHFUKAYNUKUQZUGZUUNEYMYNURUSUDZUEUFZUGZIYQUI @@ -168678,7 +168678,7 @@ Superior limit (lim sup) ( vw wbr cc wcel cfv cmin cabs clt wral nfcv cmpt crli cv cle co wrex crp wi cr wa eqid fmpt sylib eqidd rlim biantrurd nfv nffvmpt1 nfov nffv nfbr wf nfim breq2 imbrov2fvoveq cbvralw fvmpt2 fvoveq1d breq1d ralimiaa ralbi - wb imbi2d 3syl syl5bb rexbidv ralbidv 3bitr2d ) ADEFUAZGUBLGMNZCUCZKUCZUD + wb imbi2d 3syl bitrid rexbidv ralbidv 3bitr2d ) ADEFUAZGUBLGMNZCUCZKUCZUD LZWBVSOZGPUEZQOZBUCZRLZUHZKESZCUIUFZBUGSZUJWLWADUCZUDLZFGPUEQOZWGRLZUHZDE SZCUIUFZBUGSABCKEWDGVSAFMNZDESZEMVSVBHDEMFVSVSUKZULUMIAWBENUJWDUNUOAVTWLJ UPAWKWSBUGAWJWRCUIWJWNWMVSOZGPUEQOZWGRLZUHZDESZAWRWIXFKDEWCWHDWCDUQDWFWGR @@ -168932,7 +168932,7 @@ Superior limit (lim sup) E. m e. RR A. y e. A ( x <_ y -> ( F ` y ) <_ m ) ) ) $= ( cr wa wcel cv cle wbr co wral wrex wi wb cvv reex syl simpllr clo1 cpnf wf wss cfv cdm cico cin cpm elpm2r mpanl12 ello1 baib elin wceq ad3antrrr - fdm eleq2d anbi1d sselda elicopnf mpbirand pm5.32da bitrd syl5bb ralbidv2 + fdm eleq2d anbi1d sselda elicopnf mpbirand pm5.32da bitrd bitrid ralbidv2 imbi1d impexp bitrdi rexbidva ) CFEUCZCFUDZGZEUAHZBIZEUEDIZJKZBEUFZAIZUBU GLZUHZMZDFNZAFNZVSVOJKZVQOZBCMZDFNZAFNVMEFFUILHZVNWDPFQHZWJVMWIRRFFCEQQUJ UKVNWIWDABDEULUMSVMWCWHAFVMVSFHZGZWBWGDFWLVPFHZGZVQWFBWACWNVOWAHZVQOVOCHZ @@ -168984,7 +168984,7 @@ Superior limit (lim sup) E. m e. RR A. x e. A ( y <_ x -> B <_ m ) ) ) $= ( vz wcel cv cle wbr cfv wi wral cr wrex syl2anc nfv cmpt clo1 wss fmpttd wf ello12 nffvmpt1 nfcv nfbr nfim wceq breq2 fveq2 breq1d imbi12d cbvralw - wb wa simpr eqid fvmpt2 imbi2d ralbidva syl5bb 2rexbidv bitrd ) ABDEUAZUB + wb wa simpr eqid fvmpt2 imbi2d ralbidva bitrid 2rexbidv bitrd ) ABDEUAZUB JZCKZIKZLMZVJVGNZFKZLMZOZIDPZFQRCQRZVIBKZLMZEVMLMZOZBDPZFQRCQRADQVGUEDQUC VHVQUQABDEQHUDGCIDFVGUFSAVPWBCFQQVPVSVRVGNZVMLMZOZBDPAWBVOWEIBDVKVNBVKBTB VLVMLBDEVJUGBLUHBVMUHUIUJWEITVJVRUKZVKVSVNWDVJVRVILULWFVLWCVMLVJVRVGUMUNU @@ -169077,7 +169077,7 @@ Superior limit (lim sup) E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) ) $= ( cc cr wa wcel cv cfv cle wbr co wral wrex wi wb cvv syl wf wss co1 cabs cdm cpnf cico cin cpm cnex reex mpanl12 elo1 baib elin wceq fdm ad3antrrr - elpm2r eleq2d anbi1d simpllr sselda elicopnf mpbirand bitrd syl5bb imbi1d + elpm2r eleq2d anbi1d simpllr sselda elicopnf mpbirand bitrd bitrid imbi1d pm5.32da impexp bitrdi ralbidv2 rexbidva ) CFEUAZCGUBZHZEUCIZBJZEKUDKDJZL MZBEUEZAJZUFUGNZUHZOZDGPZAGPZWBVRLMZVTQZBCOZDGPZAGPVPEFGUINIZVQWGRFSIGSIV PWLUJUKFGCESSUSULVQWLWGABDEUMUNTVPWFWKAGVPWBGIZHZWEWJDGWNVSGIZHZVTWIBWDCW @@ -169188,7 +169188,7 @@ Superior limit (lim sup) ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) ) $= ( vc vm vn vp cr wcel wa wi wb wral wceq cv cle wbr wrex cmpt cdm wss co1 clo1 cneg o1dm a1i lo1dm adantr ralrimiva dmmptg syl sseq1d simpr adantlr - cabs cfv simplr absled ancom lenegcon1 syl2anc anbi2d syl5bb bitrd imbi2d + cabs cfv simplr absled ancom lenegcon1 syl2anc anbi2d bitrid bitrd imbi2d ralbidva rexbidv biimpd breq2 anbi1d rexralbidv 3anidm12 syl6an rexlimdva rspc2ev cif simplrr wn simplrl ifclda max2 ad2antlr renegcld letr syl3anc mpan2d sylibd max1 anim12d ancomsd sylibrd imim2d ralimdva reximdv rspcev @@ -169621,7 +169621,7 @@ Superior limit (lim sup) co lo1res cfv cmpt feqmptd reseq1d resmpt3 eqtrdi eleq1d wral wrex sstrid inss1 wf elinel1 ffvelrn syl2an ello1mpt cif imbi1i impexp bitri ad2antrr elin wb sselda elicopnf baibd syl2anc anbi1d simplrl maxle syl3anc bitr4d - wss imbi1d bitr3id pm5.74da syl5bb ralbidv2 simprl ifcld ello12r syl22anc + wss imbi1d bitr3id pm5.74da bitrid ralbidv2 simprl ifcld ello12r syl22anc simprr 3expia rexlimdvva impbid2 ) ADKLZDCUAUBUEZUCZKLZWNDUFAWPHBWNUDZHMZ DUGZUHZKLZWMAWOWTKAWOHBWSUHZWNUCWTADXBWNAHBNDEUIUJHBWNWSUKULUMAXAIMZWROPZ WSJMZOPZQZHWQUNZJNUOINUOWMAHIWQWSJAWQBNBWNUQFUPABNDURZWRBLZWSNLWRWQLZEWRB @@ -169670,7 +169670,7 @@ Superior limit (lim sup) cin cfv cmpt feqmptd reseq1d resmpt3 eqtrdi eleq1d cabs wral inss1 sstrid wrex elinel1 ffvelrn syl2an elo1mpt cif elin imbi1i impexp bitri ad2antrr wf wss sselda elicopnf baibd syl2anc anbi1d simplrl syl3anc bitr4d imbi1d - maxle pm5.74da syl5bb ralbidv2 simprl ifcld simprr elo12r 3expia syl22anc + maxle pm5.74da bitrid ralbidv2 simprl ifcld simprr elo12r 3expia syl22anc wb bitr3id sylbid rexlimdvva impbid2 ) ADKLZDCUAUBUCZUDZKLZWPDUEAWRHBWPUF ZHMZDUGZUHZKLZWOAWQXBKAWQHBXAUHZWPUDXBADXDWPAHBNDEUIUJHBWPXAUKULUMAXCIMZW TOPZXAUNUGJMZOPZQZHWSUOZJRURIRURWOAHIWSXAJAWSBRBWPUPFUQABNDVIZWTBLZXANLWT @@ -170064,7 +170064,7 @@ seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 ) $= o1compt $p |- ( ph -> ( F o. ( y e. B |-> C ) ) e. O(1) ) $= ( vz cv cr wcel cle wbr wi cmpt fmpttd wa cfv wral wrex nfv nfcv nffvmpt1 wb nfbr nfim wceq breq2 fveq2 breq2d imbi12d cbvralw simpr fvmpt2 syl2anc - eqid imbi2d ralbidva syl5bb rexbidv adantr mpbird o1co ) ABNDEGHCEFUAZIJA + eqid imbi2d ralbidva bitrid rexbidv adantr mpbird o1co ) ABNDEGHCEFUAZIJA CEFDKUBLAGOZPQZUCBOZNOZRSZVKVNVJUDZRSZTZNEUEZBPUFZVMCOZRSZVKFRSZTZCEUEZBP UFZMAVTWFUJVLAVSWEBPVSWBVKWAVJUDZRSZTZCEUEAWEVRWINCEVOVQCVOCUGCVKVPRCVKUH CRUHCEFVNUIUKULWINUGVNWAUMZVOWBVQWHVNWAVMRUNWJVPWGVKRVNWAVJUOUPUQURAWIWDC @@ -172061,7 +172061,7 @@ seq N ( + , F ) e. dom ~~> ) ) $= 1rp a1i reximi syl ex syl5bir exlimdv syl5 wi wceq fveq2 raleqdv cbvrexvw wb rspcdva eluzelz eleq2s eqid climcau sylan r19.29uz ralimdv mpan9 an32s weq adantll simplrr eleq1d rspccva fvoveq1d breq1d cbvralvw adantl oveq2d - sylib fveq2d raleqbidv rexralbidv syl5bb caucvg adantlll impbida ad2antrl + sylib fveq2d raleqbidv rexralbidv bitrid caucvg adantlll impbida ad2antrl breq2 cau4 bitr4d rexlimdvaa pm5.21ndd ) EUBLZDFLZMZCNZDOZUCLZCINZPOZQZIG RZDUDUHZLZXOXNBNZDOZUEUFUGOZANZSUIZMZCYBPOZQZBGRZATQZYADJNZUJUDLZJUKZXLXS YAYNJDUDXTULUMXLYMXSJYMDYLUDUIZXLXSDYLUDUNXLYOXSXLYOMZXOXNYLUEUFUGOUOSUIZ @@ -177256,7 +177256,7 @@ attributed to Nicole Oresme (1323-1382). This is Metamath 100 proof fveq2 eleq1d wral eqeltrd ralrimiva weq cbvralvw ad2antrr fznn0sub adantl sylib rspcdva mulcld fsumcl serf ffvelrnda cabs clt wbr cuz wrex c1 cn c2 crp cdiv cab adantlr cli cdm adantr cbvsumv fvoveq1 sumeq1d eqtrid fveq2d - simpr eqeq2d eqeq1 rexbidv syl5bb cbvabv oveq1i oveq2i breq2i mertenslem2 + simpr eqeq2d eqeq1 rexbidv bitrid cbvabv oveq1i oveq2i breq2i mertenslem2 cbvrexvw breq1d anbi2i eluznn0 simpll isumcl syl2anc simplll ad2antlr syl wb eqid sylan oveq2d sumeq2dv eqtr4d eqtrd mulcomd oveq12d 3eqtr3rd fvmpt ovex fsumser fsumsub subdid peano2nn0 nn0zd iserex mpbid isumsplit nn0cnd @@ -183645,7 +183645,7 @@ and cancel them ( ~ rpnnen2lem10 ), since these are the same for both cc fveq2d 3eqtr3d breq2d breq1d orbi12d mpbird nnnn0 fvco3 wfn 1stcof ffn 3syl fnfvelrn syl2anc eqeltrrd suprubd breqtrrdi wi ltletr syl3anc mpan2d sylan simpr ruclem10 ltled eqbrtrd breq1 ralrn suprleub syl31anc eqbrtrid - ralrimiva wb lelttr mpand orim12d mpd lttri2d neneqd nrexdv risset syl5bb + ralrimiva wb lelttr mpand orim12d mpd lttri2d neneqd nrexdv risset bitrid eqeq1 rexrn mtbird eldifd ) AFPHUCZAFUDIUEZUCZPUFUGZPNAUAOUUKAUUKPUHZUUKU IUJZOUMZUNUKQOUUKULZABCODEGHIJKLMUOZUPZAUUMUUNUUPUUQUQZAUNPRUUPUUOUAUMZUK QOUUKULUAPURZUSAUUMUUNUUPUUQUTUAOUUOUNUKPUUKVAVBZVDVCZAFUUIRZUUTHSZFVEZUA @@ -183907,7 +183907,7 @@ infinite descent (here implemented by strong induction). This is divides $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. n e. ZZ ( n x. M ) = N ) ) $= ( vx vy cdvds wbr cop cv cz wcel wa cmul co wceq wrex copab df-br df-dvds - rexbidv eleq2i bitri oveq2 eqeq1d eqeq2 opelopab2 syl5bb ) BCFGZBCHZDIZJK + rexbidv eleq2i bitri oveq2 eqeq1d eqeq2 opelopab2 bitrid ) BCFGZBCHZDIZJK EIZJKLAIZUJMNZUKOZAJPZLDEQZKZBJKCJKLULBMNZCOZAJPZUHUIFKUQBCFRFUPUIDEASUAU BUOURUKOZAJPUTDEBCJJUJBOZUNVAAJVBUMURUKUJBULMUCUDTUKCOVAUSAJUKCURUETUFUG $. @@ -184578,7 +184578,7 @@ infinite descent (here implemented by strong induction). This is ( cdvds wbr cabs cfv wceq cz wcel wa wi cc0 simpr breq1 wb 0dvds adantr zcn abs00ad adantl dvdszrcl bicomd bitrd fveq2 abs0 eqtrdi eqeq2d bitr4d syl5ib sylan9bb expd wn cle wne simprl neqne dvdsleabs2 syl3anc eqcom bitr3di a1dd - eqeq1d expcomd cr abscld letri3 syl2anr syl5bb biimprd syld pm2.61ian com34 + eqeq1d expcomd cr abscld letri3 syl2anr bitrid biimprd syld pm2.61ian com34 a1d mpdd mpcom imp ) ABCDZBACDZAEFZBEFZGZAHIZBHIZJZVQVRWAKZABUABLGZWDVQWEKW FWDJZVQVRWAVQVRJVRWGWAVQVRMWGVRVSLGZWAWFVRLACDZWDWHBLACNWDWIALGZWHWBWIWJOWC APQWBWJWHOWCWBWHWJWBAARZSUBQUCUJWGVTLVSWFVTLGZWDWFVTLEFZLBLEUDUEUFQUGUHUIUK @@ -185022,7 +185022,7 @@ infinite descent (here implemented by strong induction). This is mpan cn0 peano2z znegcl ad2antlr zcn mulcl peano2cn simpl negcon2 syl2anc recnd eqcom sylancr mulcli mp3an23 2t1e2 oveq1i 2m1e1 eqtri eqtr2di adddi addsubass oveq2i mp3an13 oveq1d eqtr4d negeqd zcnd mulneg2 sylancl eqeq1d - negsubdi syl5bb bitrd biimpa oveq2 rspcev rexlimdva2 recn syl2anr mulneg1 + negsubdi bitrid bitrd biimpa oveq2 rspcev rexlimdva2 recn syl2anr mulneg1 bitr4id oveq1 orim12d impel jaodan sylbi cdiv halfnz reeanv mulcom eqeq2d eqtr3 subadd mp3an3 subcl cc0 2cnne0 divmul ancoms subdi mp3an1 syl2an wi wne w3a zsubcl eleq1 syl5ibcom sylbird sylbid rexlimivv sylbir mto pm5.17 @@ -185066,7 +185066,7 @@ infinite descent (here implemented by strong induction). This is Carneiro, 5-Sep-2016.) $) oddm1even $p |- ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) ) $= ( vn cz wcel c2 cv cmul co c1 caddc wceq wrex cmin cdvds wn wa simpl zcnd - wbr 1cnd 2cnd simpr mulcld subadd2d mulcomd eqeq1d syl5bb bitr3d rexbidva + wbr 1cnd 2cnd simpr mulcld subadd2d mulcomd eqeq1d bitrid bitr3d rexbidva eqcom odd2np1 wb 2z peano2zm divides sylancr 3bitr4d ) ACDZEBFZGHZIJHAKZB CLUSEGHZAIMHZKZBCLZEANSOEVCNSZURVAVDBCURUSCDZPZVCUTKZVAVDVHAIUTVHAURVGQRV HTVHEUSVHUAZVHUSURVGUBRZUCUDVIUTVCKVHVDVCUTUJVHUTVBVCVHEUSVJVKUEUFUGUHUIB @@ -185606,7 +185606,7 @@ equal to the half of the predecessor of the odd number (which is an even biidd c1 caddc co cz wral eldifi adantlr ralrimiva rspcsbela nfcv nfcsb1v csb nfbr nfn csbeq1a notbid rspc syl syl5com a1d imp32 adantr ssfi expcom jca cfn imp simpll ssel fsumzcl anim1i opeo cc zcnd addcom mpbird ex opoe - con1d impbid bitr3 bicom 3imtr4g cn0 hashcl nn0zd oddp1even syl5bb bibi1d + con1d impbid bitr3 bicom 3imtr4g cn0 hashcl nn0zd oddp1even bitrid bibi1d notnotb simprr eldifn hashunsng sylc cvv wnel vex a1i df-nel sylibr com12 elun elsni eleq1w syl5ibr jaoi sylbi fsumsplitsnun syl121anc notbi bitrdi wo 3imtr4d findcard2d ) AHUAUDZIUEZJKZHYNCDUFZJKZLHUGJKZYSLHUBUDZIUEZJKZH @@ -185998,7 +185998,7 @@ equal to the half of the predecessor of the odd number (which is an even nnre zsubcl syldan cc nncn zcnd mulcomd modval nn0cnd zmulcl zcn subexsub syl2an2 adantr mpbid eqtr3d dvds0lem syl31anc wreu wb divalg2 breq1 oveq2 breq2d anbi12d riota2 syl2anc mpbi2and eqcomd sneqd snriota eqtr4d eleq2d - syl syl5bb elrab bitrdi ) CEFZAUAFZGZBCAHIZJZBDUBZAKLZACXJMIZNLZGZDOUCZFZ + syl bitrid elrab bitrdi ) CEFZAUAFZGZBCAHIZJZBDUBZAKLZACXJMIZNLZGZDOUCZFZ BOFBAKLZACBMIZNLZGZGXIBXHPZFZXGXPXIYBXIYBXHYAFXHCAHUDUEBXHYAUFUGBXHUHUIXG YAXOBXGYAXNDOUJZPZXOXGXHYCXGYCXHXGXHAKLZACXHMIZNLZYCXHJZXECTFZAUKFZYEXFCU LZAUMZCAUNQXGCAUOIZUPUQZEFZAEFZYFEFZYNARIZYFJYGXGYMXEXFYMTFZXEYIXFATFXFAU @@ -186026,7 +186026,7 @@ equal to the half of the predecessor of the odd number (which is an even modremain $p |- ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( ( N mod D ) = R <-> E. z e. ZZ ( ( z x. D ) + R ) = N ) ) $= - ( cmo co wceq cz wcel cn cn0 wbr wa wrex eqcom wb 3ad2ant3 adantr syl5bb + ( cmo co wceq cz wcel cn cn0 wbr wa wrex eqcom wb 3ad2ant3 adantr bitrid cc clt cv cmul caddc cmin cdvds divalgmodcl 3adant3r ibar adantl 3ad2ant2 w3a nnz simp1 zsubcld divides syl2anc zcn 3ad2ant1 nn0cn zmulcld subadd2d nn0z simpr zcnd rexbidva bitrd 3bitr2d ) DBEFZCGCVIGZDHIZBJIZCKIZCBUALZMZ @@ -186713,7 +186713,7 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact add12d eqtr4d pm5.501 bicomd animorrl syl 2timesd eqtrd addid2d 2cnd mulcld id 2times adantr simpl 0cnd addcomd pm2.61dan ifnot eqtr3id 3eqtr2rd hadrot nbn2 had1 bitr3id cad1 oveq2d wxo notbid df-xor bitr4di ibar simplll ifclda - biorf con1bid syl5bb simpr intnanrd had0 cad0 addcld addid1d sylan9eqr ) DE + biorf con1bid bitrid simpr intnanrd had0 cad0 addcld addid1d sylan9eqr ) DE UAZCABCUBZDFGZABCUCZUDDUEHZFGZIHZADFGZBDFGZIHZCDFGZIHZJWQCKZABLZDFGZABUFZXA FGZIHZXFDIHZXCXHXIAXNXOJXIAKZXEDDIHZIHZDXEIHZDIHZXNXOXPXRDXEDIHZIHXTXPXEDDW QXEEUAZCAWQFEUAZYBUGBDFEUHUIZUJZWQCAUKZYFUMXPDXEDYFYEYFULUNXPXKXEXMXQIXPXJB @@ -187804,7 +187804,7 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact Chapman, 21-Mar-2011.) $) gcdcllem2 $p |- ( ( M e. ZZ /\ N e. ZZ ) -> R = S ) $= ( vx cz wcel wa cv cdvds wbr weq breq1 elrab2 wral breq2 cpr ralprg eqrdv - anbi12d ralbidv anbi2d syl5bb bitr4id ) EJKFJKLZIBCUIIMZBKUJJKZUJENOZUJFN + anbi12d ralbidv anbi2d bitrid bitr4id ) EJKFJKLZIBCUIIMZBKUJJKZUJENOZUJFN OZLZLZUJCKZAMZENOZUQFNOZLUNAUJJBAIPZURULUSUMUQUJENQUQUJFNQUDHRUPUKUJDMZNO ZDEFUAZSZLUIUOUQVANOZDVCSVDAUJJCUTVEVBDVCUQUJVANQUEGRUIVDUNUKVBULUMDEFJJV AEUJNTVAFUJNTUBUFUGUHUC $. @@ -188258,7 +188258,7 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact bezoutlem2 $p |- ( ph -> G e. M ) $= ( wcel cn co wceq cz wrex cc0 cr clt cinf c1 cuz cfv wss c0 wne cv cmul caddc ssrab3 nnuz sseqtri cabs bezoutlem1 ne0i syl6 crab eqid rexcom wa - cc zcnd adantr ad2antll mulcld ad2antrl addcomd eqeq2d 2rexbidva syl5bb + cc zcnd adantr ad2antll mulcld ad2antrl addcomd eqeq2d 2rexbidva bitrid zcn rabbidv eqtrid eleq2d sylibrd wn wo neorian sylibr mpjaod infssuzcl sylancr eqeltrid ) AGHUAUBUCZHLAHUDUEUFZUGHUHUIZWGHNHOWHDUJZEBUJZUKPZFC UJZUKPZULPZQZCRSBRSZDOHIUMUNUOAETUIZWIFTUIZAWREUPUFZHNWIABCDEFHIJKUQHWT @@ -188274,7 +188274,7 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact bezoutlem3 $p |- ( ph -> ( C e. M -> G || C ) ) $= ( wcel co wceq cmul caddc cz vs vt vu vv cdvds wbr wa cmo cc0 cn wn cle clt cr crp wrex simpr eqeq1 2rexbidv weq oveq1d eqeq2d oveq2d cbvrex2vw - cv oveq2 bitrdi elrab2 sylib simpld nnred bezoutlem2 syl5bb nnrpd modlt + cv oveq2 bitrdi elrab2 sylib simpld nnred bezoutlem2 bitrid nnrpd modlt adantr syl2anc nnzd zmodcld nn0red ltnled mpbid wi cdiv cfl cmin simprd ad2antrr simprll simprrl nndivred flcld zmulcld zsubcld simprlr simprrr cfv zcnd mulcld addsub4d mulassd oveq12d joinlmuladdmuld subdid 3eqtr4d @@ -188317,7 +188317,7 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact bezoutlem4 $p |- ( ph -> ( A gcd B ) e. M ) $= ( co wbr cdvds cmul cz wrex wcel vs vt vu cgcd wceq cle gcddvds syl2anc vv cv wa simpld wb gcdcld nn0zd divides mpbid simprd reeanv caddc wi cn - bezoutlem2 weq oveq2 oveq1d eqeq2d oveq2d cbvrex2vw eqeq1 syl5bb elrab2 + bezoutlem2 weq oveq2 oveq1d eqeq2d oveq2d cbvrex2vw eqeq1 bitrid elrab2 2rexbidv sylib simprrl simprll zmulcld simprrr simprlr zaddcld dvdsmul2 adantr mul32d oveq12d joinlmuladdmuld breqtrd oveq1 oveqan12d syl5ibcom zcnd breq2d breq2 imbi2d syl5ibrcom expr com23 rexlimdvva mpd rexlimdvv @@ -190934,7 +190934,7 @@ being prime ( ` Prime = { p e. NN | ... ` ), but even if ` p e. NN0 ` was ( vn cprime wcel c1 wa cn cv cdvds wbr wss wceq wi bitri ancom bitr4i wal wb 3bitri wne crab cpr c2 cuz cfv wo wral 1nprm eleq1 biimpcd mtoi neqned pm4.71i c2o cen isprm isprm2lem eqss imbi2i 1idssfct jcab mpbiran2 adantr - pm5.74ri bitrd expcom pm5.32d syl5bb anass eluz2b3 anbi1i dfss2 breq1 vex + pm5.74ri bitrd expcom pm5.32d bitrid anass eluz2b3 anbi1i dfss2 breq1 vex pm5.32ri elrab elpr imbi12i impexp albii df-ral anbi2i ) BDEZWDBFUAZGBHEZ CIZBJKZCHUBZFBUCZLZGZWEGZBUDUEUFEZAIZBJKZWOFMWOBMUGZNZAHUHZGZWDWEWDBFWDBF MZFDEZUIXAWDXBBFDUJUKULUMUNWEWDWLWDWFWIUOUPKZGWEWLBCUQWEWFXCWKWFWEXCWKSWF @@ -190955,7 +190955,7 @@ being prime ( ` Prime = { p e. NN | ... ` ), but even if ` p e. NN0 ` was pm4.38 df-ne nesym anbi12i ioran bitr4i bitrdi syl6 syld eluzelz caddc 1z imp zltp1le mpan df-2 breq1i bitr4di zltlem1 anbi12d peano2zm elfz mp3an2 bitr4d bitr3d anasss expcom pm5.32d fzssuz 2eluzge1 uzss ax-mp sstri nnuz - 2z sseqtrri sseli pm4.71ri notbid syl5bb pm5.74da bi2.04 3bitr3g ralbidv2 + 2z sseqtrri sseli pm4.71ri notbid bitrid pm5.74da bi2.04 3bitr3g ralbidv2 wss con2b pm5.32i bitri ) BUACBDEFZCZAUBZBUCGZXQHIZXQBIZUDZJZAKUEZLXPXRMZ ADBHUFNZUGNZUEZLABUHXPYCYGXPYBYDAKYFXPXRXQKCZYAJZJXRXQYFCZMZJYHYBJYJYDJXP XRYIYKYIYHYAMZLZMXPXRLZYKYHYAUIYNYMYJYNYMYHYJLYJYNYHYLYJYHYNYLYJOZYHXPXRY @@ -191115,7 +191115,7 @@ being prime ( ` Prime = { p e. NN | ... ` ), but even if ` p e. NN0 ` was cprime wceq wrex dvdszrcl divides 3syl cuz cfv 2z a1i simplr breq2 adantl mpbird w3a zre 3ad2ant1 3ad2ant3 0lt1 0red 1red syl3anc mpani imp 3adant3 lttr 3jca 3exp mpd ltmulgt12 syl caddc df-2 breq1i zltp1le mpancom bicomd - 1zzd syl5bb eluz2 syl3anbrc simpl biimpa sylibr nprm syl2anc eleq1 notbid + 1zzd bitrid eluz2 syl3anbrc simpl biimpa sylibr nprm syl2anc eleq1 notbid ex mpbid rexlimdva2 sylbid ) ABCUAHZCUFIZUBZFAWRGUCZBUDUEZCUGZGJUHZWTAWRB JIZCJIZKZWRXDLFBCUIZGBCUJUKAXCWTGJAXAJIZKZXCKZXBUFIZUBZWTXKXAMULUMZIZBXNI ZXMXKMJIZXIMXANHZXOXQXKUNUOAXIXCUPXKXROXAPHZXKXSBXBPHZXKXTBCPHZXJYAXCAYAX @@ -195059,7 +195059,7 @@ given prime (or other positive integer) that divides the number. For id pccld nnexpcld nndivdvds mpdan c1 cuz cfv wo elnn1uz2 cc0 wne w3a nncn nnne0 3anass sylanbrc diveq1 oveq2 eqeq2d simpr rspcedvd ex pm2.24 sylbid jca syl6 com12 exprmfct breq1 biimpcd necon3bd cmul prmnn mpbid nndivides - syl2anr eqcom ad2antrr ad2antlr nncnd divmul syl3anc syl5bb anim1i sylibr + syl2anr eqcom ad2antrr ad2antlr nncnd divmul syl3anc bitrid anim1i sylibr nnmulcld eldifsn cz nnzd dvdsmul2 2nn0 nn0expcld nn0cnd 3jca mulass breq2 breqtrd a1d exp31 com23 rexlimdva syldd impd jaoi sylbi mp2d imp ) BEFZBG AUBZUCHZIZAJUDZUEZCUBZBKLZCMGUFUGZUDZYDGBGGBUHHZUCHZUIHZKLZUEZYOBKLZYIYMN @@ -195554,7 +195554,7 @@ given prime (or other positive integer) that divides the number. For 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 - syl5bir biantru elinel1 3bitr4g pc11 syl2anc syl5bb dom2d mpi eqeltri + syl5bir biantru elinel1 3bitr4g pc11 syl2anc bitrid dom2d mpi eqeltri fzfi fzfid mapfi hashdom hashmap prhash2ex hashfz1 oveq12d breqtrd prfi ) ABUCZCUDPUEZBGUFZUGUDZQPUHZPFUIRZUJRZUGUDZSFUMRZUKAUXMUXQUKULZ UXLUXPUNULZAUXPUOTUXTUXNUXOUJUPAUAUBUXLUXPDUXODUCZUQTZUYAUAUCZURRZQUS @@ -195779,7 +195779,7 @@ given prime (or other positive integer) that divides the number. For wb syl2anc mpbird mpbid ad2antlr simprr anbi2d fveq2d c0 simprbi eleq2d cin elin imnan sylnibr cif csu sylancl 0le0 eqtrdi cseq cc lelttrd csup sylib elfzuz eluznn syl2an ssrab2 eqsstrdi syldan ralrimiva iunss unssd - sylibr cbvralvw syl5bb elun1 sylbir dfrex2 peano2zd eldifi eldifn prmnn + sylibr cbvralvw bitrid elun1 sylbir dfrex2 peano2zd eldifi eldifn prmnn prmz eleqtrdi elfz5 mtbid ltnled zltp1le elfznn mpd elfzle2 letrd elfzd dvdsle simplr jca elrabd eleqtrrd fveq2 eliuni elun2 rexlimdvaa syl5bir pm2.61d eqelssd hashfz1 eqtr2d noel simprl biantrud bitr4di ltp1d bitrd @@ -195867,7 +195867,7 @@ given prime (or other positive integer) that divides the number. For syl oveq2d oveq1d eqtrd breq12d 2cn nncnd addassd wfn ralrn rexbii sylibr syl2anc ffn suprcld 2rp rpreccl ax-mp ltsubrp resubcl suprlub 2re nnmulcl syl31anc rexrn peano2nnd reexpcl ltnrd cdif cmpt peano2nn nnexpcl nnsqcld - csqrt cbvralvw ralbidv syl5bb cbvrabv cbvsumv eqbrtrid prmreclem5 ex nnzd + csqrt cbvralvw ralbidv bitrid cbvrabv cbvsumv eqbrtrid prmreclem5 ex nnzd simpll eluznn sylan simpl iserex isumrecl elfznn eleqtrdi fsumser ltadd2d recni isumsplit nncn pncan sumeq1d breq1d bitr4d isumsup ltsubaddd adddid 3bitr2d mulcom 2timesi oveq2i eqtr4di 3eqtr4d expmuld expp1 3eqtr3d expcl @@ -196266,7 +196266,7 @@ given prime (or other positive integer) that divides the number. For A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) $= ( wcel cv c2 cexp co caddc cz wrex wceq cab eleq2i wa wi id ovex eqeltrdi cvv a1i rexlimdvva rexlimivv oveq1 oveq1d eqeq2d 2rexbidv cbvrex2vw eqeq1 - weq oveq2d syl5bb elab3 bitri ) EFMEGNZANZOPQZBNZOPQZRQZCNZOPQZDNZOPQZRQZ + weq oveq2d bitrid elab3 bitri ) EFMEGNZANZOPQZBNZOPQZRQZCNZOPQZDNZOPQZRQZ RQZUAZDSTCSTZBSTASTZGUBZMEHNZOPQZINZOPQZRQZJNZOPQZKNZOPQZRQZRQZUAZKSTJSTZ ISTHSTZFVSELUCVRWMGEUIWLEUIMZHISSVTSMWBSMUDZWKWNJKSSWKWNUEWOWESMWGSMUDUDW KEWJUIWKUFWDWIRUGUHUJUKULVRVDWDVNRQZUAZDSTCSTZISTHSTVDEUAZWMVQWRVDWAVHRQZ @@ -196545,7 +196545,7 @@ with complex numbers (gaussian integers) instead, so that we only have ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) ) $= ( vj cv crn cin wcel wex cabs cfv c2 cexp co caddc cmul wceq cgz wrex c1 cmin cfz c0 wne 4sqlem11 n0 sylib cmo wa cc0 vex weq eqeq1 rexbidv - elab2 cab abid rexeqi oveq1 oveq1d eqeq2d cbvrexvw syl5bb rexab rnmpt + elab2 cab abid rexeqi oveq1 oveq1d eqeq2d cbvrexvw bitrid rexab rnmpt 3bitri eleq2i rexcom4 r19.41v exbii bitri 3bitr4i ovex ceqsexv rexbii oveq2 anbi12i elin reeanv w3a cz cle wbr clt cdvds cr crp cn 3ad2ant1 cn0 syl nn0red nnrpd nnred syl22anc elfzelzd zsqcl2 zsqcl nn0zd mpbid @@ -197081,7 +197081,7 @@ with complex numbers (gaussian integers) instead, so that we only have ( vz vw cfv cv wex cn wrex wcel cvv vk vf cvdwm wbr crn ccnv csn cima cpw cvdwa cin c0 wne co wss cn0 wb wf fex sylancl wceq wa fveq2 rneqd imaeq1d cnveq pweqd ineqan12d neeq1d exbidv df-vdwmc brabga syl2anc cxp wfn velpw - vdwapf ffn sseq1 syl5bb rexrn 4syl elin exbii df-rex 3bitr4ri cop eqtr4di + vdwapf ffn sseq1 bitrid rexrn 4syl elin exbii df-rex 3bitr4ri cop eqtr4di n0 df-ov sseq1d rexxp 3bitr3g bitrd ) ADCUCUDZDUJNZUEZCUFZGOUGZUHZUIZUKZU LUMZGPZFOZHOZWPUNZWTUOZHQRFQRZGPADUPSZCTSZWOXDUQJAEBCURETSXKKIEBTCUSUTUAO ZUJNZUEZUBOZUFZWSUHZUIZUKZULUMZGPXDUAUBDCUCUPTXLDVAZXOCVAZVBZXTXCGYCXSXBU @@ -197139,7 +197139,7 @@ with complex numbers (gaussian integers) instead, so that we only have vm wss wral cmpt crn chash wceq wa cmap wrex wb wf fex sylancl cfz coprab c1 w3a df-br df-vdwpc eleq2i bitri simp1 oveq2d eqtr4di simp2 oveqd simp3 fveq2d cnveqd fveq1d imaeq12d sseq12d raleqbidv mpteq12dv eqeq12d anbi12d - sneqd rneqd rexeqbidv rexbidv eloprabga syl5bb syl3anc ) AGPQZFUCQZDUDQZG + sneqd rneqd rexeqbidv rexbidv eloprabga bitrid syl3anc ) AGPQZFUCQZDUDQZG FUEZDUFUGZIRCRJRSZUHTZXBFUISZTZDUJZXCDSZUKZULZUNZCEUOZCEXGUPZUQZURSZGUSZU TZJPEVATZVBZIPVBZVCNLAHBDVDHUDQWSMKHBUDDVEVFXAWTDUEZXCXBUARZUISZTZUBRZUJZ XCYDSZUKZULZUNZCVIUMRZVGTZUOZCYKYFUPZUQZURSZYJUSZUTZJPYKVATZVBZIPVBZUMUAU @@ -197346,7 +197346,7 @@ with complex numbers (gaussian integers) instead, so that we only have subcl 3eqtrd fssdm vdwapid1 3sstr4d ex eqtr4d c0 wne eluzfz1 elfzuz3 cz ne0d nnzd uzid uzaddcl uztrn eluzle ralrimiva r19.2z rexlimiv mpbir2and fznn peano2nnd eluzfz2 iftrue 3syl addid2d sseq12d jaod sylbid ralrimiv - idd rexeqdv rexun eqeq2d rexbidva rexsn syl5bb bitrd abbidv rnmpt df-sn + idd rexeqdv rexun eqeq2d rexbidva rexsn bitrid bitrd abbidv rnmpt df-sn orbi12d uneq12i unab eqtri 3eqtr4g fzfi dffn4 mpbi fofi mp2an hashunsng wfo cvv wi sylan ralbidv rneqd fveqeq2d fveq1 rspc2ev vdwpc mpbird orcd pm2.61dan ) AENVCZPVDZVEZRVFVGVHZQUUBOUUCVIZQVFVGVHNUUDVIZVJAVWTVKVXCVX @@ -197641,7 +197641,7 @@ with complex numbers (gaussian integers) instead, so that we only have cle simpllr elfzle2 leadd1dd nncnd 2timesd breqtrrd cuz nnaddcld nnuz cz eleqtrdi ad2antrr nnzd elfz5 syl2anc mpbird ffvelrnd fvoveq1 fmptd cbvmptv biimpar syldan rspcv syl cvdwa ccnv csn cima wss wex cn0 2nn0 - eluznn0 vdwmc simprll rspcev syl5bi orbi12d syl5bb cmin vex orcd expr + eluznn0 vdwmc simprll rspcev syl5bi orbi12d bitrid cmin vex orcd expr simprlr simprr vdwlem8 exlimdv sylbid syld ralrimdva syl6an rexlimdva rexlimdvva mpd fzfi simprrl mpan sylan2 simp1l simp1r simp2ll simp2lr mapfi w3a simp2rl simp2rr simp3 oveq1d fveq2d mpteq2dv eqtrid vdwlem9 @@ -197918,7 +197918,7 @@ with complex numbers (gaussian integers) instead, so that we only have ( a + ( m x. d ) ) e. ( `' F " { c } ) ) $= ( vu vw vy vz wcel cn cv cmul co caddc wral wrex wn vx cfn wf wa ccnv csn cima cc0 c1 cmin cfz crab simpll simplr weq oveq1 oveq2d cbvralvw ralbidv - wi eleq1d syl5bb oveq2 cbvrex2vw raleqdv 2rexbidv notbid cbvrabv c0 simpr + wi eleq1d bitrid oveq2 cbvrex2vw raleqdv 2rexbidv notbid cbvrabv c0 simpr wne sneq imaeq2d eleq2d cbvrexvw sylnib rabn0 rexnal ralbii ralnex sylibr bitri vdwnnlem3 iman mpbir ) AUBLZMADUCZUDZENZCNZGNZOPZQPZDUEZFNZUFZUGZLZ CUHBNZUIUJPZUKPZRZGMSEMSZBMRZFASZUTWHXETZUDZTXGAWMWNHNZUFZUGZLZCXARZGMSEM @@ -198048,7 +198048,7 @@ with complex numbers (gaussian integers) instead, so that we only have eqtrd sylancr eqtr4d oveq12d simpr fdm 3ad2ant3 sylan9eqr ad2antrr fveq1d raleqdv breq1d oveq2d eqeltrd eqtr3d sseq1d rabss wb eleq2d rabid biimpar bitrdi adantl hashbcss mp3an2i sselda syldan wfn elmapi ad3antlr fniniseg - elpwi ffn 3syl mpbirand anassrs pm5.74da ralbidva syl5bb anbi12d rexbidva + elpwi ffn 3syl mpbirand anassrs pm5.74da ralbidva bitrid anbi12d rexbidva bitr2d rexeqbidv bitrd imbi2d albidv rabbidva eqtr4di infeq1d simp1 simp3 simp2 fexd xrltso infex ovmpod ) IRSZCJSZCRHUCZUDZUAUBIHRUEGUFZKUFZUGUHUI UJZNUFZUBUFZUHZAUFZUGUHZUIUJZQUFZUGUHZUAUFZUKZUUKEUFZUHUUEUKZVJZQUUHULZUM @@ -198292,7 +198292,7 @@ with complex numbers (gaussian integers) instead, so that we only have csn elv biimpi simprr 0ex snid ffvelrn sylancl pwid ffvelrnd nn0red rexrd vex cxr hashxrcl mp1i wfn ffnd fnfvelrn syl2anc suprzub simprl xrletrd wb fvex elpreima 3syl mpbir2and fveq2 breq1d sseq1i snss bitr4i sneq imaeq2d - ffn eleq2d syl5bb anbi12d breq2d anbi1d rspc2ev syl112anc sylanr2 fvelrnb + ffn eleq2d bitrid anbi12d breq2d anbi1d rspc2ev syl112anc sylanr2 fvelrnb ramub mpbid c1 cfz ax-mp cfn mpbird syl syl5ibcom breq1 cmin cop ad2antll cn simpll1 simpll3 nnm1nn0 wf1o f1osn f1of snssd sylancr ovex sylibr cdom fss fzfid ssdomg ssfid hashdom hashfz1 breqtrd hashcl ffvelrnda nn0ltlem1 @@ -204769,7 +204769,7 @@ as a product (if ` G ` is a multiplication), a sum (if ` G ` is an prdsleval $p |- ( ph -> ( F .<_ G <-> A. x e. I ( F ` x ) ( le ` ( R ` x ) ) ( G ` x ) ) ) $= ( vf vg wbr cop cv wcel wa cfv cple wral copab df-br cpr wss cvv fnex - wfn syl2anc fndmd prdsle prss anbi1i opabbii eqtr4di eleq2d syl5bb wb + wfn syl2anc fndmd prdsle prss anbi1i opabbii eqtr4di eleq2d bitrid wb vex wceq fveq1 breqan12d ralbidv opelopab2a bitrd ) AFGIUCZFGUDZUAUEZ CUFUBUEZCUFUGZBUEZVQUHZVTVRUHZVTDUHUIUHZUCZBHUJZUGZUAUBUKZUFZVTFUHZVT GUHZWCUCZBHUJZVOVPIUFAWHFGIULAIWGVPAIVQVRUMCUNZWEUGZUAUBUKWGABCLDEUAU @@ -205006,7 +205006,7 @@ as a product (if ` G ` is a multiplication), a sum (if ` G ` is an 16-Aug-2015.) $) pwsle $p |- ( ( R e. V /\ I e. W ) -> .<_ = ( oR O i^i ( B X. B ) ) ) $= ( vf vg vx wcel wa cfv cple eqid cv cpr csca csn cxp cprds co cbs wss wbr - wral copab cofr cin vex prss pwsval fveq2d eqtrid sseq2d syl5bb fvconst2g + wral copab cofr cin vex prss pwsval fveq2d eqtrid sseq2d bitrid fvconst2g anbi1d wceq ad4ant14 eqtr4di breqd ralbidva simpll simplr simprl pwselbas ffnd simprr inidm eqidd ofrfvalg bitr4d pm5.32da brinxp2 bitr4di opabbidv bitr3d cvv fvexd simpr snex xpexg sylancl c0 wne snnzg adantr dmxp prdsle @@ -205861,7 +205861,7 @@ topology is based on the order and not the extended metric (which would wceq ccom ccnv wrex cdm wfn wfo adantr fndmd rexeqdv fnbrfvb sylan anbi1d fofn syl wex ancom fvex breldm pm4.71ri bitri exbii brco 3bitr4i ad2antrr vex df-rex 3expa an32s anassrs impl pm5.32da bitr3d r19.41v bitrdi simprr - rexbidva eqid fveqeq2 rspcev sylancl biantrurd 3bitr4d syl5bb bitrd brcnv + rexbidva eqid fveqeq2 rspcev sylancl biantrurd 3bitr4d bitrid bitrd brcnv anbi1i 3bitr4ri 3bitr3g imasle breqd simprl expcom vtocl2ga com12 3impib ) AIHUCZJHUCZIEUDZJEUDZFUEZIJGUEZUFZXMXNUGAXSANUHZEUDZOUHZEUDZFUEZXTYBGUE ZUFZUIAXOYCFUEZIYBGUEZUFZUIAXSUINOIJHHXTIUQZYFYIAYJYDYGYEYHYJYAXOYCFXTIEU @@ -206169,7 +206169,7 @@ topology is based on the order and not the extended metric (which would X_ k e. 2o if ( k = (/) , A , B ) <-> ( X e. A /\ Y e. B ) ) $= ( c0 cop c1o cpr c2o cv wceq cif cixp wcel cfv wa cvv elex eleq1d wfn w3a xpsfrnel fnpr2ob biimpri 3ad2ant1 3anass fnpr2o biantrurd fvpr0o bi2anan9 - anim12i fvpr1o bitr3d syl5bb pm5.21nii bitri ) FDGHEGIZCJCKFLABMNOURJUAZF + anim12i fvpr1o bitr3d bitrid pm5.21nii bitri ) FDGHEGIZCJCKFLABMNOURJUAZF URPZAOZHURPZBOZUBZDAOZEBOZQZABCURUCVDDROZEROZQZVGUSVAVJVCVJUSDEUDUEUFVEVH VFVIDASEBSULVDUSVAVCQZQZVJVGUSVAVCUGVJVKVLVGVJUSVKDERRUHUIVHVAVEVIVCVFVHU TDADERUJTVIVBEBDERUMTUKUNUOUPUQ $. @@ -206497,7 +206497,7 @@ topology is based on the order and not the extended metric (which would wfo mp1i f1ofo ovexd f1olecpbl imasleval mpd3an23 wi f1ocnvfv sylancr mpd breq12d c2o wral cbs con0 fvexd 2on a1i wfn fnpr2o prdsleval df2o3 raleqi eleqtrd 0ex 1oex fveq2 2fveq3 breq123d ralpr fvpr0o fveq2d eqtr4di fvpr1o - bitri anbi12d syl5bb bitrd 3bitr3d ) AUOBUPUQCUPURZUHUINOUOUHUSUPUQUIUSUP + bitri anbi12d bitrid bitrd 3bitr3d ) AUOBUPUQCUPURZUHUINOUOUHUSUPUQUIUSUP URUTZVAZVBZUODUPUQEUPURZYNVBZIVGZYLYPFVCVBZUOFUPUQGUPURZVDVEZVFVBZVGZBCUP ZDEUPZIVGBDJVGZCEKVGZVHZAYLYMVIZVJYPUUIVJYRUUCVKAUUDYMVBZYLUUIAUUJBCYMVEZ YLBCYMVLABNVJZCOVJZUUKYLVMUDUEUHUINOYMBCYMVNZVOVPVQZAUUDNOVRZVJZUUJUUIVJA @@ -207583,7 +207583,7 @@ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> wi pweq ineq1d raleqbidv bibi12d simprr ad2antrr mresspw ad3antrrr sseldd sseq2 rspcdva mpbid mrcssidd vex elpw sylibr elinel2 elind sstr2 ralimdva imp cbvralvw sylib mpbird impbida exlimdv mrcf fssd cmrc fvexi feq1 fveq1 - ex bitrdi anbi12d spcev sylan impbid syl5bb bitri ) BDUAJKBDUBJKZDLZXTGMZ + ex bitrdi anbi12d spcev sylan impbid bitrid bitri ) BDUAJKBDUBJKZDLZXTGMZ UCZHMZBKZYAYCLZNOZUEUFZYCPZQZHXTRZSZGUDZSXSEMZBKZAMZCJZYMPZAYMLZNOZRZQZEX TRZSBGDHUGXSYLUUBYLYBYDIMZYAJZYCPZIYFRZQZHXTRZSZGUDZXSUUBYKUUIGYBYJUUHYBY IUUGHXTYBYHUUFYDYBIYFUUDUHZYCPYHUUFYBUUKYGYCYBYAUIUUKYGUJXTXTYAUKIYFYAULU @@ -207677,7 +207677,7 @@ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> wel fmpttd fssxp vpwex xpex ssexg sylancl adantlr elpwi ad2antlr acsfiel2 ralbidva ralbii ralcom bitri bitr4di elrint2 adantl funmpt funiunfv ax-mp wfun sseq1i weq iuneq2d inss1 sspwd sstrid sselda ad2antrr fvmptd3 sseq1d - syl5bb bitr3id 3bitr4d jca feq1 imaeq1 unieqd bibi2d ralbidv spcedv isacs + bitrid bitr3id 3bitr4d jca feq1 imaeq1 unieqd bibi2d ralbidv spcedv isacs anbi12d sylanbrc ismred2 mptru vtoclg ) CJZUAKZYHLZMKZNZBUAKZBLZMKZNCBAYH BUBZYIYMYKYOYHBUAUCYPYJYNMYHBUDUEUFYLUGYIYJDYIYJLZOUGDYIYQDJZYINZYRYJYHMK ZYRYHUHZYSYRYTNYRYJOUUAYRYHUIUJUKUOULYRYIOZYJYRUMUNZYINZUGUUBUUCYTNZYJYJE @@ -207707,7 +207707,7 @@ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> cmpt cin cima cuni cacs cfv ciun wfun funmpt funiunfv mp1i elinel1 elpwid elpwi sylan9ssr velpw sylibr adantll weq eqeq1 ifbid eqid snex ifex fvmpt 0ex iuneq2dv eqtr3d sseq1d iunss sseq1 bibi1d snssg adantr bitr3d 0ss a1i - biimt wn pm2.21 ifbothda ralbidv ad3antlr syl5bb inss1 sspwd sstrid ralss + biimt wn pm2.21 ifbothda ralbidv ad3antlr bitrid inss1 sspwd sstrid ralss 2thd bi2.04 ralbii elpwg biimparc ad2antlr eleq1 imbi1d ceqsralv biantrud simplrr elin bitr4di vex elpw2 bitr3di 3bitrd 3bitrrd rabbidva wf snelpwi simpll 0elpw ifcl sylancl fmpttd isacs1i syl2anc eqeltrd ) DCHZBDHZIZADJZ @@ -208124,7 +208124,7 @@ concepts associated with those structures (product, substructure...) ( va vr ccat wcel ccid cfv cmpt wceq cv co w3a wex cop wne ne0d 3ad2antr1 wa c0 n0 sylib exdistrv simpll simplr2 simplr1 simplr3 simprl simprr 3jca jca wi wsb simplll eleq1d anbi1d simpllr simplr anidm bitrdi simpr oveq1d - anbi12d eleq12d oveq2d eleq2d oveq12d syl5bb anbi2d opeq1d eqidd oveq123d + anbi12d eleq12d oveq2d eleq2d oveq12d bitrid anbi2d opeq1d eqidd oveq123d 3anbi123d eqeq12d imbi12d sbiedvw sbt chvarvv syl13anc ex exlimdvv mp2and syl5bir id neeq1d ralrimiva adantr simpr2 rspcdva 3ad2ant1 simp23 3anbi1d wral eleq1w oveq1 opeq1 oveqd df-3an bitri bitr4di exp45 3imp exlimdv mpd @@ -208627,7 +208627,7 @@ concepts associated with those structures (product, substructure...) catpropd $p |- ( ph -> ( C e. Cat <-> D e. Cat ) ) $= ( vg vf vy vz vh vw co wceq wral wa wcel vx cv cop cco cfv chom wrex ccat cbs wi simpl 2ralimi adantl ralimi a1i wb nfra1 nfv oveq1 eleq1d cbvralvw - oveq2 ralbidv syl5bb cbvralw oveqd eleq12d raleqbidv oveq1d ralcom bitrdi + oveq2 ralbidv bitrid cbvralw oveqd eleq12d raleqbidv oveq1d ralcom bitrdi opeq2 opeq1 biimpi ancri r19.26 eqid chomf adantr ad4antr ad5antr simpllr ccomf ad2antrr simp-4r simplr simpr comfeqval eqeq12d ralimdva ralbi syl6 ex impancom impr syl anbi2d syl5bir expdimp an32s expimpd an4s expr syl56 @@ -210015,7 +210015,7 @@ concepts associated with those structures (product, substructure...) 5-Apr-2020.) $) ciclcl $p |- ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> R e. ( Base ` C ) ) $= ( ccat wcel ccic cfv wbr cbs ciso c0 csupp co cicfval breqd cop cxp wne cvv - wa wfn wb isofn fvexd 0ex a1i df-br elsuppfng syl5bb syl3anc opelxp1 adantr + wa wfn wb isofn fvexd 0ex a1i df-br elsuppfng bitrid syl3anc opelxp1 adantr w3a syl6bi sylbid imp ) ADEZBCAFGZHZBAIGZEZUQUSBCAJGZKLMZHZVAUQURVCBCANOUQV DBCPZUTUTQZEZVEVBGKRZTZVAUQVBVFUAZVBSEZKSEZVDVIUBAUCUQAJUDVLUQUEUFVDVEVCEVJ VKVLUMVIBCVCUGVEVBSSVFKUHUIUJVGVAVHBCUTUTUKULUNUOUP $. @@ -210024,7 +210024,7 @@ concepts associated with those structures (product, substructure...) 5-Apr-2020.) $) cicrcl $p |- ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> S e. ( Base ` C ) ) $= ( ccat wcel ccic cfv wbr cbs ciso c0 csupp co cicfval breqd cop cxp wne cvv - wa wfn wb isofn fvexd 0ex a1i df-br elsuppfng syl5bb syl3anc opelxp2 adantr + wa wfn wb isofn fvexd 0ex a1i df-br elsuppfng bitrid syl3anc opelxp2 adantr w3a syl6bi sylbid imp ) ADEZBCAFGZHZCAIGZEZUQUSBCAJGZKLMZHZVAUQURVCBCANOUQV DBCPZUTUTQZEZVEVBGKRZTZVAUQVBVFUAZVBSEZKSEZVDVIUBAUCUQAJUDVLUQUEUFVDVEVCEVJ VKVLUMVIBCVCUGVEVBSSVFKUHUIUJVGVAVHBCUTUTUKULUNUOUP $. @@ -210225,7 +210225,7 @@ which when given operations from the base category (using ~ df-resc ) ( vz vs vt cv wcel wceq wa wex cdm cssc wbr cxp cfv cpw cixp wss co wfn wrex wral brssc fndm adantl adantr fndmd eqtr3d dmeqd dmxpid 3eqtr3g ex id sqxpeqd fneq2d syl5ibrcom impbid anbi1d exbidv pweq rexeqdv ceqsexgv - syl5bb wb syl bitrd df-rex cvv w3a 3anass elixp2 vex xpex fnex pm4.71ri + bitrid wb syl bitrd df-rex cvv w3a 3anass elixp2 vex xpex fnex pm4.71ri mpan2 3bitr4i anbi2d an12 bitrdi exsimpl isset sylibr a1i ssexg adantrd wi expcom elpw sseq1 raleqdv cop fvex fveq2 df-ov eqtr4di sseq12d ralxp anbi12d pm5.21ndd 3bitrd ) AFGUAUBZFLMOZXLUCZLOZGUDZUEZUFPZMEUEZUJZXLDQ @@ -217602,7 +217602,7 @@ that F(A') is isomorphic to B'.". Therefore, the category of sets and op1std feq1d mpbird wfn csbex fnmpoi op2ndd fneq1d mpbiri ad2antrr adantr wf ccat simplrl simplrr ffvelrnd simprl simprr nat1st2nd natcl ralrimivva funcf2 catcocl evlf2 fuchom xpchom2 evlf1 feq23d oveq2 fveq2 df-ov oveq2d - oveq12d eqtr4di ralxp oveq1 oveq1d 2ralbidv syl5bb sylibr r19.21bi fveq2d + oveq12d eqtr4di ralxp oveq1 oveq1d 2ralbidv bitrid sylibr r19.21bi fveq2d feq123d catidcl 3eqtr4d fveq12d 3ad2ant1 eqeltrrd opelxp eleqtrd oveq123d w3a xpchom opeq12d anasss xpcid evlf2val catlid ccom fucid fveq1d syl2anc fvco3 eqtrd funcid 3eqtrd id simp21 simp22 simp23 simp3l simp3r evlfcllem @@ -218253,7 +218253,7 @@ that F(A') is isomorphic to B'.". Therefore, the category of sets and syl2anc eqtrdi opeq12d oveq12d curf2val curf12 oveq123d ad2antrr ad2antlr ccid opelxpi opelxpd adantl catidcl xpchom2 eleqtrrd funcco xpcco2 fveq2d df-ov eqtr4di catrid catlid 3eqtr2d feq2d mpbid oveq2 eqeq12d ralxp oveq1 - wf funcf2 2ralbidv syl5bb sylibr funcfn2 1st2nd 3eqtr4d ) ABCDUGFUHLZUJMZ + wf funcf2 2ralbidv bitrid sylibr funcfn2 1st2nd 3eqtr4d ) ABCDUGFUHLZUJMZ YDUKMZNZEUJMZEUKMZNZYDEAYEYHYFYIAYEYHOZKPZUAPZYELZYLYMYHLZOZUACULMZQKBULM ZQZAYPKUAYRYQAYLYRRZYMYQRZUMZUMZYNYMYLFUJMZMZUJMZMZYOUUCYRYQBCDYDFYLYMYDS ZACUNRZUUBITZADUNRZUUBABCUOLZUNRZUUKAEUULDUPLZRZUUMUUKUMJUULDEUQURUSZTAFB @@ -219755,7 +219755,7 @@ that F(A') is isomorphic to B'.". Therefore, the category of sets and $( Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) $) oduleg $p |- ( ( A e. V /\ B e. W ) -> ( A G B <-> B .<_ A ) ) $= - ( wbr ccnv wcel wa cple cfv oduleval eqtr4i breqi brcnvg syl5bb ) ABDLA + ( wbr ccnv wcel wa cple cfv oduleval eqtr4i breqi brcnvg bitrid ) ABDLA BEMZLAGNBHNOBAELABDUCDCPQUCKCEFIJRSTABGHEUAUB $. $} @@ -220296,7 +220296,7 @@ either the theorem or its proof (Remark: That is not true - it becomes 12-Oct-2011.) $) pltval $p |- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) ) $= - ( wcel wbr wne wa wb cid cdif pltfval breqd wn brdif adantl anbi2d syl5bb + ( wcel wbr wne wa wb cid cdif pltfval breqd wn brdif adantl anbi2d bitrid ideqg necon3bbid sylan9bb 3impb ) EAKZGBKZHCKZGHDLZGHFLZGHMZNZOUIULGHFPQZ LZUJUKNZUOUIDUPGHADEFIJRSUQUMGHPLZTZNURUOGHFPUAURUTUNUMUKUTUNOUJUKUSGHGHC UEUFUBUCUDUGUH $. @@ -220665,7 +220665,7 @@ either the theorem or its proof (Remark: That is not true - it becomes ( wbr wral wi wa breq1 cv crab wcel wceq ralrab imbi1i ralbii anbi12i cpo posref syl2anc imbi12d rspcva syl5com mpand adantr idd rgen breq2 ralbidv imbi2d rspcv syl wb simpr posasymb syl3anc biimpd ancomsd syl2and biimprd - mpii ralrimivw adantl bicomd sylan9bb syl5ib adantlr jca ex impbid syl5bb + mpii ralrimivw adantl bicomd sylan9bb syl5ib adantlr jca ex impbid bitrid pm5.5 ) DUAZBUAZIPZDCUAZJIPZCFUBZQZWDEUAZIPZDWIQZWEWKIPZRZEFQZSWDJIPZWFRZ DFQZWQWLRZDFQZWNRZEFQZSZAWEFUCZSZWEJUDZWJWSWPXCWHWQWFDCFWGWDJITZUEWOXBEFW MXAWNWHWQWLDCFXHUEUFUGUHXFXDXGXFWSJWEIPZXCWEJIPZXGAWSXIRXEAJFUCZWSXIOAJJI @@ -221419,7 +221419,7 @@ net proof size (existence part)? $) posglbmo $p |- ( ( K e. Poset /\ S C_ B ) -> E* x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) $= ( vw wcel wa cv wbr wral wi weq breq1 ralbidv imbi12d cpo simprrl simprlr - wss wrmo simplrr rspcdva simprll simprrr simplrl wb ancom posasymb syl5bb + wss wrmo simplrr rspcdva simprll simprrr simplrl wb ancom posasymb bitrid mpd w3a 3expb ad4ant13 mpbi2and ex ralrimivva breq2 imbi2d anbi12d sylibr rmo4 ) FUAKZEDUDZLZAMZBMZGNZBEOZCMZVKGNZBEOZVNVJGNZPZCDOZLZJMZVKGNZBEOZVP VNWAGNZPZCDOZLZLZAJQZPZJDOADOVTADUEVIWJAJDDVIVJDKZWADKZLZLZWHWIWNWHLZWAVJ @@ -221548,7 +221548,7 @@ Totally ordered sets (tosets) ( K e. Toset <-> ( .< Or B /\ ( _I |` B ) C_ .<_ ) ) ) $= ( vx vy wcel cv wbr wo wral wa weq wb pleval2 bitri cpo wpo cid cres ctos wss w3o wor 3expb equcom orbi2i bitrdi 3com23 orbi12d df-3or or32 orordir - w3a bitr4di 2ralbidva pm5.32i pospo anbi1d syl5bb istos df-so anbi1i an32 + w3a bitr4di 2ralbidva pm5.32i pospo anbi1d bitrid istos df-so anbi1i an32 3bitr4g ) CEKZCUAKZILZJLZDMZVMVLDMZNZJAOIAOZPZABUBZUCAUDDUFZPZVLVMBMZIJQZ VMVLBMZUGZJAOIAOZPZCUEKABUHZVTPZVRVKWFPVJWGVKVQWFVKVPWEIJAAVKVLAKZVMAKZPP ZVPWBWCNZWDWCNZNZWEWLVNWMVOWNVKWJWKVNWMRABCDVLVMFGHSUIVKWJWKVOWNRZVKWKWJW @@ -222501,7 +222501,7 @@ Totally ordered sets (tosets) oduclatb $p |- ( O e. CLat <-> D e. CLat ) $= ( ccla wcel cvv c0 club cfv eqid codu cpo cdm wceq cglb wa eqeq1d anbi12d dmeqd isclat elex wn noel wss ssid base0 clatlubcl mpan2 mto fvprc eqtrid - eleq1d mtbiri con4i cbs oduposb ancom odulub oduglb syl5bb odubas 3bitr4g + eleq1d mtbiri con4i cbs oduposb ancom odulub oduglb bitrid odubas 3bitr4g cpw pm5.21nii ) BDEZBFEZADEZBDUAVFVGVFUBZVGGDEZVIGGHIZIZGEZVKUCVIGGUDVLGU EGGVJGUFVJJUGUHUIVHAGDVHABKIGCBKUJUKULUMUNVFBLEZBHIZMZBUOIZVCZNZBOIZMZVQN ZPZPALEZAHIZMZVQNZAOIZMZVQNZPZPVEVGVFVMWCWBWJABFCUPWBWAVRPVFWJVRWAUQVFWAW @@ -222762,7 +222762,7 @@ Totally ordered sets (tosets) conversely. (Contributed by Stefan O'Rear, 30-Jan-2015.) $) odudlatb $p |- ( K e. V -> ( K e. DLat <-> D e. DLat ) ) $= ( vx vy vz wcel clat cv cjn cfv co cmee wceq wral wa cdlat eqid isdlat - cbs latdisd bicomd pm5.32i odulatb anbi1d syl5bb odujoin odumeet 3bitr4g + cbs latdisd bicomd pm5.32i odulatb anbi1d bitrid odujoin odumeet 3bitr4g odubas ) BCHZBIHZEJZFJZGJZBKLZMBNLZMUNUOURMUNUPURMUQMOGBUALZPFUSPEUSPZQZA IHZUNUOUPURMUQMUNUOUQMUNUPUQMURMOGUSPFUSPEUSPZQZBRHARHVAUMVCQULVDUMUTVCUM VCUTEFGUSUQBURUSSZUQSZURSZUBUCUDULUMVBVCABCDUEUFUGEFGUSUQBURVEVFVGTEFGUSU @@ -222930,7 +222930,7 @@ Totally ordered sets (tosets) cdrs cun wceq drsbn0 neneqd fvprc fveq2d base0 eqtr4di nsyl2 cproset cple simp1 wbr isdrs cpo ipopos posprs mp1i 2thd ipobas neeq1 rexeq raleqbi1dv id syl simpll simplrl simpr ipole syl3anc simplrr unss rexbidva 2ralbidva - bitrdi anbi2d bitr3d 3anass 3bitr4g syl5bb pm5.21nii ) DEFZUBGZDHGZWFDIJZ + bitrdi anbi2d bitr3d 3anass 3bitr4g bitrid pm5.21nii ) DEFZUBGZDHGZWFDIJZ AKZBKZUCCKZLZCDMZBDNADNZOZWEWDPFZIUDWFWEWOIWOWDWOQZUEUFWFUAZWOIPFIWQWDIPD EUGUHUIUJUKWFWGWMUNWEWDULGZWOIJZWHWJWDUMFZUOZWIWJWTUOZRZCWOMZBWONZAWONZOZ WFWNABCWOWDWTWPWTQZUPWFWRWSXFRZRWFWGWMRZRXGWNWFWRWFXIXJWFWRWFWDUQGWRWFDWD @@ -223737,7 +223737,7 @@ Totally ordered sets (tosets) -> ( ph <-> ( ( B R x /\ C R x ) /\ A. y e. X ( ( B R y /\ C R y ) -> x R y ) ) ) ) @= ( cv wbr wral wi wa wcel breq1 cpr wceq wb ralprg sylan9bb imbi1d ralbidv - raleq anbi12d adantll syl5bb ) ACNZBNZHOZCEPZDNZULHOZDEPZUMULHOZQZCLPZRZH + raleq anbi12d adantll bitrid ) ACNZBNZHOZCEPZDNZULHOZDEPZUMULHOZQZCLPZRZH ISZEFGUAZUBZRFJSGKSRZRFUMHOZGUMHOZRZFULHOZGULHOZRZUSQZCLPZRZMVEVFVBVOUCVC VEVFRZUOVIVAVNVEUOUNCVDPVFVIUNCEVDUHUNVGVHCFGJKULFUMHTULGUMHTUDUEVPUTVMCL VPURVLUSVEURUQDVDPVFVLUQDEVDUHUQVJVKDFGJKUPFULHTUPGULHTUDUEUFUGUIUJUK @. @@ -223754,7 +223754,7 @@ Totally ordered sets (tosets) spwex @p |- ( ( R e. PosetRel /\ A e. V ) -> ( E. x e. X ph <-> ( R supw A ) e. X ) ) @= ( cps wcel wa wreu cv wbr wral wb cvv adantr wi crio wrex cspw reubii cdm - co dmexg eqeltrid riotaclbgBAD syl syl5bb spweu reurex impbid1 spwval + co dmexg eqeltrid riotaclbgBAD syl bitrid spweu reurex impbid1 spwval eleq1d ex 3bitr4d ) FKLZEGLZMZABHNZCOZBOZFPCEQDOVDFPDEQVEVDFPUACHQMZBHUBZHLZABHU CZFEUDUGZHLUTVCVHRVAVCVFBHNZUTVHAVFBHJUEUTHSLVKVHRUTHFUFSIFKUHUIVFBHSUJUK @@ -224645,7 +224645,7 @@ arbitrary magmas (then it should be called "iterated sum"). If the magma is crab wcel cseq cuz wrex wex cio chash wf1o ccom ccnv cdif cima wsbc cif c1 csb cgsu cmpo df-gsum a1i simprl fveq2d eqtr4di oveqd eqeq1d anbi12d raleqbidv rabeqbidv weq oveq2 eqeq12d oveq1 cbvralvw ovanraleqv cbvrabv - id syl5bb eqtri csbeq1d fvexi rabex2 simplrr rneqd simpr sseq12d adantr + id bitrid eqtri csbeq1d fvexi rabex2 simplrr rneqd simpr sseq12d adantr dmeqd eqtrd eleq1d seqeq2d seqeq3d fveq1d eqeq2d rexbidv exbidv difeq2d ad2antrr iotabidv imaeq2d cnveqd imaeq1d 3eqtr4d sbceq1d cnvexg eqeltrd imaexg 3syl fveq2 adantl oveq2d f1oeq2d bitrd ifbieq12d elexd iotaex @@ -227408,7 +227408,7 @@ According to Wikipedia ("Endomorphism", 25-Jan-2024, $( Two ways of saying a function is a mapping of ` A ` to itself. (Contributed by AV, 27-Jan-2024.) $) elefmndbas $p |- ( A e. V -> ( F e. B <-> F : A --> A ) ) $= - ( wcel cmap co wf efmndbas eleq2i id elmapd syl5bb ) CBHCAAIJZHAEHZAACKBQ + ( wcel cmap co wf efmndbas eleq2i id elmapd bitrid ) CBHCAAIJZHAEHZAACKBQ CABDFGLMRAACEERNZSOP $. $d F f $. @@ -228117,7 +228117,7 @@ According to Wikipedia ("Endomorphism", 25-Jan-2024, ( wcel wa co wceq wral eqeq12d oveq2 cpr prid1g eleqtrrdi sgrp2nmndlem2 cv prid2g simpl syldan wi oveq1 id syl5ib wn simprl simprr neqne adantr wne sgrp2nmndlem3 syl3anc ex pm2.61i oveq12d jca31 syl2an raleqi ralprg - jca syl5bb ralbidv eqeq1d anbi12d bitrd mpbird ) CGNZDHNZOZBUEZAUEZIPZV + jca bitrid ralbidv eqeq1d anbi12d bitrd mpbird ) CGNZDHNZOZBUEZAUEZIPZV RQZBERZAERZCCIPZCQZDCIPZDQZOZCDIPZCQZDDIPZDQZOZOZVOCENZDENZWNVPVOCCDUAZ ECDGUBJUCVPDWQECDHUFJUCWOWPOZWEWGWMWOWPWOWEWOWPUGABCDCEFIJKLMUDUHZCDQZW RWGUIWRWEWTWGWSWTWDWFCDCDCIUJWTUKZSULWTUMZWRWGXBWROZWOWPCDURZWGXBWOWPUN @@ -229197,7 +229197,7 @@ with the same (relevant) properties is also a group. (Contributed by grplmulf1o $p |- ( ( G e. Grp /\ X e. B ) -> F : B -1-1-onto-> B ) $= ( vy wcel wa cv co cfv grpcl 3expa eqid wceq syl13anc cgrp grpinvcl eqcom cminusg syldanl wb simpll adantrl simprl simplr grplcan c0g adantr oveq1d - grprinv simprr grpass grplid ad2ant2rl 3eqtr3d eqeq1d bitr3d syl5bb f1o2d + grprinv simprr grpass grplid ad2ant2rl 3eqtr3d eqeq1d bitr3d bitrid f1o2d ) EUAKZFBKZLZAJBBFAMZCNZFEUDOZOZJMZCNZDIVEVFVHBKZVIBKBCEFVHGHPQVEVFVKBKZV LBKZVMBKZBEVJFGVJRZUBZVEVOVPVQBCEVKVLGHPQUEZVHVMSVMVHSZVGVNVPLZLZVLVISZVH VMUCWCFVMCNZVISZWAWDWCVEVQVNVFWFWAUFVEVFWBUGZVGVPVQVNVTUHVGVNVPUIVEVFWBUJ @@ -229599,7 +229599,7 @@ with the same (relevant) properties is also a group. (Contributed by ( ( F ` A ) : X -1-1-onto-> X /\ `' ( F ` A ) = ( F ` ( I ` A ) ) ) ) $= ( vb wcel wa cfv wf1o wceq co cmpt cgrp cv grpcl 3expa grpinvcl syldanl ccnv eqid eqcom c0g grplinv adantr oveq1d simpll simplr simprl syl13anc - grpass grplid ad2ant2r 3eqtr3rd eqeq2d syl5bb wb simprr adantrr grplcan + grpass grplid ad2ant2r 3eqtr3rd eqeq2d bitrid wb simprr adantrr grplcan bitrd f1ocnv2d grplactfval adantl f1oeq1d cnveqd cbvmptv eqtrdi eqeq12d oveq2 syl anbi12d mpbird ) EUANZAGNZOZGGADPZQZWDUGZAFPZDPZRZOGGHGAHUBZB SZTZQZWLUGZMGWGMUBZBSZTZRZOWCHMGGWKWPWLWLUHWAWBWJGNZWKGNZGBEAWJJKUCUDZW