From 86cf5e61f14809b717dbd65570686564300f1750 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Tue, 24 Dec 2024 07:43:37 -0700 Subject: [PATCH] Rename ffvelrn to ffvelcdm in iset.mm This is to match set.mm naming. This is a search and replace followed by running scripts/rewrap Also rename one reference in mmil.html . --- iset.mm | 1574 ++++++++++++++++++++++++------------------------- mmil.raw.html | 2 +- 2 files changed, 788 insertions(+), 788 deletions(-) diff --git a/iset.mm b/iset.mm index f6697503c7..5e31788444 100644 --- a/iset.mm +++ b/iset.mm @@ -50801,7 +50801,7 @@ We use their notation ("onto" under the arrow). (Contributed by NM, $( A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.) $) - ffvelrn $p |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B ) $= + ffvelcdm $p |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B ) $= ( wf wcel wa cfv crn wfn ffn fnfvelrn sylan wi frn sseld adantr mpd ) ABDEZ CAFZGCDHZDIZFZUABFZSDAJTUCABDKACDLMSUCUDNTSUBBUAABDOPQR $. @@ -50810,7 +50810,7 @@ We use their notation ("onto" under the arrow). (Contributed by NM, $( A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.) $) ffvelrni $p |- ( C e. A -> ( F ` C ) e. B ) $= - ( wf wcel cfv ffvelrn mpan ) ABDFCAGCDHBGEABCDIJ $. + ( wf wcel cfv ffvelcdm mpan ) ABDFCAGCDHBGEABCDIJ $. $} ${ @@ -50818,7 +50818,7 @@ We use their notation ("onto" under the arrow). (Contributed by NM, $( A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) $) ffvelrnda $p |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B ) $= - ( wf wcel cfv ffvelrn sylan ) ABCEGDBHDEICHFBCDEJK $. + ( wf wcel cfv ffvelcdm sylan ) ABCEGDBHDEICHFBCDEJK $. ffvelrnd.2 $e |- ( ph -> C e. A ) $. $( A function's value belongs to its codomain. (Contributed by Mario @@ -50943,12 +50943,12 @@ We use their notation ("onto" under the arrow). (Contributed by NM, dffo3 $p |- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) ) $= ( wfo wf crn wceq wa cv cfv wrex wral dffo2 cab wb wcel wal wi wfn fnrnfv - ffn eqeq1d syl dfbi2 simpr ffvelrn adantr eqeltrd exp31 biantrurd bitr4id - rexlimdv albidv abeq1 df-ral 3bitr4g bitrd pm5.32i bitri ) CDEFCDEGZEHZDI - ZJVBBKZAKZELZIZACMZBDNZJCDEOVBVDVJVBVDVIBPZDIZVJVBECUAZVDVLQCDEUCVMVCVKDA - BCEUBUDUEVBVIVEDRZQZBSVNVITZBSVLVJVBVOVPBVBVOVIVNTZVPJVPVIVNUFVBVQVPVBVHV - NACVBVFCRZVHVNVBVRJZVHJVEVGDVSVHUGVSVGDRVHCDVFEUHUIUJUKUNULUMUOVIBDUPVIBD - UQURUSUTVA $. + ffn eqeq1d syl dfbi2 simpr ffvelcdm adantr eqeltrd exp31 rexlimdv bitr4id + biantrurd albidv abeq1 df-ral 3bitr4g bitrd pm5.32i bitri ) CDEFCDEGZEHZD + IZJVBBKZAKZELZIZACMZBDNZJCDEOVBVDVJVBVDVIBPZDIZVJVBECUAZVDVLQCDEUCVMVCVKD + ABCEUBUDUEVBVIVEDRZQZBSVNVITZBSVLVJVBVOVPBVBVOVIVNTZVPJVPVIVNUFVBVQVPVBVH + VNACVBVFCRZVHVNVBVRJZVHJVEVGDVSVHUGVSVGDRVHCDVFEUHUIUJUKULUNUMUOVIBDUPVIB + DUQURUSUTVA $. $( Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) $) @@ -51069,11 +51069,11 @@ We use their notation ("onto" under the arrow). (Contributed by NM, $( A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.) $) ffnfv $p |- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) ) $= - ( vy wf wfn cv cfv wcel wral ffn ffvelrn ralrimiva jca crn wss simpl wceq - wa wrex fvelrnb biimpd nfra1 nfv wi rsp eleq1 biimpcd syl6 rexlimd sylan9 - ssrdv df-f sylanbrc impbii ) BCDFZDBGZAHZDIZCJZABKZTZUQURVBBCDLUQVAABBCUS - DMNOVCURDPZCQUQURVBRVCEVDCUREHZVDJZUTVESZABUAZVBVECJZURVFVHABVEDUBUCVBVGV - IABVAABUDVIAUEVBUSBJVAVGVIUFVAABUGVGVAVIUTVECUHUIUJUKULUMBCDUNUOUP $. + ( vy wf wfn cv cfv wcel wral wa ffn ffvelcdm ralrimiva jca crn simpl wceq + wss wrex fvelrnb biimpd nfra1 nfv wi rsp eleq1 biimpcd syl6 rexlimd ssrdv + sylan9 df-f sylanbrc impbii ) BCDFZDBGZAHZDIZCJZABKZLZUQURVBBCDMUQVAABBCU + SDNOPVCURDQZCTUQURVBRVCEVDCUREHZVDJZUTVESZABUAZVBVECJZURVFVHABVEDUBUCVBVG + VIABVAABUDVIAUEVBUSBJVAVGVIUFVAABUGVGVAVIUTVECUHUIUJUKUMULBCDUNUOUP $. $} ${ @@ -51128,13 +51128,13 @@ We use their notation ("onto" under the arrow). (Contributed by NM, ffvresb $p |- ( Fun F -> ( ( F |` A ) : A --> B <-> A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) ) $= ( wfun cres wf cv cdm wcel cfv wa wral fdm cin dmres inss2 adantl wfn wss - eqsstri eqsstrrdi sselda wceq fvres ffvelrn eqeltrrd jca ralrimiva ralimi - crn simpl dfss3 sylibr funfn fnssres sylanb sylan2 eleq1d syl5ibr ralimia - simpr fnfvrnss syl2anc df-f sylanbrc ex impbid2 ) DEZBCDBFZGZAHZDIZJZVLDK - ZCJZLZABMZVKVQABVKVLBJZLZVNVPVKBVMVLVKBVJIZVMBCVJNWABVMOVMDBPBVMQUAUBUCVT - VLVJKZVOCVSWBVOUDVKVLBDUEZRBCVLVJUFUGUHUIVIVRVKVIVRLZVJBSZVJUKCTZVKVRVIBV - MTZWEVRVNABMWGVQVNABVNVPULUJABVMUMUNVIDVMSWGWEDUOVMBDUPUQURZWDWEWBCJZABMZ - WFWHVRWJVIVQWIABVQWIVSVPVNVPVBVSWBVOCWCUSUTVARABCVJVCVDBCVJVEVFVGVH $. + eqsstri eqsstrrdi sselda wceq fvres ffvelcdm eqeltrrd jca ralrimiva simpl + crn ralimi dfss3 sylibr funfn fnssres sylanb sylan2 simpr syl5ibr ralimia + eleq1d fnfvrnss syl2anc df-f sylanbrc ex impbid2 ) DEZBCDBFZGZAHZDIZJZVLD + KZCJZLZABMZVKVQABVKVLBJZLZVNVPVKBVMVLVKBVJIZVMBCVJNWABVMOVMDBPBVMQUAUBUCV + TVLVJKZVOCVSWBVOUDVKVLBDUEZRBCVLVJUFUGUHUIVIVRVKVIVRLZVJBSZVJUKCTZVKVRVIB + VMTZWEVRVNABMWGVQVNABVNVPUJULABVMUMUNVIDVMSWGWEDUOVMBDUPUQURZWDWEWBCJZABM + ZWFWHVRWJVIVQWIABVQWIVSVPVNVPUSVSWBVOCWCVBUTVARABCVJVCVDBCVJVEVFVGVH $. $} ${ @@ -51266,7 +51266,7 @@ We use their notation ("onto" under the arrow). (Contributed by NM, by Mario Carneiro, 27-Dec-2014.) $) fcompt $p |- ( ( A : D --> E /\ B : C --> D ) -> ( A o. B ) = ( x e. C |-> ( A ` ( B ` x ) ) ) ) $= - ( vy wf wa cv cfv wcel ffvelrn adantll wfn cmpt wceq ffn dffn5im syl + ( vy wf wa cv cfv wcel ffvelcdm adantll wfn cmpt wceq ffn dffn5im syl adantl adantr fveq2 fmptco ) EFBHZDECHZIZAGDEAJZCKZGJZBKZUIBKCBUFUHDLUIEL UEDEUHCMNUGCDOZCADUIPQUFULUEDECRUAADCSTUGBEOZBGEUKPQUEUMUFEFBRUBGEBSTUJUI BUCUD $. @@ -51324,13 +51324,13 @@ We use their notation ("onto" under the arrow). (Contributed by NM, fsn2 $p |- ( F : { A } --> B <-> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) ) $= ( csn wf cfv cvv wcel cop wceq wa wfn ffn snid funfvex mpan2 syl wb cima - funfni adantr ffvelrn crn dffn3 biimpi cdm imadmrn imaeq2d eqtr3id fnsnfv - elex fndm eqtr4d feq3 mpbid jca wss snssi ancoms sylan impbii fsng anbi2d - fss mpan syl5bb pm5.21nii ) AEZBCFZACGZHIZVKBIZCAVKJEKZLZVJCVIMZVLVIBCNZV - PAVIIZVLADOZVLVIACACPUAQRVMVLVNVKBULUBVJVMVIVKEZCFZLZVLVOVJWBVJVMWAVJVRVM - VSVIBACUCQVJVPWAVQVPVICUDZCFZWAVPWDVICUEUFVPWCVTKWDWASVPWCCVITZVTVPWCCCUG - ZTWECUHVPWFVICVICUMUIUJVPVRVTWEKVSVIACUKQUNWCVTVICUORUPRUQVMVTBURZWAVJVKB - USWAWGVJVIVTBCVEUTVAVBVLWAVNVMAHIVLWAVNSDAVKHHCVCVFVDVGVH $. + funfni elex adantr ffvelcdm crn dffn3 biimpi imadmrn fndm imaeq2d eqtr3id + cdm fnsnfv eqtr4d feq3 mpbid jca wss snssi fss ancoms sylan impbii anbi2d + fsng mpan syl5bb pm5.21nii ) AEZBCFZACGZHIZVKBIZCAVKJEKZLZVJCVIMZVLVIBCNZ + VPAVIIZVLADOZVLVIACACPUAQRVMVLVNVKBUBUCVJVMVIVKEZCFZLZVLVOVJWBVJVMWAVJVRV + MVSVIBACUDQVJVPWAVQVPVICUEZCFZWAVPWDVICUFUGVPWCVTKWDWASVPWCCVITZVTVPWCCCU + LZTWECUHVPWFVICVICUIUJUKVPVRVTWEKVSVIACUMQUNWCVTVICUORUPRUQVMVTBURZWAVJVK + BUSWAWGVJVIVTBCUTVAVBVCVLWAVNVMAHIVLWAVNSDAVKHHCVEVFVDVGVH $. $} $( The cross product of two singletons. (Contributed by Mario Carneiro, @@ -51493,7 +51493,7 @@ We use their notation ("onto" under the arrow). (Contributed by NM, $( The value of a constant function. (Contributed by NM, 30-May-1999.) $) fvconst $p |- ( ( F : A --> { B } /\ C e. A ) -> ( F ` C ) = B ) $= - ( csn wf wcel wa cfv wceq ffvelrn elsni syl ) ABEZDFCAGHCDIZNGOBJANCDKOBLM + ( csn wf wcel wa cfv wceq ffvelcdm elsni syl ) ABEZDFCAGHCDIZNGOBJANCDKOBLM $. ${ @@ -52016,13 +52016,13 @@ is the image of an element of its domain (see ~ foima ). (Contributed the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.) $) foco2 $p |- ( ( F : B --> C /\ G : A --> B /\ ( F o. G ) : A -onto-> C ) -> F : B -onto-> C ) $= - ( vy vx vz wf ccom wfo w3a cv cfv wceq wrex wral wa wcel adantll sylanbrc - simp1 foelrn ffvelrn fvco3 fveq2 eqeq2d rspcev syl2anc rexbidv syl5ibrcom - eqeq1 rexlimdva syl5 impl ralrimiva 3impa dffo3 ) BCDIZABEIZACDEJZKZLUSFM - ZGMZDNZOZGBPZFCQZBCDKUSUTVBUBUSUTVBVHUSUTRZVBRVGFCVIVBVCCSZVGVBVJRVCHMZVA - NZOZHAPVIVGHACVCVAUCVIVMVGHAVIVKASZRZVGVMVLVEOZGBPZVOVKENZBSZVLVRDNZOZVQU - TVNVSUSABVKEUDTUTVNWAUSABVKDEUETVPWAGVRBVDVROVEVTVLVDVRDUFUGUHUIVMVFVPGBV - CVLVEULUJUKUMUNUOUPUQGFBCDURUA $. + ( vy vx vz wf ccom wfo w3a cv cfv wceq wrex wral wa wcel adantll ffvelcdm + simp1 foelrn fvco3 fveq2 eqeq2d rspcev syl2anc eqeq1 syl5ibrcom rexlimdva + rexbidv syl5 impl ralrimiva 3impa dffo3 sylanbrc ) BCDIZABEIZACDEJZKZLUSF + MZGMZDNZOZGBPZFCQZBCDKUSUTVBUBUSUTVBVHUSUTRZVBRVGFCVIVBVCCSZVGVBVJRVCHMZV + ANZOZHAPVIVGHACVCVAUCVIVMVGHAVIVKASZRZVGVMVLVEOZGBPZVOVKENZBSZVLVRDNZOZVQ + UTVNVSUSABVKEUATUTVNWAUSABVKDEUDTVPWAGVRBVDVROVEVTVLVDVRDUEUFUGUHVMVFVPGB + VCVLVEUIULUJUKUMUNUOUPGFBCDUQUR $. $} ${ @@ -52378,11 +52378,11 @@ is the image of an element of its domain (see ~ foima ). (Contributed fcofo $p |- ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) -> F : A -onto-> B ) $= ( vy vx wf ccom cid cres wceq w3a cfv wrex wral wfo simp1 wcel 3ad2antl2 - cv ffvelrn simpl3 fveq1d fvco3 fvresi adantl 3eqtr3rd fveq2 eqeq2d rspcev - wa syl2anc ralrimiva dffo3 sylanbrc ) ABDGZBACGZDCHZIBJZKZLZUPETZFTZDMZKZ - FANZEBOABDPUPUQUTQVAVFEBVAVBBRZUKZVBCMZARZVBVIDMZKZVFUQUPVGVJUTBAVBCUASVH - VBURMZVBUSMZVKVBVHVBURUSUPUQUTVGUBUCUQUPVGVMVKKUTBAVBDCUDSVGVNVBKVABVBUEU - FUGVEVLFVIAVCVIKVDVKVBVCVIDUHUIUJULUMFEABDUNUO $. + cv wa ffvelcdm simpl3 fveq1d fvresi adantl 3eqtr3rd eqeq2d rspcev syl2anc + fvco3 fveq2 ralrimiva dffo3 sylanbrc ) ABDGZBACGZDCHZIBJZKZLZUPETZFTZDMZK + ZFANZEBOABDPUPUQUTQVAVFEBVAVBBRZUAZVBCMZARZVBVIDMZKZVFUQUPVGVJUTBAVBCUBSV + HVBURMZVBUSMZVKVBVHVBURUSUPUQUTVGUCUDUQUPVGVMVKKUTBAVBDCUKSVGVNVBKVABVBUE + UFUGVEVLFVIAVCVIKVDVKVBVCVIDULUHUIUJUMFEABDUNUO $. $} ${ @@ -52411,14 +52411,14 @@ is the image of an element of its domain (see ~ foima ). (Contributed cocan1 $p |- ( ( F : B -1-1-> C /\ H : A --> B /\ K : A --> B ) -> ( ( F o. H ) = ( F o. K ) <-> H = K ) ) $= ( vx wf ccom cfv wceq wral wcel fvco3 3ad2antl2 wb wfn ffn syl syl2anc cv - wf1 wa 3ad2antl3 eqeq12d simpl1 ffvelrn f1fveq syl12anc ralbidva 3ad2ant1 - w3a bitrd f1f simp2 fnfco simp3 eqfnfv 3bitr4d ) BCDUBZABEHZABFHZULZGUAZD - EIZJZVDDFIZJZKZGALZVDEJZVDFJZKZGALZVEVGKZEFKZVCVIVMGAVCVDAMZUCZVIVKDJZVLD - JZKZVMVRVFVSVHVTVAUTVQVFVSKVBABVDDENOVBUTVQVHVTKVAABVDDFNUDUEVRUTVKBMZVLB - MZWAVMPUTVAVBVQUFVAUTVQWBVBABVDEUGOVBUTVQWCVAABVDFUGUDBCVKVLDUHUIUMUJVCVE - AQZVGAQZVOVJPVCDBQZVAWDVCBCDHZWFUTVAWGVBBCDUNUKBCDRSZUTVAVBUOZBADEUPTVCWF - VBWEWHUTVAVBUQZBADFUPTGAVEVGURTVCEAQZFAQZVPVNPVCVAWKWIABERSVCVBWLWJABFRSG - AEFURTUS $. + wf1 w3a wa 3ad2antl3 eqeq12d simpl1 ffvelcdm f1fveq syl12anc ralbidva f1f + bitrd 3ad2ant1 simp2 fnfco simp3 eqfnfv 3bitr4d ) BCDUBZABEHZABFHZUCZGUAZ + DEIZJZVDDFIZJZKZGALZVDEJZVDFJZKZGALZVEVGKZEFKZVCVIVMGAVCVDAMZUDZVIVKDJZVL + DJZKZVMVRVFVSVHVTVAUTVQVFVSKVBABVDDENOVBUTVQVHVTKVAABVDDFNUEUFVRUTVKBMZVL + BMZWAVMPUTVAVBVQUGVAUTVQWBVBABVDEUHOVBUTVQWCVAABVDFUHUEBCVKVLDUIUJUMUKVCV + EAQZVGAQZVOVJPVCDBQZVAWDVCBCDHZWFUTVAWGVBBCDULUNBCDRSZUTVAVBUOZBADEUPTVCW + FVBWEWHUTVAVBUQZBADFUPTGAVEVGURTVCEAQZFAQZVPVNPVCVAWKWIABERSVCVBWLWJABFRS + GAEFURTUS $. $} ${ @@ -52722,16 +52722,16 @@ is the image of an element of its domain (see ~ foima ). (Contributed p. 33. (Contributed by NM, 27-Apr-2004.) $) isocnv $p |- ( H Isom R , S ( A , B ) -> `' H Isom S , R ( B , A ) ) $= ( vx vy vz vw wf1o cv wbr cfv wb wral wa wiso wcel wceq f1ocnvfv2 adantrr - ccnv f1ocnv adantr adantrl breq12d adantlr wf syl ffvelrn anim12dan breq1 - f1of fveq2 breq1d bibi12d bicom bitrdi breq2d breq2 rspc2va sylan sylanl1 - an32s bitr3d ralrimivva jca df-isom 3imtr4i ) ABEJZFKZGKZCLZVKEMZVLEMZDLZ - NZGAOFAOZPZBAEUBZJZHKZIKZDLZWBVTMZWCVTMZCLZNZIBOHBOZPABCDEQBADCVTQVSWAWIV - JWAVRABEUCZUDVSWHHIBBVSWBBRZWCBRZPZPWEEMZWFEMZDLZWDWGVJWMWPWDNVRVJWMPWNWB - WOWCDVJWKWNWBSWLABWBETUAVJWLWOWCSWKABWCETUEUFUGVJBAVTUHZVRWMWPWGNZVJWAWQW - JBAVTUMUIWQWMVRWRWQWMPWEARZWFARZPVRWRWQWKWSWLWTBAWBVTUJBAWCVTUJUKVQWRWNVO - DLZWEVLCLZNZFGWEWFAAVKWESZVQXBXANXCXDVMXBVPXAVKWEVLCULXDVNWNVODVKWEEUNUOU - PXBXAUQURVLWFSZXAWPXBWGXEVOWOWNDVLWFEUNUSVLWFWECUTUPVAVBVDVCVEVFVGFGABCDE - VHHIBADCVTVHVI $. + ccnv f1ocnv adantr adantrl breq12d adantlr wf f1of syl ffvelcdm anim12dan + breq1 fveq2 breq1d bibi12d bicom bitrdi breq2 rspc2va sylan an32s sylanl1 + breq2d bitr3d ralrimivva jca df-isom 3imtr4i ) ABEJZFKZGKZCLZVKEMZVLEMZDL + ZNZGAOFAOZPZBAEUBZJZHKZIKZDLZWBVTMZWCVTMZCLZNZIBOHBOZPABCDEQBADCVTQVSWAWI + VJWAVRABEUCZUDVSWHHIBBVSWBBRZWCBRZPZPWEEMZWFEMZDLZWDWGVJWMWPWDNVRVJWMPWNW + BWOWCDVJWKWNWBSWLABWBETUAVJWLWOWCSWKABWCETUEUFUGVJBAVTUHZVRWMWPWGNZVJWAWQ + WJBAVTUIUJWQWMVRWRWQWMPWEARZWFARZPVRWRWQWKWSWLWTBAWBVTUKBAWCVTUKULVQWRWNV + ODLZWEVLCLZNZFGWEWFAAVKWESZVQXBXANXCXDVMXBVPXAVKWEVLCUMXDVNWNVODVKWEEUNUO + UPXBXAUQURVLWFSZXAWPXBWGXEVOWOWNDVLWFEUNVDVLWFWECUSUPUTVAVBVCVEVFVGFGABCD + EVHHIBADCVTVHVI $. $( Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.) $) @@ -52753,12 +52753,12 @@ is the image of an element of its domain (see ~ foima ). (Contributed either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) $) isores2 $p |- ( H Isom R , S ( A , B ) <-> H Isom R , ( S i^i ( B X. B ) ) ( A , B ) ) $= - ( vx vy wf1o cv wbr cfv wb wral wa cxp wiso wcel ffvelrn ralbidva df-isom - cin wf f1of adantrr adantrl brinxp syl2anc anassrs bibi2d pm5.32i 3bitr4i - sylan ) ABEHZFIZGIZCJZUNEKZUOEKZDJZLZGAMZFAMZNUMUPUQURDBBOUAZJZLZGAMZFAMZ - NABCDEPABCVCEPUMVBVGUMVAVFFAUMUNAQZNZUTVEGAVIUOAQZNUSVDUPUMVHVJUSVDLZUMAB - EUBZVHVJNZVKABEUCVLVMNUQBQZURBQZVKVLVHVNVJABUNERUDVLVJVOVHABUOERUEUQURBBD - UFUGULUHUISSUJFGABCDETFGABCVCETUK $. + ( vx vy wf1o cv wbr cfv wb wral cxp wiso wcel ffvelcdm ralbidva df-isom + wa cin f1of adantrr adantrl brinxp syl2anc anassrs bibi2d pm5.32i 3bitr4i + wf sylan ) ABEHZFIZGIZCJZUNEKZUOEKZDJZLZGAMZFAMZTUMUPUQURDBBNUAZJZLZGAMZF + AMZTABCDEOABCVCEOUMVBVGUMVAVFFAUMUNAPZTZUTVEGAVIUOAPZTUSVDUPUMVHVJUSVDLZU + MABEUKZVHVJTZVKABEUBVLVMTUQBPZURBPZVKVLVHVNVJABUNEQUCVLVJVOVHABUOEQUDUQUR + BBDUEUFULUGUHRRUIFGABCDESFGABCVCESUJ $. $} $( An isomorphism from one well-order to another can be restricted on either @@ -52901,21 +52901,21 @@ H Isom ( R i^i ( A X. A ) ) , S ( A , B ) ) $= $( Lemma for ~ isopo . (Contributed by Stefan O'Rear, 16-Nov-2014.) $) isopolem $p |- ( H Isom R , S ( A , B ) -> ( S Po B -> R Po A ) ) $= ( va vb vc vd ve vf cv wbr wa wi wral wcel ex wb anbi12d wiso wpo w3a cfv - wn wf1o isof1o f1of ffvelrn 3anim123d 3syl imp breq12 anidms notbid breq1 - wf wceq anbi1d imbi12d breq2 imbi1d anbi2d rspc3v syl simpl simpr1 isorel - syl12anc simpr2 simpr3 sylibrd com23 imp31 ralrimivvva df-po 3imtr4g ) AB - CDEUAZFLZVSDMZUEZVSGLZDMZWBHLZDMZNZVSWDDMZOZNZHBPGBPFBPZILZWKCMZUEZWKJLZC - MZWNKLZCMZNZWKWPCMZOZNZKAPJAPIAPZBDUBACUBVRWJXBVRWJNXAIJKAAAVRWJWKAQZWNAQ - ZWPAQZUCZXAVRXFWJXAVRXFWJXAOVRXFNZWJWKEUDZXHDMZUEZXHWNEUDZDMZXKWPEUDZDMZN - ZXHXMDMZOZNZXAXGXHBQZXKBQZXMBQZUCZWJXROVRXFYBVRABEUFABEUQZXFYBOABCDEUGABE - UHYCXCXSXDXTXEYAYCXCXSABWKEUIRYCXDXTABWNEUIRYCXEYAABWPEUIRUJUKULWIXRXJXHW - BDMZWENZXHWDDMZOZNXJXLXKWDDMZNZYFOZNFGHXHXKXMBBBVSXHURZWAXJWHYGYKVTXIYKVT - XISVSXHVSXHDUMUNUOYKWFYEWGYFYKWCYDWEVSXHWBDUPUSVSXHWDDUPUTTWBXKURZYGYJXJY - LYEYIYFYLYDXLWEYHWBXKXHDVAWBXKWDDUPTVBVCWDXMURZYJXQXJYMYIXOYFXPYMYHXNXLWD - XMXKDVAVCWDXMXHDVAUTVCVDVEXGWMXJWTXQXGWLXIXGVRXCXCWLXISVRXFVFZVRXCXDXEVGZ - YOABWKWKCDEVHVIUOXGWRXOWSXPXGWOXLWQXNXGVRXCXDWOXLSYNYOVRXCXDXEVJZABWKWNCD - EVHVIXGVRXDXEWQXNSYNYPVRXCXDXEVKZABWNWPCDEVHVITXGVRXCXEWSXPSYNYOYQABWKWPC - DEVHVIUTTVLRVMVNVORFGHBDVPIJKACVPVQ $. + wn wf1o isof1o f1of ffvelcdm 3anim123d 3syl imp wceq breq12 anidms notbid + breq1 anbi1d imbi12d breq2 imbi1d anbi2d rspc3v syl simpl simpr1 syl12anc + wf isorel simpr2 simpr3 sylibrd com23 imp31 ralrimivvva df-po 3imtr4g ) A + BCDEUAZFLZVSDMZUEZVSGLZDMZWBHLZDMZNZVSWDDMZOZNZHBPGBPFBPZILZWKCMZUEZWKJLZ + CMZWNKLZCMZNZWKWPCMZOZNZKAPJAPIAPZBDUBACUBVRWJXBVRWJNXAIJKAAAVRWJWKAQZWNA + QZWPAQZUCZXAVRXFWJXAVRXFWJXAOVRXFNZWJWKEUDZXHDMZUEZXHWNEUDZDMZXKWPEUDZDMZ + NZXHXMDMZOZNZXAXGXHBQZXKBQZXMBQZUCZWJXROVRXFYBVRABEUFABEVHZXFYBOABCDEUGAB + EUHYCXCXSXDXTXEYAYCXCXSABWKEUIRYCXDXTABWNEUIRYCXEYAABWPEUIRUJUKULWIXRXJXH + WBDMZWENZXHWDDMZOZNXJXLXKWDDMZNZYFOZNFGHXHXKXMBBBVSXHUMZWAXJWHYGYKVTXIYKV + TXISVSXHVSXHDUNUOUPYKWFYEWGYFYKWCYDWEVSXHWBDUQURVSXHWDDUQUSTWBXKUMZYGYJXJ + YLYEYIYFYLYDXLWEYHWBXKXHDUTWBXKWDDUQTVAVBWDXMUMZYJXQXJYMYIXOYFXPYMYHXNXLW + DXMXKDUTVBWDXMXHDUTUSVBVCVDXGWMXJWTXQXGWLXIXGVRXCXCWLXISVRXFVEZVRXCXDXEVF + ZYOABWKWKCDEVIVGUPXGWRXOWSXPXGWOXLWQXNXGVRXCXDWOXLSYNYOVRXCXDXEVJZABWKWNC + DEVIVGXGVRXDXEWQXNSYNYPVRXCXDXEVKZABWNWPCDEVIVGTXGVRXCXEWSXPSYNYOYQABWKWP + CDEVIVGUSTVLRVMVNVORFGHBDVPIJKACVPVQ $. $( An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.) $) @@ -52929,20 +52929,20 @@ H Isom ( R i^i ( A X. A ) ) , S ( A , B ) ) $= $d A a b c x y z $. $d B a b c x y z $. $( Lemma for ~ isoso . (Contributed by Stefan O'Rear, 16-Nov-2014.) $) isosolem $p |- ( H Isom R , S ( A , B ) -> ( S Or B -> R Or A ) ) $= - ( vx vy vz va vb vc cv wbr wo wi wral wa wcel cfv ffvelrn wiso wpo df-3an - wor isopolem w3a wf1o wf isof1o f1of 3anim123d 3syl imp wceq breq1 orbi1d - ex imbi12d breq2 orbi2d orbi12d imbi2d rspc3v wb isorel 3adantr3 3adantr2 - syl ancom2s 3adantr1 sylibrd sylan2br anassrs ralrimdva ralrimdvva df-iso - anim12d 3imtr4g ) ABCDEUAZBDUBZFLZGLZDMZWAHLZDMZWDWBDMZNZOZHBPGBPFBPZQACU - BZILZJLZCMZWKKLZCMZWNWLCMZNZOZKAPZJAPIAPZQBDUDACUDVSVTWJWIWTABCDEUEVSWIWS - IJAAVSWKARZWLARZQZQWIWRKAVSXCWNARZWIWROZXCXDQVSXAXBXDUFZXEXAXBXDUCVSXFQZW - IWKESZWLESZDMZXHWNESZDMZXKXIDMZNZOZWRXGXHBRZXIBRZXKBRZUFZWIXOOVSXFXSVSABE - UGABEUHZXFXSOABCDEUIABEUJXTXAXPXBXQXDXRXTXAXPABWKETUQXTXBXQABWLETUQXTXDXR - ABWNETUQUKULUMWHXOXHWBDMZXHWDDMZWFNZOXJYBWDXIDMZNZOFGHXHXIXKBBBWAXHUNZWCY - AWGYCWAXHWBDUOYFWEYBWFWAXHWDDUOUPURWBXIUNZYAXJYCYEWBXIXHDUSYGWFYDYBWBXIWD - DUSUTURWDXKUNZYEXNXJYHYBXLYDXMWDXKXHDUSWDXKXIDUOVAVBVCVHXGWMXJWQXNVSXAXBW - MXJVDXDABWKWLCDEVEVFXGWOXLWPXMVSXAXDWOXLVDXBABWKWNCDEVEVGVSXBXDWPXMVDZXAV - SXDXBYIABWNWLCDEVEVIVJVAURVKVLVMVNVOVQFGHBDVPIJKACVPVR $. + ( vx vy vz va vb vc cv wbr wo wi wral wa wcel cfv ffvelcdm wpo wor df-3an + wiso isopolem w3a wf1o wf isof1o f1of ex 3anim123d 3syl wceq breq1 orbi1d + imp imbi12d breq2 orbi2d orbi12d imbi2d rspc3v wb isorel 3adantr3 ancom2s + syl 3adantr2 3adantr1 sylibrd anassrs ralrimdva ralrimdvva anim12d df-iso + sylan2br 3imtr4g ) ABCDEUDZBDUAZFLZGLZDMZWAHLZDMZWDWBDMZNZOZHBPGBPFBPZQAC + UAZILZJLZCMZWKKLZCMZWNWLCMZNZOZKAPZJAPIAPZQBDUBACUBVSVTWJWIWTABCDEUEVSWIW + SIJAAVSWKARZWLARZQZQWIWRKAVSXCWNARZWIWROZXCXDQVSXAXBXDUFZXEXAXBXDUCVSXFQZ + WIWKESZWLESZDMZXHWNESZDMZXKXIDMZNZOZWRXGXHBRZXIBRZXKBRZUFZWIXOOVSXFXSVSAB + EUGABEUHZXFXSOABCDEUIABEUJXTXAXPXBXQXDXRXTXAXPABWKETUKXTXBXQABWLETUKXTXDX + RABWNETUKULUMUQWHXOXHWBDMZXHWDDMZWFNZOXJYBWDXIDMZNZOFGHXHXIXKBBBWAXHUNZWC + YAWGYCWAXHWBDUOYFWEYBWFWAXHWDDUOUPURWBXIUNZYAXJYCYEWBXIXHDUSYGWFYDYBWBXIW + DDUSUTURWDXKUNZYEXNXJYHYBXLYDXMWDXKXHDUSWDXKXIDUOVAVBVCVHXGWMXJWQXNVSXAXB + WMXJVDXDABWKWLCDEVEVFXGWOXLWPXMVSXAXDWOXLVDXBABWKWNCDEVEVIVSXBXDWPXMVDZXA + VSXDXBYIABWNWLCDEVEVGVJVAURVKVQVLVMVNVOFGHBDVPIJKACVPVR $. $} $( An isomorphism preserves strict ordering. (Contributed by Stefan O'Rear, @@ -55257,8 +55257,8 @@ ordered pairs (for use in defining operations). This is a special case 27-Aug-2006.) $) fovrn $p |- ( ( F : ( R X. S ) --> C /\ A e. R /\ B e. S ) -> ( A F B ) e. C ) $= - ( cxp wf wcel co wa cop opelxpi cfv df-ov ffvelrn eqeltrid sylan2 3impb ) D - EGZCFHZADIZBEIZABFJZCIZUBUCKUAABLZTIZUEABDEMUAUGKUDUFFNCABFOTCUFFPQRS $. + ( cxp wf wcel co wa cop opelxpi cfv df-ov ffvelcdm eqeltrid sylan2 3impb ) + DEGZCFHZADIZBEIZABFJZCIZUBUCKUAABLZTIZUEABDEMUAUGKUDUFFNCABFOTCUFFPQRS $. ${ fovrnd.1 $e |- ( ph -> F : ( R X. S ) --> C ) $. @@ -56187,14 +56187,14 @@ ordered pairs (for use in defining operations). This is a special case $( The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.) $) off $p |- ( ph -> ( F oF R G ) : C --> U ) $= - ( vz cof co wf cv cfv cmpt wcel wa wral cin inss1 eqsstrri ffvelrn syl2an - sseli inss2 ralrimivva adantr wceq oveq1 eleq1d oveq2 syl21anc eqid fmptd - rspc2va wfn ffn syl eqidd offval feq1d mpbird ) AFJKLGUBUCZUDFJUAFUAUEZKU - FZVPLUFZGUCZUGZUDAUAFVSJVTAVPFUHZUIVQHUHZVRIUHZBUEZCUEZGUCZJUHZCIUJBHUJZV - SJUHZADHKUDZVPDUHZWBWAPFDVPFDEUKZDTDEULUMUPDHVPKUNUOAEILUDZVPEUHZWCWAQFEV - PFWLETDEUQUMUPEIVPLUNUOAWHWAAWGBCHIOURUSWGWIVQWEGUCZJUHBCVQVRHIWDVQUTWFWO - JWDVQWEGVAVBWEVRUTWOVSJWEVRVQGVCVBVGVDVTVEVFAFJVOVTAUADEVQVRGFKLMNAWJKDVH - PDHKVIVJAWMLEVHQEILVIVJRSTAWKUIVQVKAWNUIVRVKVLVMVN $. + ( vz cof co wf cv cfv cmpt wcel wa wral cin inss1 eqsstrri sseli ffvelcdm + syl2an inss2 ralrimivva adantr wceq oveq1 eleq1d oveq2 rspc2va eqid fmptd + syl21anc wfn ffn syl eqidd offval feq1d mpbird ) AFJKLGUBUCZUDFJUAFUAUEZK + UFZVPLUFZGUCZUGZUDAUAFVSJVTAVPFUHZUIVQHUHZVRIUHZBUEZCUEZGUCZJUHZCIUJBHUJZ + VSJUHZADHKUDZVPDUHZWBWAPFDVPFDEUKZDTDEULUMUNDHVPKUOUPAEILUDZVPEUHZWCWAQFE + VPFWLETDEUQUMUNEIVPLUOUPAWHWAAWGBCHIOURUSWGWIVQWEGUCZJUHBCVQVRHIWDVQUTWFW + OJWDVQWEGVAVBWEVRUTWOVSJWEVRVQGVCVBVDVGVTVEVFAFJVOVTAUADEVQVRGFKLMNAWJKDV + HPDHKVIVJAWMLEVHQEILVIVJRSTAWKUIVQVKAWNUIVRVKVLVMVN $. ${ $d H x $. $d G x $. $d C x $. @@ -64266,18 +64266,18 @@ the first case of his notation (simple exponentiation) and subscript it set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) $) mapsncnv $p |- `' F = ( y e. B |-> ( S X. { y } ) ) $= - ( cv cmap co wcel cfv wceq wa copab csn cxp ccnv cmpt wf elmapi ffvelrn - snid sylancl eqid mapsnconst jca eleq1 xpeq2d eqeq2d anbi12d syl5ibrcom - sneq imp fconst6g snex elmap sylibr fvconst2 eqcomd fveq1 impbii oveq2i - vex mp1i eleq2i anbi1i xpeq1i eqeq2i anbi2i 3bitr4i df-mpt eqtri cnveqi - opabbii cnvopab 3eqtr4i ) AKZCDLMZNZBKZFWAOZPZQZBARZWDCNZWADWDSZTZPZQZB - AREUAZBCWKUBWGWMBAWACFSZLMZNZWFQZWIWAWOWJTZPZQZWGWMWRXAWQWFXAWQXAWFWECN - ZWAWOWESZTZPZQWQXBXEWQWOCWAUCFWONZXBWACWOUDFIUFZWOCFWAUEUGCWOWAFWOUHHIU - IUJWFWIXBWTXEWDWECUKWFWSXDWAWFWJXCWOWDWEUPULUMUNUOUQWIWTWRWIWRWTWSWPNZW - DFWSOZPZQWIXHXJWIWOCWSUCXHWOWDCURCWOWSHFIUSUTVAWIXIWDXFXIWDPWIXGWOWDFBV - GVBVHVCUJWTWQXHWFXJWAWSWPUKWTWEXIWDFWAWSVDUMUNUOUQVEWCWQWFWBWPWADWOCLGV - FVIVJWLWTWIWKWSWADWOWJGVKVLVMVNVRWNWGABRZUAWHEXKEAWBWEUBXKJABWBWEVOVPVQ - WGABVSVPBACWKVOVT $. + ( cv cmap co wcel cfv wceq wa copab csn cxp ccnv cmpt wf elmapi sylancl + snid ffvelcdm eqid mapsnconst jca sneq xpeq2d eqeq2d anbi12d syl5ibrcom + eleq1 imp fconst6g snex elmap sylibr fvconst2 mp1i eqcomd impbii oveq2i + fveq1 eleq2i anbi1i xpeq1i eqeq2i anbi2i 3bitr4i opabbii df-mpt cnvopab + vex eqtri cnveqi 3eqtr4i ) AKZCDLMZNZBKZFWAOZPZQZBARZWDCNZWADWDSZTZPZQZ + BAREUAZBCWKUBWGWMBAWACFSZLMZNZWFQZWIWAWOWJTZPZQZWGWMWRXAWQWFXAWQXAWFWEC + NZWAWOWESZTZPZQWQXBXEWQWOCWAUCFWONZXBWACWOUDFIUFZWOCFWAUGUECWOWAFWOUHHI + UIUJWFWIXBWTXEWDWECUPWFWSXDWAWFWJXCWOWDWEUKULUMUNUOUQWIWTWRWIWRWTWSWPNZ + WDFWSOZPZQWIXHXJWIWOCWSUCXHWOWDCURCWOWSHFIUSUTVAWIXIWDXFXIWDPWIXGWOWDFB + VQVBVCVDUJWTWQXHWFXJWAWSWPUPWTWEXIWDFWAWSVGUMUNUOUQVEWCWQWFWBWPWADWOCLG + VFVHVIWLWTWIWKWSWADWOWJGVJVKVLVMVNWNWGABRZUAWHEXKEAWBWEUBXKJABWBWEVOVRV + SWGABVPVRBACWKVOVT $. $( Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) $) @@ -65320,13 +65320,13 @@ the first case of his notation (simple exponentiation) and subscript it $( A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.) $) 2dom $p |- ( 2o ~<_ A -> E. x e. A E. y e. A -. x = y ) $= - ( vf c2o cdom wbr c0 csn cpr cv wf1 wceq wn wrex cfv wcel ffvelrn sylancl - notbid wex df2o2 breq1i brdomi sylbi wf f1f 0ex prid1 p0ex prid2 0nep0 wb - neii f1fveq mpanr12 mtbiri eqeq1 eqeq2 rspc2ev syl3anc exlimiv syl ) ECFG - ZHHIZJZCDKZLZDUAZAKZBKZMZNZBCOACOZVDVFCFGVIEVFCFUBUCVFCDUDUEVHVNDVHHVGPZC - QZVEVGPZCQZVOVQMZNZVNVHVFCVGUFZHVFQZVPVFCVGUGZHVEUHUIZVFCHVGRSVHWAVEVFQZV - RWCHVEUJUKZVFCVEVGRSVHVSHVEMZHVEULUNVHWBWEVSWGUMWDWFVFCHVEVGUOUPUQVMVTVOV - KMZNABVOVQCCVJVOMVLWHVJVOVKURTVKVQMWHVSVKVQVOUSTUTVAVBVC $. + ( vf c2o cdom wbr c0 csn cpr cv wf1 wceq wn wrex cfv wcel ffvelcdm notbid + sylancl wex df2o2 breq1i brdomi sylbi f1f 0ex prid1 p0ex prid2 0nep0 neii + wf wb f1fveq mpanr12 mtbiri eqeq1 eqeq2 rspc2ev syl3anc exlimiv syl ) ECF + GZHHIZJZCDKZLZDUAZAKZBKZMZNZBCOACOZVDVFCFGVIEVFCFUBUCVFCDUDUEVHVNDVHHVGPZ + CQZVEVGPZCQZVOVQMZNZVNVHVFCVGUMZHVFQZVPVFCVGUFZHVEUGUHZVFCHVGRTVHWAVEVFQZ + VRWCHVEUIUJZVFCVEVGRTVHVSHVEMZHVEUKULVHWBWEVSWGUNWDWFVFCHVEVGUOUPUQVMVTVO + VKMZNABVOVQCCVJVOMVLWHVJVOVKURSVKVQMWHVSVKVQVOUSSUTVAVBVC $. $} ${ @@ -65487,7 +65487,7 @@ the first case of his notation (simple exponentiation) and subscript it $( A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.) $) enm $p |- ( ( A ~~ B /\ E. x x e. A ) -> E. y y e. B ) $= - ( vf cv wcel wex cen wbr wi wf1o bren wf f1of wa cfv ffvelrn syl exlimiv + ( vf cv wcel wex cen wbr wi wf1o bren wf f1of wa cfv ffvelcdm syl exlimiv elex2 ex sylbi com12 impcom ) AFZCGZAHCDIJZBFDGBHZUGUHUIKAUHUGUIUHCDEFZLZ EHUGUIKZCDEMUKULEUKCDUJNZULCDUJOUMUGUIUMUGPUFUJQZDGUICDUFUJRBUNDUASUBSTUC UDTUE $. @@ -65665,26 +65665,26 @@ the first case of his notation (simple exponentiation) and subscript it Mario Carneiro, 15-Nov-2014.) $) xpdom2 $p |- ( A ~<_ B -> ( C X. A ) ~<_ ( C X. B ) ) $= ( vf vz vw vv vu cdom cv wa cuni cop cvv wcel wi wceq wb vex vx vy brdomi - wbr wf1 cxp csn cdm crn cfv wf f1f ffvelrn ex anim2d adantld elxp4 opelxp - syl 3imtr4g adantl wrex elxp2 fvex opth f1fveq ancoms anbi2d ad2ant2l imp - syl5bb adantlr dmeqd unieqd op1sta eqtrdi op2nda fveq2d opeq12d eqeqan12d - sneq rneqd ad2antlr eqeq12 bitrdi 3bitr4d exp53 com23 rexlimivv rexlimdvv - syl2anb com12 reldom brrelex1i xpexg sylancr adantr brrelex2i exlimddv + wbr wf1 cxp csn cdm crn cfv wf f1f ffvelcdm ex syl anim2d adantld 3imtr4g + elxp4 opelxp adantl wrex elxp2 fvex f1fveq ancoms anbi2d ad2ant2l adantlr + opth syl5bb sneq dmeqd unieqd op1sta eqtrdi rneqd op2nda fveq2d eqeqan12d + imp opeq12d eqeq12 bitrdi 3bitr4d exp53 com23 rexlimivv rexlimdvv syl2anb + ad2antlr com12 reldom brrelex1i xpexg sylancr adantr brrelex2i exlimddv dom3d ) ABJUDZABEKZUEZCAUFZCBUFZJUDEABEUCXAXCLUAUBXDXEUAKZUGZUHZMZXGUIZMZ XBUJZNZUBKZUGZUHZMZXOUIZMZXBUJZNZOOXCXFXDPZXMXEPZQXAXCXFXIXKNRZXICPZXKAPZ - LZLYEXLBPZLZYBYCXCYGYIYDXCYFYHYEXCABXBUKZYFYHQABXBULYJYFYHABXKXBUMUNUSUOU - PXFCAUQXIXLCBURUTVAXCYBXNXDPZLZXMYARZXFXNRZSZQXAYLXCYOYBXFFKZGKZNZRZGAVBF + LZLYEXLBPZLZYBYCXCYGYIYDXCYFYHYEXCABXBUKZYFYHQABXBULYJYFYHABXKXBUMUNUOUPU + QXFCAUSXIXLCBUTURVAXCYBXNXDPZLZXMYARZXFXNRZSZQXAYLXCYOYBXFFKZGKZNZRZGAVBF CVBZXNHKZIKZNZRZIAVBHCVBZXCYOQZYKFGXFCAVCHIXNCAVCYTUUEUUFYTUUDUUFHICAYSUU ACPZUUBAPZLZUUDUUFQZQFGCAYPCPZYQAPZLZUUIYSUUJUUMUUIYSUUDXCYOUUMUUILZYSUUD LZLXCLYPYQXBUJZNZUUAUUBXBUJZNZRZYPUUARZYQUUBRZLZYMYNUUNXCUUTUVCSZUUOUUNXC UVDUULUUHXCUVDQUUKUUGUULUUHLZXCUVDUUTUVAUUPUURRZLUVEXCLZUVCYPUUPUUAUURFTZ - YQXBOOETGTZVDVEUVGUVFUVBUVAXCUVEUVFUVBSABYQUUBXBVFVGVHVKUNVIVJVLUUOYMUUTS - UUNXCYSUUDXMUUQYAUUSYSXIYPXLUUPYSXIYRUGZUHZMYPYSXHUVKYSXGUVJXFYRWAZVMVNYP - YQUVHUVIVOVPYSXKYQXBYSXKUVJUIZMYQYSXJUVMYSXGUVJUVLWBVNYPYQUVHUVIVQVPVRVSU - UDXQUUAXTUURUUDXQUUCUGZUHZMUUAUUDXPUVOUUDXOUVNXNUUCWAZVMVNUUAUUBHTZITZVOV - PUUDXSUUBXBUUDXSUVNUIZMUUBUUDXRUVSUUDXOUVNUVPWBVNUUAUUBUVQUVRVQVPVRVSVTWC - UUOYNUVCSUUNXCUUOYNYRUUCRUVCXFYRXNUUCWDYPYQUUAUUBUVHUVIVEWEWCWFWGWHWIWJVJ - WKWLVAXAXDOPZXCXACOPZAOPUVTDABJWMWNCAOOWOWPWQXAXEOPZXCXAUWABOPUWBDABJWMWR + YQXBOOETGTZVDVJUVGUVFUVBUVAXCUVEUVFUVBSABYQUUBXBVEVFVGVKUNVHWAVIUUOYMUUTS + UUNXCYSUUDXMUUQYAUUSYSXIYPXLUUPYSXIYRUGZUHZMYPYSXHUVKYSXGUVJXFYRVLZVMVNYP + YQUVHUVIVOVPYSXKYQXBYSXKUVJUIZMYQYSXJUVMYSXGUVJUVLVQVNYPYQUVHUVIVRVPVSWBU + UDXQUUAXTUURUUDXQUUCUGZUHZMUUAUUDXPUVOUUDXOUVNXNUUCVLZVMVNUUAUUBHTZITZVOV + PUUDXSUUBXBUUDXSUVNUIZMUUBUUDXRUVSUUDXOUVNUVPVQVNUUAUUBUVQUVRVRVPVSWBVTWK + UUOYNUVCSUUNXCUUOYNYRUUCRUVCXFYRXNUUCWCYPYQUUAUUBUVHUVIVJWDWKWEWFWGWHWIWA + WJWLVAXAXDOPZXCXACOPZAOPUVTDABJWMWNCAOOWOWPWQXAXEOPZXCXAUWABOPUWBDABJWMWR CBOOWOWPWQWTWS $. $} @@ -65965,30 +65965,30 @@ the first case of his notation (simple exponentiation) and subscript it Mario Carneiro, 16-Nov-2014.) $) xpmapenlem $p |- ( ( A X. B ) ^m C ) ~~ ( ( A ^m C ) X. ( B ^m C ) ) $= ( cmap cvv wcel cfv wceq cxp co cop wfn fnmap xpex fnovex mp3an cv c1st - wf wa elmap ffvelrn sylanb xp1st syl fmptd sylibr xp2nd opelxpi syl2anc - c2nd sylib ffvelrnda 1st2nd2 ad2antlr cmpt feqmptd simplr fveq1d 1stexg - ax-mp fvex 2ndexg opex fvmpt2 mpan2 adantl eqtrd fveq2d op1st mpteq2dva - vex eqtrdi eqtrid eqtr4d opeq12d simpll ad2antrr op1stg sylan9eq op2ndg - op2nd simpr impbida en3i ) ABDEUAZFPUBZDFPUBZEFPUBZUAZGHUCZIPQQUAUDZWRQ - RFQRZWSQRUEDEJKUFZLWRFQQPUGUHWTXAXDDQRXEWTQRUEJLDFQQPUGUHXDEQRXEXAQRUEK - LEFQQPUGUHUFAUIZWSRZGWTRZHXARZXCXBRXHFDGUKXIXHCFCUIZXGSZUJSZDGXHXKFRZUL - ZXLWRRZXMDRXHFWRXGUKZXNXPWRFXGXFLUMZFWRXKXGUNUOZXLDEUPUQMURDFGJLUMUSZXH - FEHUKXJXHCFXLVCSZEHXOXPYAERXSXLDEUTUQNUREFHKLUMUSZGHWTXAVAVBBUIZXBRZFWR - IUKIWSRYDCFXKYCUJSZSZXKYCVCSZSZUCZWRIYDXNULYFDRYHERYIWRRYDFDXKYEYDYEWTR - FDYEUKYCWTXAUPDFYEJLUMVDZVEYDFEXKYGYDYGXARFEYGUKYCWTXAUTEFYGKLUMVDZVEYF - YHDEVAVBOURWRFIXFLUMUSXHYDULZXGITZYCXCTZYLYMULZYCYEYGUCZXCYDYCYPTXHYMYC - WTXAVFVGYOYEGYGHYOYECFYFVHZGYDYEYQTXHYMYDCFDYEYJVIVGYOGCFXMVHYQMYOCFXMY - FYOXNULZXMYIUJSYFYRXLYIUJYRXLXKISZYIYRXKXGIYLYMXNVJVKXNYSYITZYOXNYIQRYT - YFYHXKYEQQYCQRZYEQRBWDZYCQVLVMCWDZVNZXKYGQQUUAYGQRUUBYCQVOVMUUCVNZVPCFY - IQIOVQVRVSVTZWAYFYHUUDUUEWBWEWCWFWGYOYGCFYHVHZHYDYGUUGTXHYMYDCFEYGYKVIV - GYOHCFYAVHUUGNYOCFYAYHYRYAYIVCSYHYRXLYIVCUUFWAYFYHUUDUUEWNWEWCWFWGWHVTY - LYNULZXGCFXLVHZIUUHCFWRXGUUHXHXQXHYDYNWIXRVDZVIUUHICFYIVHUUIOUUHCFYIXLU - UHXNULZYIXMYAUCZXLUUKYFXMYHYAUUHXNYFXKGSZXMUUHXKYEGUUHYEXCUJSZGUUHYCXCU - JYLYNWOZWAUUHXIXJUUNGTXHXIYDYNXTWJZXHXJYDYNYBWJZGHWTXAWKVBVTVKXNXMQRZUU - MXMTXLQRZUURXKXGQQAWDUUCVNZXLQVLVMCFXMQGMVQVRWLUUHXNYHXKHSZYAUUHXKYGHUU - HYGXCVCSZHUUHYCXCVCUUOWAUUHXIXJUVBHTUUPUUQGHWTXAWMVBVTVKXNYAQRZUVAYATUU - SUVCUUTXLQVOVMCFYAQHNVQVRWLWHUUKXPXLUULTUUHFWRXKXGUUJVEXLDEVFUQWGWCWFWG - WPWQ $. + wf wa elmap ffvelcdm sylanb xp1st syl fmptd sylibr c2nd opelxpi syl2anc + xp2nd sylib ffvelrnda 1st2nd2 ad2antlr feqmptd simplr fveq1d vex 1stexg + cmpt ax-mp fvex 2ndexg fvmpt2 mpan2 adantl eqtrd fveq2d op1st mpteq2dva + opex eqtrdi eqtrid eqtr4d op2nd opeq12d simpll ad2antrr op1stg sylan9eq + simpr op2ndg impbida en3i ) ABDEUAZFPUBZDFPUBZEFPUBZUAZGHUCZIPQQUAUDZWR + QRFQRZWSQRUEDEJKUFZLWRFQQPUGUHWTXAXDDQRXEWTQRUEJLDFQQPUGUHXDEQRXEXAQRUE + KLEFQQPUGUHUFAUIZWSRZGWTRZHXARZXCXBRXHFDGUKXIXHCFCUIZXGSZUJSZDGXHXKFRZU + LZXLWRRZXMDRXHFWRXGUKZXNXPWRFXGXFLUMZFWRXKXGUNUOZXLDEUPUQMURDFGJLUMUSZX + HFEHUKXJXHCFXLUTSZEHXOXPYAERXSXLDEVCUQNUREFHKLUMUSZGHWTXAVAVBBUIZXBRZFW + RIUKIWSRYDCFXKYCUJSZSZXKYCUTSZSZUCZWRIYDXNULYFDRYHERYIWRRYDFDXKYEYDYEWT + RFDYEUKYCWTXAUPDFYEJLUMVDZVEYDFEXKYGYDYGXARFEYGUKYCWTXAVCEFYGKLUMVDZVEY + FYHDEVAVBOURWRFIXFLUMUSXHYDULZXGITZYCXCTZYLYMULZYCYEYGUCZXCYDYCYPTXHYMY + CWTXAVFVGYOYEGYGHYOYECFYFVMZGYDYEYQTXHYMYDCFDYEYJVHVGYOGCFXMVMYQMYOCFXM + YFYOXNULZXMYIUJSYFYRXLYIUJYRXLXKISZYIYRXKXGIYLYMXNVIVJXNYSYITZYOXNYIQRY + TYFYHXKYEQQYCQRZYEQRBVKZYCQVLVNCVKZVOZXKYGQQUUAYGQRUUBYCQVPVNUUCVOZWDCF + YIQIOVQVRVSVTZWAYFYHUUDUUEWBWEWCWFWGYOYGCFYHVMZHYDYGUUGTXHYMYDCFEYGYKVH + VGYOHCFYAVMUUGNYOCFYAYHYRYAYIUTSYHYRXLYIUTUUFWAYFYHUUDUUEWHWEWCWFWGWIVT + YLYNULZXGCFXLVMZIUUHCFWRXGUUHXHXQXHYDYNWJXRVDZVHUUHICFYIVMUUIOUUHCFYIXL + UUHXNULZYIXMYAUCZXLUUKYFXMYHYAUUHXNYFXKGSZXMUUHXKYEGUUHYEXCUJSZGUUHYCXC + UJYLYNWNZWAUUHXIXJUUNGTXHXIYDYNXTWKZXHXJYDYNYBWKZGHWTXAWLVBVTVJXNXMQRZU + UMXMTXLQRZUURXKXGQQAVKUUCVOZXLQVLVNCFXMQGMVQVRWMUUHXNYHXKHSZYAUUHXKYGHU + UHYGXCUTSZHUUHYCXCUTUUOWAUUHXIXJUVBHTUUPUUQGHWTXAWOVBVTVJXNYAQRZUVAYATU + USUVCUUTXLQVPVNCFYAQHNVQVRWMWIUUKXPXLUULTUUHFWRXKXGUUJVEXLDEVFUQWGWCWFW + GWPWQ $. $} $( Equinumerosity law for set exponentiation of a Cartesian product. @@ -67365,51 +67365,51 @@ texts assume excluded middle (in which case the two intersection ( vz vw vf cv cin wcel wss c0 wa wi wal cen wbr wceq syl cvv eleq1d ensym vv wral wne cfn cint w3a com wrex isfi breq1 anbi2d imbi1d albidv weq en0 csuc sylib anim1i ancoms adantll wn pm3.24 pm2.21i sylan2b ax-gen a1i nfv - df-ne nfa1 simpl wf1o wex bren cima cfv ssel wf vex sucid ffvelrn sylancl - f1of impel adantr adantlll imaeq2 ima0 eqtrdi inteq int0 ssv sseqin2 mpbi - ineq1d biimprd adantl wfun f1ofun ad3antlr elelsuc wb f1odm eleq2d mpbird - cdm jca simpr funfvima sylc ne0i crn imassrn ccnv dff1o2 simp3bi sseqtrid - wfn sstr2 anim1d f1of1 sssucid f1imaen2g mpanr12 ensymd imaex sseq1 neeq1 - wf1 jctird anbi12d breq2 ineq1 ineq2 ex syl6 mpd csn cun com24 spcv com4r - imbi12d sylan9 exp5c com14 imp43 wo 0elnn ad3antrrr mpjaodan fvex intunsn - rspc2v f1ofn fnsnfv uneq2d df-suc imaeq2i imaundi eqtr2i wfo f1ofo inteqd - foima eqtrd eqtr3id ad2antlr mpbid exp43 exlimdv syl5bi sylani imp alrimd - expimpd finds2 sp exp4a syl5 rexlimiv sylbi com13 alrimiv cbvral2v df-3an - impd imbi1i albii 3imtr4i ) DGZEGZHZCIZECUCDCUCZAGZCJZUWPKUDZLZUWPUEIZLZU - WPUFZCIZMZANUWPBGZHZCIZBCUCACUCUWQUWRUWTUGZUXCMZANUWOUXDAUWOUWSUWTUXCUWTU - WSUWOUXCUWTUWPUXEOPZBUHUIUWSUWOUXCMZMZBUWPUJUXJUXLBUHUXJUXEUWPOPZUXEUHIZU - XLUWPUXEUAUXNUWOUWSUXMUXCUXNUWOUWSUXMUXCUXNUWOUWSUXMLZUXCMZANZUXPUXQUWSKU - WPOPZLZUXCMZANZUWSUBGZUWPOPZLZUXCMZANZUWSUYBUQZUWPOPZLZUXCMZANZUWOBUBUXEK - QZUXPUXTAUYLUXOUXSUXCUYLUXMUXRUWSUXEKUWPOUKULUMUNBUBUOZUXPUYEAUYMUXOUYDUX - CUYMUXMUYCUWSUXEUYBUWPOUKULUMUNUXEUYGQZUXPUYJAUYNUXOUYIUXCUYNUXMUYHUWSUXE - UYGUWPOUKULUMUNUYAUWOUXTAUXSUWPKQZUWRLZUXCUWRUXRUYPUWQUXRUWRUYPUXRUYOUWRU - XRUWPKOPUYOKUWPUAUWPUPURUSUTVAUWRUYOUYOVBZUXCUWPKVIUYOUYQLUXCUYOVCVDVERVF - VGUYBUHIZUWOUYFUYKMUYRUWOLZUYFUYJAUYSAVHUYEAVJUYRUWOUYFUYJMUYRUYIUYFUWOUX - CUWSUYRUWQUYHUYFUXKMZUWQUWRVKUYRUWQUYHUYTUYHUYGUWPFGZVLZFVMUYRUWQLZUYTUYG - UWPFVNVUCVUBUYTFVUCVUBUYFUWOUXCVUCVUBLUYFUWOLZLZVUAUYBVOZUFZUYBVUAVPZHZCI - ZUXCVUEVUHCIZVUJUWQVUBVUDVUKUYRUWQVUBLVUKVUDUWQVUHUWPIZVUKVUBUWPCVUHVQVUB - UYGUWPVUAVRUYBUYGIZVULUYGUWPVUAWCUYBUBVSZVTZUYGUWPUYBVUAWAWBWDWEWFVUEUYBK - QZVUKVUJMZKUYBIZVUPVUQVUEVUPVUFKQZVUQVUPVUFVUAKVOKUYBKVUAWGVUAWHWIVUSVUJV - UKVUSVUIVUHCVUSVUISVUHHZVUHVUSVUGSVUHVUSVUGKUFSVUFKWJWKWIWOVUHSJVUTVUHQVU - HWLVUHSWMWNWITWPRWQVUEVURLZVUFKUDZVUQVVAKVUAVPZVUFIZVVBVVAVUAWRZKVUAXFZIZ - LVURVVDVVAVVEVVGVUBVVEVUCVUDVURUYGUWPVUAWSWTVVAVVGKUYGIZVURVVHVUEKUYBXAWQ - VUBVVGVVHXBVUCVUDVURVUBVVFUYGKUYGUWPVUAXCXDWTXEXGVUEVURXHUYBKVUAXIXJVUFVV - CXKRVUEVVBVUQMZVURUWQVUBVUDVVIUYRUWQVUBUYFUWOVVIUWOVUBUYFUWQVVIUWOVUBUYFU - WQVVBVUQVUBUYFLZUWQVVBLZVUKUWOVUJVVJVVKVUGCIZVUKUWOVUJMZMVUBVVKVUFCJZVVBL - ZUYBVUFOPZLZUYFVVLVUBVVKVVOVVPVUBUWQVVNVVBVUBVUFUWPJUWQVVNMVUBVUAXLZVUFUW - PVUAUYBXMVUBVUAUYGXRZVUAXNWRVVRUWPQUYGUWPVUAXOXPXQVUFUWPCXSRXTVUBVUFUYBVU - BUYGUWPVUAYIZUWPSIZVUFUYBOPZUYGUWPVUAYAAVSVVTVWALUYBUYGJUYBSIVWBUYBYBVUNU - YGUWPUYBVUASYCYDWBYEYJUYEVVQVVLMAVUFVUAUYBFVSZYFUWPVUFQZUYDVVQUXCVVLVWDUW - SVVOUYCVVPVWDUWQVVNUWRVVBUWPVUFCYGUWPVUFKYHYKUWPVUFUYBOYLYKVWDUXBVUGCUWPV - UFWJTUUCUUAUUDVVLVUKVVMUWNVUJVUGUWLHZCIDEVUGVUHCCUWKVUGQUWMVWECUWKVUGUWLY - MTUWLVUHQVWEVUICUWLVUHVUGYNTUUNYOYPUUBUUEUUFUUGWFWEYQUYRVUPVURUUHUWQVUBVU - DUYBUUIUUJUUKYQVUBVUJUXCXBVUCVUDVUBVUIUXBCVUBVUIVUFVUHYRZYSZUFUXBVUFVUHUY - BVUASSVWCVUNUULUUMVUBVWGUWPVUBVWGVUAUYGVOZUWPVUBVWGVUFVUAUYBYRZVOZYSZVWHV - UBVWFVWJVUFVUBVVSVUMVWFVWJQUYGUWPVUAUUOVUOUYGUYBVUAUUPWBUUQVWHVUAUYBVWIYS - ZVOVWKUYGVWLVUAUYBUURUUSVUAUYBVWIUUTUVAWIVUBUYGUWPVUAUVBVWHUWPQUYGUWPVUAU - VCUYGUWPVUAUVERUVFUVDUVGTUVHUVIUVJUVKUVLUVPUVMYTUVNUVOYOUVQUXPAUVRYPUVSYT - UVTUWAUWBUWCUWGUWDUXGUWNUWKUXEHZCIABDECCADUOUXFVWMCUWPUWKUXEYMTBEUOVWMUWM - CUXEUWLUWKYNTUWEUXIUXDAUXHUXAUXCUWQUWRUWTUWFUWHUWIUWJ $. + df-ne nfa1 simpl wf1o wex bren cima cfv ssel wf f1of vex ffvelcdm sylancl + sucid impel adantr adantlll imaeq2 ima0 eqtrdi inteq int0 ineq1d ssv mpbi + sseqin2 biimprd adantl cdm f1ofun ad3antlr elelsuc wb f1odm eleq2d mpbird + wfun jca simpr funfvima sylc ne0i crn imassrn wfn dff1o2 simp3bi sseqtrid + ccnv sstr2 anim1d wf1 f1of1 sssucid f1imaen2g mpanr12 ensymd jctird imaex + sseq1 neeq1 anbi12d breq2 ineq1 ineq2 ex syl6 mpd csn cun com24 sylan9 wo + imbi12d spcv rspc2v com4r exp5c com14 imp43 0elnn ad3antrrr mpjaodan fvex + intunsn f1ofn fnsnfv uneq2d df-suc imaeq2i imaundi eqtr2i wfo f1ofo foima + eqtrd inteqd eqtr3id mpbid exp43 exlimdv syl5bi expimpd sylani imp alrimd + ad2antlr finds2 sp exp4a syl5 rexlimiv sylbi impd alrimiv cbvral2v df-3an + com13 imbi1i albii 3imtr4i ) DGZEGZHZCIZECUCDCUCZAGZCJZUWPKUDZLZUWPUEIZLZ + UWPUFZCIZMZANUWPBGZHZCIZBCUCACUCUWQUWRUWTUGZUXCMZANUWOUXDAUWOUWSUWTUXCUWT + UWSUWOUXCUWTUWPUXEOPZBUHUIUWSUWOUXCMZMZBUWPUJUXJUXLBUHUXJUXEUWPOPZUXEUHIZ + UXLUWPUXEUAUXNUWOUWSUXMUXCUXNUWOUWSUXMUXCUXNUWOUWSUXMLZUXCMZANZUXPUXQUWSK + UWPOPZLZUXCMZANZUWSUBGZUWPOPZLZUXCMZANZUWSUYBUQZUWPOPZLZUXCMZANZUWOBUBUXE + KQZUXPUXTAUYLUXOUXSUXCUYLUXMUXRUWSUXEKUWPOUKULUMUNBUBUOZUXPUYEAUYMUXOUYDU + XCUYMUXMUYCUWSUXEUYBUWPOUKULUMUNUXEUYGQZUXPUYJAUYNUXOUYIUXCUYNUXMUYHUWSUX + EUYGUWPOUKULUMUNUYAUWOUXTAUXSUWPKQZUWRLZUXCUWRUXRUYPUWQUXRUWRUYPUXRUYOUWR + UXRUWPKOPUYOKUWPUAUWPUPURUSUTVAUWRUYOUYOVBZUXCUWPKVIUYOUYQLUXCUYOVCVDVERV + FVGUYBUHIZUWOUYFUYKMUYRUWOLZUYFUYJAUYSAVHUYEAVJUYRUWOUYFUYJMUYRUYIUYFUWOU + XCUWSUYRUWQUYHUYFUXKMZUWQUWRVKUYRUWQUYHUYTUYHUYGUWPFGZVLZFVMUYRUWQLZUYTUY + GUWPFVNVUCVUBUYTFVUCVUBUYFUWOUXCVUCVUBLUYFUWOLZLZVUAUYBVOZUFZUYBVUAVPZHZC + IZUXCVUEVUHCIZVUJUWQVUBVUDVUKUYRUWQVUBLVUKVUDUWQVUHUWPIZVUKVUBUWPCVUHVQVU + BUYGUWPVUAVRUYBUYGIZVULUYGUWPVUAVSUYBUBVTZWCZUYGUWPUYBVUAWAWBWDWEWFVUEUYB + KQZVUKVUJMZKUYBIZVUPVUQVUEVUPVUFKQZVUQVUPVUFVUAKVOKUYBKVUAWGVUAWHWIVUSVUJ + VUKVUSVUIVUHCVUSVUISVUHHZVUHVUSVUGSVUHVUSVUGKUFSVUFKWJWKWIWLVUHSJVUTVUHQV + UHWMVUHSWOWNWITWPRWQVUEVURLZVUFKUDZVUQVVAKVUAVPZVUFIZVVBVVAVUAXFZKVUAWRZI + ZLVURVVDVVAVVEVVGVUBVVEVUCVUDVURUYGUWPVUAWSWTVVAVVGKUYGIZVURVVHVUEKUYBXAW + QVUBVVGVVHXBVUCVUDVURVUBVVFUYGKUYGUWPVUAXCXDWTXEXGVUEVURXHUYBKVUAXIXJVUFV + VCXKRVUEVVBVUQMZVURUWQVUBVUDVVIUYRUWQVUBUYFUWOVVIUWOVUBUYFUWQVVIUWOVUBUYF + UWQVVBVUQVUBUYFLZUWQVVBLZVUKUWOVUJVVJVVKVUGCIZVUKUWOVUJMZMVUBVVKVUFCJZVVB + LZUYBVUFOPZLZUYFVVLVUBVVKVVOVVPVUBUWQVVNVVBVUBVUFUWPJUWQVVNMVUBVUAXLZVUFU + WPVUAUYBXMVUBVUAUYGXNZVUAXRXFVVRUWPQUYGUWPVUAXOXPXQVUFUWPCXSRXTVUBVUFUYBV + UBUYGUWPVUAYAZUWPSIZVUFUYBOPZUYGUWPVUAYBAVTVVTVWALUYBUYGJUYBSIVWBUYBYCVUN + UYGUWPUYBVUASYDYEWBYFYGUYEVVQVVLMAVUFVUAUYBFVTZYHUWPVUFQZUYDVVQUXCVVLVWDU + WSVVOUYCVVPVWDUWQVVNUWRVVBUWPVUFCYIUWPVUFKYJYKUWPVUFUYBOYLYKVWDUXBVUGCUWP + VUFWJTUUCUUDUUAVVLVUKVVMUWNVUJVUGUWLHZCIDEVUGVUHCCUWKVUGQUWMVWECUWKVUGUWL + YMTUWLVUHQVWEVUICUWLVUHVUGYNTUUEYOYPUUFUUGUUHUUIWFWEYQUYRVUPVURUUBUWQVUBV + UDUYBUUJUUKUULYQVUBVUJUXCXBVUCVUDVUBVUIUXBCVUBVUIVUFVUHYRZYSZUFUXBVUFVUHU + YBVUASSVWCVUNUUMUUNVUBVWGUWPVUBVWGVUAUYGVOZUWPVUBVWGVUFVUAUYBYRZVOZYSZVWH + VUBVWFVWJVUFVUBVVSVUMVWFVWJQUYGUWPVUAUUOVUOUYGUYBVUAUUPWBUUQVWHVUAUYBVWIY + SZVOVWKUYGVWLVUAUYBUURUUSVUAUYBVWIUUTUVAWIVUBUYGUWPVUAUVBVWHUWPQUYGUWPVUA + UVCUYGUWPVUAUVDRUVEUVFUVGTUVPUVHUVIUVJUVKUVLUVMYTUVNUVOYOUVQUXPAUVRYPUVSY + TUVTUWAUWBUWGUWCUWDUXGUWNUWKUXEHZCIABDECCADUOUXFVWMCUWPUWKUXEYMTBEUOVWMUW + MCUXEUWLUWKYNTUWEUXIUXDAUXHUXAUXCUWQUWRUWTUWFUWHUWIUWJ $. $} ${ @@ -68470,16 +68470,16 @@ all reals (greatest real number) for which all positive reals are greater. A. x e. B A. y e. B ( x = y <-> ( -. x S y /\ -. y S x ) ) -> A. u e. A A. v e. A ( u = v <-> ( -. u R v /\ -. v R u ) ) ) ) $= ( cv wceq wbr wn wa wb wral wcel notbid anbi12d bibi12d wiso wi wf isof1o - cfv wf1o f1of ffvelrn anim12d 3syl imp eqeq1 breq1 breq2 eqeq2 rspc2v syl - ex wf1 f1of1 f1fveq sylan bicomd isorel ancom2s sylibrd ralrimdvva ) EFGH - IUAZAJZBJZKZVIVJHLZMZVJVIHLZMZNZOZBFPAFPZDJZCJZKZVSVTGLZMZVTVSGLZMZNZOZDC - EEVHVSEQZVTEQZNZNZVRVSIUEZVTIUEZKZWLWMHLZMZWMWLHLZMZNZOZWGWKWLFQZWMFQZNZV - RWTUBVHWJXCVHEFIUFZEFIUCZWJXCUBEFGHIUDZEFIUGXEWHXAWIXBXEWHXAEFVSIUHURXEWI - XBEFVTIUHURUIUJUKVQWTWLVJKZWLVJHLZMZVJWLHLZMZNZOABWLWMFFVIWLKZVKXGVPXLVIW - LVJULXMVMXIVOXKXMVLXHVIWLVJHUMRXMVNXJVIWLVJHUNRSTVJWMKZXGWNXLWSVJWMWLUOXN - XIWPXKWRXNXHWOVJWMWLHUNRXNXJWQVJWMWLHUMRSTUPUQWKWAWNWFWSWKWNWAVHEFIUSZWJW - NWAOVHXDXOXFEFIUTUQEFVSVTIVAVBVCWKWCWPWEWRWKWBWOEFVSVTGHIVDRVHWIWHWEWROVH - WIWHNNWDWQEFVTVSGHIVDRVESTVFVG $. + cfv wf1o f1of ffvelcdm ex anim12d 3syl imp eqeq1 breq1 breq2 eqeq2 rspc2v + syl wf1 f1of1 f1fveq sylan bicomd isorel ancom2s sylibrd ralrimdvva ) EFG + HIUAZAJZBJZKZVIVJHLZMZVJVIHLZMZNZOZBFPAFPZDJZCJZKZVSVTGLZMZVTVSGLZMZNZOZD + CEEVHVSEQZVTEQZNZNZVRVSIUEZVTIUEZKZWLWMHLZMZWMWLHLZMZNZOZWGWKWLFQZWMFQZNZ + VRWTUBVHWJXCVHEFIUFZEFIUCZWJXCUBEFGHIUDZEFIUGXEWHXAWIXBXEWHXAEFVSIUHUIXEW + IXBEFVTIUHUIUJUKULVQWTWLVJKZWLVJHLZMZVJWLHLZMZNZOABWLWMFFVIWLKZVKXGVPXLVI + WLVJUMXMVMXIVOXKXMVLXHVIWLVJHUNRXMVNXJVIWLVJHUORSTVJWMKZXGWNXLWSVJWMWLUPX + NXIWPXKWRXNXHWOVJWMWLHUORXNXJWQVJWMWLHUNRSTUQURWKWAWNWFWSWKWNWAVHEFIUSZWJ + WNWAOVHXDXOXFEFIUTUREFVSVTIVAVBVCWKWCWPWEWRWKWBWOEFVSVTGHIVDRVHWIWHWEWROV + HWIWHNNWDWQEFVTVSGHIVDRVESTVFVG $. $} ${ @@ -69305,13 +69305,13 @@ readily usable (e.g., by ~ djudom and ~ djufun ) while the simpler corresponding function is a function. (Contributed by AV, 26-Jun-2022.) $) updjudhf $p |- ( ph -> H : ( A |_| B ) --> C ) $= - ( cfv c0 wceq wcel ex wf wi syl c1o cdju cv c1st c2nd eldju2ndl ffvelrn - cif wa sylan9r imp wn wne df-ne eldju2ndr syl5bir wo wdc eldju1st neeq1 - 1n0 mpbiri orim2i adantl dcne sylibr ifcldadc fmptd ) ABCDUAZBUBZUCLZMN - ZVIUDLZFLZVLGLZUGEHAVIVHOZUHZVKVMVNEVPVKVMEOZVOVKVLCOZAVQVOVKVRCDVIUEPA - CEFQZVRVQRIVSVRVQCEVLFUFPSUIUJVPVKUKZVNEOZVTVJMULZVPWAVJMUMVOWBVLDOZAWA - VOWBWCCDVIUNPADEGQZWCWARJWDWCWADEVLGUFPSUIUOUJVPVKWBUPZVKUQVOWEAVOVKVJT - NZUPWECDVIURWFWBVKWFWBTMULUTVJTMUSVAVBSVCVJMVDVEVFKVG $. + ( cfv c0 wceq wcel ex wf wi syl c1o cdju cv c1st cif eldju2ndl ffvelcdm + wa sylan9r imp wn wne df-ne eldju2ndr syl5bir wo wdc eldju1st 1n0 neeq1 + c2nd mpbiri orim2i adantl dcne sylibr ifcldadc fmptd ) ABCDUAZBUBZUCLZM + NZVIUTLZFLZVLGLZUDEHAVIVHOZUGZVKVMVNEVPVKVMEOZVOVKVLCOZAVQVOVKVRCDVIUEP + ACEFQZVRVQRIVSVRVQCEVLFUFPSUHUIVPVKUJZVNEOZVTVJMUKZVPWAVJMULVOWBVLDOZAW + AVOWBWCCDVIUMPADEGQZWCWARJWDWCWADEVLGUFPSUHUNUIVPVKWBUOZVKUPVOWEAVOVKVJ + TNZUOWECDVIUQWFWBVKWFWBTMUKURVJTMUSVAVBSVCVJMVDVEVFKVG $. $d A a x $. $d F a x $. $d H a $. $d ph a $. $( The composition of the mapping of an element of the disjoint union to @@ -70544,13 +70544,13 @@ elements or fails to hold (is equal to ` (/) ` ) for some element. 29-Jun-2022.) $) exmidomniim $p |- ( EXMID -> A. x x e. Omni ) $= ( vf vy wem cv wcel c2o c0 wceq c1o wo wi wa wn wdc exmidexmid syl adantr - wral wb comni wf cfv wrex wal exmiddc orcomd ffvelrn df2o3 eleqtrdi elpri - cpr ord ralimdva adantl dfrex2dc sylibrd orim1d mpd ex alrimiv cvv isomni - con3d elv sylibr ) DAEZUAFZADVGGBEZUBZCEZVIUCZHIZCVGUDZVLJIZCVGSZKZLZBUEZ - VHDVRBDVJVQDVJMZVPNZVPKZVQDWBVJDVPWADVPOVPWAKVPPVPUFQUGRVTWAVNVPVTWAVMNZC - VGSZNZVNVJWAWELDVJWDVPVJWCVOCVGVJVKVGFMZVMVOWFVLHJULZFVMVOKWFVLGWGVGGVKVI - UHUIUJVLHJUKQUMUNVDUODVNWETZVJDVNOWHVNPVMCVGUPQRUQURUSUTVAVHVSTACVGBVBVCV - EVFVA $. + wral wb comni wf cfv wal exmiddc orcomd cpr ffvelcdm df2o3 eleqtrdi elpri + wrex ord ralimdva con3d adantl dfrex2dc sylibrd orim1d mpd ex alrimiv cvv + isomni elv sylibr ) DAEZUAFZADVGGBEZUBZCEZVIUCZHIZCVGULZVLJIZCVGSZKZLZBUD + ZVHDVRBDVJVQDVJMZVPNZVPKZVQDWBVJDVPWADVPOVPWAKVPPVPUEQUFRVTWAVNVPVTWAVMNZ + CVGSZNZVNVJWAWELDVJWDVPVJWCVOCVGVJVKVGFMZVMVOWFVLHJUGZFVMVOKWFVLGWGVGGVKV + IUHUIUJVLHJUKQUMUNUOUPDVNWETZVJDVNOWHVNPVMCVGUQQRURUSUTVAVBVHVSTACVGBVCVD + VEVFVB $. $} ${ @@ -113161,11 +113161,11 @@ a function (ordinarily on a subset of ` CC ` ) and produces a new shftf $p |- ( ( F : B --> C /\ A e. CC ) -> ( F shift A ) : { x e. CC | ( x - A ) e. B } --> C ) $= ( vy wf cc wcel wa co cv cmin wfn cfv wceq simpr simpl syl2an cshi shftfn - crab wral ffn sylan oveq1 elrab shftval ffvelrn eqeltrd sylan2b ralrimiva - eleq1d ffnfv sylanbrc ) CDEHZBIJZKZEBUALZAMZBNLZCJZAIUCZOZGMZUTPZDJZGVDUD - VDDUTHUQECOURVECDEUEABCEFUBUFUSVHGVDVFVDJUSVFIJZVFBNLZCJZKZVHVCVKAVFIVAVF - QVBVJCVAVFBNUGUNUHUSVLKVGVJEPZDUSURVIVGVMQVLUQURRVIVKSBVFEFUITUSUQVKVMDJV - LUQURSVIVKRCDVJEUJTUKULUMGVDDUTUOUP $. + crab wral ffn sylan oveq1 eleq1d elrab shftval ffvelcdm eqeltrd ralrimiva + sylan2b ffnfv sylanbrc ) CDEHZBIJZKZEBUALZAMZBNLZCJZAIUCZOZGMZUTPZDJZGVDU + DVDDUTHUQECOURVECDEUEABCEFUBUFUSVHGVDVFVDJUSVFIJZVFBNLZCJZKZVHVCVKAVFIVAV + FQVBVJCVAVFBNUGUHUIUSVLKVGVJEPZDUSURVIVGVMQVLUQURRVIVKSBVFEFUJTUSUQVKVMDJ + VLUQURSVIVKRCDVJEUKTULUNUMGVDDUTUOUP $. $( Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) $) @@ -120248,60 +120248,60 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) nfif eqeltrrd weq breq1 fveq2 csbeq1d fvmptg eqtrd wi cmpt eluzfz2 ccnv eleqtrdi sselda f1ocnvfv2 f1ocnv fzssuz a1i leisorel syl122anc eqbrtrrd eluz elfzuzb ssrdv fsum3cvg addid2 addid1 addcl eleqtrrd iftrue iffalse - ex simpll ssneld eluzdc fmptd ffvelrn syl2an elnnuz biimpri 3jca eluzle - w3a elfz2 wral eleq2d sselid ralrimiva rspc zdcle ifcldadc cdif fveqeq2 - eldifi elfzelz eldifn fvmpt2 vtoclga simpl nfim anbi2d imbi12d vtoclg1f - csbeq1 cbvmpt elfznn 3eqtr4rd seq3coll eqcomd f1oeq2 summodclem3 fveq2d - eqtri 3eqtr2d breqtrd ) AUEGKUFZLJUGZUXFUGZLUEHUHUFZUGZUIABCEGKUXGMNOAB - KUJUGZUXGTAUHLUKULZBLJAUXLBJUMZUXLBJUNZAUXLBUOUOJUPZUXMAUHBUQUGZUKULZBU - OUOJUPZUXOUBAUXQUXLURUXRUXOUSAUXPLUHUKAUXLUQUGZUXPLAUXLBDUTZAUHLAVAALRV - BZVCUAVDALVEVFZLVGVFUXSLURRLVLLVHVIVJZVKZUXQBUXLUOUOJVMVNVOZUXLBUOUOJVP - VNZUXLBJVQVNZALUHUJUGZVFLUXLVFZALVEUYHRWDUUCUHLUUAVNZVRVSZAFBKUXGUKULZA - FUTZBVFZUYMUYLVFZAUYNVTZUYMUXKVFZUXGUYMUJUGVFZUYOABUXKUYMTUUDZUYPUYRUYM - UXGWAWBZUYPUYMJUUBZUGZJUGZUYMUXGWAAUXMUYNVUCUYMURUYFUXLBUYMJUUEWEUYPVUB - LWAWBZVUCUXGWAWBZUYPVUBUXLVFZVUDABUXLUYMVUAAUXMBUXLVUAUMBUXLVUAUNUYFUXL - BJUUFBUXLVUAVQVIWCZVUBUHLWFVNUYPUXOUXLWGWHZBWGWHVUFUYIVUDVUEUSAUXOUYNUY - EWIVUHUYPUXLWJWGUXLUYHWJUHLUUGUYHWKWJUHWLWMWNWNWOWNUUHUYPBWJWGUYPBUXKWJ - ABUXKWHZUYNTWIUXKWKWJKWLZWMWNWPWOWPVUGAUYIUYNUYJWIUXLBVUBLJUUIUUJVOUUKU - YPUYMWKVFZUXGWKVFZUYRUYTUSUYPUYQVUKUYSKUYMWQVNAVULUYNAUXGUXKVFVULUYKKUX - GWQVNWIUYMUXGUULWRWSUYMKUXGUUMWTUVBUUNUUOAUXHLUEIUHUFUGUXPUXIUGUXJABUEX - HUCUDGJIKLXAUCUTZXHVFZXAVUMUEULVUMURAVUMUUPXBVUNVUMXAUEULVUMURAVUMUUQXB - VUNUDUTZXHVFVTVUMVUOUEULXHVFAVUMVUOUURXBAXCUBALUXLUXQUYJUYDUUSTAWKXHGUN - VUMWKVFZVUMGUGZXHVFVUMUXKVFAEWKEUTZBVFZCXAXDZXHGAVURWKVFZVTZVURUXKVFZVU - TXHVFZVVCXIZVVBVVCVTZVUSVVDVUSXIZVVBVUSVVDVVCAVUSVVDVVAAVUSVTVUTCXHVUSV - UTCURAVUSCXAUUTXBNXEXFXFVVGVVDVVFVVGVUTXAXHVUSCXAUVAZXGXJZXBVVFVUSXKZVU - SVVGXLAVVCVVJVVAOXFVUSXMVNXNVVBVVEVTZVVGVVDVVKAVVEVVGAVVAVVEUVCVVBVVEXO - ABUXKVURTUVDXPVVIVNVVBVVCXKZVVCVVEXLAKWKVFVVAVVLSKVURUVEWEVVCXMVNXNZMUV - FKVUMWQWKXHVUMGUVGUVHAVUMUYHVFZVTZVUMIUGZVUMLWAWBZEVUMJUGZCXQZXAXDZXHVV - OVUMVEVFZVVTXHVFVVPVVTURVVNVWAAVWAVVNVUMUVIUVJXBZVVOVVQVVSXAXHVVOVVQVTZ - VVRBVFZVVSXAXDZVVSXHVWCVWDVVSXAVWCUXQBVUMJAUXQBJUNZVVNVVQAUXRUXQBJUMVWF - UBUXQBUOUOJVPUXQBJVQVIZXRVWCUHWKVFZUXPWKVFZVUPUVMUHVUMWAWBZVUMUXPWAWBZV - TVUMUXQVFZVWCVWHVWIVUPVWCVAAVWIVVNVVQAUXPLWKUYCUYAXEXRVVNVUPAVVQUHVUMWQ - XSUVKVWCVWJVWKVVNVWJAVVQUHVUMUVLXSVWCVWKVVQVVOVVQXOAVWKVVQUSVVNVVQAUXPL - VUMWAUYCXTXRWSYAVUMUHUXPUVNWTZVRYBVWCVVRWKVFVVDEWKUVOZVWEXHVFZVWCUXKWKV - VRVUJVWCBUXKVVRAVUIVVNVVQTXRVWCUXLBVUMJAUXNVVNVVQUYGXRVWCVWLVUMUXLVFZVW - MAVWLVWPUSVVNVVQAUXQUXLVUMUYDUVPXRVOVRVSUVQAVWNVVNVVQAVVDEWKVVMUVRXRVVD - VWOEVVRWKEVWEXHVWDEVVSXAVWDEYCEVVRCYDEXAYEZYKYFVURVVRURZVUTVWEXHVWRVUSV - WDCVVSXAVURVVRBYGEVVRCYHYIYJUVSXPYLVVOVVQXIVTXCVVOVUPLWKVFZVVQXKVVOVUMV - WBVBAVWSVVNUYAWIVUMLUVTWRUWAZFVUMUYMLWAWBZEUYMJUGZCXQZXAXDZVVTVEXHIFUCY - MZVXAVVQVXCVVSXAUYMVUMLWAYNVXEEVXBVVRCUYMVUMJYOYPYIQYQWRVWTXEVUMKUXPJUG - ZUKULZBUWBZVFVUQXAURZAVURGUGZXAURVXIEVUMVXHVURVUMXAGUWCVURVXHVFZVXJVUTX - AVXKVVAVVDVXJVUTURVXKVURVXGVFVVAVURVXGBUWDVURKVXFUWEVNVXKVUTXAXHVXKVVGV - UTXAURVURVXGBUWFVVHVNZXGXJEWKVUTXHGMUWGWRVXLYRUWHXBAVUOUXQVFZVTZVUOJUGZ - BVFZEVXOCXQZXAXDZVXQVXOGUGZVUOIUGZVXNVXPVXQXAAUXQBVUOJVWGWCZYBZVXNVXOWK - VFZVXRXHVFZVXSVXRURVXNVXOUXKVFVYCVXNBUXKVXOAVUIVXMTWIVYAVSKVXOWQVNZVXNV - XPAVYCVTZVYDVYAVXNAVYCAVXMUWIVYEYAVVBVVDYSVYFVYDYSEVXOBVYFVYDEVYFEYCEVX - RXHVXPEVXQXAVXPEYCEVXOCYDVWQYKYFUWJVURVXOURZVVBVYFVVDVYDVYGVVAVYCAVURVX - OWKYGUWKVYGVUTVXRXHVYGVUSVXPCVXQXAVURVXOBYGEVXOCYHYIYJUWLVVMUWMXPZFVXOU - YNEUYMCXQZXAXDZVXRWKXHGUYMVXOURUYNVXPVYIVXQXAUYMVXOBYGEUYMVXOCUWNYIGEWK - VUTYTFWKVYJYTMEFWKVUTVYJFVUTYEUYNEVYIXAUYNEYCEUYMCYDVWQYKEFYMVUSUYNCVYI - XAVURUYMBYGEUYMCYHYIUWOUXCYQWRVXNVXTVUOLWAWBZVXQXAXDZVXQVXNVUOVEVFZVYLX - HVFVXTVYLURVXMVYMAVUOUXPUWPXBVXNVYLVXQXHVXNVYKVXQXAVXNVUOUXPWAWBZVYKVXM - VYNAVUOUHUXPWFXBAVYNVYKUSVXMAUXPLVUOWAUYCXTWIVOYBZVXNVXRVXQXHVYBVYHYLXE - FVUOVXDVYLVEXHIFUDYMZVXAVYKVXCVXQXAUYMVUOLWAYNVYPEVXBVXOCUYMVUOJYOYPYIQ - YQWRVYOYRUWQUWRABCDEFGHIJUXPLMNAUXPVEVFUYBAUXPLVEUYCRXERYAAUXLBUXTUMZUX - QBUXTUMZUAAUXLUXQURVYQVYRUSAUXQUXLUYDUWSUXLUXQBUXTUWTVNVOUYFPQUXAAUXPLU - XIUYCUXBUXDUXE $. + ex simpll ssneld eluzdc fmptd ffvelcdm syl2an elnnuz biimpri w3a eluzle + 3jca elfz2 wral eleq2d sselid ralrimiva rspc zdcle ifcldadc cdif eldifi + fveqeq2 elfzelz eldifn fvmpt2 vtoclga simpl nfim anbi2d vtoclg1f csbeq1 + imbi12d cbvmpt eqtri elfznn 3eqtr4rd seq3coll eqcomd f1oeq2 summodclem3 + fveq2d 3eqtr2d breqtrd ) AUEGKUFZLJUGZUXFUGZLUEHUHUFZUGZUIABCEGKUXGMNOA + BKUJUGZUXGTAUHLUKULZBLJAUXLBJUMZUXLBJUNZAUXLBUOUOJUPZUXMAUHBUQUGZUKULZB + UOUOJUPZUXOUBAUXQUXLURUXRUXOUSAUXPLUHUKAUXLUQUGZUXPLAUXLBDUTZAUHLAVAALR + VBZVCUAVDALVEVFZLVGVFUXSLURRLVLLVHVIVJZVKZUXQBUXLUOUOJVMVNVOZUXLBUOUOJV + PVNZUXLBJVQVNZALUHUJUGZVFLUXLVFZALVEUYHRWDUUCUHLUUAVNZVRVSZAFBKUXGUKULZ + AFUTZBVFZUYMUYLVFZAUYNVTZUYMUXKVFZUXGUYMUJUGVFZUYOABUXKUYMTUUDZUYPUYRUY + MUXGWAWBZUYPUYMJUUBZUGZJUGZUYMUXGWAAUXMUYNVUCUYMURUYFUXLBUYMJUUEWEUYPVU + BLWAWBZVUCUXGWAWBZUYPVUBUXLVFZVUDABUXLUYMVUAAUXMBUXLVUAUMBUXLVUAUNUYFUX + LBJUUFBUXLVUAVQVIWCZVUBUHLWFVNUYPUXOUXLWGWHZBWGWHVUFUYIVUDVUEUSAUXOUYNU + YEWIVUHUYPUXLWJWGUXLUYHWJUHLUUGUYHWKWJUHWLWMWNWNWOWNUUHUYPBWJWGUYPBUXKW + JABUXKWHZUYNTWIUXKWKWJKWLZWMWNWPWOWPVUGAUYIUYNUYJWIUXLBVUBLJUUIUUJVOUUK + UYPUYMWKVFZUXGWKVFZUYRUYTUSUYPUYQVUKUYSKUYMWQVNAVULUYNAUXGUXKVFVULUYKKU + XGWQVNWIUYMUXGUULWRWSUYMKUXGUUMWTUVBUUNUUOAUXHLUEIUHUFUGUXPUXIUGUXJABUE + XHUCUDGJIKLXAUCUTZXHVFZXAVUMUEULVUMURAVUMUUPXBVUNVUMXAUEULVUMURAVUMUUQX + BVUNUDUTZXHVFVTVUMVUOUEULXHVFAVUMVUOUURXBAXCUBALUXLUXQUYJUYDUUSTAWKXHGU + NVUMWKVFZVUMGUGZXHVFVUMUXKVFAEWKEUTZBVFZCXAXDZXHGAVURWKVFZVTZVURUXKVFZV + UTXHVFZVVCXIZVVBVVCVTZVUSVVDVUSXIZVVBVUSVVDVVCAVUSVVDVVAAVUSVTVUTCXHVUS + VUTCURAVUSCXAUUTXBNXEXFXFVVGVVDVVFVVGVUTXAXHVUSCXAUVAZXGXJZXBVVFVUSXKZV + USVVGXLAVVCVVJVVAOXFVUSXMVNXNVVBVVEVTZVVGVVDVVKAVVEVVGAVVAVVEUVCVVBVVEX + OABUXKVURTUVDXPVVIVNVVBVVCXKZVVCVVEXLAKWKVFVVAVVLSKVURUVEWEVVCXMVNXNZMU + VFKVUMWQWKXHVUMGUVGUVHAVUMUYHVFZVTZVUMIUGZVUMLWAWBZEVUMJUGZCXQZXAXDZXHV + VOVUMVEVFZVVTXHVFVVPVVTURVVNVWAAVWAVVNVUMUVIUVJXBZVVOVVQVVSXAXHVVOVVQVT + ZVVRBVFZVVSXAXDZVVSXHVWCVWDVVSXAVWCUXQBVUMJAUXQBJUNZVVNVVQAUXRUXQBJUMVW + FUBUXQBUOUOJVPUXQBJVQVIZXRVWCUHWKVFZUXPWKVFZVUPUVKUHVUMWAWBZVUMUXPWAWBZ + VTVUMUXQVFZVWCVWHVWIVUPVWCVAAVWIVVNVVQAUXPLWKUYCUYAXEXRVVNVUPAVVQUHVUMW + QXSUVMVWCVWJVWKVVNVWJAVVQUHVUMUVLXSVWCVWKVVQVVOVVQXOAVWKVVQUSVVNVVQAUXP + LVUMWAUYCXTXRWSYAVUMUHUXPUVNWTZVRYBVWCVVRWKVFVVDEWKUVOZVWEXHVFZVWCUXKWK + VVRVUJVWCBUXKVVRAVUIVVNVVQTXRVWCUXLBVUMJAUXNVVNVVQUYGXRVWCVWLVUMUXLVFZV + WMAVWLVWPUSVVNVVQAUXQUXLVUMUYDUVPXRVOVRVSUVQAVWNVVNVVQAVVDEWKVVMUVRXRVV + DVWOEVVRWKEVWEXHVWDEVVSXAVWDEYCEVVRCYDEXAYEZYKYFVURVVRURZVUTVWEXHVWRVUS + VWDCVVSXAVURVVRBYGEVVRCYHYIYJUVSXPYLVVOVVQXIVTXCVVOVUPLWKVFZVVQXKVVOVUM + VWBVBAVWSVVNUYAWIVUMLUVTWRUWAZFVUMUYMLWAWBZEUYMJUGZCXQZXAXDZVVTVEXHIFUC + YMZVXAVVQVXCVVSXAUYMVUMLWAYNVXEEVXBVVRCUYMVUMJYOYPYIQYQWRVWTXEVUMKUXPJU + GZUKULZBUWBZVFVUQXAURZAVURGUGZXAURVXIEVUMVXHVURVUMXAGUWDVURVXHVFZVXJVUT + XAVXKVVAVVDVXJVUTURVXKVURVXGVFVVAVURVXGBUWCVURKVXFUWEVNVXKVUTXAXHVXKVVG + VUTXAURVURVXGBUWFVVHVNZXGXJEWKVUTXHGMUWGWRVXLYRUWHXBAVUOUXQVFZVTZVUOJUG + ZBVFZEVXOCXQZXAXDZVXQVXOGUGZVUOIUGZVXNVXPVXQXAAUXQBVUOJVWGWCZYBZVXNVXOW + KVFZVXRXHVFZVXSVXRURVXNVXOUXKVFVYCVXNBUXKVXOAVUIVXMTWIVYAVSKVXOWQVNZVXN + VXPAVYCVTZVYDVYAVXNAVYCAVXMUWIVYEYAVVBVVDYSVYFVYDYSEVXOBVYFVYDEVYFEYCEV + XRXHVXPEVXQXAVXPEYCEVXOCYDVWQYKYFUWJVURVXOURZVVBVYFVVDVYDVYGVVAVYCAVURV + XOWKYGUWKVYGVUTVXRXHVYGVUSVXPCVXQXAVURVXOBYGEVXOCYHYIYJUWNVVMUWLXPZFVXO + UYNEUYMCXQZXAXDZVXRWKXHGUYMVXOURUYNVXPVYIVXQXAUYMVXOBYGEUYMVXOCUWMYIGEW + KVUTYTFWKVYJYTMEFWKVUTVYJFVUTYEUYNEVYIXAUYNEYCEUYMCYDVWQYKEFYMVUSUYNCVY + IXAVURUYMBYGEUYMCYHYIUWOUWPYQWRVXNVXTVUOLWAWBZVXQXAXDZVXQVXNVUOVEVFZVYL + XHVFVXTVYLURVXMVYMAVUOUXPUWQXBVXNVYLVXQXHVXNVYKVXQXAVXNVUOUXPWAWBZVYKVX + MVYNAVUOUHUXPWFXBAVYNVYKUSVXMAUXPLVUOWAUYCXTWIVOYBZVXNVXRVXQXHVYBVYHYLX + EFVUOVXDVYLVEXHIFUDYMZVXAVYKVXCVXQXAUYMVUOLWAYNVYPEVXBVXOCUYMVUOJYOYPYI + QYQWRVYOYRUWRUWSABCDEFGHIJUXPLMNAUXPVEVFUYBAUXPLVEUYCRXERYAAUXLBUXTUMZU + XQBUXTUMZUAAUXLUXQURVYQVYRUSAUXQUXLUYDUWTUXLUXQBUXTUXAVNVOUYFPQUXBAUXPL + UXIUYCUXCUXDUXE $. $} ${ @@ -121427,7 +121427,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) $) isumcl $p |- ( ph -> sum_ k e. Z A e. CC ) $= - ( csu caddc cseq cli cfv cc isum cdm wcel fclim ffvelrn sylancr eqeltrd + ( csu caddc cseq cli cfv cc isum cdm wcel fclim ffvelcdm sylancr eqeltrd wf ) AFBCLMDENZOPZQABCDEFGHIJRAOSZQOUEUFUHTUGQTUAKUHQUFOUBUCUD $. summulc.6 $e |- ( ph -> B e. CC ) $. @@ -124292,79 +124292,79 @@ Infinite sums (cont.) fveq2d breq1d sylan2 crp simplll ad2antrr a1i mertenslemub simpr eleq1d ralrimiva rspcdva fvmptg cvv rexbii adantll eqeq12d nfcv nfov ad3antrrr fveq2 anbi2i rspc sylc cab sylbid rexlimdva mpd isumrecl isumge0 climi2 - rphalfcld breqtrrd isumclim2 eluznn serf ffvelrn syl2an abssubd pncan2d - c2 wf cdm isumsplit nncn ax-1cn sylancl oveq2d fsum3ser 3eqtr4d anassrs - pncan fvoveq1 cbvralv bitrdi cmpt simplbi nnrpd zsubcld fzfigd fsumrecl - nnzd elfznn0 0red nnm1nn0 eluzfz1 eqcomd fv0p1e1 eqtr4di rspceeqv eqeq1 - rexbidv elab2g mpbird letrd nn0ex mptex biimpri syl2an2 readdcl seq3feq - 1nn0 recnd serf0 climi0 fveq2i oveq1i oveq2i breq2i ralbii sylib absidd - cbvsumv sumeq2i rspccva nfv nfsum1 nfbr cbvral bitr4di eqeltrrid biimpi - breqtrdi csb nfcsb1v nfeq2 csbeq1a nfel1 eqeq2i abbii mertenslemi1 expr - eqtri ex syl5bir expdimp ) AJULZUMNUNUOZUPZUQFIURZUSUTVAUPZLUUMVBUTZUQH - ULZPUPZHURZVFUMUTZVBUTZVCVDZJQULZVGUPZVEZQVHVIUNUYIVJUTZEUYIUYOUSUTVFUM - UTVGUPFIURVKUTHURVAUPLVCVDJCULZVGUPVECUQVIZAUYLUYKUYSQJUYJVFVHVLAVMZAUY - NUYRALUFUUDZAUYQAUYPHPUNUQVNAWAZAUYOUQVOZVPZUYPVQZVUKUYPEVAUPZVRSVUKETV - SVTZUDUUAAUYPHPUNUQVNVUIVULVUNUDVUKUNVUMUYPWBVUKETWCSUUEZUUBWDWEAUYIVHV - OZVPZUYKVQAFINUNUQVNVUIUAUBUEUUFUUCAVUCVUFQVHAVUAVHVOZVPZVUCKULZVFUMUTZ - VGUPZIULZNUPZIURZVAUPZUYSVCVDZKVUBVEZVUFVUSVUCUYIVFUMUTZVGUPZVVDIURZVAU - PZUYSVCVDZJVUBVEVVHVUSUYTVVMJVUBAVURUYIVUBVOZUYTVVMWFZVURVVNVPAVUPVVOUY - IVUAUUGVUQUYMVVLUYSVCVUQUYMUYLUYKUSUTZVAUPVVLVUQUYKUYLAUQWGUYJUUNUYIUQV - OZUYKWGVOVUPAINUNUQVNVUIAVVCUQVOZVPZVVDFWGUAUBVTZUUHUYIWHZUQWGUYIUYJUUI - UUJZAUYLWGVOVUPAFINUNUQVNVUIUAUBUEWIWJUUKVUQVVPVVKVAVUQUYKVVJFIURZUMUTZ - UYKUSUTVWCVVPVVKVUQUYKVWCVWBVUQFINVVIVVJVVJWKZVUQVVIVUQVVQVVIUQVOZVUPVV - QAVWAWLZUYIWMWNZWOVUQVVCVVJVOZVPZAVVRVVDFWPZAVUPVWIWQZVUQVWFVWIVVRVWHVV - CVVIWRWSZUAWTZVWJAVVRFWGVOZVWLVWMUBWTVUQUYJXAUUOZVOZUMNVVIUOVWPVOAVWQVU - PUEWJZVUQINUNVVIUQVNVWHAVVRVVDWGVOZVUPVVTXBXDXCWIUULVUQUYLVWDUYKUSVUQUY - LUNVVIVFUSUTZVJUTZFIURZVWCUMUTVWDVUQFINUNVVIVVJUQVNVWEVWHAVVRVWKVUPUAXB - ZAVVRVWOVUPUBXBZVWRUUPVUQVXBUYKVWCUMVUQVXBVUDFIURUYKVUQVXAVUDFIVUQVWTUY - IUNVJVUQUYIWGVOZVFWGVOVWTUYIWPVUPVXEAUYIUUQWLUURUYIVFUVDUUSUUTXEVUQFINU - NUYIVVCUNVGUPZVOZVUQVVRVWKVVCXFZVXCXGVUQUYIUQVXFVWGVNXHVXGVUQVVRVWOVXHV - XDXGUVAXIXJXIXJVUQVVJVVDFIVWNXKUVBXMXIXNXOUVCXLVVMVVGJKVUBUYIVUTWPZVVLV - VFUYSVCVXIVVKVVEVAVXIVVJVVBVVDIUYIVUTVFVGUMUVEXEXMXNUVFUVGAVURVVHVUFVUR - VVHVPBAVUFUHABVUFABVPZUYIPUPZVAUPZUYNVUAVBUTZUNVUAVFUSUTZVJUTZVVBUIULZN - UPZUIURZVAUPZKURZVFUMUTZVBUTZVCVDZJUJULZVGUPZVEZUJUQVIZVUFVXJVXLVXMVXOV - VFKURZVFUMUTZVBUTZVCVDZJVYEVEZUJUQVIVYGVXJVXKVYJUJJKUQVUTPUPZUVHZUNUQVN - VXJWAZVXJVXMVYIVXJUYNVUAAUYNXPVOBVUHWJVXJVUABVURABVURVVHUHUVIWLZUVJWEVX - JVYHVXJVXOVVFKVXJUNVXNVYOVXJVUAVFVXJVUAVYPUVNVXJVMUVKUVLVXJVUTVXOVOZVPZ - VVEVYRVVDINVVAVVBVVBWKVYRVVAVYRVUTUQVOZVVAUQVOZVYQVYSVXJVUTVXNUVOWLVUTW - MWNZWOVYRVVCVVBVOZVPZVVDVQWUCAVVRVWSABVYQWUBXQVYRVYTWUBVVRWUAVVCVVAWRWS - VVTWTVYRVWQUMNVVAUOVWPVOAVWQBVYQUEXRVYRINUNVVAUQVNWUAVYRAVVRVWSABVYQWQV - VTWSXDXCWIVSUVMZVXJUNVHFIURZVAUPZVYHVXJUVPVXJWUEAWUEWGVOBAFINVFVHVLVUGV - VCVHVOZAVVRVWKVVCWHZUAXOZWUGAVVRVWOWUHUBXOAVWQUMNVFUOVWPVOUEAINUNVFUQVN - VFUQVOAUWNXSVVTXDXCWIWJZVSZWUDVXJWUEWUJWCVXJDFVUAGIKNWUFAVVRVWKBUAXBAVV - RVWOBUBXBAVWQBUEWJUGVXJWUFGVOZWUFVVFWPZKVXOVIZVXJUNVXOVOZWUFVHVVDIURZVA - UPZWPWUNVXJVXNVXFVOWUOVXJVXNUQVXFVXJVURVXNUQVOVYPVUAUVQWNVNXHUNVXNUVRWN - VXJWUQWUFVXJWUPWUEVAAWUPWUEWPBAVHVVDFIWUIXKWJXMUVSKUNVXOVVFWUQWUFVUTUNW - PZVVEWUPVAWURVVBVHVVDIWURVVBVFVGUPVHVGVUTUVTVLUWAXEXMUWBWTVXJWUFVRVOWUL - WUNWFWUKDULZVVFWPZKVXOVIZWUNDWUFGVRWUSWUFWPWUTWUMKVXOWUSWUFVVFUWCUWDUGU - WEWNUWFVYPXTUWGZWDWEVXJVVQVPZVVQVXKVRVOZUYIVYNUPVXKWPVXJVVQYAZWVCUYPVRV - OZWVDHUQUYIUYOUYIWPZUYPVXKVRUYOUYIPYMZYBAWVFHUQVEZBVVQAWVFHUQVUNYCZXRWV - EYDKUYIVYMVXKUQVRVYNVUTUYIPYMZVYNWKZYEWTAVYNUNXAVDBAHVYNUNYFUQVNVUIVYNY - FVOAKUQVYMUWHUWIXSAUMVYNUNUOUMPUNUOZVWPAICUMVRHVYNPUNVUIAVXGVPVVCVYNUPZ - VVCPUPZVRVXGVVRAWVOVRVOZWVNWVOWPVVRVXGVXHUWJVXGAVVRWVPVXHVVSWVFWVPHUQVV - CUYOVVCWPUYPWVOVRUYOVVCPYMYBAWVIVVRWVJWJAVVRYAYDXGZKVVCVYMWVOUQVRVYNVUT - VVCPYMWVLYEUWKWVQVTUYOVXFVOAVUJUYOVYNUPZUYPWPZUYOXFVUKVUJWVFWVSAVUJYAVU - NKUYOVYMUYPUQVRVYNVUTUYOPYMWVLYEWTZXGVVCVRVOVUEVRVOVPVVCVUEUMUTVRVOAVVC - VUEUWLWLUWMUDVTVUKWVRVUKWVRUYPVRWVTVUNVTUWOUWPWJUWQVYLVYFUJUQVYKVYCJVYE - VYJVYBVXLVCVYIVYAVXMVBVYHVXTVFUMVXOVVFVXSKVVFVXSWPVYQVVEVXRVAVVBVVDVXQI - UIVVCVXPNYMZUXEUWRZXSUXFZUWSUWTUXAUXBYGUXCVXJVYFVUFUJUQVXJVYDUQVOZVPZVY - FVYMVYBVCVDZKVYEVEZVUFWWEVYFVXKVYBVCVDZJVYEVEZWWGWWEVYCWWHJVYEWWEUYIVYE - VOZVPZVXLVXKVYBVCWWKAVVQVXLVXKWPZABWWDWWJXQWWDWWJVVQVXJUYIVYDWRYHAUYPVA - UPZUYPWPZHUQVEVVQWWLAWWNHUQVUKUYPVUNVUOUXDYCWWNWWLHUYIUQWVGWWMVXLUYPVXK - WVGUYPVXKVAWVHXMWVHYIUXGWSWTXNXLWWFWWHKJVYEWWFJUXHKVXKVYBVCKVXKYJKVCYJK - VXMVYAVBKVXMYJKVBYJKVXTVFUMVXOVXSKKVXOYJUXIKUMYJKVFYJYKYKUXJVUTUYIWPVYM - VXKVYBVCWVKXNUXKZUXLVXJWWDWWGVUFVXJWWDWWGVPZVPZBCDUKUJEFVXTGHIJKLMNOPQW - WQAVUJUYOMUPEWPABWWPWQZRWSWWQAVUJUYPVUMWPWWRSWSWWQAVUJEWGVOWWRTWSWWQAVV - RVWKWWRUAWSWWQAVVRVWOWWRUBWSWWQAVVRVVCOUPUNVVCVJUTEVVCUYOUSUTNUPVKUTHUR - WPWWRUCWSAWVMVWPVOBWWPUDXRAVWQBWWPUEXRALXPVOBWWPUFXRUGUHVXJVXTVRVOWWPVX - JVXTVYHVRWWCWUDUXMWJBWWPBWWDWWIVPZVPZABWWPVPWWTWWPWWSBWWGWWIWWDWWOYNYNU - XNYHVXJUNVXTWBVDWWPVXJUNVYHVXTWBWVBWWCUXOWJVXJUKULZVXTWBVDZUKGVEWWPVXJW - XBUKGVXJWXAGVOZVPZDIVXPFUXPZVUAGUIKNWXAWXDVXPUQVOZVPZWXFVWKIUQVEZVXQWXE - WPZWXDWXFYAZAWXHBWXCWXFAVWKIUQUAYCYLVWKWXIIVXPUQIVXQWXEIVXPFUXQZUXRVVCV - XPWPZVVDVXQFWXEWWAIVXPFUXSZYIYOYPWXGWXFVWOIUQVEZWXEWGVOZWXJAWXNBWXCWXFA - VWOIUQUBYCYLVWOWXOIVXPUQIWXEWGWXKUXTWXLFWXEWGWXMYBYOYPAVWQBWXCUEXRGWVAD - YQWUSVXSWPZKVXOVIZDYQUGWVAWXQDWUTWXPKVXOVVFVXSWUSWWBUYAYGUYBUYEVXJWXCYA - VXJVURWXCVYPWJXTYCWJUYCUYDYRYSYTUYFUYGUYHYRYSYT $. + c2 rphalfcld breqtrrd isumclim2 eluznn serf ffvelcdm syl2an abssubd cdm + wf pncan2d isumsplit nncn ax-1cn pncan sylancl fsum3ser 3eqtr4d anassrs + oveq2d fvoveq1 cbvralv bitrdi cmpt simplbi nnrpd zsubcld fzfigd elfznn0 + nnzd fsumrecl 0red 1nn0 nnm1nn0 eluzfz1 eqcomd fv0p1e1 eqtr4di rspceeqv + eqeq1 rexbidv elab2g mpbird letrd nn0ex biimpri syl2an2 readdcl seq3feq + mptex climi0 cbvsumv fveq2i sumeq2i oveq1i oveq2i breq2i ralbii rspccva + recnd serf0 sylib absidd nfv nfsum1 nfbr cbvral bitr4di biimpi breqtrdi + eqeltrrid csb nfcsb1v nfeq2 csbeq1a nfel1 abbii eqtri mertenslemi1 expr + eqeq2i ex syl5bir expdimp ) AJULZUMNUNUOZUPZUQFIURZUSUTVAUPZLUUDVBUTZUQ + HULZPUPZHURZVFUMUTZVBUTZVCVDZJQULZVGUPZVEZQVHVIUNUYIVJUTZEUYIUYOUSUTVFU + MUTVGUPFIURVKUTHURVAUPLVCVDJCULZVGUPVECUQVIZAUYLUYKUYSQJUYJVFVHVLAVMZAU + YNUYRALUFUUEZAUYQAUYPHPUNUQVNAWAZAUYOUQVOZVPZUYPVQZVUKUYPEVAUPZVRSVUKET + VSVTZUDUUAAUYPHPUNUQVNVUIVULVUNUDVUKUNVUMUYPWBVUKETWCSUUFZUUBWDWEAUYIVH + VOZVPZUYKVQAFINUNUQVNVUIUAUBUEUUGUUCAVUCVUFQVHAVUAVHVOZVPZVUCKULZVFUMUT + ZVGUPZIULZNUPZIURZVAUPZUYSVCVDZKVUBVEZVUFVUSVUCUYIVFUMUTZVGUPZVVDIURZVA + UPZUYSVCVDZJVUBVEVVHVUSUYTVVMJVUBAVURUYIVUBVOZUYTVVMWFZVURVVNVPAVUPVVOU + YIVUAUUHVUQUYMVVLUYSVCVUQUYMUYLUYKUSUTZVAUPVVLVUQUYKUYLAUQWGUYJUUNUYIUQ + VOZUYKWGVOVUPAINUNUQVNVUIAVVCUQVOZVPZVVDFWGUAUBVTZUUIUYIWHZUQWGUYIUYJUU + JUUKZAUYLWGVOVUPAFINUNUQVNVUIUAUBUEWIWJUULVUQVVPVVKVAVUQUYKVVJFIURZUMUT + ZUYKUSUTVWCVVPVVKVUQUYKVWCVWBVUQFINVVIVVJVVJWKZVUQVVIVUQVVQVVIUQVOZVUPV + VQAVWAWLZUYIWMWNZWOVUQVVCVVJVOZVPZAVVRVVDFWPZAVUPVWIWQZVUQVWFVWIVVRVWHV + VCVVIWRWSZUAWTZVWJAVVRFWGVOZVWLVWMUBWTVUQUYJXAUUMZVOZUMNVVIUOVWPVOAVWQV + UPUEWJZVUQINUNVVIUQVNVWHAVVRVVDWGVOZVUPVVTXBXDXCWIUUOVUQUYLVWDUYKUSVUQU + YLUNVVIVFUSUTZVJUTZFIURZVWCUMUTVWDVUQFINUNVVIVVJUQVNVWEVWHAVVRVWKVUPUAX + BZAVVRVWOVUPUBXBZVWRUUPVUQVXBUYKVWCUMVUQVXBVUDFIURUYKVUQVXAVUDFIVUQVWTU + YIUNVJVUQUYIWGVOZVFWGVOVWTUYIWPVUPVXEAUYIUUQWLUURUYIVFUUSUUTUVDXEVUQFIN + UNUYIVVCUNVGUPZVOZVUQVVRVWKVVCXFZVXCXGVUQUYIUQVXFVWGVNXHVXGVUQVVRVWOVXH + VXDXGUVAXIXJXIXJVUQVVJVVDFIVWNXKUVBXMXIXNXOUVCXLVVMVVGJKVUBUYIVUTWPZVVL + VVFUYSVCVXIVVKVVEVAVXIVVJVVBVVDIUYIVUTVFVGUMUVEXEXMXNUVFUVGAVURVVHVUFVU + RVVHVPBAVUFUHABVUFABVPZUYIPUPZVAUPZUYNVUAVBUTZUNVUAVFUSUTZVJUTZVVBUIULZ + NUPZUIURZVAUPZKURZVFUMUTZVBUTZVCVDZJUJULZVGUPZVEZUJUQVIZVUFVXJVXLVXMVXO + VVFKURZVFUMUTZVBUTZVCVDZJVYEVEZUJUQVIVYGVXJVXKVYJUJJKUQVUTPUPZUVHZUNUQV + NVXJWAZVXJVXMVYIVXJUYNVUAAUYNXPVOBVUHWJVXJVUABVURABVURVVHUHUVIWLZUVJWEV + XJVYHVXJVXOVVFKVXJUNVXNVYOVXJVUAVFVXJVUAVYPUVNVXJVMUVKUVLVXJVUTVXOVOZVP + ZVVEVYRVVDINVVAVVBVVBWKVYRVVAVYRVUTUQVOZVVAUQVOZVYQVYSVXJVUTVXNUVMWLVUT + WMWNZWOVYRVVCVVBVOZVPZVVDVQWUCAVVRVWSABVYQWUBXQVYRVYTWUBVVRWUAVVCVVAWRW + SVVTWTVYRVWQUMNVVAUOVWPVOAVWQBVYQUEXRVYRINUNVVAUQVNWUAVYRAVVRVWSABVYQWQ + VVTWSXDXCWIVSUVOZVXJUNVHFIURZVAUPZVYHVXJUVPVXJWUEAWUEWGVOBAFINVFVHVLVUG + VVCVHVOZAVVRVWKVVCWHZUAXOZWUGAVVRVWOWUHUBXOAVWQUMNVFUOVWPVOUEAINUNVFUQV + NVFUQVOAUVQXSVVTXDXCWIWJZVSZWUDVXJWUEWUJWCVXJDFVUAGIKNWUFAVVRVWKBUAXBAV + VRVWOBUBXBAVWQBUEWJUGVXJWUFGVOZWUFVVFWPZKVXOVIZVXJUNVXOVOZWUFVHVVDIURZV + AUPZWPWUNVXJVXNVXFVOWUOVXJVXNUQVXFVXJVURVXNUQVOVYPVUAUVRWNVNXHUNVXNUVSW + NVXJWUQWUFVXJWUPWUEVAAWUPWUEWPBAVHVVDFIWUIXKWJXMUVTKUNVXOVVFWUQWUFVUTUN + WPZVVEWUPVAWURVVBVHVVDIWURVVBVFVGUPVHVGVUTUWAVLUWBXEXMUWCWTVXJWUFVRVOWU + LWUNWFWUKDULZVVFWPZKVXOVIZWUNDWUFGVRWUSWUFWPWUTWUMKVXOWUSWUFVVFUWDUWEUG + UWFWNUWGVYPXTUWHZWDWEVXJVVQVPZVVQVXKVRVOZUYIVYNUPVXKWPVXJVVQYAZWVCUYPVR + VOZWVDHUQUYIUYOUYIWPZUYPVXKVRUYOUYIPYMZYBAWVFHUQVEZBVVQAWVFHUQVUNYCZXRW + VEYDKUYIVYMVXKUQVRVYNVUTUYIPYMZVYNWKZYEWTAVYNUNXAVDBAHVYNUNYFUQVNVUIVYN + YFVOAKUQVYMUWIUWNXSAUMVYNUNUOUMPUNUOZVWPAICUMVRHVYNPUNVUIAVXGVPVVCVYNUP + ZVVCPUPZVRVXGVVRAWVOVRVOZWVNWVOWPVVRVXGVXHUWJVXGAVVRWVPVXHVVSWVFWVPHUQV + VCUYOVVCWPUYPWVOVRUYOVVCPYMYBAWVIVVRWVJWJAVVRYAYDXGZKVVCVYMWVOUQVRVYNVU + TVVCPYMWVLYEUWKWVQVTUYOVXFVOAVUJUYOVYNUPZUYPWPZUYOXFVUKVUJWVFWVSAVUJYAV + UNKUYOVYMUYPUQVRVYNVUTUYOPYMWVLYEWTZXGVVCVRVOVUEVRVOVPVVCVUEUMUTVRVOAVV + CVUEUWLWLUWMUDVTVUKWVRVUKWVRUYPVRWVTVUNVTUXDUXEWJUWOVYLVYFUJUQVYKVYCJVY + EVYJVYBVXLVCVYIVYAVXMVBVYHVXTVFUMVXOVVFVXSKVVFVXSWPVYQVVEVXRVAVVBVVDVXQ + IUIVVCVXPNYMZUWPUWQZXSUWRZUWSUWTUXAUXBYGUXFVXJVYFVUFUJUQVXJVYDUQVOZVPZV + YFVYMVYBVCVDZKVYEVEZVUFWWEVYFVXKVYBVCVDZJVYEVEZWWGWWEVYCWWHJVYEWWEUYIVY + EVOZVPZVXLVXKVYBVCWWKAVVQVXLVXKWPZABWWDWWJXQWWDWWJVVQVXJUYIVYDWRYHAUYPV + AUPZUYPWPZHUQVEVVQWWLAWWNHUQVUKUYPVUNVUOUXGYCWWNWWLHUYIUQWVGWWMVXLUYPVX + KWVGUYPVXKVAWVHXMWVHYIUXCWSWTXNXLWWFWWHKJVYEWWFJUXHKVXKVYBVCKVXKYJKVCYJ + KVXMVYAVBKVXMYJKVBYJKVXTVFUMVXOVXSKKVXOYJUXIKUMYJKVFYJYKYKUXJVUTUYIWPVY + MVXKVYBVCWVKXNUXKZUXLVXJWWDWWGVUFVXJWWDWWGVPZVPZBCDUKUJEFVXTGHIJKLMNOPQ + WWQAVUJUYOMUPEWPABWWPWQZRWSWWQAVUJUYPVUMWPWWRSWSWWQAVUJEWGVOWWRTWSWWQAV + VRVWKWWRUAWSWWQAVVRVWOWWRUBWSWWQAVVRVVCOUPUNVVCVJUTEVVCUYOUSUTNUPVKUTHU + RWPWWRUCWSAWVMVWPVOBWWPUDXRAVWQBWWPUEXRALXPVOBWWPUFXRUGUHVXJVXTVRVOWWPV + XJVXTVYHVRWWCWUDUXOWJBWWPBWWDWWIVPZVPZABWWPVPWWTWWPWWSBWWGWWIWWDWWOYNYN + UXMYHVXJUNVXTWBVDWWPVXJUNVYHVXTWBWVBWWCUXNWJVXJUKULZVXTWBVDZUKGVEWWPVXJ + WXBUKGVXJWXAGVOZVPZDIVXPFUXPZVUAGUIKNWXAWXDVXPUQVOZVPZWXFVWKIUQVEZVXQWX + EWPZWXDWXFYAZAWXHBWXCWXFAVWKIUQUAYCYLVWKWXIIVXPUQIVXQWXEIVXPFUXQZUXRVVC + VXPWPZVVDVXQFWXEWWAIVXPFUXSZYIYOYPWXGWXFVWOIUQVEZWXEWGVOZWXJAWXNBWXCWXF + AVWOIUQUBYCYLVWOWXOIVXPUQIWXEWGWXKUXTWXLFWXEWGWXMYBYOYPAVWQBWXCUEXRGWVA + DYQWUSVXSWPZKVXOVIZDYQUGWVAWXQDWUTWXPKVXOVVFVXSWUSWWBUYEYGUYAUYBVXJWXCY + AVXJVURWXCVYPWJXTYCWJUYCUYDYRYSYTUYFUYGUYHYRYSYT $. $} $d n s ph $. @@ -132803,29 +132803,29 @@ integers has a least element (schema form). (Contributed by NM, ` N ` reaches zero by the ` N ` th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.) $) nn0seqcvgd $p |- ( ph -> ( F ` N ) = 0 ) $= - ( cfv cc0 wceq cle wbr cmin co cn0 wcel wi clt wa cr 0nn0 ffvelrn sylancl - vm wf eqeltrd nn0red leidd cv c1 caddc fveq2 oveq2 breq12d eqbrtrrd recnd - imbi2d subid1d breqtrrd a1i wne wb posdif syl2anr adantr adantl peano2nn0 - nn0re breq1 cz syl2an nn0zd nn0z zsubcl zltlem1 syl2anc cc ax-1cn subsub4 - nn0cn mp3an3 breq2d bitrd 3bitr2d biimpa an32s a1d ffvelrnda zred syl3anc - ltletr sylibd syland expdimp wdc wo 0zd zdceq dcne mpjaodan anasss expcom - a2d 3adant1 fnn0ind pm2.43i subidd breqtrd ffvelrnd nn0ge0d 0re mpbir2and - sylib letri3 ) ADCHZIJZXOIKLZIXOKLZAXODDMNZIKAXOXSKLZADOPZYADDKLAXTQZADIC - HZOFAOOCUEZIOPYCOPEUAOOICUBUCUFZYEADADYEUGZUHZAUDUIZCHZDYHMNZKLZQAYCDIMNZ - KLZQZABUIZCHZDYOMNZKLZQZAYOUJUKNZCHZDYTMNZKLZQZYBUDBDDYHIJZYKYMAUUEYIYCYJ - YLKYHICULYHIDMUMUNUQYHYOJZYKYRAUUFYIYPYJYQKYHYOCULYHYODMUMUNUQYHYTJZYKUUC - AUUGYIUUAYJUUBKYHYTCULYHYTDMUMUNUQYHDJZYKXTAUUHYIXOYJXSKYHDCULYHDDMUMUNUQ - YNYAAYCDYLKADYCDKFYGUOADADYFUPZURUSUTYOOPZYODRLZYSUUDQYAUUJUUKSZAYRUUCAUU - LYRUUCQZAUUJUUKUUMAUUJSZUUKSZUUAIJZUUMUUAIVAZUUOUUPSUUCYRUUNUUPUUKUUCUUNU - UPSZUUKUUCUURUUKIYQRLZUUAYQRLZUUCUUNUUKUUSVBZUUPUUJYOTPDTPUVAAYOVHYFYODVC - VDVEUUPUUTUUSVBUUNUUAIYQRVIVFUUNUUTUUCVBUUPUUNUUTUUAYQUJMNZKLZUUCUUNUUAVJ - PZYQVJPZUUTUVCVBUUNUUAAYDYTOPUUAOPUUJEYOVGOOYTCUBVKZVLZADVJPYOVJPUVEUUJAD - YEVLYOVMDYOVNVKZUUAYQVOVPUUNUVBUUBUUAKADVQPZYOVQPZUVBUUBJZUUJUUIYOVTUVIUV - JUJVQPUVKVRDYOUJVSWAVKWBWCZVEWDWEWFWGUUOUUQYRUUCUUNUUQYRSUUCQUUKUUNUUQUUA - YPRLZYRUUCGUUNUVMYRSZUUTUUCUUNUUATPYPTPYQTPUVNUUTQUUNUUAUVFUGUUNYPAOOYOCE - WHUGUUNYQUVHWIUUAYPYQWKWJUVLWLWMVEWNUUOUUPWOZUUPUUQWPUUOUVDIVJPUVOUUNUVDU - UKUVGVEUUOWQUUAIWRVPUUAIWSXMWTXAXBXCXDXEWJXFADUUIXGXHAXOAOODCEYEXIZXJAXOT - PITPXPXQXRSVBAXOUVPUGXKXOIXNUCXL $. + ( cfv cc0 wceq cle wbr cmin co cn0 wcel wi clt wa cr 0nn0 sylancl eqeltrd + vm wf ffvelcdm nn0red leidd cv c1 caddc fveq2 oveq2 imbi2d eqbrtrrd recnd + breq12d subid1d breqtrrd a1i wne nn0re posdif syl2anr adantr breq1 adantl + wb cz peano2nn0 syl2an nn0zd nn0z zsubcl zltlem1 syl2anc cc nn0cn subsub4 + ax-1cn mp3an3 breq2d bitrd 3bitr2d biimpa an32s a1d ffvelrnda zred ltletr + syl3anc sylibd syland expdimp wdc wo 0zd zdceq dcne sylib mpjaodan anasss + expcom a2d 3adant1 fnn0ind pm2.43i subidd breqtrd ffvelrnd nn0ge0d letri3 + 0re mpbir2and ) ADCHZIJZXOIKLZIXOKLZAXODDMNZIKAXOXSKLZADOPZYADDKLAXTQZADI + CHZOFAOOCUEZIOPYCOPEUAOOICUFUBUCZYEADADYEUGZUHZAUDUIZCHZDYHMNZKLZQAYCDIMN + ZKLZQZABUIZCHZDYOMNZKLZQZAYOUJUKNZCHZDYTMNZKLZQZYBUDBDDYHIJZYKYMAUUEYIYCY + JYLKYHICULYHIDMUMUQUNYHYOJZYKYRAUUFYIYPYJYQKYHYOCULYHYODMUMUQUNYHYTJZYKUU + CAUUGYIUUAYJUUBKYHYTCULYHYTDMUMUQUNYHDJZYKXTAUUHYIXOYJXSKYHDCULYHDDMUMUQU + NYNYAAYCDYLKADYCDKFYGUOADADYFUPZURUSUTYOOPZYODRLZYSUUDQYAUUJUUKSZAYRUUCAU + ULYRUUCQZAUUJUUKUUMAUUJSZUUKSZUUAIJZUUMUUAIVAZUUOUUPSUUCYRUUNUUPUUKUUCUUN + UUPSZUUKUUCUURUUKIYQRLZUUAYQRLZUUCUUNUUKUUSVHZUUPUUJYOTPDTPUVAAYOVBYFYODV + CVDVEUUPUUTUUSVHUUNUUAIYQRVFVGUUNUUTUUCVHUUPUUNUUTUUAYQUJMNZKLZUUCUUNUUAV + IPZYQVIPZUUTUVCVHUUNUUAAYDYTOPUUAOPUUJEYOVJOOYTCUFVKZVLZADVIPYOVIPUVEUUJA + DYEVLYOVMDYOVNVKZUUAYQVOVPUUNUVBUUBUUAKADVQPZYOVQPZUVBUUBJZUUJUUIYOVRUVIU + VJUJVQPUVKVTDYOUJVSWAVKWBWCZVEWDWEWFWGUUOUUQYRUUCUUNUUQYRSUUCQUUKUUNUUQUU + AYPRLZYRUUCGUUNUVMYRSZUUTUUCUUNUUATPYPTPYQTPUVNUUTQUUNUUAUVFUGUUNYPAOOYOC + EWHUGUUNYQUVHWIUUAYPYQWJWKUVLWLWMVEWNUUOUUPWOZUUPUUQWPUUOUVDIVIPUVOUUNUVD + UUKUVGVEUUOWQUUAIWRVPUUAIWSWTXAXBXCXDXEXFWKXGADUUIXHXIAXOAOODCEYEXJZXKAXO + TPITPXPXQXRSVHAXOUVPUGXMXOIXLUBXN $. $} ${ @@ -132885,7 +132885,7 @@ integers has a least element (schema form). (Contributed by NM, 28-May-2014.) $) algrf $p |- ( ph -> R : Z --> S ) $= ( vx vy wf cv wcel wa cfv vex c1st ccom csn cxp cseq wceq fvconst2g sylan - adantr eqeltrd algrflem simpl ffvelrn syl2an eqeltrid seqf feq1i sylibr + adantr eqeltrd algrflem simpl ffvelcdm syl2an eqeltrid seqf feq1i sylibr co ) AGDEUAUBZGBUCUDZFUEZOGDCOAMNUTDVAFGHJAMPZGQZRVCVASZBDABDQZVDVEBUFKGB VCDUGUHAVFVDKUIUJAVCDQZNPZDQZRZRVCVHUTUSVCESZDVCVHEMTNTUKADDEOVGVKDQVJLVG VIULDDVCEUMUNUOUPGDCVBIUQUR $. @@ -133168,18 +133168,18 @@ integers has a least element (schema form). (Contributed by NM, eucalg $p |- ( ( M e. NN0 /\ N e. NN0 ) -> ( 1st ` ( R ` N ) ) = ( M gcd N ) ) $= ( cn0 wcel cfv cgcd cc0 c2nd wceq syl fveq2d fvres vz wa c1st co cop wf nn0uz - cxp 0zd opelxpi eqeltrid eucalgf algrf ffvelrn sylancom 1st2nd2 df-ov eqtr4di - a1i fveq2i op2ndg eqtrid cuz cz xp2nd nn0zd uzid eucalgcvga mpd eqtr3d oveq2d - eqid xp1st nn0gcdid0 3syl 3eqtrrd cres eucalginv ffvelrni 3eqtr4d alginv 0nn0 - cv sylancl 3eqtr3d ialgr0 eqtrdi 3eqtrd ) FKLZGKLZUBZGDMZUCMZWLNMZODMZNMZFGNU - DZWKWNWMWLPMZNUDZWMONUDZWMWKWNWMWRUEZNMWSWKWLXANWKWLKKUHZLZWLXAQWIWJKXBDUFZXC - WKCDXBEOKUGIWKUIZWKCFGUEZXBJFGKKUJUKZXBXBEUFWKABEHULZUSZUMZKXBGDUNUOZWLKKUPRS - WMWRNUQURWKWROWMNWKCPMZDMZPMZWROWKXMWLPWKXLGDWKXLXFPMGCXFPJUTFGKKVAVBSSWKCXBL - ZXNOQZXGXOXLXLVCMLZXPXOXLVDLXQXOXLCKKVEVFXLVGRABCDEXLXLHIXLVLVHVIRVJVKWKXCWMK - LWTWMQXKWLKKVMWMVNVOVPWKWLNXBVQZMZWOXRMZWNWPWIWJXOXSXTQXGUACDXBEXRGIXHUAWCZXB - LZYAEMZNMZYANMYCXRMZYAXRMABEYAHVRYBYCXBLYEYDQXBXBYAEXHVSYCXBNTRYAXBNTVTWAUOWK - XCXSWNQXKWLXBNTRWKWOXBLZXTWPQWKXDOKLYFXJWBKXBODUNWDWOXBNTRWEWKWPXFNMWQWKWOXFN - WKWOCXFWKCDXBEOKUGIXEXGXIWFJWGSFGNUQURWH $. + cxp 0zd opelxpi eqeltrid eucalgf algrf ffvelcdm sylancom 1st2nd2 df-ov fveq2i + a1i eqtr4di op2ndg eqtrid cuz cz xp2nd uzid eqid eucalgcvga mpd eqtr3d oveq2d + nn0zd xp1st nn0gcdid0 3syl 3eqtrrd cres cv eucalginv ffvelrni 3eqtr4d sylancl + alginv 0nn0 3eqtr3d ialgr0 eqtrdi 3eqtrd ) FKLZGKLZUBZGDMZUCMZWLNMZODMZNMZFGN + UDZWKWNWMWLPMZNUDZWMONUDZWMWKWNWMWRUEZNMWSWKWLXANWKWLKKUHZLZWLXAQWIWJKXBDUFZX + CWKCDXBEOKUGIWKUIZWKCFGUEZXBJFGKKUJUKZXBXBEUFWKABEHULZUSZUMZKXBGDUNUOZWLKKUPR + SWMWRNUQUTWKWROWMNWKCPMZDMZPMZWROWKXMWLPWKXLGDWKXLXFPMGCXFPJURFGKKVAVBSSWKCXB + LZXNOQZXGXOXLXLVCMLZXPXOXLVDLXQXOXLCKKVEVLXLVFRABCDEXLXLHIXLVGVHVIRVJVKWKXCWM + KLWTWMQXKWLKKVMWMVNVOVPWKWLNXBVQZMZWOXRMZWNWPWIWJXOXSXTQXGUACDXBEXRGIXHUAVRZX + BLZYAEMZNMZYANMYCXRMZYAXRMABEYAHVSYBYCXBLYEYDQXBXBYAEXHVTYCXBNTRYAXBNTWAWCUOW + KXCXSWNQXKWLXBNTRWKWOXBLZXTWPQWKXDOKLYFXJWDKXBODUNWBWOXBNTRWEWKWPXFNMWQWKWOXF + NWKWOCXFWKCDXBEOKUGIXEXGXIWFJWGSFGNUQUTWH $. $} @@ -136012,65 +136012,65 @@ reduced fraction representation (no common factors, denominator eqtri sylib cfn 0z fzofig sylancr eqeltrid wdc gcdcld nn0zd zdceq ssfirab 1zzd dfphi2 fveq2i eqtr4di simprbi dvdsmul2 opelxpi eqeltrd wfun cdm crth dvdstr wfn f1ofn fnfun fndm sseqtrrid funimass4 ccnv mp2an sseqtrri sseli - xpss12 f1ocnvfv2 wf f1ocnv f1of ffvelrn opelxp rpmul funfvima2 imp syldan - cbvmptv ex ssrdv eqssd wf1 f1of1 a1i zmulcld f1imaeng eqbrtrrd 1z sylancl - xpfi hashen hashxp rabeqi oveq12d 3eqtr4d ) AKUCUDZFUCUDZJUCUDZUEUFZHIUEU - FZUGUDZHUGUDZIUGUDZUEUFAFJUHZUCUDZUWHUWKAUWQUWHSZUWPKUIUJZAGKUKZUWPKUIAUW - TUWPAUWTUWPULZUAUMZGUDZUWPTZUAKUNZAUXDUAKAUXBKTZUPZUXCUXBHUOUFZUXBIUOUFZU - QZUWPUXGUXBDTZUXJURTZUXCUXJSUXFUXKAUXFUXKUXBUWLUSUFZUTSZCUMZUWLUSUFZUTSZU - XNCUXBDKUXOUXBSUXPUXMUTUXOUXBUWLUSVAVBRVCZVDZVEZUXGUXHVFTUXIVFTUXLUXGUXBH - UXGUXBVGTZUXBVFTUXGUXKUYAUXTUYAUXBVJUWLVHUFZDUXBVJUWLVIZLVKVLUXBVMVLZUXGH - WBTZHVFTZAUYEUXFAUYEIWBTZHIUSUFUTSZOVNZVOZHVPZVLUXGHUYJVQVRUXGUXBIUYDUXGU - YGIVFTZAUYGUXFAUYEUYGUYHOVSZVOZIVPZVLUXGIUYNVQVRUXHUXIVFVFWCVTBUXBBUMZHUO - UFZUYPIUOUFZUQZUXJDURGUYPUXBSUYQUXHUYRUXIUYPUXBHUOVAUYPUXBIUOVAWAZNWDVTUX - GUXHFTZUXIJTZUXJUWPTUXGUXHVJHVHUFZTZUXHHUSUFZUTSZVUAUXGUYAUYEVUDUXGUXBUYB - TZUYAUXFVUGAUXFUXBDUYBUXSLWEVEUYCVLZUYJUXBHWFVTUXGVUEUXBHUSUFZUTUXGUYAUYE - VUEVUISVUHUYJUXBHWGVTUXGVUIUTWHUJZVUIUTSZUXGVUIUXMUTWHUXGVUIUXBWIUJZVUIUW - LWIUJZVUIUXMWHUJZUXGVULVUIHWIUJZUXGUYAHVGTZVULVUOUPVUHUXGHUYJWJZUXBHWKVTZ - WLUXGVUIHIUXGVUIUXGUYAVUPUXBVJSZHVJSZUPZWNZVUIWBTZVUHVUQUXGUYEHVJWMVVBUYJ - HWOVVAHVJVUSVUTWPWQWRUXBHWSWTZWJZVUQUXGIUYNWJZUXGVULVUOVURXAXBUXGVUIVGTUY - AUWLVGTZVUSUWLVJSZUPZWNZVULVUMUPVUNXDVVEVUHUXGUWLUXGHIUYJUYNXCZWJZUXGUWLW - BTZUWLVJWMVVJVVKUWLWOVVIUWLVJVUSVVHWPWQWRZVUIUXBUWLXEXFXGUXFUXNAUXFUXKUXN - UXRUUAVEZXHUXGVVCVUJVUKXIVVDVUIXJVLXKXNUXOHUSUFZUTSZVUFCUXHVUCFUXOUXHSVVP - VUEUTUXOUXHHUSVAVBPVCXLUXGUXIVJIVHUFZTZUXIIUSUFZUTSZVUBUXGUYAUYGVVSVUHUYN - UXBIWFVTUXGVVTUXBIUSUFZUTUXGUYAUYGVVTVWBSVUHUYNUXBIWGVTUXGVWBUTWHUJZVWBUT - SZUXGVWBUXMUTWHUXGVWBUXBWIUJZVWBUWLWIUJZVWBUXMWHUJZUXGVWEVWBIWIUJZUXGUYAI - VGTZVWEVWHUPVUHVVFUXBIWKVTZWLUXGVWHIUWLWIUJZVWFUXGVWEVWHVWJXAUXGVUPVWIVWK - VUQVVFHIUUBVTUXGVWBVGTZVWIVVGVWHVWKUPVWFXDUXGVWBUXGUYAVWIVUSIVJSZUPZWNZVW - BWBTZVUHVVFUXGUYGIVJWMVWOUYNIWOVWNIVJVUSVWMWPWQWRUXBIWSWTZWJZVVFVVLVWBIUW - LUUHXOXGUXGVWLUYAVVGVVJVWEVWFUPVWGXDVWRVUHVVLVVNVWBUXBUWLXEXFXGVVOXHUXGVW - PVWCVWDXIVWQVWBXJVLXKXNUXOIUSUFZUTSZVWACUXIVVRJUXOUXISVWSVVTUTUXOUXIIUSVA - VBQVCXLUXHUXIFJUUCVTUUDXMAGUUEZKGUUFZULZUXAUXEXIADEGXPZGDUUIZVXAABDEGHILM - NOUUGZDEGUUJZDGUUKWRZADKVXBKUXQCDXQZDRUXQCDXRXSZAVXDVXEVXBDSVXFVXGDGUULWR - UUMZUAKUWPGUUNVTXTAUBUWPUWTAUBUMZUWPTZVXLUWTTAVXMUPZVXLGUUOZUDZGUDZVXLUWT - AVXDVXLETZVXQVXLSVXMVXFUWPEVXLUWPVUCVVRUHZEFVUCULJVVRULUWPVXSULFVVQCVUCXQ - ZVUCPVVQCVUCXRXSJVWTCVVRXQZVVRQVWTCVVRXRXSFVUCJVVRUUSUUPMUUQUURZDEVXLGUUT - YAZAVXMVXPKTZVXQUWTTZVXNVXPDTZVXPUWLUSUFZUTSZVYDAEDVXOUVAZVXRVYFVXMAVXDED - VXOXPVYIVXFDEGUVBEDVXOUVCWRVYBEDVXLVXOUVDYAZVXNVXPHUSUFZUTSZVXPIUSUFZUTSZ - VYHVXNVXPHUOUFZHUSUFZVYKUTVXNVXPVGTZUYEVYPVYKSVXNVXPUYBTVYQVXNVXPDUYBVYJL - WEVXPVJUWLVIVLZAUYEVXMUYIVOZVXPHWGVTVXNVYOVUCTZVYPUTSZVXNVYOFTZVYTWUAUPVX - NWUBVXPIUOUFZJTZVXNVYOWUCUQZUWPTWUBWUDUPVXNVXLWUEUWPVXNVXQVXLWUEVYCVXNVYF - WUEURTZVXQWUESVYJVXNVYOVFTWUCVFTWUFVXNVXPHVXNVYQVXPVFTVYRVXPVMVLZVXNUYEUY - FVYSUYKVLVXNHVYSVQVRVXNVXPIWUGVXNUYGUYLAUYGVXMUYMVOZUYOVLVXNIWUHVQVRVYOWU - CVFVFWCVTUAVXPUXJWUEDURGUXBVXPSUXHVYOUXIWUCUXBVXPHUOVAUXBVXPIUOVAWAGBDUYS - YBUADUXJYBNBUADUYSUXJUYTUVJYEWDVTYCAVXMWPYDVYOWUCFJUVEYFZWLVVQWUACVYOVUCF - UXOVYOSVVPVYPUTUXOVYOHUSVAVBPVCYFXAYCVXNWUCIUSUFZVYMUTVXNVYQUYGWUJVYMSVYR - WUHVXPIWGVTVXNWUCVVRTZWUJUTSZVXNWUDWUKWULUPVXNWUBWUDWUIXAVWTWULCWUCVVRJUX - OWUCSVWSWUJUTUXOWUCIUSVAVBQVCYFXAYCVXNVYQVUPVWIVYLVYNUPVYHXDVYRAVUPVXMAHU - YIWJZVOAVWIVXMAIUYMWJZVOVXPHIUVFXOXGUXQVYHCVXPDKUXOVXPSUXPVYGUTUXOVXPUWLU - SVAVBRVCXLAVYDVYEAVXAVXCVYDVYEXDVXHVXKKVXPGUVGVTUVHUVIYDUVKUVLUVMADEGUVNZ - KDULZKYGTZUWTKUIUJAVXDWUOVXFDEGUVOVLWUPAVXJUVPAKVXIYGRAUXQCDADUYBYGLAVJVG - TZVVGUYBYGTYHAHIWUMWUNUVQZVJUWLYIYJYKAUXQYLZCDAUXODTZUPZUXPVGTUTVGTZWUTWV - BUXPWVBUXOUWLWVAUXOVGTZAWVDUXOUYBDUXOVJUWLVILVKVEAVVGWVAWUSVOYMYNWVBYQUXP - UTYOVTXMYPYKZDEKGYGUVRXOUVSAUWPYGTZWUQUWRUWSXIAFYGTZJYGTZWVFAFVXTYGPAVVQC - VUCAWURVUPVUCYGTYHWUMVJHYIYJAVVQYLZCVUCAUXOVUCTZUPZVVPVGTWVCWVIWVKVVPWVKU - XOHWVJWVDAUXOVJHVIVEAVUPWVJWUMVOYMYNUVTVVPUTYOUWAXMYPYKZAJVYAYGQAVWTCVVRA - WURVWIVVRYGTYHWUNVJIYIYJAVWTYLZCVVRAUXOVVRTZUPZVWSVGTWVCWVMWVOVWSWVOUXOIW - VNWVDAUXOVJIVIVEAVWIWVNWUNVOYMYNWVOYQVWSUTYOVTXMYPYKZFJUWBVTWVEUWPKUWCVTX - TAWVGWVHUWQUWKSWVLWVPFJUWDVTYCAVVMUWMUWHSAHIUYIUYMXCVVMUWMUXQCUYBXQZUCUDU - WHCUWLYRKWVQUCKVXIWVQRUXQCDUYBLUWEYEYSYTVLAUWNUWIUWOUWJUEAUYEUWNUWISUYIUY - EUWNVXTUCUDUWICHYRFVXTUCPYSYTVLAUYGUWOUWJSUYMUYGUWOVYAUCUDUWJCIYRJVYAUCQY - SYTVLUWFUWG $. + xpss12 f1ocnvfv2 wf f1ocnv ffvelcdm cbvmptv opelxp rpmul funfvima2 syldan + f1of imp ssrdv eqssd wf1 f1of1 a1i zmulcld f1imaeng eqbrtrrd sylancl xpfi + ex 1z hashen hashxp rabeqi oveq12d 3eqtr4d ) AKUCUDZFUCUDZJUCUDZUEUFZHIUE + UFZUGUDZHUGUDZIUGUDZUEUFAFJUHZUCUDZUWHUWKAUWQUWHSZUWPKUIUJZAGKUKZUWPKUIAU + WTUWPAUWTUWPULZUAUMZGUDZUWPTZUAKUNZAUXDUAKAUXBKTZUPZUXCUXBHUOUFZUXBIUOUFZ + UQZUWPUXGUXBDTZUXJURTZUXCUXJSUXFUXKAUXFUXKUXBUWLUSUFZUTSZCUMZUWLUSUFZUTSZ + UXNCUXBDKUXOUXBSUXPUXMUTUXOUXBUWLUSVAVBRVCZVDZVEZUXGUXHVFTUXIVFTUXLUXGUXB + HUXGUXBVGTZUXBVFTUXGUXKUYAUXTUYAUXBVJUWLVHUFZDUXBVJUWLVIZLVKVLUXBVMVLZUXG + HWBTZHVFTZAUYEUXFAUYEIWBTZHIUSUFUTSZOVNZVOZHVPZVLUXGHUYJVQVRUXGUXBIUYDUXG + UYGIVFTZAUYGUXFAUYEUYGUYHOVSZVOZIVPZVLUXGIUYNVQVRUXHUXIVFVFWCVTBUXBBUMZHU + OUFZUYPIUOUFZUQZUXJDURGUYPUXBSUYQUXHUYRUXIUYPUXBHUOVAUYPUXBIUOVAWAZNWDVTU + XGUXHFTZUXIJTZUXJUWPTUXGUXHVJHVHUFZTZUXHHUSUFZUTSZVUAUXGUYAUYEVUDUXGUXBUY + BTZUYAUXFVUGAUXFUXBDUYBUXSLWEVEUYCVLZUYJUXBHWFVTUXGVUEUXBHUSUFZUTUXGUYAUY + EVUEVUISVUHUYJUXBHWGVTUXGVUIUTWHUJZVUIUTSZUXGVUIUXMUTWHUXGVUIUXBWIUJZVUIU + WLWIUJZVUIUXMWHUJZUXGVULVUIHWIUJZUXGUYAHVGTZVULVUOUPVUHUXGHUYJWJZUXBHWKVT + ZWLUXGVUIHIUXGVUIUXGUYAVUPUXBVJSZHVJSZUPZWNZVUIWBTZVUHVUQUXGUYEHVJWMVVBUY + JHWOVVAHVJVUSVUTWPWQWRUXBHWSWTZWJZVUQUXGIUYNWJZUXGVULVUOVURXAXBUXGVUIVGTU + YAUWLVGTZVUSUWLVJSZUPZWNZVULVUMUPVUNXDVVEVUHUXGUWLUXGHIUYJUYNXCZWJZUXGUWL + WBTZUWLVJWMVVJVVKUWLWOVVIUWLVJVUSVVHWPWQWRZVUIUXBUWLXEXFXGUXFUXNAUXFUXKUX + NUXRUUAVEZXHUXGVVCVUJVUKXIVVDVUIXJVLXKXNUXOHUSUFZUTSZVUFCUXHVUCFUXOUXHSVV + PVUEUTUXOUXHHUSVAVBPVCXLUXGUXIVJIVHUFZTZUXIIUSUFZUTSZVUBUXGUYAUYGVVSVUHUY + NUXBIWFVTUXGVVTUXBIUSUFZUTUXGUYAUYGVVTVWBSVUHUYNUXBIWGVTUXGVWBUTWHUJZVWBU + TSZUXGVWBUXMUTWHUXGVWBUXBWIUJZVWBUWLWIUJZVWBUXMWHUJZUXGVWEVWBIWIUJZUXGUYA + IVGTZVWEVWHUPVUHVVFUXBIWKVTZWLUXGVWHIUWLWIUJZVWFUXGVWEVWHVWJXAUXGVUPVWIVW + KVUQVVFHIUUBVTUXGVWBVGTZVWIVVGVWHVWKUPVWFXDUXGVWBUXGUYAVWIVUSIVJSZUPZWNZV + WBWBTZVUHVVFUXGUYGIVJWMVWOUYNIWOVWNIVJVUSVWMWPWQWRUXBIWSWTZWJZVVFVVLVWBIU + WLUUHXOXGUXGVWLUYAVVGVVJVWEVWFUPVWGXDVWRVUHVVLVVNVWBUXBUWLXEXFXGVVOXHUXGV + WPVWCVWDXIVWQVWBXJVLXKXNUXOIUSUFZUTSZVWACUXIVVRJUXOUXISVWSVVTUTUXOUXIIUSV + AVBQVCXLUXHUXIFJUUCVTUUDXMAGUUEZKGUUFZULZUXAUXEXIADEGXPZGDUUIZVXAABDEGHIL + MNOUUGZDEGUUJZDGUUKWRZADKVXBKUXQCDXQZDRUXQCDXRXSZAVXDVXEVXBDSVXFVXGDGUULW + RUUMZUAKUWPGUUNVTXTAUBUWPUWTAUBUMZUWPTZVXLUWTTAVXMUPZVXLGUUOZUDZGUDZVXLUW + TAVXDVXLETZVXQVXLSVXMVXFUWPEVXLUWPVUCVVRUHZEFVUCULJVVRULUWPVXSULFVVQCVUCX + QZVUCPVVQCVUCXRXSJVWTCVVRXQZVVRQVWTCVVRXRXSFVUCJVVRUUSUUPMUUQUURZDEVXLGUU + TYAZAVXMVXPKTZVXQUWTTZVXNVXPDTZVXPUWLUSUFZUTSZVYDAEDVXOUVAZVXRVYFVXMAVXDE + DVXOXPVYIVXFDEGUVBEDVXOUVIWRVYBEDVXLVXOUVCYAZVXNVXPHUSUFZUTSZVXPIUSUFZUTS + ZVYHVXNVXPHUOUFZHUSUFZVYKUTVXNVXPVGTZUYEVYPVYKSVXNVXPUYBTVYQVXNVXPDUYBVYJ + LWEVXPVJUWLVIVLZAUYEVXMUYIVOZVXPHWGVTVXNVYOVUCTZVYPUTSZVXNVYOFTZVYTWUAUPV + XNWUBVXPIUOUFZJTZVXNVYOWUCUQZUWPTWUBWUDUPVXNVXLWUEUWPVXNVXQVXLWUEVYCVXNVY + FWUEURTZVXQWUESVYJVXNVYOVFTWUCVFTWUFVXNVXPHVXNVYQVXPVFTVYRVXPVMVLZVXNUYEU + YFVYSUYKVLVXNHVYSVQVRVXNVXPIWUGVXNUYGUYLAUYGVXMUYMVOZUYOVLVXNIWUHVQVRVYOW + UCVFVFWCVTUAVXPUXJWUEDURGUXBVXPSUXHVYOUXIWUCUXBVXPHUOVAUXBVXPIUOVAWAGBDUY + SYBUADUXJYBNBUADUYSUXJUYTUVDYEWDVTYCAVXMWPYDVYOWUCFJUVEYFZWLVVQWUACVYOVUC + FUXOVYOSVVPVYPUTUXOVYOHUSVAVBPVCYFXAYCVXNWUCIUSUFZVYMUTVXNVYQUYGWUJVYMSVY + RWUHVXPIWGVTVXNWUCVVRTZWUJUTSZVXNWUDWUKWULUPVXNWUBWUDWUIXAVWTWULCWUCVVRJU + XOWUCSVWSWUJUTUXOWUCIUSVAVBQVCYFXAYCVXNVYQVUPVWIVYLVYNUPVYHXDVYRAVUPVXMAH + UYIWJZVOAVWIVXMAIUYMWJZVOVXPHIUVFXOXGUXQVYHCVXPDKUXOVXPSUXPVYGUTUXOVXPUWL + USVAVBRVCXLAVYDVYEAVXAVXCVYDVYEXDVXHVXKKVXPGUVGVTUVJUVHYDUWAUVKUVLADEGUVM + ZKDULZKYGTZUWTKUIUJAVXDWUOVXFDEGUVNVLWUPAVXJUVOAKVXIYGRAUXQCDADUYBYGLAVJV + GTZVVGUYBYGTYHAHIWUMWUNUVPZVJUWLYIYJYKAUXQYLZCDAUXODTZUPZUXPVGTUTVGTZWUTW + VBUXPWVBUXOUWLWVAUXOVGTZAWVDUXOUYBDUXOVJUWLVILVKVEAVVGWVAWUSVOYMYNWVBYQUX + PUTYOVTXMYPYKZDEKGYGUVQXOUVRAUWPYGTZWUQUWRUWSXIAFYGTZJYGTZWVFAFVXTYGPAVVQ + CVUCAWURVUPVUCYGTYHWUMVJHYIYJAVVQYLZCVUCAUXOVUCTZUPZVVPVGTWVCWVIWVKVVPWVK + UXOHWVJWVDAUXOVJHVIVEAVUPWVJWUMVOYMYNUWBVVPUTYOUVSXMYPYKZAJVYAYGQAVWTCVVR + AWURVWIVVRYGTYHWUNVJIYIYJAVWTYLZCVVRAUXOVVRTZUPZVWSVGTWVCWVMWVOVWSWVOUXOI + WVNWVDAUXOVJIVIVEAVWIWVNWUNVOYMYNWVOYQVWSUTYOVTXMYPYKZFJUVTVTWVEUWPKUWCVT + XTAWVGWVHUWQUWKSWVLWVPFJUWDVTYCAVVMUWMUWHSAHIUYIUYMXCVVMUWMUXQCUYBXQZUCUD + UWHCUWLYRKWVQUCKVXIWVQRUXQCDUYBLUWEYEYSYTVLAUWNUWIUWOUWJUEAUYEUWNUWISUYIU + YEUWNVXTUCUDUWICHYRFVXTUCPYSYTVLAUYGUWOUWJSUYMUYGUWOVYAUCUDUWJCIYRJVYAUCQ + YSYTVLUWFUWG $. $} ${ @@ -138638,64 +138638,64 @@ given prime (or other positive integer) that divides the number. For nfel1 rspc sylc nnexpcld wn 1nn a1i wdc prmdc adantl ifcldadc nfcv nfov nfif id oveq12d ifbieq1d fvmptf syl2anc eqeltrd sylan2br nnmulcl seq3-1 eleq1 1nprm mtbiri iffalsed 1ex fvmpt ax-mp eqtrdi prmgt1 cz wb 1z prmz - clt zltnle sylancr mpbid 3eqtr4d wne wf pcmptcl simpld peano2nn ffvelrn - adantrr pccld nn0cnd ad2antrl simprr iftrued eqtrd 3eqtrd syl2an2r nnzd - nnz nnne0 jca syl3anc expr cdvds sylan9eq wo syl2an addid2d nfv csbeq1d - ad2antlr nfcvd csbiegf rspcv pcidlem oveq1 eqeq1d syl5ibrcom nnre ltp1d - breq1d mtbid eqeq2d nnuz eleqtrdi adantlr seq3p1 simprd ffvelrnda pcmul - cr prmnn nnred breqtrrd 3imtr4d simplrr necomd prmdvdsexpr necon3ad mpd - leidd iftrue breq2d mtbird mpbird iffalse exmiddc 3syl mpjaodan addid1d - pceq0 zltlen simprl nnleltp1 biantrud 3bitr4rd biimprd zdceq dcne sylib - mpjaod expcom a2d nnind mpcom ) GMNADGUEFOUFZUGZPQZDGUHUIZCRULZSZJADUAU - JZUWTUGZPQZDUXFUHUIZCRULZSZUKADOUWTUGZPQZDOUHUIZCRULZSZUKADUBUJZUWTUGZP - QZDUXQUHUIZCRULZSZUKADUXQOUMQZUWTUGZPQZDUYCUHUIZCRULZSZUKAUXEUKUAUBGUXF - OSZUXKUXPAUYIUXHUXMUXJUXOUYIUXGUXLDPUXFOUWTUNUOUYIUXIUXNCRUXFODUHUPUQUR - USUXFUXQSZUXKUYBAUYJUXHUXSUXJUYAUYJUXGUXRDPUXFUXQUWTUNUOUYJUXIUXTCRUXFU - XQDUHUPUQURUSUXFUYCSZUXKUYHAUYKUXHUYEUXJUYGUYKUXGUYDDPUXFUYCUWTUNUOUYKU - XIUYFCRUXFUYCDUHUPUQURUSUXFGSZUXKUXEAUYLUXHUXBUXJUXDUYLUXGUXADPUXFGUWTU - NUOUYLUXIUXCCRUXFGDUHUPUQURUSADOPQZRUXMUXOADUTNZUYMRSZKDVAVBZAUXLODPAUX - LOFUGZOAUCUDUEMFOAVDUCUJZOVEUGZNZAUYRMNZUYRFUGZMNZUYRVCAVUATZVUBUYRUTNZ - UYREUYRBVFZVGQZOULZMVUDVUAVUHMNVUBVUHSAVUAVHZVUDVUEVUGOMVUDVUETZUYRVUFV - UDVUAVUEVUIVIVUJVUEBVJNZEUTVKZVUFVJNZVUDVUEVHAVULVUAVUEIVLVUKVUMEUYRUTE - VUFVJEUYRBVMZVPEUJZUYRSZBVUFVJEUYRBVNZVOVQVRVSOMNZVUDVUEVTTWAWBVUAVUEWC - AUYRWDWEWFZEUYRVUOUTNZVUOBVGQZOULZVUHMFMEUYRWGZVUEEVUGOEUYRUTVVCVPEUYRV - UFVGVVCEVGWGZVUNWHEOWGZWIVUPVUTVUEVVAVUGOVUOUYRUTWSVUPVUOUYRBVUFVGVUPWJ - VUQWKWLHWMWNVUSWOWPZVUAUDUJZMNTZUYRVVGUEQMNZAUYRVVGWQZWEWRVURUYQOSWAEOV - VBOMFVUOOSZVUTVVAOVVKVUTOUTNWTVUOOUTWSXAXBHXCXDXEXFUOAUYNUXORSKUYNUXNCR - UYNODXLUIZUXNVTZDXGUYNOXHNDXHNZVVLVVMXIXJDXKZODXMXNXOXBVBXPUXQMNZAUYBUY - HAVVPUYBUYHUKZAVVPTZUYCDSZVVQUYCDXQZAVVPVVSVVQAVVPVVSTZTZUXSRSZUXSDUYCF - UGZPQZUMQZCSZUYBUYHVWBVWGVWCRVWEUMQZCSVWBVWHVWEDDCVGQZPQZCVWBVWEVWBVWEV - WBDVWDAUYNVWAKVIZAVVPVWDMNZVVSAMMFXRZUYCMNZVWLVVPAVWMMMUWTXRZABEFHIXSZX - TZUXQYAZMMUYCFYBZUUAZYCYDYEUUBVWBVWDVWIDPVWBVWDUYCUTNZUYCEUYCBVFZVGQZOU - LZVXCVWIVWBVWNVXDMNZVWDVXDSZVVPVWNAVVSVWRYFAVVPVXEVVSVVRVXAVXCOMVVRVXAT - ZUYCVXBVVPVWNAVXAVWRUUEVXGVXAVULVXBVJNZVVRVXAVHAVULVVPVXAIVLVUKVXHEUYCU - TEVXBVJEUYCBVMZVPVUOUYCSZBVXBVJEUYCBVNZVOVQZVRVSVURVVRVXAVTZTWAWBVVRVWN - VXAWCZVVPVWNAVWRWEZUYCWDZVBWFZYCEUYCVVBVXDMFMEUYCWGZVXAEVXCOVXAEUUCEUYC - VXBVGVXRVVDVXIWHVVEWIVXJVUTVXAVVAVXCOVUOUYCUTWSVXJVUOUYCBVXBVGVXJWJVXKW - KWLHWMZWNVWBVXAVXCOVWBUYCDUTAVVPVVSYGZVWKWOYHVWBUYCDVXBCVGVXTVWBVXBEDBV - FZCVWBEUYCDBVXTUUDVWBUYNVYACSVWKEDBCUTUYNECUUFLUUGVBYIWKYJUOAUYNVWACVJN - ZVWJCSKAVYBVWAAUYNVULVYBKIVUKVYBEDUTVUODSBCVJLVOUUHVRVICDUUIYKYJVWCVWFV - WHCUXSRVWEUMUUJUUKUULVWBUYARUXSVWBUXTCRVWBUYCUXQUHUIZUXTVVPVYCVTZAVVSVV - PUXQUYCXLUIZVYDVVPUXQUXQUUMUUNVVPUXQXHNUYCXHNZVYEVYDXIUXQYMVVPUYCVWRYLZ - UXQUYCXMWNXOYFVWBUYCDUXQUHVXTUUOUUPXBUUQVWBUYEVWFUYGCAVVPUYEVWFSZVVSVVR - UYEDUXRVWDUEQZPQZVWFVVRUYDVYIDPVVRUCUDUEMFOUXQVVRUXQMUYSAVVPVHUURUUSAUY - TVUCVVPVVFUUTVVHVVIVVRVVJWEUVAUOVVRUYNUXRXHNZUXRRXQZTZVWDXHNZVWDRXQZTZV - YJVWFSAUYNVVPKVIZVVRUXRMNZVYMAMMUXQUWTAVWMVWOVWPUVBUVCZVYRVYKVYLUXRYMUX - RYNYOVBVVRVWLVYPVWTVWLVYNVYOVWDYMVWDYNYOVBUXRVWDDUVDYPYIZYCVWBUYFCRVWBD - DUYCUHVWBDADUVENVWAADAUYNDMNZKDUVFVBZUVGVIUVOVXTUVHYHURUVIYQAVVPVVTVVQA - VVPVVTTZTZUYHUYBWUDUYEUXSUYGUYAWUDUYEVWFUXSRUMQUXSAVVPVYHVVTVYTYCWUDVWE - RUXSUMWUDVXAVWERSZVXMWUDVXATZWUEDVWDYRUIZVTZWUFWUGDVXCYRUIZWUFDUYCXQWUI - VTWUFUYCDAVVPVVTVXAUVJUVKWUFWUIDUYCWUFUYNVXAVXHWUIDUYCSUKAUYNWUCVXAKVLZ - WUDVXAVHZWUFVXAVULVXHWUKAVULWUCVXAIVLVXLVRDUYCVXBUVLYPUVMUVNWUFVWDVXCDY - RWUDVXAVWDVXDVXCWUDVWNVXEVXFVVPVWNAVVTVWRYFZAVVPVXEVVTVXQYCVXSWNZVXAVXC - OUVPYSUVQUVRWUFUYNVWLWUEWUHXIWUJWUDVWLVXAAVWMWUCVWNVWLVWQWULVWSYKVIDVWD - UWEWNUVSWUDVXMTZVWEUYMRWUNVWDODPWUDVXMVWDVXDOWUMVXAVXCOUVTYSUOAUYOWUCVX - MUYPVLYIWUDVWNVXNVXAVXMYTWULVXPVXAUWAUWBUWCUOWUDUXSWUDUXSWUDDUXRAUYNWUC - KVIZAVVPVYRVVTVYSYCYDYEUWDYJWUDUYFUXTCRWUDDUYCXLUIZUYFVVTTZUXTUYFWUDVVN - VYFWUPWUQXIWUDUYNVVNWUOVVOVBVVPVYFAVVTVYGYFDUYCUWFWNAWUAWUCVVPUXTWUPXIW - UBAVVPVVTUWGDUXQUWHYKWUDVVTUYFAVVPVVTYGUWIUWJUQURUWKYQVVRVVSWCZVVSVVTYT - VVRVYFVVNWURVVRUYCVXOYLVVRUYNVVNVYQVVOVBUYCDUWLWNUYCDUWMUWNUWOUWPUWQUWR - UWS $. + clt zltnle sylancr mpbid 3eqtr4d wne wf pcmptcl simpld peano2nn adantrr + ffvelcdm pccld nn0cnd ad2antrl simprr iftrued eqtrd 3eqtrd syl2an2r nnz + nnzd nnne0 jca syl3anc expr cdvds sylan9eq wo syl2an ad2antlr nfv nfcvd + addid2d csbeq1d csbiegf rspcv oveq1 eqeq1d syl5ibrcom nnre ltp1d breq1d + pcidlem mtbid eqeq2d nnuz eleqtrdi adantlr seq3p1 ffvelrnda pcmul prmnn + simprd nnred leidd breqtrrd 3imtr4d simplrr necomd prmdvdsexpr necon3ad + cr mpd iftrue breq2d mtbird pceq0 iffalse exmiddc 3syl mpjaodan addid1d + mpbird zltlen simprl nnleltp1 biantrud 3bitr4rd zdceq dcne sylib mpjaod + biimprd expcom a2d nnind mpcom ) GMNADGUEFOUFZUGZPQZDGUHUIZCRULZSZJADUA + UJZUWTUGZPQZDUXFUHUIZCRULZSZUKADOUWTUGZPQZDOUHUIZCRULZSZUKADUBUJZUWTUGZ + PQZDUXQUHUIZCRULZSZUKADUXQOUMQZUWTUGZPQZDUYCUHUIZCRULZSZUKAUXEUKUAUBGUX + FOSZUXKUXPAUYIUXHUXMUXJUXOUYIUXGUXLDPUXFOUWTUNUOUYIUXIUXNCRUXFODUHUPUQU + RUSUXFUXQSZUXKUYBAUYJUXHUXSUXJUYAUYJUXGUXRDPUXFUXQUWTUNUOUYJUXIUXTCRUXF + UXQDUHUPUQURUSUXFUYCSZUXKUYHAUYKUXHUYEUXJUYGUYKUXGUYDDPUXFUYCUWTUNUOUYK + UXIUYFCRUXFUYCDUHUPUQURUSUXFGSZUXKUXEAUYLUXHUXBUXJUXDUYLUXGUXADPUXFGUWT + UNUOUYLUXIUXCCRUXFGDUHUPUQURUSADOPQZRUXMUXOADUTNZUYMRSZKDVAVBZAUXLODPAU + XLOFUGZOAUCUDUEMFOAVDUCUJZOVEUGZNZAUYRMNZUYRFUGZMNZUYRVCAVUATZVUBUYRUTN + ZUYREUYRBVFZVGQZOULZMVUDVUAVUHMNVUBVUHSAVUAVHZVUDVUEVUGOMVUDVUETZUYRVUF + VUDVUAVUEVUIVIVUJVUEBVJNZEUTVKZVUFVJNZVUDVUEVHAVULVUAVUEIVLVUKVUMEUYRUT + EVUFVJEUYRBVMZVPEUJZUYRSZBVUFVJEUYRBVNZVOVQVRVSOMNZVUDVUEVTTWAWBVUAVUEW + CAUYRWDWEWFZEUYRVUOUTNZVUOBVGQZOULZVUHMFMEUYRWGZVUEEVUGOEUYRUTVVCVPEUYR + VUFVGVVCEVGWGZVUNWHEOWGZWIVUPVUTVUEVVAVUGOVUOUYRUTWSVUPVUOUYRBVUFVGVUPW + JVUQWKWLHWMWNVUSWOWPZVUAUDUJZMNTZUYRVVGUEQMNZAUYRVVGWQZWEWRVURUYQOSWAEO + VVBOMFVUOOSZVUTVVAOVVKVUTOUTNWTVUOOUTWSXAXBHXCXDXEXFUOAUYNUXORSKUYNUXNC + RUYNODXLUIZUXNVTZDXGUYNOXHNDXHNZVVLVVMXIXJDXKZODXMXNXOXBVBXPUXQMNZAUYBU + YHAVVPUYBUYHUKZAVVPTZUYCDSZVVQUYCDXQZAVVPVVSVVQAVVPVVSTZTZUXSRSZUXSDUYC + FUGZPQZUMQZCSZUYBUYHVWBVWGVWCRVWEUMQZCSVWBVWHVWEDDCVGQZPQZCVWBVWEVWBVWE + VWBDVWDAUYNVWAKVIZAVVPVWDMNZVVSAMMFXRZUYCMNZVWLVVPAVWMMMUWTXRZABEFHIXSZ + XTZUXQYAZMMUYCFYCZUUAZYBYDYEUUEVWBVWDVWIDPVWBVWDUYCUTNZUYCEUYCBVFZVGQZO + ULZVXCVWIVWBVWNVXDMNZVWDVXDSZVVPVWNAVVSVWRYFAVVPVXEVVSVVRVXAVXCOMVVRVXA + TZUYCVXBVVPVWNAVXAVWRUUBVXGVXAVULVXBVJNZVVRVXAVHAVULVVPVXAIVLVUKVXHEUYC + UTEVXBVJEUYCBVMZVPVUOUYCSZBVXBVJEUYCBVNZVOVQZVRVSVURVVRVXAVTZTWAWBVVRVW + NVXAWCZVVPVWNAVWRWEZUYCWDZVBWFZYBEUYCVVBVXDMFMEUYCWGZVXAEVXCOVXAEUUCEUY + CVXBVGVXRVVDVXIWHVVEWIVXJVUTVXAVVAVXCOVUOUYCUTWSVXJVUOUYCBVXBVGVXJWJVXK + WKWLHWMZWNVWBVXAVXCOVWBUYCDUTAVVPVVSYGZVWKWOYHVWBUYCDVXBCVGVXTVWBVXBEDB + VFZCVWBEUYCDBVXTUUFVWBUYNVYACSVWKEDBCUTUYNECUUDLUUGVBYIWKYJUOAUYNVWACVJ + NZVWJCSKAVYBVWAAUYNVULVYBKIVUKVYBEDUTVUODSBCVJLVOUUHVRVICDUUOYKYJVWCVWF + VWHCUXSRVWEUMUUIUUJUUKVWBUYARUXSVWBUXTCRVWBUYCUXQUHUIZUXTVVPVYCVTZAVVSV + VPUXQUYCXLUIZVYDVVPUXQUXQUULUUMVVPUXQXHNUYCXHNZVYEVYDXIUXQYLVVPUYCVWRYM + ZUXQUYCXMWNXOYFVWBUYCDUXQUHVXTUUNUUPXBUUQVWBUYEVWFUYGCAVVPUYEVWFSZVVSVV + RUYEDUXRVWDUEQZPQZVWFVVRUYDVYIDPVVRUCUDUEMFOUXQVVRUXQMUYSAVVPVHUURUUSAU + YTVUCVVPVVFUUTVVHVVIVVRVVJWEUVAUOVVRUYNUXRXHNZUXRRXQZTZVWDXHNZVWDRXQZTZ + VYJVWFSAUYNVVPKVIZVVRUXRMNZVYMAMMUXQUWTAVWMVWOVWPUVEUVBZVYRVYKVYLUXRYLU + XRYNYOVBVVRVWLVYPVWTVWLVYNVYOVWDYLVWDYNYOVBUXRVWDDUVCYPYIZYBVWBUYFCRVWB + DDUYCUHVWBDADUVNNVWAADAUYNDMNZKDUVDVBZUVFVIUVGVXTUVHYHURUVIYQAVVPVVTVVQ + AVVPVVTTZTZUYHUYBWUDUYEUXSUYGUYAWUDUYEVWFUXSRUMQUXSAVVPVYHVVTVYTYBWUDVW + ERUXSUMWUDVXAVWERSZVXMWUDVXATZWUEDVWDYRUIZVTZWUFWUGDVXCYRUIZWUFDUYCXQWU + IVTWUFUYCDAVVPVVTVXAUVJUVKWUFWUIDUYCWUFUYNVXAVXHWUIDUYCSUKAUYNWUCVXAKVL + ZWUDVXAVHZWUFVXAVULVXHWUKAVULWUCVXAIVLVXLVRDUYCVXBUVLYPUVMUVOWUFVWDVXCD + YRWUDVXAVWDVXDVXCWUDVWNVXEVXFVVPVWNAVVTVWRYFZAVVPVXEVVTVXQYBVXSWNZVXAVX + COUVPYSUVQUVRWUFUYNVWLWUEWUHXIWUJWUDVWLVXAAVWMWUCVWNVWLVWQWULVWSYKVIDVW + DUVSWNUWEWUDVXMTZVWEUYMRWUNVWDODPWUDVXMVWDVXDOWUMVXAVXCOUVTYSUOAUYOWUCV + XMUYPVLYIWUDVWNVXNVXAVXMYTWULVXPVXAUWAUWBUWCUOWUDUXSWUDUXSWUDDUXRAUYNWU + CKVIZAVVPVYRVVTVYSYBYDYEUWDYJWUDUYFUXTCRWUDDUYCXLUIZUYFVVTTZUXTUYFWUDVV + NVYFWUPWUQXIWUDUYNVVNWUOVVOVBVVPVYFAVVTVYGYFDUYCUWFWNAWUAWUCVVPUXTWUPXI + WUBAVVPVVTUWGDUXQUWHYKWUDVVTUYFAVVPVVTYGUWIUWJUQURUWOYQVVRVVSWCZVVSVVTY + TVVRVYFVVNWURVVRUYCVXOYMVVRUYNVVNVYQVVOVBUYCDUWKWNUYCDUWLUWMUWNUWPUWQUW + RUWS $. pcmpt2.6 $e |- ( ph -> M e. ( ZZ>= ` N ) ) $. $( Dividing two prime count maps yields a number with all dividing primes @@ -138755,14 +138755,14 @@ given prime (or other positive integer) that divides the number. For ( vp cn wcel wceq cv cpc co cprime wa wbr cc0 cn0 ancoms ralrimiva adantl wral cmul c1 cseq cfv cle cif pccl simpr simpl oveq1 pcmpt iftrue iffalse wn cdvds cz wi dvdsle sylan con3dimp wb pceq0 adantr mpbird eqtr4d wdc wo - prmz nnzd zdcle syl2anc exmiddc syl mpjaodan eqtrd pcmptcl simprd ffvelrn - wf mpancom nnnn0d nnnn0 pc11 ) CFGZCUABUBUCZUDZCHZEIZWFJKZWHCJKZHZELTZWDW - KELWHLGZWDWKWMWDMZWIWHCUENZWJOUFZWJWNAIZCJKZWJWHABCDWDWRPGZALTWMWDWSALWQL - GWDWSWQCUGQRZSWMWDUHZWMWDUIWQWHCJUJUKWNWOWPWJHZWOUNZWOXBWNWOWJOULSWNXCMZW - POWJXCWPOHWNWOWJOUMSXDWJOHZWHCUONZUNZWNXFWOWMWHUPGZWDXFWOUQWHVHZWHCURUSUT - WNXEXGVAXCWHCVBVCVDVEWNWOVFZWOXCVGWNXHCUPGXJWMXHWDXIVCWNCXAVIWHCVJVKWOVLV - MVNVOQRWDWFPGCPGWGWLVAWDWFFFWEVSZWDWFFGWDFFBVSXKWDWRABDWTVPVQFFCWEVRVTWAC - WBWFCEWCVKVD $. + prmz nnzd zdcle syl2anc exmiddc mpjaodan eqtrd wf pcmptcl simprd ffvelcdm + syl mpancom nnnn0d nnnn0 pc11 ) CFGZCUABUBUCZUDZCHZEIZWFJKZWHCJKZHZELTZWD + WKELWHLGZWDWKWMWDMZWIWHCUENZWJOUFZWJWNAIZCJKZWJWHABCDWDWRPGZALTWMWDWSALWQ + LGWDWSWQCUGQRZSWMWDUHZWMWDUIWQWHCJUJUKWNWOWPWJHZWOUNZWOXBWNWOWJOULSWNXCMZ + WPOWJXCWPOHWNWOWJOUMSXDWJOHZWHCUONZUNZWNXFWOWMWHUPGZWDXFWOUQWHVHZWHCURUSU + TWNXEXGVAXCWHCVBVCVDVEWNWOVFZWOXCVGWNXHCUPGXJWMXHWDXIVCWNCXAVIWHCVJVKWOVL + VSVMVNQRWDWFPGCPGWGWLVAWDWFFFWEVOZWDWFFGWDFFBVOXKWDWRABDWTVPVQFFCWEVRVTWA + CWBWFCEWCVKVD $. $} ${ @@ -144606,29 +144606,29 @@ everywhere defined internal operation (see ~ mndcl ), whose operation is Mario Carneiro, 7-Nov-2015.) $) mhmpropd $p |- ( ph -> ( J MndHom K ) = ( L MndHom M ) ) $= ( co wcel wa cfv wceq vf vw vz cmhm cmnd cbs cv wf cplusg wral c0g w3a wb - fveq2d adantlr ffvelrn anim12dan ralrimivva oveq1 eqeq12d oveq2 cbvral2vw - sylib rspc2va syl2anr anassrs 2ralbidva adantrl raleqbi1dv adantr 3bitr3d - raleq simprll mndpropd grpidpropdg simprlr anbi12d pm5.32da feq23d anbi1d - syl mpbid 3anass 3bitr4g bitrd eqid ismhm eqrdv ) AUAFGUDPZHIUDPZAFUEQZGU - EQZRZFUFSZGUFSZUAUGZUHZBUGZCUGZFUISZPZWPSZWRWPSZWSWPSZGUISZPZTZCWNUJZBWNU - JZFUKSZWPSZGUKSZTZULZRZHUEQZIUEQZRZHUFSZIUFSZWPUHZWRWSHUISZPZWPSZXCXDIUIS - ZPZTZCXSUJZBXSUJZHUKSZWPSZIUKSZTZULZRZWPWIQWPWJQAXOWMYNRYOAWMXNYNAWMRZWQX - IXMRZRZYAYIYMRZRZXNYNYPDEWPUHZYQRUUAYSRYRYTYPUUAYQYSAWMUUAYQYSUMAWMUUARZR - ZXIYIXMYMUUCXGCDUJZBDUJZYGCDUJZBDUJZXIYIAUUAUUEUUGUMWMAUUARZXGYGBCDDUUHWR - DQZWSDQZRZRXBYDXFYFAUUKXBYDTUUAAUUKRXAYCWPNUNUOAUUAUUKXFYFTZUUAUUKRXCEQZX - DEQZRUBUGZUCUGZXEPZUUOUUPYEPZTZUCEUJUBEUJZUULAUUAUUIUUMUUJUUNDEWRWPUPDEWS - WPUPUQAWRWSXEPZWRWSYEPZTZCEUJBEUJUUTAUVCBCEEOURUVCUUSUUOWSXEPZUUOWSYEPZTB - CUBUCEEWRUUOTUVAUVDUVBUVEWRUUOWSXEUSWRUUOWSYEUSUTWSUUPTUVDUUQUVEUURWSUUPU - UOXEVAWSUUPUUOYEVAUTVBVCUUSUULXCUUPXEPZXCUUPYEPZTUBUCXCXDEEUUOXCTUUQUVFUU - RUVGUUOXCUUPXEUSUUOXCUUPYEUSUTUUPXDTUVFXFUVGYFUUPXDXCXEVAUUPXDXCYEVAUTVDV - EVFUTVGVHAUUEXIUMZUUBADWNTZUVHJUUDXHBDWNXGCDWNVLVIWAVJAUUGYIUMZUUBADXSTZU - VJLUUFYHBDXSYGCDXSVLVIWAVJVKUUCXKYKXLYLUUCXJYJWPUUCBCDFHUEUEAUVIUUBJVJAUV - KUUBLVJAWKWLUUAVMZUUCWKXPUVLAWKXPUMUUBABCDFHJLNVNZVJWBAUUKXAYCTUUBNUOVOUN - UUCBCEGIUEUEAEWOTUUBKVJAEXTTUUBMVJAWKWLUUAVPZUUCWLXQUVNAWLXQUMUUBABCEGIKM - OVNZVJWBAWREQWSEQRUVCUUBOUOVOUTVQVFVRYPUUAWQYQAUUAWQUMWMADEWNWOWPJKVSVJVT - YPUUAYAYSAUUAYAUMWMADEXSXTWPLMVSVJVTVKWQXIXMWCYAYIYMWCWDVRAWMXRYNAWKXPWLX - QUVMUVOVQVTWEBCWNWOWTXEFGWPXLXJWNWFWOWFWTWFXEWFXJWFXLWFWGBCXSXTYBYEHIWPYL - YJXSWFXTWFYBWFYEWFYJWFYLWFWGWDWH $. + adantlr ffvelcdm anim12dan ralrimivva oveq1 eqeq12d oveq2 cbvral2vw sylib + fveq2d rspc2va syl2anr anassrs 2ralbidva adantrl raleq raleqbi1dv 3bitr3d + adantr simprll mndpropd mpbid grpidpropdg simprlr anbi12d pm5.32da feq23d + syl anbi1d 3anass 3bitr4g bitrd eqid ismhm eqrdv ) AUAFGUDPZHIUDPZAFUEQZG + UEQZRZFUFSZGUFSZUAUGZUHZBUGZCUGZFUISZPZWPSZWRWPSZWSWPSZGUISZPZTZCWNUJZBWN + UJZFUKSZWPSZGUKSZTZULZRZHUEQZIUEQZRZHUFSZIUFSZWPUHZWRWSHUISZPZWPSZXCXDIUI + SZPZTZCXSUJZBXSUJZHUKSZWPSZIUKSZTZULZRZWPWIQWPWJQAXOWMYNRYOAWMXNYNAWMRZWQ + XIXMRZRZYAYIYMRZRZXNYNYPDEWPUHZYQRUUAYSRYRYTYPUUAYQYSAWMUUAYQYSUMAWMUUARZ + RZXIYIXMYMUUCXGCDUJZBDUJZYGCDUJZBDUJZXIYIAUUAUUEUUGUMWMAUUARZXGYGBCDDUUHW + RDQZWSDQZRZRXBYDXFYFAUUKXBYDTUUAAUUKRXAYCWPNVCUNAUUAUUKXFYFTZUUAUUKRXCEQZ + XDEQZRUBUGZUCUGZXEPZUUOUUPYEPZTZUCEUJUBEUJZUULAUUAUUIUUMUUJUUNDEWRWPUODEW + SWPUOUPAWRWSXEPZWRWSYEPZTZCEUJBEUJUUTAUVCBCEEOUQUVCUUSUUOWSXEPZUUOWSYEPZT + BCUBUCEEWRUUOTUVAUVDUVBUVEWRUUOWSXEURWRUUOWSYEURUSWSUUPTUVDUUQUVEUURWSUUP + UUOXEUTWSUUPUUOYEUTUSVAVBUUSUULXCUUPXEPZXCUUPYEPZTUBUCXCXDEEUUOXCTUUQUVFU + URUVGUUOXCUUPXEURUUOXCUUPYEURUSUUPXDTUVFXFUVGYFUUPXDXCXEUTUUPXDXCYEUTUSVD + VEVFUSVGVHAUUEXIUMZUUBADWNTZUVHJUUDXHBDWNXGCDWNVIVJWAVLAUUGYIUMZUUBADXSTZ + UVJLUUFYHBDXSYGCDXSVIVJWAVLVKUUCXKYKXLYLUUCXJYJWPUUCBCDFHUEUEAUVIUUBJVLAU + VKUUBLVLAWKWLUUAVMZUUCWKXPUVLAWKXPUMUUBABCDFHJLNVNZVLVOAUUKXAYCTUUBNUNVPV + CUUCBCEGIUEUEAEWOTUUBKVLAEXTTUUBMVLAWKWLUUAVQZUUCWLXQUVNAWLXQUMUUBABCEGIK + MOVNZVLVOAWREQWSEQRUVCUUBOUNVPUSVRVFVSYPUUAWQYQAUUAWQUMWMADEWNWOWPJKVTVLW + BYPUUAYAYSAUUAYAUMWMADEXSXTWPLMVTVLWBVKWQXIXMWCYAYIYMWCWDVSAWMXRYNAWKXPWL + XQUVMUVOVRWBWEBCWNWOWTXEFGWPXLXJWNWFWOWFWTWFXEWFXJWFXLWFWGBCXSXTYBYEHIWPY + LYJXSWFXTWFYBWFYEWFYJWFYLWFWGWDWH $. $} ${ @@ -149399,39 +149399,39 @@ F C_ ( CC X. X ) ) $= upxp $p |- ( ( A e. D /\ F : A --> B /\ G : A --> C ) -> E! h ( h : A --> ( B X. C ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) ) $= ( vx wcel wceq cfv cvv wa wfn c1st c2nd vz wf w3a cxp ccom weu cop mptexg - cmpt eueq sylib 3ad2ant1 ffn adantl wral ffvelrn opelxpi syl2an ralrimiva - anandirs 3adant1 eqid fmpt ffnd adantr xpss sselid 3ad2antl1 adantll cres - cv fveq1 coeq1i fveq1i eqtrdi 3ad2ant2 ad2antlr simpr1 fvco3 sylan fvresd - 3eqtrrd 3ad2ant3 eqopi syl12anc fveq2 opeq12d eqeltrrd fvmptd3 eqfnfvd ex - simpr eqtr4d crn wss wfo fo1st fofn ax-mp fnssres mp2an frnd fnco mp3an2i - ssv simpl2 ffvelrnd simpl3 opelxpd fveq2d 3adantl1 op1stg syl2anc eqtr4di - eqtrd fo2nd op2ndg 3jca feq1 coeq2 eqeq2d syl5ibrcom impbid eubidv mpbird - 3anbi123d ) ADMZABHUBZACIUBZUCZABCUDZGVKZUBZHEYLUEZNZIFYLUEZNZUCZGUFYLLAL - VKZHOZYSIOZUGZUIZNZGUFZYGYHUUEYIYGUUCPMUUELAUUBDUHGUUCUJUKULYJYRUUDGYJYRU - UDYJYRUUDYJYRQZUAAYLUUCYRYLARZYJYMYOUUGYQAYKYLUMULUNYJUUCARZYRYJAYKUUCYJU - UBYKMZLAUOZAYKUUCUBZYHYIUUJYGYHYIQUUILAYHYIYSAMZUUIYHUULQYTBMUUACMUUIYIUU - LQABYSHUPACYSIUPYTUUABCUQURUTUSVALAYKUUBUUCUUCVBZVCUKZVDZVEUUFUAVKZAMZQZU - UPYLOZUUPHOZUUPIOZUGZUUPUUCOZUURUUSPPUDZMZUUSSOZUUTNUUSTOZUVANUUSUVBNYRUU - QUVEYJYMYOUUQUVEYQYMUUQQYKUVDUUSBCVFAYKUUPYLUPZVGVHVIUURUUTUUPSYKVJZYLUEZ - OZUUSUVIOZUVFYRUUTUVKNZYJUUQYOYMUVMYQYOUUTUUPYNOUVKUUPHYNVLUUPYNUVJEUVIYL - JVMVNVOVPVQUUFYMUUQUVKUVLNYJYMYOYQVRZAYKUUPUVIYLVSVTUURUUSYKSYRUUQUUSYKMZ - YJYMYOUUQUVOYQUVHVHVIZWAWBUURUVAUUPTYKVJZYLUEZOZUUSUVQOZUVGYRUVAUVSNZYJUU - QYQYMUWAYOYQUVAUUPYPOUVSUUPIYPVLUUPYPUVRFUVQYLKVMVNVOWCVQUUFYMUUQUVSUVTNU - VNAYKUUPUVQYLVSVTUURUUSYKTUVPWAWBUUSUUTUVAPPWDWEZUURLUUPUUBUVBAUUCYKUUMYS - UUPNYTUUTUUAUVAYSUUPHWFYSUUPIWFWGZUUFUUQWLUURUUSUVBYKUWBUVPWHWIWMWJWKYJYR - UUDUUKHEUUCUEZNZIFUUCUEZNZUCYJUUKUWEUWGUUNYJHUVIUUCUEZUWDYJUAAHUWHYHYGHAR - YIABHUMVPUVIYKRZYJUUHUUCWNYKWOZUWHARSPRZYKPWOZUWIPPSWPUWKWQPPSWRWSYKXEZPY - KSWTXAUUOYJAYKUUCUUNXBZYKAUVIUUCXCXDYJUUQQZUUPUWHOZUVCUVIOZUVBUVIOZUUTYJU - UKUUQUWPUWQNUUNAYKUUPUVIUUCVSVTUWOUVCUVBUVIUWOLUUPUUBUVBAUUCYKUUMUWCYJUUQ - WLZUWOUUTUVABCUWOABUUPHYGYHYIUUQXFUWSXGZUWOACUUPIYGYHYIUUQXHUWSXGZXIWIZXJ - UWOUWRUVBSOZUUTUWOUVBYKSYHYIUUQUVBYKMZYGYHYIUUQUXDYHUUQQUUTBMZUVACMZUXDYI - UUQQABUUPHUPACUUPIUPUUTUVABCUQURUTXKZWAUWOUXEUXFUXCUUTNUWTUXAUUTUVABCXLXM - XOWBWJEUVIUUCJVMXNYJIUVQUUCUEZUWFYJUAAIUXHYIYGIARYHACIUMWCUVQYKRZYJUUHUWJ - UXHARTPRZUWLUXIPPTWPUXJXPPPTWRWSUWMPYKTWTXAUUOUWNYKAUVQUUCXCXDUWOUUPUXHOZ - UVCUVQOZUVBUVQOZUVAYJUUKUUQUXKUXLNUUNAYKUUPUVQUUCVSVTUWOUVCUVBUVQUXBXJUWO - UXMUVBTOZUVAUWOUVBYKTUXGWAUWOUXEUXFUXNUVANUWTUXAUUTUVABCXQXMXOWBWJFUVQUUC - KVMXNXRUUDYMUUKYOUWEYQUWGAYKYLUUCXSUUDYNUWDHYLUUCEXTYAUUDYPUWFIYLUUCFXTYA - YFYBYCYDYE $. + cmpt eueq sylib 3ad2ant1 ffn adantl wral ffvelcdm opelxpi syl2an anandirs + cv ralrimiva 3adant1 eqid fmpt ffnd adantr sselid 3ad2antl1 adantll fveq1 + xpss cres coeq1i fveq1i eqtrdi 3ad2ant2 simpr1 fvco3 sylan fvresd 3eqtrrd + ad2antlr 3ad2ant3 eqopi syl12anc fveq2 opeq12d eqeltrrd fvmptd3 eqtr4d ex + simpr eqfnfvd crn wss wfo fo1st fofn ax-mp ssv fnssres mp2an frnd mp3an2i + fnco simpl2 ffvelrnd simpl3 opelxpd fveq2d 3adantl1 syl2anc eqtrd eqtr4di + op1stg fo2nd op2ndg 3jca feq1 coeq2 eqeq2d 3anbi123d impbid eubidv mpbird + syl5ibrcom ) ADMZABHUBZACIUBZUCZABCUDZGUTZUBZHEYLUEZNZIFYLUEZNZUCZGUFYLLA + LUTZHOZYSIOZUGZUIZNZGUFZYGYHUUEYIYGUUCPMUUELAUUBDUHGUUCUJUKULYJYRUUDGYJYR + UUDYJYRUUDYJYRQZUAAYLUUCYRYLARZYJYMYOUUGYQAYKYLUMULUNYJUUCARZYRYJAYKUUCYJ + UUBYKMZLAUOZAYKUUCUBZYHYIUUJYGYHYIQUUILAYHYIYSAMZUUIYHUULQYTBMUUACMUUIYIU + ULQABYSHUPACYSIUPYTUUABCUQURUSVAVBLAYKUUBUUCUUCVCZVDUKZVEZVFUUFUAUTZAMZQZ + UUPYLOZUUPHOZUUPIOZUGZUUPUUCOZUURUUSPPUDZMZUUSSOZUUTNUUSTOZUVANUUSUVBNYRU + UQUVEYJYMYOUUQUVEYQYMUUQQYKUVDUUSBCVKAYKUUPYLUPZVGVHVIUURUUTUUPSYKVLZYLUE + ZOZUUSUVIOZUVFYRUUTUVKNZYJUUQYOYMUVMYQYOUUTUUPYNOUVKUUPHYNVJUUPYNUVJEUVIY + LJVMVNVOVPWBUUFYMUUQUVKUVLNYJYMYOYQVQZAYKUUPUVIYLVRVSUURUUSYKSYRUUQUUSYKM + ZYJYMYOUUQUVOYQUVHVHVIZVTWAUURUVAUUPTYKVLZYLUEZOZUUSUVQOZUVGYRUVAUVSNZYJU + UQYQYMUWAYOYQUVAUUPYPOUVSUUPIYPVJUUPYPUVRFUVQYLKVMVNVOWCWBUUFYMUUQUVSUVTN + UVNAYKUUPUVQYLVRVSUURUUSYKTUVPVTWAUUSUUTUVAPPWDWEZUURLUUPUUBUVBAUUCYKUUMY + SUUPNYTUUTUUAUVAYSUUPHWFYSUUPIWFWGZUUFUUQWLUURUUSUVBYKUWBUVPWHWIWJWMWKYJY + RUUDUUKHEUUCUEZNZIFUUCUEZNZUCYJUUKUWEUWGUUNYJHUVIUUCUEZUWDYJUAAHUWHYHYGHA + RYIABHUMVPUVIYKRZYJUUHUUCWNYKWOZUWHARSPRZYKPWOZUWIPPSWPUWKWQPPSWRWSYKWTZP + YKSXAXBUUOYJAYKUUCUUNXCZYKAUVIUUCXEXDYJUUQQZUUPUWHOZUVCUVIOZUVBUVIOZUUTYJ + UUKUUQUWPUWQNUUNAYKUUPUVIUUCVRVSUWOUVCUVBUVIUWOLUUPUUBUVBAUUCYKUUMUWCYJUU + QWLZUWOUUTUVABCUWOABUUPHYGYHYIUUQXFUWSXGZUWOACUUPIYGYHYIUUQXHUWSXGZXIWIZX + JUWOUWRUVBSOZUUTUWOUVBYKSYHYIUUQUVBYKMZYGYHYIUUQUXDYHUUQQUUTBMZUVACMZUXDY + IUUQQABUUPHUPACUUPIUPUUTUVABCUQURUSXKZVTUWOUXEUXFUXCUUTNUWTUXAUUTUVABCXOX + LXMWAWMEUVIUUCJVMXNYJIUVQUUCUEZUWFYJUAAIUXHYIYGIARYHACIUMWCUVQYKRZYJUUHUW + JUXHARTPRZUWLUXIPPTWPUXJXPPPTWRWSUWMPYKTXAXBUUOUWNYKAUVQUUCXEXDUWOUUPUXHO + ZUVCUVQOZUVBUVQOZUVAYJUUKUUQUXKUXLNUUNAYKUUPUVQUUCVRVSUWOUVCUVBUVQUXBXJUW + OUXMUVBTOZUVAUWOUVBYKTUXGVTUWOUXEUXFUXNUVANUWTUXAUUTUVABCXQXLXMWAWMFUVQUU + CKVMXNXRUUDYMUUKYOUWEYQUWGAYKYLUUCXSUUDYNUWDHYLUUCEXTYAUUDYPUWFIYLUUCFXTY + AYBYFYCYDYE $. $} ${ @@ -149483,39 +149483,39 @@ F C_ ( CC X. X ) ) $= E! h e. ( U Cn T ) ( F = ( P o. h ) /\ G = ( Q o. h ) ) ) $= ( wcel cvv vx vz ccn co ccom wceq wex wmo wreu cuni cfv cop cmpt ctx eqid wa cv txcnmpt oveq2i eleqtrrdi wf cnf c1st cxp wfn ffn adantr crn wss wfo - cres fo1st ax-mp ssv fnssres mp2an ffvelrn opelxpi syl2an anandirs fmpttd - fofn ffnd frnd fnco mp3an2i fvco3 sylan fveq2 opeq12d simpr simpll simplr - ffvelrnd opelxpd fvmptd3 fveq2d fvresd op1stg syl2anc eqtrd 3eqtrrd eqtri - eqfnfvd reseq2i coeq1i eqtr4di c2nd adantl fo2nd op2ndg jca32 eleq1 coeq2 - eqeq2d anbi12d spcegv sylc w3a wal ctop cntop2 unieqi txuni eqtr4id feq3d - syl5ib anim1d 3anass syl6ibr alrimiv weu cntop1 uniexg syl upxp syl2an3an - wi eumo moim df-reu eu5 bitri sylanbrc ) HFCUCUDSZIFDUCUDSZUPZGUQZFEUCUDZ - SZHAUUHUEZUFZIBUUHUEZUFZUPZUPZGUGZUUPGUHZUUOGUUIUIZUUGUAFUJZUAUQZHUKZUVAI - UKZULZUMZUUISZUVFHAUVEUEZUFZIBUVEUEZUFZUPZUPZUUQUUGUVEFCDUNUDZUCUDUUIUACD - FHIUVEUUTUUTUOZUVEUOZUREUVMFUCMUSUTZUUGUVFUVHUVJUVPUUEUUTJHVAZUUTKIVAZUVH - UUFHFCUUTJUVNNVBZIFDUUTKUVNOVBZUVQUVRUPZHVCJKVDZVKZUVEUEZUVGUWAUBUUTHUWDU - VQHUUTVEUVRUUTJHVFVGUWCUWBVEZUWAUVEUUTVEZUVEVHUWBVIZUWDUUTVEVCTVEZUWBTVIZ - UWETTVCVJUWHVLTTVCWBVMUWBVNZTUWBVCVOVPUWAUUTUWBUVEUWAUAUUTUVDUWBUVQUVRUVA - UUTSZUVDUWBSZUVQUWKUPUVBJSUVCKSUWLUVRUWKUPUUTJUVAHVQUUTKUVAIVQUVBUVCJKVRV - SVTWAZWCZUWAUUTUWBUVEUWMWDZUWBUUTUWCUVEWEWFUWAUBUQZUUTSZUPZUWPUWDUKZUWPUV - EUKZUWCUKZUWPHUKZUWPIUKZULZUWCUKZUXBUWAUUTUWBUVEVAZUWQUWSUXAUFUWMUUTUWBUW - PUWCUVEWGWHUWRUWTUXDUWCUWRUAUWPUVDUXDUUTUVEUWBUVOUVAUWPUFUVBUXBUVCUXCUVAU - WPHWIUVAUWPIWIWJUWAUWQWKZUWRUXBUXCJKUWRUUTJUWPHUVQUVRUWQWLUXGWNZUWRUUTKUW - PIUVQUVRUWQWMUXGWNZWOWPZWQUWRUXEUXDVCUKZUXBUWRUXDUWBVCUVQUVRUWQUXDUWBSZUV - QUWQUPUXBJSZUXCKSZUXLUVRUWQUPUUTJUWPHVQUUTKUWPIVQUXBUXCJKVRVSVTZWRUWRUXMU - XNUXKUXBUFUXHUXIUXBUXCJKWSWTXAXBXDAUWCUVEAVCLVKUWCQLUWBVCPXEXCZXFXGVSUUEU - VQUVRUVJUUFUVSUVTUWAIXHUWBVKZUVEUEZUVIUWAUBUUTIUXRUVRIUUTVEUVQUUTKIVFXIUX - QUWBVEZUWAUWFUWGUXRUUTVEXHTVEZUWIUXSTTXHVJUXTXJTTXHWBVMUWJTUWBXHVOVPUWNUW - OUWBUUTUXQUVEWEWFUWRUWPUXRUKZUWTUXQUKZUXDUXQUKZUXCUWAUXFUWQUYAUYBUFUWMUUT - UWBUWPUXQUVEWGWHUWRUWTUXDUXQUXJWQUWRUYCUXDXHUKZUXCUWRUXDUWBXHUXOWRUWRUXMU - XNUYDUXCUFUXHUXIUXBUXCJKXKWTXAXBXDBUXQUVEBXHLVKUXQRLUWBXHPXEXCZXFXGVSXLUU - PUVLGUVEUUIUUHUVEUFZUUJUVFUUOUVKUUHUVEUUIXMUYFUULUVHUUNUVJUYFUUKUVGHUUHUV - EAXNXOUYFUUMUVIIUUHUVEBXNXOXPXPXQXRUUGUUPUUTUWBUUHVAZUULUUNXSZYRZGXTUYHGU - HZUURUUGUYIGUUGUUPUYGUUOUPUYHUUGUUJUYGUUOUUJUUTEUJZUUHVAUUGUYGUUHFEUUTUYK - UVNUYKUOVBUUGUYKUWBUUHUUTUUECYASZDYASZUYKUWBUFUUFHFCYBIFDYBUYLUYMUPUYKUVM - UJUWBEUVMMYCCDJKNOYDYEVSYFYGYHUYGUULUUNYIYJYKUUGUYHGYLZUYJUUEUUTTSZUVQUUF - UVRUYNUUEFYASUYOHFCYMFYAYNYOUVSUVTUUTJKTABGHIUXPUYEYPYQUYHGYSYOUUPUYHGYTX - RUUSUUPGYLUUQUURUPUUOGUUIUUAUUPGUUBUUCUUD $. + cres fo1st fofn ax-mp ssv fnssres ffvelcdm opelxpi syl2an anandirs fmpttd + mp2an ffnd mp3an2i fvco3 sylan fveq2 opeq12d simpr simpll ffvelrnd simplr + frnd opelxpd fvmptd3 fveq2d fvresd op1stg syl2anc 3eqtrrd eqfnfvd reseq2i + fnco eqtrd eqtri coeq1i c2nd adantl fo2nd op2ndg jca32 eleq1 coeq2 eqeq2d + eqtr4di anbi12d spcegv sylc w3a wi ctop cntop2 unieqi txuni eqtr4id feq3d + wal syl5ib anim1d 3anass syl6ibr alrimiv weu cntop1 uniexg upxp syl2an3an + syl eumo moim df-reu eu5 bitri sylanbrc ) HFCUCUDSZIFDUCUDSZUPZGUQZFEUCUD + ZSZHAUUHUEZUFZIBUUHUEZUFZUPZUPZGUGZUUPGUHZUUOGUUIUIZUUGUAFUJZUAUQZHUKZUVA + IUKZULZUMZUUISZUVFHAUVEUEZUFZIBUVEUEZUFZUPZUPZUUQUUGUVEFCDUNUDZUCUDUUIUAC + DFHIUVEUUTUUTUOZUVEUOZUREUVMFUCMUSUTZUUGUVFUVHUVJUVPUUEUUTJHVAZUUTKIVAZUV + HUUFHFCUUTJUVNNVBZIFDUUTKUVNOVBZUVQUVRUPZHVCJKVDZVKZUVEUEZUVGUWAUBUUTHUWD + UVQHUUTVEUVRUUTJHVFVGUWCUWBVEZUWAUVEUUTVEZUVEVHUWBVIZUWDUUTVEVCTVEZUWBTVI + ZUWETTVCVJUWHVLTTVCVMVNUWBVOZTUWBVCVPWBUWAUUTUWBUVEUWAUAUUTUVDUWBUVQUVRUV + AUUTSZUVDUWBSZUVQUWKUPUVBJSUVCKSUWLUVRUWKUPUUTJUVAHVQUUTKUVAIVQUVBUVCJKVR + VSVTWAZWCZUWAUUTUWBUVEUWMWMZUWBUUTUWCUVEXCWDUWAUBUQZUUTSZUPZUWPUWDUKZUWPU + VEUKZUWCUKZUWPHUKZUWPIUKZULZUWCUKZUXBUWAUUTUWBUVEVAZUWQUWSUXAUFUWMUUTUWBU + WPUWCUVEWEWFUWRUWTUXDUWCUWRUAUWPUVDUXDUUTUVEUWBUVOUVAUWPUFUVBUXBUVCUXCUVA + UWPHWGUVAUWPIWGWHUWAUWQWIZUWRUXBUXCJKUWRUUTJUWPHUVQUVRUWQWJUXGWKZUWRUUTKU + WPIUVQUVRUWQWLUXGWKZWNWOZWPUWRUXEUXDVCUKZUXBUWRUXDUWBVCUVQUVRUWQUXDUWBSZU + VQUWQUPUXBJSZUXCKSZUXLUVRUWQUPUUTJUWPHVQUUTKUWPIVQUXBUXCJKVRVSVTZWQUWRUXM + UXNUXKUXBUFUXHUXIUXBUXCJKWRWSXDWTXAAUWCUVEAVCLVKUWCQLUWBVCPXBXEZXFXOVSUUE + UVQUVRUVJUUFUVSUVTUWAIXGUWBVKZUVEUEZUVIUWAUBUUTIUXRUVRIUUTVEUVQUUTKIVFXHU + XQUWBVEZUWAUWFUWGUXRUUTVEXGTVEZUWIUXSTTXGVJUXTXITTXGVMVNUWJTUWBXGVPWBUWNU + WOUWBUUTUXQUVEXCWDUWRUWPUXRUKZUWTUXQUKZUXDUXQUKZUXCUWAUXFUWQUYAUYBUFUWMUU + TUWBUWPUXQUVEWEWFUWRUWTUXDUXQUXJWPUWRUYCUXDXGUKZUXCUWRUXDUWBXGUXOWQUWRUXM + UXNUYDUXCUFUXHUXIUXBUXCJKXJWSXDWTXABUXQUVEBXGLVKUXQRLUWBXGPXBXEZXFXOVSXKU + UPUVLGUVEUUIUUHUVEUFZUUJUVFUUOUVKUUHUVEUUIXLUYFUULUVHUUNUVJUYFUUKUVGHUUHU + VEAXMXNUYFUUMUVIIUUHUVEBXMXNXPXPXQXRUUGUUPUUTUWBUUHVAZUULUUNXSZXTZGYGUYHG + UHZUURUUGUYIGUUGUUPUYGUUOUPUYHUUGUUJUYGUUOUUJUUTEUJZUUHVAUUGUYGUUHFEUUTUY + KUVNUYKUOVBUUGUYKUWBUUHUUTUUECYASZDYASZUYKUWBUFUUFHFCYBIFDYBUYLUYMUPUYKUV + MUJUWBEUVMMYCCDJKNOYDYEVSYFYHYIUYGUULUUNYJYKYLUUGUYHGYMZUYJUUEUUTTSZUVQUU + FUVRUYNUUEFYASUYOHFCYNFYAYOYRUVSUVTUUTJKTABGHIUXPUYEYPYQUYHGYSYRUUPUYHGYT + XRUUSUUPGYMUUQUURUPUUOGUUIUUAUUPGUUBUUCUUD $. $} ${ @@ -150332,31 +150332,31 @@ F C_ ( CC X. X ) ) $= ( cfv co wcel syl wceq vz vw vv vu cv cop cmpo ctx ccnv chmeo ctop ctopon hmeocn cntop1 toptopon sylib cnmpt1st cnmpt21f cnmpt2nd cnmpt2t cuni c1st ccn cxp c2nd cmpt wf1o op1std fveq2d op2ndd opeq12d mpompt eqcomi wa eqid - vex wf cnf xp1st ffvelrn syl2an xp2nd opelxpd hmeof1o f1ocnv f1of 3syl wb - adantr ad2antrl ad2antll f1ocnvfvb syl3anc eqcom 3bitr4g anbi12d 3bitr4rd - eqop f1ocnv2d simprd eqtrdi cntop2 hmeocnvcn eqeltrd ishmeo sylanbrc ) AB - CJKBUEZDPZCUEZEPZUFZUGZFGUHQZHIUHQZVCQRXLUIZXNXMVCQZRXLXMXNUJQRABCXHXJFGH - IJKAFUKRZFJULPRADFHVCQRZXQADFHUJQRZXRNDFHUMSZDFHUNSFJLUOUPZAGUKRZGKULPRAE - GIVCQRZYBAEGIUJQRZYCOEGIUMSZEGIUNSGKMUOUPZABCXGDFGFHJKYAYFABCFGJKYAYFUQXT - URABCXIEFGGIJKYAYFABCFGJKYAYFUSYEURUTAXOUAUBHVAZIVAZUAUEZDUIZPZUBUEZEUIZP - ZUFZUGZXPAXOUCYGYHVDZUCUEZVBPZYJPZYRVEPZYMPZUFZVFZYPAJKVDZYQXLVGXOUUDTAUD - UCUUEYQUDUEZVBPZDPZUUFVEPZEPZUFZUUCXLUDUUEUUKVFXLBCUDJKUUKXKUUFXGXIUFTZUU - HXHUUJXJUULUUGXGDXGXIUUFBVPZCVPZVHVIUULUUIXIEXGXIUUFUUMUUNVJVIVKVLVMAUUFU - UERZVNUUHUUJYGYHAJYGDVQZUUGJRZUUHYGRUUOAXRUUPXTDFHJYGLYGVOZVRSUUFJKVSZJYG - UUGDVTWAAKYHEVQZUUIKRZUUJYHRUUOAYCUUTYEEGIKYHMYHVOZVRSUUFJKWBZKYHUUIEVTWA - WCAYRYQRZVNYTUUBJKAYGJYJVQZYSYGRZYTJRUVDAJYGDVGZYGJYJVGUVEAXSUVGNDFHJYGLU - URWDSZJYGDWEYGJYJWFWGYRYGYHVSZYGJYSYJVTWAAYHKYMVQZUUAYHRZUUBKRUVDAKYHEVGZ - YHKYMVGUVJAYDUVLOEGIKYHMUVBWDSZKYHEWEYHKYMWFWGYRYGYHWBZYHKUUAYMVTWAWCAUUO - UVDVNZVNZYSUUHTZUUAUUJTZVNZUUGYTTZUUIUUBTZVNZYRUUKTZUUFUUCTZUVPUVQUVTUVRU - WAUVPUUHYSTZYTUUGTZUVQUVTUVPUVGUUQUVFUWEUWFWHAUVGUVOUVHWIUUOUUQAUVDUUSWJU - VDUVFAUUOUVIWKJYGUUGYSDWLWMYSUUHWNUUGYTWNWOUVPUUJUUATZUUBUUITZUVRUWAUVPUV - LUVAUVKUWGUWHWHAUVLUVOUVMWIUUOUVAAUVDUVCWJUVDUVKAUUOUVNWKKYHUUIUUAEWLWMUU - AUUJWNUUIUUBWNWOWPUVDUWCUVSWHAUUOYRUUHUUJYGYHWRWKUUOUWDUWBWHAUVDUUFYTUUBJ - KWRWJWQWSWTUAUBUCYGYHUUCYOYRYIYLUFTZYTYKUUBYNUWIYSYIYJYIYLYRUAVPZUBVPZVHV - IUWIUUAYLYMYIYLYRUWJUWKVJVIVKVLXAAUAUBYKYNHIFGYGYHAHUKRZHYGULPRAXRUWLXTDF - HXBSHYGUURUOUPZAIUKRZIYHULPRAYCUWNYEEGIXBSIYHUVBUOUPZAUAUBYIYJHIHFYGYHUWM - UWOAUAUBHIYGYHUWMUWOUQAXSYJHFVCQRNDFHXCSURAUAUBYLYMHIIGYGYHUWMUWOAUAUBHIY - GYHUWMUWOUSAYDYMIGVCQROEGIXCSURUTXDXLXMXNXEXF $. + vex wf cnf xp1st ffvelcdm syl2an xp2nd opelxpd hmeof1o f1ocnv f1of adantr + 3syl wb ad2antrl ad2antll f1ocnvfvb syl3anc 3bitr4g anbi12d eqop 3bitr4rd + eqcom f1ocnv2d simprd eqtrdi cntop2 hmeocnvcn eqeltrd ishmeo sylanbrc ) A + BCJKBUEZDPZCUEZEPZUFZUGZFGUHQZHIUHQZVCQRXLUIZXNXMVCQZRXLXMXNUJQRABCXHXJFG + HIJKAFUKRZFJULPRADFHVCQRZXQADFHUJQRZXRNDFHUMSZDFHUNSFJLUOUPZAGUKRZGKULPRA + EGIVCQRZYBAEGIUJQRZYCOEGIUMSZEGIUNSGKMUOUPZABCXGDFGFHJKYAYFABCFGJKYAYFUQX + TURABCXIEFGGIJKYAYFABCFGJKYAYFUSYEURUTAXOUAUBHVAZIVAZUAUEZDUIZPZUBUEZEUIZ + PZUFZUGZXPAXOUCYGYHVDZUCUEZVBPZYJPZYRVEPZYMPZUFZVFZYPAJKVDZYQXLVGXOUUDTAU + DUCUUEYQUDUEZVBPZDPZUUFVEPZEPZUFZUUCXLUDUUEUUKVFXLBCUDJKUUKXKUUFXGXIUFTZU + UHXHUUJXJUULUUGXGDXGXIUUFBVPZCVPZVHVIUULUUIXIEXGXIUUFUUMUUNVJVIVKVLVMAUUF + UUERZVNUUHUUJYGYHAJYGDVQZUUGJRZUUHYGRUUOAXRUUPXTDFHJYGLYGVOZVRSUUFJKVSZJY + GUUGDVTWAAKYHEVQZUUIKRZUUJYHRUUOAYCUUTYEEGIKYHMYHVOZVRSUUFJKWBZKYHUUIEVTW + AWCAYRYQRZVNYTUUBJKAYGJYJVQZYSYGRZYTJRUVDAJYGDVGZYGJYJVGUVEAXSUVGNDFHJYGL + UURWDSZJYGDWEYGJYJWFWHYRYGYHVSZYGJYSYJVTWAAYHKYMVQZUUAYHRZUUBKRUVDAKYHEVG + ZYHKYMVGUVJAYDUVLOEGIKYHMUVBWDSZKYHEWEYHKYMWFWHYRYGYHWBZYHKUUAYMVTWAWCAUU + OUVDVNZVNZYSUUHTZUUAUUJTZVNZUUGYTTZUUIUUBTZVNZYRUUKTZUUFUUCTZUVPUVQUVTUVR + UWAUVPUUHYSTZYTUUGTZUVQUVTUVPUVGUUQUVFUWEUWFWIAUVGUVOUVHWGUUOUUQAUVDUUSWJ + UVDUVFAUUOUVIWKJYGUUGYSDWLWMYSUUHWRUUGYTWRWNUVPUUJUUATZUUBUUITZUVRUWAUVPU + VLUVAUVKUWGUWHWIAUVLUVOUVMWGUUOUVAAUVDUVCWJUVDUVKAUUOUVNWKKYHUUIUUAEWLWMU + UAUUJWRUUIUUBWRWNWOUVDUWCUVSWIAUUOYRUUHUUJYGYHWPWKUUOUWDUWBWIAUVDUUFYTUUB + JKWPWJWQWSWTUAUBUCYGYHUUCYOYRYIYLUFTZYTYKUUBYNUWIYSYIYJYIYLYRUAVPZUBVPZVH + VIUWIUUAYLYMYIYLYRUWJUWKVJVIVKVLXAAUAUBYKYNHIFGYGYHAHUKRZHYGULPRAXRUWLXTD + FHXBSHYGUURUOUPZAIUKRZIYHULPRAYCUWNYEEGIXBSIYHUVBUOUPZAUAUBYIYJHIHFYGYHUW + MUWOAUAUBHIYGYHUWMUWOUQAXSYJHFVCQRNDFHXCSURAUAUBYLYMHIIGYGYHUWMUWOAUAUBHI + YGYHUWMUWOUSAYDYMIGVCQROEGIXCSURUTXDXLXMXNXEXF $. $} ${ @@ -153976,8 +153976,8 @@ S C_ ( P ( ball ` D ) T ) ) $= ( vx vw vz vy cc wa co clt cfv wcel vf wss ccncf ccn cv wbr wral crp wrex wf wi cmin cabs wb wceq simplll simprl simprr ccom cxp oveqi ovres eqtrid cres ad2ant2l ssel2 eqid cnmetdval syl2an eqtrd syl22anc breq1d ad2ant2lr - ffvelrn syl2anc simpllr imbi12d anassrs ralbidva rexbidv ralbidv pm5.32da - sseldd cxmet cnxmet xmetres2 mpan eqeltrid metcn elcncf 3bitr4rd eqrdv ) + ffvelcdm syl2anc simpllr sseldd imbi12d anassrs ralbidva rexbidv pm5.32da + ralbidv cxmet cnxmet xmetres2 mpan eqeltrid metcn elcncf 3bitr4rd eqrdv ) AOUBZBOUBZPZUAABUCQZEFUDQZWOABUAUEZUJZKUEZLUEZCQZMUEZRUFZWTWRSZXAWRSZDQZN UEZRUFZUKZLAUGZMUHUIZNUHUGZKAUGZPZWSWTXAULQUMSZXCRUFZXEXFULQUMSZXHRUFZUKZ LAUGZMUHUIZNUHUGZKAUGZPWRWQTZWRWPTWOWSXNYDWOWSPZXMYCKAYFWTATZPZXLYBNUHYHX @@ -153986,8 +153986,8 @@ S C_ ( P ( ball ` D ) T ) ) $= JXBWTXAYOAAUTVDZQYPCYQWTXAGVAWTXAAAYOVBVCVEYMWTOTXAOTYPXPUOYNAOWTVFAOXAVF WTXAYOYOVGZVHVIVJVKVLYKXGXRXHRYKXGXEXFYOQZXRYKXEBTZXFBTZXGYSUOWSYGYTWOYIA BWTWRVNVMZWSYIUUAWOYGABXAWRVNVEZYTUUAPXGXEXFYOBBUTVDZQYSDUUDXEXFHVAXEXFBB - YOVBVCVOYKXEOTXFOTYSXRUOYKBOXEWMWNWSYJVPZUUBWCYKBOXFUUEUUCWCXEXFYOYRVHVOV - JVLVQVRVSVTWAVSWBWMCAWDSZTDBWDSZTYEXOUNWNWMCYQUUFGYOOWDSTZWMYQUUFTWEYOAOW + YOVBVCVOYKXEOTXFOTYSXRUOYKBOXEWMWNWSYJVPZUUBVQYKBOXFUUEUUCVQXEXFYOYRVHVOV + JVLVRVSVTWAWCVTWBWMCAWDSZTDBWDSZTYEXOUNWNWMCYQUUFGYOOWDSTZWMYQUUFTWEYOAOW FWGWHWNDUUDUUGHUUHWNUUDUUGTWEYOBOWFWGWHKNMLCDWREFABIJWIVIKNMLABWRWJWKWL $. $} @@ -156189,31 +156189,31 @@ Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and syl syl2anc sseldd dvlemap ssidd cxp txtopon toponrestid simprd ccn cop mp2an ccnp addcncntop dvcl mpdan opelxpd toponunii cncnpi limccnp2cntop elrabi adantl cvv wfn ffnd adantr cnex ssexg sylancl inidm wf ffvelrnda - eqidd addcld ofvalg mpidan oveq12d ffvelrn syl2an ffvelrnd eqtrd oveq1d - addsub4d subcld ssrab2 sstrid breq1 simprbi subap0d divdirapd mpteq2dva - sselda elrab eleqtrrd addcl off mpbir2and ) ABGHQRZCDEQUERZUFRUGBIFCUHR - ZUIUJUJZSZYNUAUBUNZBUOUGZUBIUKZUAUNZYOUJZBYOUJZULRZUUBBULRZUMRZUPZBUQRZ - SAYRHUAUUAUUBEUJZBEUJZULRZUUFUMRZUPZBUQRSZABHCEUFRUGZYRUUOUROAUAUBIBHCY - PEUUNFYPUSZPUUNUSMLKUTVAZVBAYNUAUUAUUBDUJZBDUJZULRZUUFUMRZUUMQRZUPZBUQR - UUIAUAUUABGHUVBUUMQFFVCRZFTTAUBUUBBIDJAICTKMVDZAYQIBAYPVESZIYPVHZVFYQIV - FAYPCVGUJSZUVGAFTVGUJSZCTVFUVIFPVIZMCFTVJVKZCYPVLVQAICUVHKAUVICUVHVMUVL - CYPVNVQVOIYPUVHUVHUSVPVRAYRGUAUUAUVBUPZBUQRSZABGCDUFRUGZYRUVNURNAUAUBIB - GCYPDUVMFUUQPUVMUSMJKUTVAZVBVSZVTAUBUUBBIELUVFUVQVTATWAZUVRPUVETTWBZUVJ - UVJUVEUVSVGUJSUVKUVKFFTTWCWHZWDAYRUVNUVPWEAYRUUOUURWEAQUVEFWFRSGHWGZUVS - SQUWAUVEFWIRUJSFPWJAGHTTAUVOGTSNAIBGCDMJKWKWLAUUPHTSOAIBHCEMLKWKWLWMUWA - QUVEFUVSUVSUVEUVTWNWOVKWPAUUHUVDBUQAUAUUAUUGUVCAUUBUUASZURZUUGUVAUULQRZ - UUFUMRUVCUWCUUEUWDUUFUMUWCUUEUUSUUJQRZUUTUUKQRZULRUWDUWCUUCUWEUUDUWFULU - WCUUBISZUUCUWEVMUWBUWGAYTUBUUBIWQZWRZUWCIIUUSUUJQITDEWSWSUUBADIWTUWBAIT - DJXAXBZAEIWTUWBAITELXAXBZAIWSSZUWBAITVFTWSSUWLUVFXCITWSXDXEZXBZUWNIXFZU - WCUWGURZUUSXIUWPUUJXIUWPUUSUUJUWCITUUBDAITDXGZUWBJXBZXHUWCITUUBEAITEXGU - WBLXBZXHXJXKWLAUWBBISZUUDUWFVMUVQUWCIIUUTUUKQITDEWSWSBUWJUWKUWNUWNUWOUW - CUWTURZUUTXIUXAUUKXIUXAUUTUUKUWCITBDUWRXHUWCITBEUWSXHXJXKXLXMUWCUUSUUJU - UTUUKAUWQUWGUUSTSUWBJUWHITUUBDXNXOUWCITUUBEUWSUWIXPZAUUTTSUWBAITBDJUVQX - PXBZAUUKTSUWBAITBELUVQXPXBZXSXQXRUWCUVAUULUUFUWCUUSUUTUWCITUUBDUWRUWIXP - UXCXTUWCUUJUUKUXBUXDXTUWCUUBBAUUATUUBAUUAITYTUBIYAUVFYBYHZABTSUWBAITBUV - FUVQVSXBZXTUWCUUBBUXEUXFUWBUUBBUOUGZAUWBUWGUXGYTUXGUBUUBIYSUUBBUOYCYIYD - WRYEYFXQYGXRYJAUAUBIBYNCYPYOUUHFUUQPUUHUSMAUCUDIIIQTTTDEWSWSUCUNZTSUDUN - ZTSURUXHUXIQRTSAUXHUXIYKWRJLUWMUWMUWOYLKUTYM $. + eqidd addcld ofvalg mpidan ffvelcdm syl2an ffvelrnd eqtrd oveq1d subcld + oveq12d addsub4d ssrab2 sstrid sselda breq1 simprbi divdirapd mpteq2dva + elrab subap0d eleqtrrd addcl off mpbir2and ) ABGHQRZCDEQUERZUFRUGBIFCUH + RZUIUJUJZSZYNUAUBUNZBUOUGZUBIUKZUAUNZYOUJZBYOUJZULRZUUBBULRZUMRZUPZBUQR + ZSAYRHUAUUAUUBEUJZBEUJZULRZUUFUMRZUPZBUQRSZABHCEUFRUGZYRUUOUROAUAUBIBHC + YPEUUNFYPUSZPUUNUSMLKUTVAZVBAYNUAUUAUUBDUJZBDUJZULRZUUFUMRZUUMQRZUPZBUQ + RUUIAUAUUABGHUVBUUMQFFVCRZFTTAUBUUBBIDJAICTKMVDZAYQIBAYPVESZIYPVHZVFYQI + VFAYPCVGUJSZUVGAFTVGUJSZCTVFUVIFPVIZMCFTVJVKZCYPVLVQAICUVHKAUVICUVHVMUV + LCYPVNVQVOIYPUVHUVHUSVPVRAYRGUAUUAUVBUPZBUQRSZABGCDUFRUGZYRUVNURNAUAUBI + BGCYPDUVMFUUQPUVMUSMJKUTVAZVBVSZVTAUBUUBBIELUVFUVQVTATWAZUVRPUVETTWBZUV + JUVJUVEUVSVGUJSUVKUVKFFTTWCWHZWDAYRUVNUVPWEAYRUUOUURWEAQUVEFWFRSGHWGZUV + SSQUWAUVEFWIRUJSFPWJAGHTTAUVOGTSNAIBGCDMJKWKWLAUUPHTSOAIBHCEMLKWKWLWMUW + AQUVEFUVSUVSUVEUVTWNWOVKWPAUUHUVDBUQAUAUUAUUGUVCAUUBUUASZURZUUGUVAUULQR + ZUUFUMRUVCUWCUUEUWDUUFUMUWCUUEUUSUUJQRZUUTUUKQRZULRUWDUWCUUCUWEUUDUWFUL + UWCUUBISZUUCUWEVMUWBUWGAYTUBUUBIWQZWRZUWCIIUUSUUJQITDEWSWSUUBADIWTUWBAI + TDJXAXBZAEIWTUWBAITELXAXBZAIWSSZUWBAITVFTWSSUWLUVFXCITWSXDXEZXBZUWNIXFZ + UWCUWGURZUUSXIUWPUUJXIUWPUUSUUJUWCITUUBDAITDXGZUWBJXBZXHUWCITUUBEAITEXG + UWBLXBZXHXJXKWLAUWBBISZUUDUWFVMUVQUWCIIUUTUUKQITDEWSWSBUWJUWKUWNUWNUWOU + WCUWTURZUUTXIUXAUUKXIUXAUUTUUKUWCITBDUWRXHUWCITBEUWSXHXJXKXLXSUWCUUSUUJ + UUTUUKAUWQUWGUUSTSUWBJUWHITUUBDXMXNUWCITUUBEUWSUWIXOZAUUTTSUWBAITBDJUVQ + XOXBZAUUKTSUWBAITBELUVQXOXBZXTXPXQUWCUVAUULUUFUWCUUSUUTUWCITUUBDUWRUWIX + OUXCXRUWCUUJUUKUXBUXDXRUWCUUBBAUUATUUBAUUAITYTUBIYAUVFYBYCZABTSUWBAITBU + VFUVQVSXBZXRUWCUUBBUXEUXFUWBUUBBUOUGZAUWBUWGUXGYTUXGUBUUBIYSUUBBUOYDYHY + EWRYIYFXPYGXQYJAUAUBIBYNCYPYOUUHFUUQPUUHUSMAUCUDIIIQTTTDEWSWSUCUNZTSUDU + NZTSURUXHUXIQRTSAUXHUXIYKWRJLUWMUWMUWOYLKUTYM $. $( The product rule for derivatives at a point. For the (simpler but more limited) function version, see ~ dvmulxx . (Contributed by Mario @@ -156478,21 +156478,21 @@ Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and ( vx vy cc wf cr wss wa cdv co cdm ccj ccom cmpt wcel wceq adantr feqmptd cfv cv wbr simpll simplr simpr dvcjbr wi wfun cpm cjf fco mpan fdmd feq2d mpbird eqsstrd cnex reex elpm2 sylanbrc dvfpm syl ffund funbrfv mpteq2dva - mpd cvv ffvelrnda cjcld ad2antrr breldmg mp3an2i ex ssrdv ffvelrn adantlr - vex cjcjd simpl a1i fveq2 fmptco 3eqtr4d oveq2d dmeqd sseqtrd ffdm simpld - fdm eqelssd mpbid ) BEAFZBGHZIZCGAJKZLZCUAZGMANZJKZTZOCWPWQWOTZMTZOWSMWON - WNCWPWTXBWNWQWPPZIZWQXBWSUBZWTXBQZXDWQABWLWMXCUCWLWMXCUDWNXCUEUFZWNXEXFUG - ZXCWNWSUHXHWNWSLZEWSWNWREGUIKZPZXIEWSFZWNWRLZEWRFZXMGHXKWNXNBEWRFZWLXOWME - EMFZWLXOUJBEEMAUKULZRWNXMBEWRWLXMBQWMWLBEWRXQUMRZUNUOWNXMBGXRWLWMUEZUPEGW - RUQURUSUTWRVAVBZVCWQXBWSVDVBRVFVEWNCWPEWSWNXLWPEWSFXTWNXIWPEWSWNCXIWPWNXI - GMWRNZJKZLZWPWNCXIYCWNWQXIPZWQYCPZWQVGPZWNYDIZWTMTZEPWQYHYBUBYECVQZYGWTWN - XIEWQWSXTVHVIYGWQWRBWLXOWMYDXQVJWLWMYDUDWNYDUEUFWQYHVGEYBVKVLVMVNWNYBWOWN - YAAGJWNCBWQATZMTZMTZOCBYJOYAAWNCBYLYJWNWQBPZIZYJWLYMYJEPWMBEWQAVOVPZVRVEW - NCDBEYKDUAZMTZYLWRMYNYJYOVIWNCDBEYJYQYKAMYOWNCBEAWLWMVSSZWNDEEMXPWNUJVTSZ - YPYJMWAWBYSYPYKMWAWBYRWCWDWEWFYFXDXBEPXEYDYIXDXAWNWPEWQWOWNAXJPZWPEWOFWNA - LZEAFZUUAGHYTWLUUBWMWLUUBUUABHBEAWGWHRWNUUABGWLUUABQWMBEAWIRXSUPEGAUQURUS - UTAVAVBZVHZVIXGWQXBVGEWSVKVLWJUNWKSWNCDWPEXAYQXBWOMUUDWNCWPEWOUUCSYSYPXAM - WAWBWC $. + mpd cvv vex ffvelrnda cjcld ad2antrr breldmg mp3an2i ssrdv ffvelcdm cjcjd + ex adantlr simpl a1i fveq2 fmptco 3eqtr4d oveq2d dmeqd sseqtrd simpld fdm + ffdm eqelssd mpbid ) BEAFZBGHZIZCGAJKZLZCUAZGMANZJKZTZOCWPWQWOTZMTZOWSMWO + NWNCWPWTXBWNWQWPPZIZWQXBWSUBZWTXBQZXDWQABWLWMXCUCWLWMXCUDWNXCUEUFZWNXEXFU + GZXCWNWSUHXHWNWSLZEWSWNWREGUIKZPZXIEWSFZWNWRLZEWRFZXMGHXKWNXNBEWRFZWLXOWM + EEMFZWLXOUJBEEMAUKULZRWNXMBEWRWLXMBQWMWLBEWRXQUMRZUNUOWNXMBGXRWLWMUEZUPEG + WRUQURUSUTWRVAVBZVCWQXBWSVDVBRVFVEWNCWPEWSWNXLWPEWSFXTWNXIWPEWSWNCXIWPWNX + IGMWRNZJKZLZWPWNCXIYCWNWQXIPZWQYCPZWQVGPZWNYDIZWTMTZEPWQYHYBUBYECVHZYGWTW + NXIEWQWSXTVIVJYGWQWRBWLXOWMYDXQVKWLWMYDUDWNYDUEUFWQYHVGEYBVLVMVQVNWNYBWOW + NYAAGJWNCBWQATZMTZMTZOCBYJOYAAWNCBYLYJWNWQBPZIZYJWLYMYJEPWMBEWQAVOVRZVPVE + WNCDBEYKDUAZMTZYLWRMYNYJYOVJWNCDBEYJYQYKAMYOWNCBEAWLWMVSSZWNDEEMXPWNUJVTS + ZYPYJMWAWBYSYPYKMWAWBYRWCWDWEWFYFXDXBEPXEYDYIXDXAWNWPEWQWOWNAXJPZWPEWOFWN + ALZEAFZUUAGHYTWLUUBWMWLUUBUUABHBEAWIWGRWNUUABGWLUUABQWMBEAWHRXSUPEGAUQURU + SUTAVAVBZVIZVJXGWQXBVGEWSVLVMWJUNWKSWNCDWPEXAYQXBWOMUUDWNCWPEWOUUCSYSYPXA + MWAWBWC $. $} ${ @@ -156503,16 +156503,16 @@ Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and ( RR _D F ) : dom ( RR _D F ) --> RR ) $= ( vx vy vz cr wf wss wa cdv co cdm cv cfv wcel cc adantr syl ccj wceq wfn wral cpm ax-resscn fss mpan2 ffdm simpld simpl fdmd simpr cnex reex elpm2 - eqsstrd sylanbrc dvfpm ffn 3syl ffvelrnda ccom fvco3 dvcj ffvelrn adantlr - sylan cmpt cjred mpteq2dva recnd feqmptd cjf fmptco 3eqtr4d oveq2d eqtr3d - a1i fveq2 fveq1d cjrebd ralrimiva ffnfv ) AFBGZAFHZIZFBJKZWFLZUAZCMZWFNZF - OZCWGUBWGFWFGWEBPFUCKOZWGPWFGZWHWEBLZPBGZWNFHWLWEAPBGZWOWCWPWDWCFPHWPUDAF - PBUEUFZQWPWOWNAHAPBUGUHRWEWNAFWEAFBWCWDUIZUJWCWDUKUOPFBULUMUNUPZBUQZWGPWF - URUSWEWKCWGWEWIWGOZIZWJWEWGPWIWFWEWLWMWSWTRZUTXBWISWFVAZNZWJSNZWJWEWMXAXE - XFTXCWGPWISWFVBVFWEXEWJTXAWEWIXDWFWEFSBVAZJKZXDWFWCWPWDXHXDTWQBAVCVFWEXGB - FJWEDADMZBNZSNZVGDAXJVGXGBWEDAXKXJWEXIAOZIZXJWCXLXJFOWDAFXIBVDVEZVHVIWEDE - APXJEMZSNXKBSXMXJXNVJWEDAFBWRVKZWEEPPSPPSGWEVLVQVKXOXJSVRVMXPVNVOVPVSQVPV - TWACWGFWFWBUP $. + eqsstrd sylanbrc dvfpm 3syl ffvelrnda ccom fvco3 sylan dvcj cmpt ffvelcdm + ffn adantlr cjred mpteq2dva recnd feqmptd cjf fveq2 fmptco 3eqtr4d oveq2d + a1i eqtr3d fveq1d cjrebd ralrimiva ffnfv ) AFBGZAFHZIZFBJKZWFLZUAZCMZWFNZ + FOZCWGUBWGFWFGWEBPFUCKOZWGPWFGZWHWEBLZPBGZWNFHWLWEAPBGZWOWCWPWDWCFPHWPUDA + FPBUEUFZQWPWOWNAHAPBUGUHRWEWNAFWEAFBWCWDUIZUJWCWDUKUOPFBULUMUNUPZBUQZWGPW + FVFURWEWKCWGWEWIWGOZIZWJWEWGPWIWFWEWLWMWSWTRZUSXBWISWFUTZNZWJSNZWJWEWMXAX + EXFTXCWGPWISWFVAVBWEXEWJTXAWEWIXDWFWEFSBUTZJKZXDWFWCWPWDXHXDTWQBAVCVBWEXG + BFJWEDADMZBNZSNZVDDAXJVDXGBWEDAXKXJWEXIAOZIZXJWCXLXJFOWDAFXIBVEVGZVHVIWED + EAPXJEMZSNXKBSXMXJXNVJWEDAFBWRVKZWEEPPSPPSGWEVLVQVKXOXJSVMVNXPVOVPVRVSQVR + VTWACWGFWFWBUP $. $} ${ @@ -160294,63 +160294,63 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is mul02d wb zmulcld dvdssq mpbid adantr breq2 syl5ibcom cle simprl neneqd wi sqeq0 syl mtbird cn0 wo zsqcl2 elnn0 sylib ecased nnzd dvdsle nnge1d 1nn jctird cr nnred 1re letri3 exmiddc mpjaodan oveq2 sylan9eqr clt cfv - lgs0 cv cprime cpc cmpt cseq nnuz wf eqid lgsfcl3 syl3anc ffvelrn lgscl - syl2an eqtrd adantlr ifbieq1d zexpcl ifcldadc fvmptd3 lgsval4 a1i zdclt - 1zzd 0z dcan2 sylc ffvelrnda seqf ffvelrnd sylibrd syld con3dimp simpl3 - iffalsed 3eqtr4rd cneg cabs lgsdilem cuz nnabscl sylan eleqtrdi simpll1 - simpll3 elnnuz biimpri simpll2 prmz pczcl syl12anc mulexpd 1t1e1 eqcomi - lgsdirprm 3eqtr4a prmdc eleq1w oveq1 prod3fmul neg1cn zmulcl neg1z dcne - mul4d ) AEFZBEFZCEFZUCZAGUOZBGUOZHZHZCGIZABJKZCLKZACLKZBCLKZJKZICGUOZUW - CUWDHZAUDMKZNIZNGOZBUDMKZNIZNGOZJKZUWEUDMKZNIZNGOZUWIUWFUWKUWMUWRUXAIUW - MUEZUWKUWMHZNUWQJKZUWQUWRUXAUVSUXDUWQIUWBUWDUWMUVSUWQUVSUWPNGUFUVSUGUVS - UHUVSUWOEFZNEFZUWPPUVQUVPUXEUVRBUIUJUKUWONULUMUNZUPUQUXCUWNNUWQJUWMUWNN - IUWKUWMNGURUSUTUXCUWTUWPNGUXCUWSUWONUXCUWSUWLUWOJKNUWOJKUWOUXCABUWCAUFF - ZUWDUWMUWCAUVPUVQUVRUWBVAZQZVBUWCBUFFUWDUWMUWCBUVPUVQUVRUWBVCZQZVBVEUXC - UWLNUWOJUWKUWMVDUTUXCUWOUWCUWOUFFUWDUWMUWCBUXLVFVBUPVGVHVIVJUWKUXBHZGUW - QJKZGUWRUXAUVSUXNGIUWBUWDUXBUVSUWQUXGVOUQUXMUWNGUWQJUXBUWNGIUWKUWMNGVKU - SUTUXMUWTNGUWKUWTUWMUWKUWTUWLNVLRZUWMUWKUWLUWSVLRZUWTUXOUWCUXPUWDUWCAUW - EVLRZUXPUWCUVPUVQUXQUXIUXKABVMVNUWCUVPUWEEFZUXQUXPVPUXIUWCABUXIUXKVQZAU - WEVRVNVSVTUWSNUWLVLWAWBUWKUXOUWLNWCRZNUWLWCRZHZUWMUWKUXOUXTUYAUWKUWLEFZ - NTFUXOUXTWFUWKUWLUWCUWLTFZUWDUWCUYDUWLGIZUWCUYEAGIZUWCAGUVSUVTUWAWDWEUW - CUXHUYEUYFVPUXJAWGWHWIUWCUWLWJFZUYDUYEWKUWCUVPUYGUXIAWLWHUWLWMWNWOVTZWP - ZWSUWLNWQUMUWKUWLUYHWRWTUWKUWLXAFNXAFUWMUYBVPUWKUWLUYHXBXCUWLNXDUMUUAUU - BUUCUUEVJUWKUWMPZUWMUXBWKUWKUYCUXFUYJUYIUKUWLNULUMUWMXEWHXFUWKUWGUWNUWH - UWQJUWDUWCUWGAGLKZUWNCGALXGUWCUVPUYKUWNIUXIAXKWHXHUWDUWCUWHBGLKZUWQCGBL - XGUWCUVQUYLUWQIUXKBXKWHXHSUWDUWCUWFUWEGLKZUXACGUWELXGUWCUXRUYMUXAIUXSUW - EXKWHXHUUFUWCUWJHZCGXIRZUWEGXIRHNUUGZNOZCUUHXJZJDTDXLZXMFZUWEUYSLKZUYSC - XNKZMKZNOZXOZNXPXJZJKZUYOAGXIRZHZUYPNOZUYOBGXIRZHZUYPNOZJKZUYRJDTUYTAUY - SLKZVUBMKZNOZXOZNXPZXJZUYRJDTUYTBUYSLKZVUBMKZNOZXOZNXPZXJZJKZJKZUWFUWIU - YNUYQVUNVUFVVGJUWCUYQVUNIUWJABCUUIVTUYNUAVURVVDVUENUYRUYNUYRTNUUJXJZUWC - UVRUWJUYRTFUVPUVQUVRUWBUUDZCUUKUULZXQUUMUYNUAXLZVVIFZHZVVLVURXJZUYNTEVU - RXRZVVLTFZVVOEFVVMUYNUVPUVRUWJVVPUVPUVQUVRUWBUWJUUNZUVPUVQUVRUWBUWJUUOZ - UWCUWJVDZADVURCVURXSZXTYAZVVQVVMVVLUUPUUQZTEVVLVURYBYDQVVNVVLVVDXJZUYNT - EVVDXRZVVQVWDEFVVMUYNUVQUVRUWJVWEUVPUVQUVRUWBUWJUURZVVSVVTBDVVDCVVDXSZX - TYAZVWCTEVVLVVDYBYDQVVNVVLXMFZUWEVVLLKZVVLCXNKZMKZNOZVWIAVVLLKZVWKMKZNO - ZVWIBVVLLKZVWKMKZNOZJKZVVLVUEXJVVOVWDJKVVNVWIVWMVWTIZVWIUEZUYNVWIVXAVVM - UYNVWIHZVWLVWOVWRJKZVWMVWTVXCVWLVWNVWQJKZVWKMKVXDVXCVWJVXEVWKMVXCUVPUVQ - VWIVWJVXEIUYNUVPVWIVVRVTUYNUVQVWIVWFVTUYNVWIVDZABVVLUVEYAUTVXCVWNVWQVWK - VXCVWNUYNUVPVVLEFZVWNEFZVWIVVRVVLUUSZAVVLYCYDZQVXCVWQUYNUVQVXGVWQEFZVWI - VWFVXIBVVLYCYDZQVXCVWIUVRUWJVWKWJFZVXFUYNUVRVWIVVSVTUYNUWJVWIVVTVTVVLCU - UTUVAZUVBYEVWIVWMVWLIUYNVWIVWLNURUSVWIVWTVXDIUYNVWIVWPVWOVWSVWRJVWIVWON - URVWIVWRNURSUSVJYFVXBVXAVVNVXBNNNJKZVWMVWTVXONUVCUVDVWIVWLNVKVXBVWPNVWS - NJVWIVWONVKVWIVWRNVKSUVFUSVVNVWIPZVWIVXBWKVVNVVQVXPVVMVVQUYNVWCUSZVVLUV - GWHZVWIXEWHXFVVNDVVLVUDVWMTVUEEVUEXSZUYSVVLIZUYTVWIVUCVWLNDUAXMUVHZVXTV - UAVWJVUBVWKMUYSVVLUWELXGUYSVVLCXNUVIZSYGVXQVVNVWIVWLNEVVNVWIHZVWJEFZVXM - VWLEFVYCUXRVXGVYDUWCUXRUWJVVMVWIUXSUQVWIVXGVVNVXIUSUWEVVLYCVNUYNVWIVXMV - VMVXNYFZVWJVWKYHVNVVNVXBHYNZVXRYIYJVVNVVOVWPVWDVWSJVVNDVVLVUQVWPTVUREVW - AVXTUYTVWIVUPVWONVYAVXTVUOVWNVUBVWKMUYSVVLALXGVYBSYGVXQVVNVWIVWONEVYCVX - HVXMVWOEFUYNVWIVXHVVMVXJYFVYEVWNVWKYHVNVYFVXRYIYJVVNDVVLVVCVWSTVVDEVWGV - XTUYTVWIVVBVWRNVYAVXTVVAVWQVUBVWKMUYSVVLBLXGVYBSYGVXQVVNVWIVWRNEVYCVXKV - XMVWREFUYNVWIVXKVVMVXLYFVYEVWQVWKYHVNVYFVXRYIYJSVJUVJSUYNUXRUVRUWJUWFVU - GIUWCUXRUWJUXSVTVVSVVTUWEDVUECVXSYKYAUYNUWIVUJVUTJKZVUMVVFJKZJKVVHUYNUW - GVYGUWHVYHJUYNUVPUVRUWJUWGVYGIVVRVVSVVTADVURCVWAYKYAUYNUVQUVRUWJUWHVYHI - VWFVVSVVTBDVVDCVWGYKYASUYNVUJVUTVUMVVFUYNVUIUYPNUFUYPUFFUYNUVKYLUYNUGUY - NUYOPZVUHPZVUIPUYNUVRGEFZVYIVVSYOCGYMUMZUYNUVPVYKVYJVVRYOAGYMUMUYOVUHYP - YQUNUYNVUTUYNTEUYRVUSUYNUAUBJEVURNTXQUYNYNZUYNTEVVLVURVWBYRVXGUBXLZEFHV - VLVYNJKEFUYNVVLVYNUVLUSZYSVVKYTQUYNVUMUYNVULUYPNEUYPEFUYNUVMYLVYMUYNVYI - VUKPZVULPVYLUYNUVQVYKVYPVWFYOBGYMUMUYOVUKYPYQUNQUYNVVFUYNTEUYRVVEUYNUAU - BJEVVDNTXQVYMUYNTEVVLVVDVWHYRVYOYSVVKYTQUVOYEVJUWCUWDPZUWDUWJWKUWCUVRVY - KVYQVVJYOCGULUMCGUVNWNXF $. + lgs0 cv cprime cpc cmpt cseq nnuz wf eqid lgsfcl3 ffvelcdm syl2an lgscl + syl3anc eqtrd adantlr ifbieq1d zexpcl 1zzd ifcldadc fvmptd3 lgsval4 a1i + 0z zdclt dcan2 sylc ffvelrnda seqf ffvelrnd syld con3dimp iffalsed cneg + sylibrd 3eqtr4rd cabs lgsdilem cuz simpl3 nnabscl sylan simpll1 simpll3 + eleqtrdi elnnuz biimpri simpll2 lgsdirprm pczcl syl12anc mulexpd eqcomi + prmz 1t1e1 3eqtr4a prmdc eleq1w oveq1 prod3fmul neg1cn neg1z mul4d dcne + zmulcl ) AEFZBEFZCEFZUCZAGUOZBGUOZHZHZCGIZABJKZCLKZACLKZBCLKZJKZICGUOZU + WCUWDHZAUDMKZNIZNGOZBUDMKZNIZNGOZJKZUWEUDMKZNIZNGOZUWIUWFUWKUWMUWRUXAIU + WMUEZUWKUWMHZNUWQJKZUWQUWRUXAUVSUXDUWQIUWBUWDUWMUVSUWQUVSUWPNGUFUVSUGUV + SUHUVSUWOEFZNEFZUWPPUVQUVPUXEUVRBUIUJUKUWONULUMUNZUPUQUXCUWNNUWQJUWMUWN + NIUWKUWMNGURUSUTUXCUWTUWPNGUXCUWSUWONUXCUWSUWLUWOJKNUWOJKUWOUXCABUWCAUF + FZUWDUWMUWCAUVPUVQUVRUWBVAZQZVBUWCBUFFUWDUWMUWCBUVPUVQUVRUWBVCZQZVBVEUX + CUWLNUWOJUWKUWMVDUTUXCUWOUWCUWOUFFUWDUWMUWCBUXLVFVBUPVGVHVIVJUWKUXBHZGU + WQJKZGUWRUXAUVSUXNGIUWBUWDUXBUVSUWQUXGVOUQUXMUWNGUWQJUXBUWNGIUWKUWMNGVK + USUTUXMUWTNGUWKUWTUWMUWKUWTUWLNVLRZUWMUWKUWLUWSVLRZUWTUXOUWCUXPUWDUWCAU + WEVLRZUXPUWCUVPUVQUXQUXIUXKABVMVNUWCUVPUWEEFZUXQUXPVPUXIUWCABUXIUXKVQZA + UWEVRVNVSVTUWSNUWLVLWAWBUWKUXOUWLNWCRZNUWLWCRZHZUWMUWKUXOUXTUYAUWKUWLEF + ZNTFUXOUXTWFUWKUWLUWCUWLTFZUWDUWCUYDUWLGIZUWCUYEAGIZUWCAGUVSUVTUWAWDWEU + WCUXHUYEUYFVPUXJAWGWHWIUWCUWLWJFZUYDUYEWKUWCUVPUYGUXIAWLWHUWLWMWNWOVTZW + PZWSUWLNWQUMUWKUWLUYHWRWTUWKUWLXAFNXAFUWMUYBVPUWKUWLUYHXBXCUWLNXDUMUUEU + UAUUBUUCVJUWKUWMPZUWMUXBWKUWKUYCUXFUYJUYIUKUWLNULUMUWMXEWHXFUWKUWGUWNUW + HUWQJUWDUWCUWGAGLKZUWNCGALXGUWCUVPUYKUWNIUXIAXKWHXHUWDUWCUWHBGLKZUWQCGB + LXGUWCUVQUYLUWQIUXKBXKWHXHSUWDUWCUWFUWEGLKZUXACGUWELXGUWCUXRUYMUXAIUXSU + WEXKWHXHUUFUWCUWJHZCGXIRZUWEGXIRHNUUDZNOZCUUGXJZJDTDXLZXMFZUWEUYSLKZUYS + CXNKZMKZNOZXOZNXPXJZJKZUYOAGXIRZHZUYPNOZUYOBGXIRZHZUYPNOZJKZUYRJDTUYTAU + YSLKZVUBMKZNOZXOZNXPZXJZUYRJDTUYTBUYSLKZVUBMKZNOZXOZNXPZXJZJKZJKZUWFUWI + UYNUYQVUNVUFVVGJUWCUYQVUNIUWJABCUUHVTUYNUAVURVVDVUENUYRUYNUYRTNUUIXJZUW + CUVRUWJUYRTFUVPUVQUVRUWBUUJZCUUKUULZXQUUOUYNUAXLZVVIFZHZVVLVURXJZUYNTEV + URXRZVVLTFZVVOEFVVMUYNUVPUVRUWJVVPUVPUVQUVRUWBUWJUUMZUVPUVQUVRUWBUWJUUN + ZUWCUWJVDZADVURCVURXSZXTYDZVVQVVMVVLUUPUUQZTEVVLVURYAYBQVVNVVLVVDXJZUYN + TEVVDXRZVVQVWDEFVVMUYNUVQUVRUWJVWEUVPUVQUVRUWBUWJUURZVVSVVTBDVVDCVVDXSZ + XTYDZVWCTEVVLVVDYAYBQVVNVVLXMFZUWEVVLLKZVVLCXNKZMKZNOZVWIAVVLLKZVWKMKZN + OZVWIBVVLLKZVWKMKZNOZJKZVVLVUEXJVVOVWDJKVVNVWIVWMVWTIZVWIUEZUYNVWIVXAVV + MUYNVWIHZVWLVWOVWRJKZVWMVWTVXCVWLVWNVWQJKZVWKMKVXDVXCVWJVXEVWKMVXCUVPUV + QVWIVWJVXEIUYNUVPVWIVVRVTUYNUVQVWIVWFVTUYNVWIVDZABVVLUUSYDUTVXCVWNVWQVW + KVXCVWNUYNUVPVVLEFZVWNEFZVWIVVRVVLUVDZAVVLYCYBZQVXCVWQUYNUVQVXGVWQEFZVW + IVWFVXIBVVLYCYBZQVXCVWIUVRUWJVWKWJFZVXFUYNUVRVWIVVSVTUYNUWJVWIVVTVTVVLC + UUTUVAZUVBYEVWIVWMVWLIUYNVWIVWLNURUSVWIVWTVXDIUYNVWIVWPVWOVWSVWRJVWIVWO + NURVWIVWRNURSUSVJYFVXBVXAVVNVXBNNNJKZVWMVWTVXONUVEUVCVWIVWLNVKVXBVWPNVW + SNJVWIVWONVKVWIVWRNVKSUVFUSVVNVWIPZVWIVXBWKVVNVVQVXPVVMVVQUYNVWCUSZVVLU + VGWHZVWIXEWHXFVVNDVVLVUDVWMTVUEEVUEXSZUYSVVLIZUYTVWIVUCVWLNDUAXMUVHZVXT + VUAVWJVUBVWKMUYSVVLUWELXGUYSVVLCXNUVIZSYGVXQVVNVWIVWLNEVVNVWIHZVWJEFZVX + MVWLEFVYCUXRVXGVYDUWCUXRUWJVVMVWIUXSUQVWIVXGVVNVXIUSUWEVVLYCVNUYNVWIVXM + VVMVXNYFZVWJVWKYHVNVVNVXBHYIZVXRYJYKVVNVVOVWPVWDVWSJVVNDVVLVUQVWPTVUREV + WAVXTUYTVWIVUPVWONVYAVXTVUOVWNVUBVWKMUYSVVLALXGVYBSYGVXQVVNVWIVWONEVYCV + XHVXMVWOEFUYNVWIVXHVVMVXJYFVYEVWNVWKYHVNVYFVXRYJYKVVNDVVLVVCVWSTVVDEVWG + VXTUYTVWIVVBVWRNVYAVXTVVAVWQVUBVWKMUYSVVLBLXGVYBSYGVXQVVNVWIVWRNEVYCVXK + VXMVWREFUYNVWIVXKVVMVXLYFVYEVWQVWKYHVNVYFVXRYJYKSVJUVJSUYNUXRUVRUWJUWFV + UGIUWCUXRUWJUXSVTVVSVVTUWEDVUECVXSYLYDUYNUWIVUJVUTJKZVUMVVFJKZJKVVHUYNU + WGVYGUWHVYHJUYNUVPUVRUWJUWGVYGIVVRVVSVVTADVURCVWAYLYDUYNUVQUVRUWJUWHVYH + IVWFVVSVVTBDVVDCVWGYLYDSUYNVUJVUTVUMVVFUYNVUIUYPNUFUYPUFFUYNUVKYMUYNUGU + YNUYOPZVUHPZVUIPUYNUVRGEFZVYIVVSYNCGYOUMZUYNUVPVYKVYJVVRYNAGYOUMUYOVUHY + PYQUNUYNVUTUYNTEUYRVUSUYNUAUBJEVURNTXQUYNYIZUYNTEVVLVURVWBYRVXGUBXLZEFH + VVLVYNJKEFUYNVVLVYNUVOUSZYSVVKYTQUYNVUMUYNVULUYPNEUYPEFUYNUVLYMVYMUYNVY + IVUKPZVULPVYLUYNUVQVYKVYPVWFYNBGYOUMUYOVUKYPYQUNQUYNVVFUYNTEUYRVVEUYNUA + UBJEVVDNTXQVYMUYNTEVVLVVDVWHYRVYOYSVVKYTQUVMYEVJUWCUWDPZUWDUWJWKUWCUVRV + YKVYQVVJYNCGULUMCGUVNWNXF $. $} ${ @@ -160410,12 +160410,12 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is cn vk vv w3a wne clt cneg cabs cv cprime clgs cmpt cseq 3anrot lgsdilem sylanb wb ancom ifbi ax-mp oveq12i 3eqtr4g simpl2 simpl3 zmulcld simprl cuz cap 0z zapne sylancl mpbird simprr mulap0d nnabscl syl2anc eleqtrdi - mpbid nnuz wf simpl1 eqid lgsfcl3 syl3anc elnnuz biimpri ffvelrn syl2an - caddc simpr ad2antrr pcmul syl122anc oveq2d prmz adantl lgscl cn0 pczcl - wn syl12anc expaddd eqtrd iftrue 3eqtr4rd 1t1e1 iffalse 3eqtr4a exmiddc - wdc prmdc syl mpjaodan eleq1w oveq2 oveq1 ifbieq1d zexpcl 1zzd ifcldadc - wo fvmptd3 prod3fmul lgsdilem2 mulcomd fveq2d lgsval4 neg1z zdclt dcan2 - eqtr4d a1i sylc ifcldcd ffvelrnda zmulcl seqf ffvelrnd mul4d 3eqtr4d ) + mpbid nnuz wf simpl1 eqid lgsfcl3 syl3anc elnnuz biimpri ffvelcdm caddc + syl2an wn simpr ad2antrr pcmul syl122anc oveq2d prmz adantl lgscl pczcl + cn0 syl12anc expaddd eqtrd iftrue 3eqtr4rd 1t1e1 iffalse 3eqtr4a wo wdc + prmdc exmiddc mpjaodan eleq1w oveq2 oveq1 ifbieq1d zexpcl 1zzd ifcldadc + syl fvmptd3 prod3fmul lgsdilem2 mulcomd fveq2d eqtr4d lgsval4 neg1z a1i + zdclt dcan2 sylc ifcldcd ffvelrnda zmulcl seqf ffvelrnd mul4d 3eqtr4d ) AEFZBEFZCEFZUCZBGUDZCGUDZHZHZBCIJZGUEKZAGUEKZHZLUFZLMZUUHUGNZIDTDUHZUIF ZAUUOUJJZUUOUUHOJZPJZLMZUKZLULNZIJZBGUEKZUUJHZUULLMZCGUEKZUUJHZUULLMZIJ ZBUGNZIDTUUPUUQUUOBOJZPJZLMZUKZLULZNZCUGNZIDTUUPUUQUUOCOJZPJZLMZUKZLULZ @@ -160428,34 +160428,34 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is GKZUUDUUCUUDUUEVEZUUGUUAGEFZUXIUUDUPUXCVHBGVIVJVKUUGCGVGKZUUEUUCUUDUUEV LZUUGUUBUXKUXLUUEUPUXDVHCGVIVJVKVMUUGUXAUXKUXFUXBUPUXEVHUUHGVIVJVQZUUHV NVOVRVPUUGUAUHZUWTFZHZUXOUVONZUUGTEUVOVSZUXOTFZUXREFUXPUUGYTUUAUUDUXSYT - UUAUUBUUFVTZUXCUXJADUVOBUVOWAZWBWCZUXTUXPUXOWDWEZTEUXOUVOWFWGRUXQUXOUWB + UUAUUBUUFVTZUXCUXJADUVOBUVOWAZWBWCZUXTUXPUXOWDWEZTEUXOUVOWFWHRUXQUXOUWB NZUUGTEUWBVSZUXTUYEEFUXPUUGYTUUBUUEUYFUYAUXDUXMADUWBCUWBWAZWBWCZUYDTEUX - OUWBWFWGRUXQUXOUIFZAUXOUJJZUXOBOJZPJZLMZUYIUYJUXOCOJZPJZLMZIJZUYIUYJUXO - UUHOJZPJZLMZUXRUYEIJUXOUVANUXQUYIUYQUYTQZUYIWSZUXQUYIHZUYSUYLUYOIJZUYTU - YQVUCUYSUYJUYKUYNWHJZPJVUDVUCUYRVUEUYJPVUCUYIUUAUUDUUBUUEUYRVUEQUXQUYIW - IZUUGUUAUXPUYIUXCWJZUUGUUDUXPUYIUXJWJZUUGUUBUXPUYIUXDWJZUUGUUEUXPUYIUXM - WJZBCUXOWKWLWMVUCUYJUYKUYNVUCUYJVUCYTUXOEFZUYJEFZUUGYTUXPUYIUYAWJUYIVUK - UXQUXOWNWOAUXOWPVOZRVUCUYIUUBUUEUYNWQFZVUFVUIVUJUXOCWRWTZVUCUYIUUAUUDUY - KWQFZVUFVUGVUHUXOBWRWTZXAXBUYIUYTUYSQUXQUYIUYSLXCWOUYIUYQVUDQUXQUYIUYMU - YLUYPUYOIUYIUYLLXCUYIUYOLXCSWOXDVUBVUAUXQVUBLLIJLUYQUYTXEVUBUYMLUYPLIUY - IUYLLXFUYIUYOLXFSUYIUYSLXFXGWOUXPUYIVUBXTZUUGUXPUXTVURUYDUXTUYIXIZVURUX - OXJZUYIXHXKXKWOXLUXQUXRUYMUYEUYPIUXQDUXOUVNUYMTUVOEUYBUUOUXOQZUUPUYIUVM - UYLLDUAUIXMZVVAUUQUYJUVLUYKPUUOUXOAUJXNZUUOUXOBOXOSXPUXPUXTUUGUYDWOZUXQ - UYIUYLLEVUCVULVUPUYLEFVUMVUQUYJUYKXQVOUXQVUBHXRZUXQUXTVUSVVDVUTXKZXSYAU + OUWBWFWHRUXQUXOUIFZAUXOUJJZUXOBOJZPJZLMZUYIUYJUXOCOJZPJZLMZIJZUYIUYJUXO + UUHOJZPJZLMZUXRUYEIJUXOUVANUXQUYIUYQUYTQZUYIWIZUXQUYIHZUYSUYLUYOIJZUYTU + YQVUCUYSUYJUYKUYNWGJZPJVUDVUCUYRVUEUYJPVUCUYIUUAUUDUUBUUEUYRVUEQUXQUYIW + JZUUGUUAUXPUYIUXCWKZUUGUUDUXPUYIUXJWKZUUGUUBUXPUYIUXDWKZUUGUUEUXPUYIUXM + WKZBCUXOWLWMWNVUCUYJUYKUYNVUCUYJVUCYTUXOEFZUYJEFZUUGYTUXPUYIUYAWKUYIVUK + UXQUXOWOWPAUXOWQVOZRVUCUYIUUBUUEUYNWSFZVUFVUIVUJUXOCWRWTZVUCUYIUUAUUDUY + KWSFZVUFVUGVUHUXOBWRWTZXAXBUYIUYTUYSQUXQUYIUYSLXCWPUYIUYQVUDQUXQUYIUYMU + YLUYPUYOIUYIUYLLXCUYIUYOLXCSWPXDVUBVUAUXQVUBLLIJLUYQUYTXEVUBUYMLUYPLIUY + IUYLLXFUYIUYOLXFSUYIUYSLXFXGWPUXPUYIVUBXHZUUGUXPUXTVURUYDUXTUYIXIZVURUX + OXJZUYIXKXTXTWPXLUXQUXRUYMUYEUYPIUXQDUXOUVNUYMTUVOEUYBUUOUXOQZUUPUYIUVM + UYLLDUAUIXMZVVAUUQUYJUVLUYKPUUOUXOAUJXNZUUOUXOBOXOSXPUXPUXTUUGUYDWPZUXQ + UYIUYLLEVUCVULVUPUYLEFVUMVUQUYJUYKXQVOUXQVUBHXRZUXQUXTVUSVVDVUTXTZXSYAU XQDUXOUWAUYPTUWBEUYGVVAUUPUYIUVTUYOLVVBVVAUUQUYJUVSUYNPVVCUUOUXOCOXOSXP VVDUXQUYIUYOLEVUCVULVUNUYOEFVUMVUOUYJUYNXQVOVVEVVFXSYASUXQDUXOUUTUYTTUV AEUVAWAZVVAUUPUYIUUSUYSLVVBVVAUUQUYJUURUYRPVVCUUOUXOUUHOXOSXPVVDUXQUYIU - YSLEVUCVULUYRWQFZUYSEFVUMVUCUYIUXAUXBVVHVUFUUGUXAUXPUYIUXEWJUUGUXBUXPUY - IUXNWJUXOUUHWRWTUYJUYRXQVOVVEVVFXSYAXDYBUUGUVQUWRUWDUWSIUUGADUVOBCUYAUX + YSLEVUCVULUYRWSFZUYSEFVUMVUCUYIUXAUXBVVHVUFUUGUXAUXPUYIUXEWKUUGUXBUXPUY + IUXNWKUXOUUHWRWTUYJUYRXQVOVVEVVFXSYAXDYBUUGUVQUWRUWDUWSIUUGADUVOBCUYAUX CUXDUXJUXMUYBYCUUGUWDCBIJZUGNZUWCNUWSUUGADUWBCBUYAUXDUXCUXMUXJUYGYCUUGU - UNVVJUWCUUGUUHVVIUGUUGBCUXGUXHYDYEYEYJSYJSUUGYTUXAUXBUWGUVCQUYAUXEUXNAD - UVAUUHVVGYFWCUUGUWJUVFUVQIJZUVIUWDIJZIJUWFUUGUWHVVKUWIVVLIUUGYTUUAUUDUW - HVVKQUYAUXCUXJADUVOBUYBYFWCUUGYTUUBUUEUWIVVLQUYAUXDUXMADUWBCUYGYFWCSUUG - UVFUVQUVIUWDUUGUVFUUGUVEUULLEUULEFUUGYGYKZUUGXRZUUGUVDXIZUUJXIZUVEXIUUG - UUAUXKVVOUXCVHBGYHVJUUGYTUXKVVPUYAVHAGYHVJZUVDUUJYIYLYMRUUGUVQUUGTEUVKU - VPUUGUAUBIEUVOLTVRVVNUUGTEUXOUVOUYCYNVUKUBUHZEFHUXOVVRIJEFUUGUXOVVRYOWO + UNVVJUWCUUGUUHVVIUGUUGBCUXGUXHYDYEYEYFSYFSUUGYTUXAUXBUWGUVCQUYAUXEUXNAD + UVAUUHVVGYGWCUUGUWJUVFUVQIJZUVIUWDIJZIJUWFUUGUWHVVKUWIVVLIUUGYTUUAUUDUW + HVVKQUYAUXCUXJADUVOBUYBYGWCUUGYTUUBUUEUWIVVLQUYAUXDUXMADUWBCUYGYGWCSUUG + UVFUVQUVIUWDUUGUVFUUGUVEUULLEUULEFUUGYHYIZUUGXRZUUGUVDXIZUUJXIZUVEXIUUG + UUAUXKVVOUXCVHBGYJVJUUGYTUXKVVPUYAVHAGYJVJZUVDUUJYKYLYMRUUGUVQUUGTEUVKU + VPUUGUAUBIEUVOLTVRVVNUUGTEUXOUVOUYCYNVUKUBUHZEFHUXOVVRIJEFUUGUXOVVRYOWP ZYPUUGUUAUUDUVKTFUXCUXJBVNVOYQRUUGUVIUUGUVHUULLEVVMVVNUUGUVGXIZVVPUVHXI - UUGUUBUXKVVTUXDVHCGYHVJVVQUVGUUJYIYLYMRUUGUWDUUGTEUVRUWCUUGUAUBIEUWBLTV + UUGUUBUXKVVTUXDVHCGYJVJVVQUVGUUJYKYLYMRUUGUWDUUGTEUVRUWCUUGUAUBIEUWBLTV RVVNUUGTEUXOUWBUYHYNVVSYPUUGUUBUUEUVRTFUXDUXMCVNVOYQRYRXBYS $. $} @@ -164030,14 +164030,14 @@ which membership in it is a bounded proposition ( ~ df-bdc ). (Contributed by BJ, 6-Aug-2024.) $) bj-charfunr $p |- ( ph -> A. x e. X DECID -. x e. A ) $= ( cv wcel wn wa wo c0 wral wi com ex adantr rsp imp adantl wceq cdif cmap - wdc cfv wne cin co wf elmapi ffvelrn 0elnn nn0eln0 orbi2d mpbid syl6 elin - syl syl5bir expd necon2bd eldif necon3ad orim12d mpdd rexlimddv ralrimiva - df-dc sylibr ) ABGZCHZIZUDZBEAVJEHZJVLVLIZKZVMAVNVPAVJDGZUEZLUFZBECUGZMZV - RLUAZBECUBZMZJZVNVPNZDOEUCUHZFVQWGHZWEJZWFAWIVNWBVSKZVPWHVNWJNWEWHVNVROHZ - WJWHEOVQUIZVNWKNVQOEUJWLVNWKEOVJVQUKPURWKWBLVRHZKWJVRULWKWMVSWBVRUMUNUOUP - QWEVNWJVPNZNWHWEVNWNWEVNJZWBVLVSVOWOVKVRLWEVNVKVSNZWAVNWPNWDWAVNVKVSVNVKJ - VJVTHWAVSVJECUQVSBVTRUSUTQSVAWOVLVRLWEVNVLWBNZWDVNWQNWAWDVNVLWBVNVLJVJWCH - WDWBVJECVBWBBWCRUSUTTSVCVDPTVETVFSVLVHVIVG $. + wdc cfv wne cin co wf elmapi ffvelcdm syl 0elnn nn0eln0 orbi2d mpbid syl6 + elin syl5bir expd necon2bd eldif necon3ad mpdd rexlimddv sylibr ralrimiva + orim12d df-dc ) ABGZCHZIZUDZBEAVJEHZJVLVLIZKZVMAVNVPAVJDGZUEZLUFZBECUGZMZ + VRLUAZBECUBZMZJZVNVPNZDOEUCUHZFVQWGHZWEJZWFAWIVNWBVSKZVPWHVNWJNWEWHVNVROH + ZWJWHEOVQUIZVNWKNVQOEUJWLVNWKEOVJVQUKPULWKWBLVRHZKWJVRUMWKWMVSWBVRUNUOUPU + QQWEVNWJVPNZNWHWEVNWNWEVNJZWBVLVSVOWOVKVRLWEVNVKVSNZWAVNWPNWDWAVNVKVSVNVK + JVJVTHWAVSVJECURVSBVTRUSUTQSVAWOVLVRLWEVNVLWBNZWDVNWQNWAWDVNVLWBVNVLJVJWC + HWDWBVJECVBWBBWCRUSUTTSVCVHPTVDTVESVLVIVFVG $. $} ${ diff --git a/mmil.raw.html b/mmil.raw.html index 684b0af428..86d9338689 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -2876,7 +2876,7 @@ f0cli -~ ffvelrn +~ ffvelcdm