diff --git a/set.mm b/set.mm index 4716c10c7..45fefbf23 100644 --- a/set.mm +++ b/set.mm @@ -131602,28 +131602,28 @@ least element (schema form). (Contributed by NM, 17-Aug-2001.) $) E. x e. A ( A. y e. A -. x < y /\ A. y e. B ( y < x -> E. z e. A y < z ) ) ) $= ( vm vn vw cz cv cle wbr wral wrex clt wa wceq wcel cneg zred c0 wn breq1 - wss wne wi cbvralv breq2 ralbidv syl5bb cbvrexv crab cinf cuz cfv simp1rl - cr znegcld simp2 simp1rr simp3 rspcdva lenegcon1d eluz2 syl3anbrc rabssdv - w3a wex n0 ssel2 zcnd negnegd simpr eqeltrd eleq1d rspcev syl2anc exlimdv - negeq ex imp sylan2b adantr rabn0 sylibr infssuzcl cbvrabv elrab2 simprbi + wss wne wi cbvralvw breq2 ralbidv syl5bb cbvrexvw crab cr cuz cfv simp1rl + cinf w3a znegcld simp2 simp1rr simp3 rspcdva lenegcon1d syl3anbrc rabssdv + eluz2 wex n0 ssel2 zcnd negnegd simpr eqeltrd negeq eleq1d rspcev syl2anc + ex exlimdv imp sylan2b adantr sylibr infssuzcl cbvrabv elrab2 simprbi syl simpll sselda ssrab2 sseldi elrabd infssuzle lenegcon2d lensymd ralrimiva - syl ralrimivw notbid imbi1d anbi12d syl12anc rexlimdvaa syl5bi 3impia ) D - IUDZDUAUEZBJZAJZKLZBDMZAINZXKXJOLZUBZBDMZXJXKOLZXJCJZOLZCDNZUFZBEMZPZADNZ - XNFJZGJZKLZFDMZGINXHXIPZYEXMYIAGIXMYFXKKLZFDMXKYGQZYIXLYKBFDXJYFXKKUCUGYL - YKYHFDXKYGYFKUHUIUJUKYJYIYEGIYJYGIRZYIPZPZHJZSZDRZHIULZUQOUMZSZDRZUUAXJOL - ZUBZBDMZXJUUAOLZYAUFZBEMZYEYOYTYSRZUUBYOYSYGSZUNUOZUDZYSUAUEZUUIYOYRHIUUK - YOYPIRZYRVGZUUJIRZUUNUUJYPKLYPUUKRUUOYGYMYIYJUUNYRUPZURYOUUNYRUSZUUOYPYGU - UOYPUURTUUOYGUUQTUUOYHYQYGKLFDYQYFYQYGKUCYMYIYJUUNYRUTYOUUNYRVAVBVCUUJYPV - DVEVFZYOYRHINZUUMYJUUTYNXIXHYGDRZGVHZUUTGDVIXHUVBUUTXHUVAUUTGXHUVAUUTXHUV - APZUUPUUJSZDRZUUTUVCYGDIYGVJZURUVCUVDYGDUVCYGUVCYGUVFVKVLXHUVAVMVNYRUVEHU - UJIYPUUJQYQUVDDYPUUJVSVOVPVQVTVRWAWBWCYRHIWDWEYSUUJWFVQZUUIYTIRUUBUUJDRZU - UBGYTIYSYGYTQUUJUUADYGYTVSVOYRUVHHGIYPYGQYQUUJDYPYGVSVOWGWHWIWSZYOUUDBDYO - XJDRZPZXJUUAUVKXJYODIXJXHXIYNWJWKZTZUVKUUAUVKYTUVKYSIYTYRHIWLYOUUIUVJUVGW - CWMZURTUVKYTXJUVKYTUVNTUVMUVKUULXJSZYSRYTUVOKLYOUULUVJUUSWCUVKYRUVOSZDRHU - VOIYPUVOQYQUVPDYPUVOVSVOUVKXJUVLURUVKUVPXJDUVKXJUVKXJUVLVKVLYOUVJVMVNWNUV - OYSUUJWOVQWPWQWRYOUUGBEYOUUBUUGUVIUUBUUFYAXTUUFCUUADXSUUAXJOUHVPVTWSWTYDU - UEUUHPAUUADXKUUAQZXQUUEYCUUHUVQXPUUDBDUVQXOUUCXKUUAXJOUCXAUIUVQYBUUGBEUVQ - XRUUFYAXKUUAXJOUHXBUIXCVPXDXEXFXG $. + rabn0 ralrimivw notbid imbi1d anbi12d syl12anc rexlimdvaa syl5bi 3impia ) + DIUDZDUAUEZBJZAJZKLZBDMZAINZXKXJOLZUBZBDMZXJXKOLZXJCJZOLZCDNZUFZBEMZPZADN + ZXNFJZGJZKLZFDMZGINXHXIPZYEXMYIAGIXMYFXKKLZFDMXKYGQZYIXLYKBFDXJYFXKKUCUGY + LYKYHFDXKYGYFKUHUIUJUKYJYIYEGIYJYGIRZYIPZPZHJZSZDRZHIULZUMOUQZSZDRZUUAXJO + LZUBZBDMZXJUUAOLZYAUFZBEMZYEYOYTYSRZUUBYOYSYGSZUNUOZUDZYSUAUEZUUIYOYRHIUU + KYOYPIRZYRURZUUJIRZUUNUUJYPKLYPUUKRUUOYGYMYIYJUUNYRUPZUSYOUUNYRUTZUUOYPYG + UUOYPUURTUUOYGUUQTUUOYHYQYGKLFDYQYFYQYGKUCYMYIYJUUNYRVAYOUUNYRVBVCVDUUJYP + VGVEVFZYOYRHINZUUMYJUUTYNXIXHYGDRZGVHZUUTGDVIXHUVBUUTXHUVAUUTGXHUVAUUTXHU + VAPZUUPUUJSZDRZUUTUVCYGDIYGVJZUSUVCUVDYGDUVCYGUVCYGUVFVKVLXHUVAVMVNYRUVEH + UUJIYPUUJQYQUVDDYPUUJVOVPVQVRVSVTWAWBWCYRHIWSWDYSUUJWEVRZUUIYTIRUUBUUJDRZ + UUBGYTIYSYGYTQUUJUUADYGYTVOVPYRUVHHGIYPYGQYQUUJDYPYGVOVPWFWGWHWIZYOUUDBDY + OXJDRZPZXJUUAUVKXJYODIXJXHXIYNWJWKZTZUVKUUAUVKYTUVKYSIYTYRHIWLYOUUIUVJUVG + WCWMZUSTUVKYTXJUVKYTUVNTUVMUVKUULXJSZYSRYTUVOKLYOUULUVJUUSWCUVKYRUVOSZDRH + UVOIYPUVOQYQUVPDYPUVOVOVPUVKXJUVLUSUVKUVPXJDUVKXJUVKXJUVLVKVLYOUVJVMVNWNU + VOYSUUJWOVRWPWQWRYOUUGBEYOUUBUUGUVIUUBUUFYAXTUUFCUUADXSUUAXJOUHVQVSWIWTYD + UUEUUHPAUUADXKUUAQZXQUUEYCUUHUVQXPUUDBDUVQXOUUCXKUUAXJOUCXAUIUVQYBUUGBEUV + QXRUUFYAXKUUAXJOUHXBUIXCVQXDXEXFXG $. $( The supremum of a bounded-above set of integers is a member of the set. (This version of ~ suprzcl avoids ~ ax-pre-sup .) (Contributed by Mario @@ -132264,21 +132264,21 @@ Rational numbers (as a subset of complex numbers) wf1o wf wi wral wfn ovex fnmpoi c1st c2nd cop 1st2nd2 df-ov syl6eqr xp1st fveq2d xp2nd oveq1 oveq2 oveq2d ovmpo syl2anc eqtrd ax-icn sylancr addcld recnd mulcl eqeltrd rgen ffnfv mpbir2an wb jca cru syl2an oveq12d eqeq12d - fveq2 vtoclga eqeqan12d fvex opth syl6bb 3bitr4d biimpd rgen2a dff13 cnre - eqeq2d 2rexbiia sylibr rexxp dffo3 df-f1o ) IIUAZJCUDWRJCUBZWRJCUCZWSWRJC - UEZEKZCLZFKZCLZMZXBXDMZUFZFWRUGEWRUGXACWRUHXCJNZEWRUGABIIAKZOBKZPQZRQZCDX - JXLRUIUJXIEWRXBWRNZXCXBUKLZOXBULLZPQZRQZJXNXCXOXPCQZXRXNXCXOXPUMZCLXSXNXB - XTCXBIIUNZURXOXPCUOUPXNXOINZXPINZXSXRMXBIIUQZXBIIUSZABXOXPIIXMXRCXOXLRQXJ - XOXLRUTXKXPMXLXQXORXKXPOPVAVBDXOXQRUIVCVDVEZXNXOXQXNXOYDVIXNOJNXPJNXQJNVF - XNXPYEVIOXPVJVGVHVKVLEWRJCVMVNZXHEFWRXNXDWRNZSZXFXGYIXRXDUKLZOXDULLZPQZRQ - ZMZXOYJMXPYKMSZXFXGXNYBYCSYJINZYKINZSYNYOVOYHXNYBYCYDYEVPYHYPYQXDIIUQXDII - USVPXOXPYJYKVQVRXNYHXCXRXEYMYFXCXRMXEYMMEXDWRXGXCXEXRYMXBXDCWAXGXOYJXQYLR - XBXDUKWAXGXPYKOPXBXDULWAVBVSVTYFWBWCYIXGXTYJYKUMZMYOXNYHXBXTXDYRYAXDIIUNW - CXOXPYJYKXBUKWDXBULWDWEWFWGWHWIEFWRJCWJVNWTXAXDXCMZEWRTZFJUGYGYTFJXDJNZXD - GKZHKZCQZMZHITGITZYTUUAXDUUBOUUCPQZRQZMZHITGITUUFGHXDWKUUEUUIGHIIUUBINUUC - INSUUDUUHXDABUUBUUCIIXMUUHCUUBXLRQXJUUBXLRUTXKUUCMXLUUGUUBRXKUUCOPVAVBDUU - BUUGRUIVCWLWMWNYSUUEEGHIIXBUUBUUCUMZMZXCUUDXDUUKXCUUJCLUUDXBUUJCWAUUBUUCC - UOUPWLWOWNVLEFWRJCWPVNWRJCWQVN $. + fveq2 vtoclga eqeqan12d fvex opth syl6bb 3bitr4d biimpd rgen2 cnre eqeq2d + dff13 2rexbiia sylibr rexxp dffo3 df-f1o ) IIUAZJCUDWRJCUBZWRJCUCZWSWRJCU + EZEKZCLZFKZCLZMZXBXDMZUFZFWRUGEWRUGXACWRUHXCJNZEWRUGABIIAKZOBKZPQZRQZCDXJ + XLRUIUJXIEWRXBWRNZXCXBUKLZOXBULLZPQZRQZJXNXCXOXPCQZXRXNXCXOXPUMZCLXSXNXBX + TCXBIIUNZURXOXPCUOUPXNXOINZXPINZXSXRMXBIIUQZXBIIUSZABXOXPIIXMXRCXOXLRQXJX + OXLRUTXKXPMXLXQXORXKXPOPVAVBDXOXQRUIVCVDVEZXNXOXQXNXOYDVIXNOJNXPJNXQJNVFX + NXPYEVIOXPVJVGVHVKVLEWRJCVMVNZXHEFWRWRXNXDWRNZSZXFXGYIXRXDUKLZOXDULLZPQZR + QZMZXOYJMXPYKMSZXFXGXNYBYCSYJINZYKINZSYNYOVOYHXNYBYCYDYEVPYHYPYQXDIIUQXDI + IUSVPXOXPYJYKVQVRXNYHXCXRXEYMYFXCXRMXEYMMEXDWRXGXCXEXRYMXBXDCWAXGXOYJXQYL + RXBXDUKWAXGXPYKOPXBXDULWAVBVSVTYFWBWCYIXGXTYJYKUMZMYOXNYHXBXTXDYRYAXDIIUN + WCXOXPYJYKXBUKWDXBULWDWEWFWGWHWIEFWRJCWLVNWTXAXDXCMZEWRTZFJUGYGYTFJXDJNZX + DGKZHKZCQZMZHITGITZYTUUAXDUUBOUUCPQZRQZMZHITGITUUFGHXDWJUUEUUIGHIIUUBINUU + CINSUUDUUHXDABUUBUUCIIXMUUHCUUBXLRQXJUUBXLRUTXKUUCMXLUUGUUBRXKUUCOPVAVBDU + UBUUGRUIVCWKWMWNYSUUEEGHIIXBUUBUUCUMZMZXCUUDXDUUKXCUUJCLUUDXBUUJCWAUUBUUC + CUOUPWKWOWNVLEFWRJCWPVNWRJCWQVN $. $} ${ @@ -134151,14 +134151,14 @@ Infinity and the extended real number system (cont.) xaddf $p |- +e : ( RR* X. RR* ) --> RR* $= ( vx vy cv cpnf wceq cmnf cc0 cif cxr wcel wral cxad wa 0xr wn cr anassrs a1i wo ifclda caddc co cxp wf pnfxr ifcli mnfxr ioran w3o elxr 3orass ord - sylbb con1d sylan2br readdcl syl2an rexrd an32s rgen2a df-xadd fmpo mpbi + sylbb con1d sylan2br readdcl syl2an rexrd an32s rgen2 df-xadd fmpo mpbi imp ) ACZDEZBCZFEZGDHZVEFEZVGDEZGFHZVKDVHFVEVGUAUBZHZHZHZHZIJZBIKAIKIIUCI - LUDVRABIVEIJZVGIJZMZVFVIVPIVIIJWAVFMVHGDINUEUFRWAVFOZMZVJVLVOIVLIJWCVJMVK - GFINUGUFRWAWBVJOZVOIJZVSWBWDMZVTWEVSWFMZVTMZVKDVNIDIJWHVKMUERWHVKOZMZVHFV - MIFIJWJVHMUGRWHWIVHOZVMIJZWGVTWIWKMZWLWGVTWMMZMVMWGVEPJZVGPJZVMPJWNWFVSVF - VJSZOZWOVFVJUHVSWRWOVSWOWQVSWOWQVSWOVFVJUIWOWQSVEUJWOVFVJUKUMULUNVDUOWMVT - VKVHSZOZWPVKVHUHVTWTWPVTWPWSVTWPWSVTWPVKVHUIWPWSSVGUJWPVKVHUKUMULUNVDUOVE - VGUPUQURQQTTUSQTTUTABIIVQILABVAVBVC $. + LUDVRABIIVEIJZVGIJZMZVFVIVPIVIIJWAVFMVHGDINUEUFRWAVFOZMZVJVLVOIVLIJWCVJMV + KGFINUGUFRWAWBVJOZVOIJZVSWBWDMZVTWEVSWFMZVTMZVKDVNIDIJWHVKMUERWHVKOZMZVHF + VMIFIJWJVHMUGRWHWIVHOZVMIJZWGVTWIWKMZWLWGVTWMMZMVMWGVEPJZVGPJZVMPJWNWFVSV + FVJSZOZWOVFVJUHVSWRWOVSWOWQVSWOWQVSWOVFVJUIWOWQSVEUJWOVFVJUKUMULUNVDUOWMV + TVKVHSZOZWPVKVHUHVTWTWPVTWPWSVTWPWSVTWPVKVHUIWPWSSVGUJWPVKVHUKUMULUNVDUOV + EVGUPUQURQQTTUSQTTUTABIIVQILABVAVBVC $. $( Value of the extended real multiplication operation. (Contributed by Mario Carneiro, 20-Aug-2015.) $) @@ -134780,9 +134780,9 @@ Infinity and the extended real number system (cont.) xmulf $p |- *e : ( RR* X. RR* ) --> RR* $= ( vx vy cv cc0 wceq wo clt wbr cpnf wa cmnf cif cxr wcel a1i orcom notbii wral wn ifclda cmul co cxp cxmu wf pnfxr mnfxr xmullem cr anbi12i syl2anb - 0xr ancom remulcld rexrd rgen2a df-xmul fmpo mpbi ) ACZDEZBCZDEZFZDDVBGHZ - UTIEZJVBDGHZUTKEZJFZDUTGHZVBIEZJUTDGHZVBKEZJFZFZIVEVHJVGVFJFZVJVMJVLVKJFZ - FZKUTVBUAUBZLZLZLZMNZBMRAMRMMUCMUDUEWCABMUTMNZVBMNZJZVDDWAMDMNWFVDJULOWFV + 0xr ancom remulcld rexrd rgen2 df-xmul fmpo mpbi ) ACZDEZBCZDEZFZDDVBGHZU + TIEZJVBDGHZUTKEZJFZDUTGHZVBIEZJUTDGHZVBKEZJFZFZIVEVHJVGVFJFZVJVMJVLVKJFZF + ZKUTVBUAUBZLZLZLZMNZBMRAMRMMUCMUDUEWCABMMUTMNZVBMNZJZVDDWAMDMNWFVDJULOWFV DSZJZVOIVTMIMNWHVOJUFOWHVOSZJZVRKVSMKMNWJVRJUGOWJVRSZJZVSWLUTVBUTVBUHWJWE WDJZVCVAFZSZJZVNVIFZSZJVQVPFZSVBUINWKWHWPWIWRWFWMWGWOWDWEUMVDWNVAVCPQUJVO WQVIVNPQUJVRWSVPVQPQVBUTUHUKUNUOTTTUPABMMWBMUDABUQURUS $. @@ -135285,44 +135285,44 @@ the expression make the whole thing evaluate to zero (on both sides), w3a syl elxr simpr pnfnlt adantr wb notbid adantl mpbird pm2.21d ad2antlr w3o ex wex ssel mnflt syl6 ancld eximdv n0 df-rex 3imtr4g imp a1d imbi12d ad2antrr 3jaod syl5bi ralimdv2 anim2d reximdva 3adant3 3expa ralnex ssel2 - mpd rexnal letric ord sylan an32s syl5bir ralimdva sylan2br breq2 cbvrexv - ralbii sylib pnfxr ralrimiv c1 caddc co rspcva adantrr ancoms sylan2 ltp1 - peano2re ancli ltletr mpand exp31 a1dd com4r xrltnr ax-mp mtbiri 2a1d cc0 - adantll 0re mpan mpan9 syl5ibr expd 3jaoi sylbi jca imbi1d rspcev sylancr - com13 syldan adantlr pm2.61dan mnfxr ral0 nltmnf rgen pm3.2i a1i pm2.61ne - mp2an ralrimivw anim12i jaodan ) DEUBZDFUBZAUCZBUCZGHZIZBDJZUUOUUNGHZUUOC - UCZGHZCDKZLZBEJZMZAEKZNDOZUUMUVFUULUUMUVFUUQBPJZUUSUVACPKZLZBEJZMZAEKZDPD - PQZUVEUVLAEUVNUURUVHUVDUVKUUQBDPUDUVNUVCUVJBEUVNUVBUVIUUSUVACDPUEUFUGUHUI - UUMDPUJZMZUUOUUNRHZBDJZAFKZUVFUUMUVOUVSUVFUUMUVOUVSUNZUURUVCBFJZMZAEKZUVF - UVTUWBAFKUWCABCDUAUWBUWBAFEUUNFOZUUNEOZUWBUUNUKULUMUOUUMUVOUWCUVFLUVSUVPU - WBUVEAEUVPUWEMZUWAUVDUURUWFUVCUVCBFEUWFUUOFOZUVCLZUUOEOZUVCLUWIUWGUUONQZU - UOSQZVFZUWFUWHMZUVCUUOUPZUWMUWGUVCUWJUWKUWFUWHUQUWEUWJUVCLUVPUWHUWEUWJUVC - UWEUWJMZUUSUVBUWOUUSIZNUUNGHZIZUWEUWRUWJUUNURUSUWJUWPUWRUTUWEUWJUUSUWQUUO - NUUNGTVAVBVCVDVGVEUWFUWKUVCLUWHUWFUWKUVCUWFUWKMUVCSUUNGHZSUUTGHZCDKZLZUVP - UXBUWEUWKUVPUXAUWSUUMUVOUXAUUMUUTDOZCVHUXCUWTMZCVHUVOUXAUUMUXCUXDCUUMUXCU - WTUUMUXCUUTFOZUWTDFUUTVIUUTVJZVKVLVMCDVNUWTCDVOVPVQVRVTUWKUVCUXBUTUWFUWKU - USUWSUVBUXAUUOSUUNGTUWKUVAUWTCDUUOSUUTGTUIZVSVBVCVGUSWAWBVGWCWDWEWFWJWGUU - MUVSIZUVFUVOUUMUXHUUNUUTRHZCDKZAFJZUVFUUMUXHMUUNUUORHZBDKZAFJZUXKUXHUUMUV - RIZAFJZUXNUVRAFWHUUMUXPUXNUUMUXOUXMAFUXOUVQIZBDKUUMUWDMZUXMUVQBDWKUXRUXQU - XLBDUUMUUODOZUWDUXQUXLLZUUMUXSMUWGUWDUXTDFUUOWIUWGUWDMUVQUXLUUOUUNWLWMWNW - OWEWPWQVQWRUXMUXJAFUXLUXIBCDUUOUUTUUNRWSWTXAXBUUMUXKMZNEOZNUUOGHZIZBDJZUU - ONGHZUVBLZBEJZMZUVFXCUYAUYEUYHUUMUYEUXKUUMUYDBDUUMUXSUWGUYDDFUUOVIUWGUWIU - YDUUOUKUUOURZUOVKXDUSUYAUYGBEUUMUXKUWIUYGLUWIUXKUUMUYGUWIUWLUXKUUMUYGLLZU - WNUWGUYKUWJUWKUXKUUMUYFUWGUVBUXKUUMUWGUVBLUYFUXKUUMUWGUVBUXKUUMMZUWGMUUOX - EXFXGZUUTRHZCDKZUVBUWGUYLUYMFOZUYOUUOXMZUYPUYLUYOUYPUXKUYOUUMUXJUYOAUYMFU - UNUYMQUXIUYNCDUUNUYMUUTRTUIXHXIXJXKUUMUWGUYOUVBLUXKUUMUWGMUYNUVACDUUMUXCU - WGUYNUVALZUUMUXCMZUXEUWGUYRDFUUTWIZUWGUXEUYRUWGUXEMUUOUYMGHZUYNUVAUWGVUAU - XEUUOXLUSUWGUWGUYPMUXEVUAUYNMUVALZUWGUYPUYQXNUWGUYPUXEVUBUUOUYMUUTXOWGWNX - PXJWNWOWEYEWJXQXRXSUWJUYGUXKUUMUWJUYFUVBUWJUYFNNGHZUYBVUCIXCNXTYAUUONNGTY - BVDYCUWKUXKUUMUYGUWKUYLUVBUYFUYLUVBUWKUXAUXKYDUUTRHZCDKZUUMUXAYDFOUXKVUEY - FUXJVUEAYDFUUNYDQUXIVUDCDUUNYDUUTRTUIXHYGUUMVUDUWTCDUYSUWTVUDUYSUXEUWTUYT - UXFUOVRWEYHUXGYIXRYJYKYLYQVQXDYMUVEUYIANEUUNNQZUURUYEUVDUYHVUFUUQUYDBDVUF - UUPUYCUUNNUUOGTVAUGVUFUVCUYGBEVUFUUSUYFUVBUUNNUUOGWSYNUGUHYOZYPYRYSYTUVMU - UMSEOSUUOGHZIZBPJZUUOSGHZUVILZBEJZMZUVMUUAVUJVUMVUIBUUBVULBEUWIVUKUVIUUOU - UCVDUUDUUEUVLVUNASEUUNSQZUVHVUJUVKVUMVUOUUQVUIBPVUOUUPVUHUUNSUUOGTVAUGVUO - UVJVULBEVUOUUSVUKUVIUUNSUUOGWSYNUGUHYOUUHUUFUUGVBUULUVGMUYBUYIUVFXCUULUYE - UVGUYHUULUYDBDUULUXSUWIUYDDEUUOVIUYJVKXDUVGUYGBEUVGUYFUVBUVAUYFCNDUUTNUUO - GWSYOVGUUIUUJVUGYPUUK $. + mpd rexnal letric ord sylan an32s ralimdva sylan2br breq2 cbvrexvw ralbii + syl5bir sylib pnfxr ralrimiv c1 caddc peano2re rspcva adantrr ancoms ltp1 + co sylan2 ancli ltletr mpand adantll exp31 a1dd com4r xrltnr ax-mp mtbiri + 2a1d cc0 0re mpan mpan9 syl5ibr expd 3jaoi sylbi com13 jca imbi1d sylancr + rspcev syldan adantlr pm2.61dan mnfxr ral0 nltmnf rgen mp2an a1i pm2.61ne + pm3.2i ralrimivw anim12i jaodan ) DEUBZDFUBZAUCZBUCZGHZIZBDJZUUOUUNGHZUUO + CUCZGHZCDKZLZBEJZMZAEKZNDOZUUMUVFUULUUMUVFUUQBPJZUUSUVACPKZLZBEJZMZAEKZDP + DPQZUVEUVLAEUVNUURUVHUVDUVKUUQBDPUDUVNUVCUVJBEUVNUVBUVIUUSUVACDPUEUFUGUHU + IUUMDPUJZMZUUOUUNRHZBDJZAFKZUVFUUMUVOUVSUVFUUMUVOUVSUNZUURUVCBFJZMZAEKZUV + FUVTUWBAFKUWCABCDUAUWBUWBAFEUUNFOZUUNEOZUWBUUNUKULUMUOUUMUVOUWCUVFLUVSUVP + UWBUVEAEUVPUWEMZUWAUVDUURUWFUVCUVCBFEUWFUUOFOZUVCLZUUOEOZUVCLUWIUWGUUONQZ + UUOSQZVFZUWFUWHMZUVCUUOUPZUWMUWGUVCUWJUWKUWFUWHUQUWEUWJUVCLUVPUWHUWEUWJUV + CUWEUWJMZUUSUVBUWOUUSIZNUUNGHZIZUWEUWRUWJUUNURUSUWJUWPUWRUTUWEUWJUUSUWQUU + ONUUNGTVAVBVCVDVGVEUWFUWKUVCLUWHUWFUWKUVCUWFUWKMUVCSUUNGHZSUUTGHZCDKZLZUV + PUXBUWEUWKUVPUXAUWSUUMUVOUXAUUMUUTDOZCVHUXCUWTMZCVHUVOUXAUUMUXCUXDCUUMUXC + UWTUUMUXCUUTFOZUWTDFUUTVIUUTVJZVKVLVMCDVNUWTCDVOVPVQVRVTUWKUVCUXBUTUWFUWK + UUSUWSUVBUXAUUOSUUNGTUWKUVAUWTCDUUOSUUTGTUIZVSVBVCVGUSWAWBVGWCWDWEWFWJWGU + UMUVSIZUVFUVOUUMUXHUUNUUTRHZCDKZAFJZUVFUUMUXHMUUNUUORHZBDKZAFJZUXKUXHUUMU + VRIZAFJZUXNUVRAFWHUUMUXPUXNUUMUXOUXMAFUXOUVQIZBDKUUMUWDMZUXMUVQBDWKUXRUXQ + UXLBDUUMUUODOZUWDUXQUXLLZUUMUXSMUWGUWDUXTDFUUOWIUWGUWDMUVQUXLUUOUUNWLWMWN + WOWEXAWPVQWQUXMUXJAFUXLUXIBCDUUOUUTUUNRWRWSWTXBUUMUXKMZNEOZNUUOGHZIZBDJZU + UONGHZUVBLZBEJZMZUVFXCUYAUYEUYHUUMUYEUXKUUMUYDBDUUMUXSUWGUYDDFUUOVIUWGUWI + UYDUUOUKUUOURZUOVKXDUSUYAUYGBEUUMUXKUWIUYGLUWIUXKUUMUYGUWIUWLUXKUUMUYGLLZ + UWNUWGUYKUWJUWKUXKUUMUYFUWGUVBUXKUUMUWGUVBLUYFUXKUUMUWGUVBUXKUUMMZUWGMUUO + XEXFXLZUUTRHZCDKZUVBUWGUYLUYMFOZUYOUUOXGZUYPUYLUYOUYPUXKUYOUUMUXJUYOAUYMF + UUNUYMQUXIUYNCDUUNUYMUUTRTUIXHXIXJXMUUMUWGUYOUVBLUXKUUMUWGMUYNUVACDUUMUXC + UWGUYNUVALZUUMUXCMZUXEUWGUYRDFUUTWIZUWGUXEUYRUWGUXEMUUOUYMGHZUYNUVAUWGVUA + UXEUUOXKUSUWGUWGUYPMUXEVUAUYNMUVALZUWGUYPUYQXNUWGUYPUXEVUBUUOUYMUUTXOWGWN + XPXJWNWOWEXQWJXRXSXTUWJUYGUXKUUMUWJUYFUVBUWJUYFNNGHZUYBVUCIXCNYAYBUUONNGT + YCVDYDUWKUXKUUMUYGUWKUYLUVBUYFUYLUVBUWKUXAUXKYEUUTRHZCDKZUUMUXAYEFOUXKVUE + YFUXJVUEAYEFUUNYEQUXIVUDCDUUNYEUUTRTUIXHYGUUMVUDUWTCDUYSUWTVUDUYSUXEUWTUY + TUXFUOVRWEYHUXGYIXSYJYKYLYMVQXDYNUVEUYIANEUUNNQZUURUYEUVDUYHVUFUUQUYDBDVU + FUUPUYCUUNNUUOGTVAUGVUFUVCUYGBEVUFUUSUYFUVBUUNNUUOGWRYOUGUHYQZYPYRYSYTUVM + UUMSEOSUUOGHZIZBPJZUUOSGHZUVILZBEJZMZUVMUUAVUJVUMVUIBUUBVULBEUWIVUKUVIUUO + UUCVDUUDUUHUVLVUNASEUUNSQZUVHVUJUVKVUMVUOUUQVUIBPVUOUUPVUHUUNSUUOGTVAUGVU + OUVJVULBEVUOUUSVUKUVIUUNSUUOGWRYOUGUHYQUUEUUFUUGVBUULUVGMUYBUYIUVFXCUULUY + EUVGUYHUULUYDBDUULUXSUWIUYDDEUUOVIUYJVKXDUVGUYGBEUVGUYFUVBUVAUYFCNDUUTNUU + OGWRYQVGUUIUUJVUGYPUUK $. $( Lemma for ~ xrinfmss . (Contributed by NM, 19-Jan-2006.) $) xrinfmsslem $p |- ( ( A C_ RR* /\ ( A C_ RR \/ -oo e. A ) ) -> E. x e. RR* @@ -135333,43 +135333,43 @@ the expression make the whole thing evaluate to zero (on both sides), syl6 a1d ad2antrr wb imbi12d adantl mpbird adantr nltmnf pm2.21d ad2antlr ex notbid 3jaod syl5bi ralimdv2 anim2d reximdva 3adant3 mpd ralnex rexnal 3expa ssel2 letric ancoms ord sylan an32s syl5bir ralimdva sylan2br breq1 - wo cbvrexv ralbii sylib mnfxr ralrimiv c1 cmin co peano2rem rspcva sylan2 - adantrr ltm1 ancri lelttr 3expb mpan2d adantll exp31 a1dd com4r cc0 mpan9 - 0re mpan syl5ibr expd xrltnr ax-mp mtbiri 3jaoi sylbi com13 imbi1d rspcev - 2a1d jca sylancr syldan pm2.61dan pnfxr ral0 pnfnlt rgen pm3.2i mp2an a1i - adantlr pm2.61ne ralrimivw anim12i jaodan ) DEUBZDFUBZBUNZAUNZGHZIZBDJZUU - QUUPGHZCUNZUUPGHZCDKZLZBEJZMZAEKZNDOZUUOUVHUUNUUOUVHUUSBPJZUVAUVCCPKZLZBE - JZMZAEKZDPDPQZUVGUVNAEUVPUUTUVJUVFUVMUUSBDPUCUVPUVEUVLBEUVPUVDUVKUVAUVCCD - PUDUEUFUGUHUUODPUIZMZUUQUUPRHZBDJZAFKZUVHUUOUVQUWAUVHUUOUVQUWAUJZUUTUVEBF - JZMZAEKZUVHUWBUWDAFKUWEABCDUOUWDUWDAFEUUQFOZUUQEOZUWDUUQUAUKULUMUUOUVQUWE - UVHLUWAUVRUWDUVGAEUVRUWGMZUWCUVFUUTUWHUVEUVEBFEUWHUUPFOZUVELZUUPEOZUVELUW - KUWIUUPSQZUUPNQZUPZUWHUWJMZUVEUUPUQZUWOUWIUVEUWLUWMUWHUWJURUWHUWLUVELUWJU - WHUWLUVEUWHUWLMUVEUUQSGHZUVBSGHZCDKZLZUVRUWTUWGUWLUVRUWSUWQUUOUVQUWSUUOUV - BDOZCUSUXAUWRMZCUSUVQUWSUUOUXAUXBCUUOUXAUWRUUOUXAUVBFOZUWRDFUVBUTUVBVAZVH - VBVCCDVDUWRCDVEVFVGVIVJUWLUVEUWTVKUWHUWLUVAUWQUVDUWSUUPSUUQGTUWLUVCUWRCDU - UPSUVBGTUHZVLVMVNVSVOUWGUWMUVELUVRUWJUWGUWMUVEUWGUWMMZUVAUVDUXFUVAIZUUQNG - HZIZUWGUXIUWMUUQVPVOUWMUXGUXIVKUWGUWMUVAUXHUUPNUUQGTVTVMVNVQVSVRWAWBVSWCW - DWEWFWGWJUUOUWAIZUVHUVQUUOUXJUVBUUQRHZCDKZAFJZUVHUUOUXJMUUPUUQRHZBDKZAFJZ - UXMUXJUUOUVTIZAFJZUXPUVTAFWHUUOUXRUXPUUOUXQUXOAFUXQUVSIZBDKUUOUWFMZUXOUVS - BDWIUXTUXSUXNBDUUOUUPDOZUWFUXSUXNLZUUOUYAMUWIUWFUYBDFUUPWKUWIUWFMUVSUXNUW - FUWIUVSUXNXAUUQUUPWLWMWNWOWPWEWQWRVGWSUXOUXLAFUXNUXKBCDUUPUVBUUQRWTXBXCXD - UUOUXMMZNEOZUUPNGHZIZBDJZNUUPGHZUVDLZBEJZMZUVHXEUYCUYGUYJUUOUYGUXMUUOUYFB - DUUOUYAUWIUYFDFUUPUTUWIUWKUYFUUPUAUUPVPZUMVHXFVOUYCUYIBEUUOUXMUWKUYILUWKU - XMUUOUYIUWKUWNUXMUUOUYILLZUWPUWIUYMUWLUWMUXMUUOUYHUWIUVDUXMUUOUWIUVDLUYHU - XMUUOUWIUVDUXMUUOMZUWIMUVBUUPXGXHXIZRHZCDKZUVDUWIUYNUYOFOZUYQUUPXJZUYRUYN - UYQUYRUXMUYQUUOUXLUYQAUYOFUUQUYOQUXKUYPCDUUQUYOUVBRTUHXKXMWMXLUUOUWIUYQUV - DLUXMUUOUWIMUYPUVCCDUUOUXAUWIUYPUVCLZUUOUXAMZUXCUWIUYTDFUVBWKZUXCUWIMUYPU - YOUUPGHZUVCUWIVUCUXCUUPXNVMUWIUXCUYRUWIMUYPVUCMUVCLZUWIUYRUYSXOUXCUYRUWIV - UDUVBUYOUUPXPXQXLXRWOWPWEXSWGXTYAYBUWLUXMUUOUYIUWLUYNUVDUYHUYNUVDUWLUWSUX - MUVBYCRHZCDKZUUOUWSYCFOUXMVUFYEUXLVUFAYCFUUQYCQUXKVUECDUUQYCUVBRTUHXKYFUU - OVUEUWRCDVUAUWRVUEVUAUXCUWRVUBUXDUMVIWEYDUXEYGYAYHUWMUYIUXMUUOUWMUYHUVDUW - MUYHNNGHZUYDVUGIXENYIYJUUPNNGTYKVQYQYLYMYNVGXFYRUVGUYKANEUUQNQZUUTUYGUVFU - YJVUHUUSUYFBDVUHUURUYEUUQNUUPGTVTUFVUHUVEUYIBEVUHUVAUYHUVDUUQNUUPGWTYOUFU - GYPZYSYTUUIUUAUVOUUOSEOUUPSGHZIZBPJZSUUPGHZUVKLZBEJZMZUVOUUBVULVUOVUKBUUC - VUNBEUWKVUMUVKUUPUUDVQUUEUUFUVNVUPASEUUQSQZUVJVULUVMVUOVUQUUSVUKBPVUQUURV - UJUUQSUUPGTVTUFVUQUVLVUNBEVUQUVAVUMUVKUUQSUUPGWTYOUFUGYPUUGUUHUUJVMUUNUVI - MUYDUYKUVHXEUUNUYGUVIUYJUUNUYFBDUUNUYAUWKUYFDEUUPUTUYLVHXFUVIUYIBEUVIUYHU - VDUVCUYHCNDUVBNUUPGWTYPVSUUKUULVUIYSUUM $. + cbvrexvw ralbii sylib mnfxr ralrimiv cmin peano2rem rspcva adantrr sylan2 + wo c1 co ltm1 ancri lelttr 3expb mpan2d adantll exp31 a1dd com4r cc0 mpan + 0re mpan9 syl5ibr expd xrltnr ax-mp mtbiri 2a1d 3jaoi sylbi imbi1d rspcev + com13 jca sylancr syldan adantlr pm2.61dan pnfxr ral0 pnfnlt pm3.2i mp2an + rgen a1i pm2.61ne ralrimivw anim12i jaodan ) DEUBZDFUBZBUNZAUNZGHZIZBDJZU + UQUUPGHZCUNZUUPGHZCDKZLZBEJZMZAEKZNDOZUUOUVHUUNUUOUVHUUSBPJZUVAUVCCPKZLZB + EJZMZAEKZDPDPQZUVGUVNAEUVPUUTUVJUVFUVMUUSBDPUCUVPUVEUVLBEUVPUVDUVKUVAUVCC + DPUDUEUFUGUHUUODPUIZMZUUQUUPRHZBDJZAFKZUVHUUOUVQUWAUVHUUOUVQUWAUJZUUTUVEB + FJZMZAEKZUVHUWBUWDAFKUWEABCDUOUWDUWDAFEUUQFOZUUQEOZUWDUUQUAUKULUMUUOUVQUW + EUVHLUWAUVRUWDUVGAEUVRUWGMZUWCUVFUUTUWHUVEUVEBFEUWHUUPFOZUVELZUUPEOZUVELU + WKUWIUUPSQZUUPNQZUPZUWHUWJMZUVEUUPUQZUWOUWIUVEUWLUWMUWHUWJURUWHUWLUVELUWJ + UWHUWLUVEUWHUWLMUVEUUQSGHZUVBSGHZCDKZLZUVRUWTUWGUWLUVRUWSUWQUUOUVQUWSUUOU + VBDOZCUSUXAUWRMZCUSUVQUWSUUOUXAUXBCUUOUXAUWRUUOUXAUVBFOZUWRDFUVBUTUVBVAZV + HVBVCCDVDUWRCDVEVFVGVIVJUWLUVEUWTVKUWHUWLUVAUWQUVDUWSUUPSUUQGTUWLUVCUWRCD + UUPSUVBGTUHZVLVMVNVSVOUWGUWMUVELUVRUWJUWGUWMUVEUWGUWMMZUVAUVDUXFUVAIZUUQN + GHZIZUWGUXIUWMUUQVPVOUWMUXGUXIVKUWGUWMUVAUXHUUPNUUQGTVTVMVNVQVSVRWAWBVSWC + WDWEWFWGWJUUOUWAIZUVHUVQUUOUXJUVBUUQRHZCDKZAFJZUVHUUOUXJMUUPUUQRHZBDKZAFJ + ZUXMUXJUUOUVTIZAFJZUXPUVTAFWHUUOUXRUXPUUOUXQUXOAFUXQUVSIZBDKUUOUWFMZUXOUV + SBDWIUXTUXSUXNBDUUOUUPDOZUWFUXSUXNLZUUOUYAMUWIUWFUYBDFUUPWKUWIUWFMUVSUXNU + WFUWIUVSUXNXKUUQUUPWLWMWNWOWPWEWQWRVGWSUXOUXLAFUXNUXKBCDUUPUVBUUQRWTXAXBX + CUUOUXMMZNEOZUUPNGHZIZBDJZNUUPGHZUVDLZBEJZMZUVHXDUYCUYGUYJUUOUYGUXMUUOUYF + BDUUOUYAUWIUYFDFUUPUTUWIUWKUYFUUPUAUUPVPZUMVHXEVOUYCUYIBEUUOUXMUWKUYILUWK + UXMUUOUYIUWKUWNUXMUUOUYILLZUWPUWIUYMUWLUWMUXMUUOUYHUWIUVDUXMUUOUWIUVDLUYH + UXMUUOUWIUVDUXMUUOMZUWIMUVBUUPXLXFXMZRHZCDKZUVDUWIUYNUYOFOZUYQUUPXGZUYRUY + NUYQUYRUXMUYQUUOUXLUYQAUYOFUUQUYOQUXKUYPCDUUQUYOUVBRTUHXHXIWMXJUUOUWIUYQU + VDLUXMUUOUWIMUYPUVCCDUUOUXAUWIUYPUVCLZUUOUXAMZUXCUWIUYTDFUVBWKZUXCUWIMUYP + UYOUUPGHZUVCUWIVUCUXCUUPXNVMUWIUXCUYRUWIMUYPVUCMUVCLZUWIUYRUYSXOUXCUYRUWI + VUDUVBUYOUUPXPXQXJXRWOWPWEXSWGXTYAYBUWLUXMUUOUYIUWLUYNUVDUYHUYNUVDUWLUWSU + XMUVBYCRHZCDKZUUOUWSYCFOUXMVUFYEUXLVUFAYCFUUQYCQUXKVUECDUUQYCUVBRTUHXHYDU + UOVUEUWRCDVUAUWRVUEVUAUXCUWRVUBUXDUMVIWEYFUXEYGYAYHUWMUYIUXMUUOUWMUYHUVDU + WMUYHNNGHZUYDVUGIXDNYIYJUUPNNGTYKVQYLYMYNYQVGXEYRUVGUYKANEUUQNQZUUTUYGUVF + UYJVUHUUSUYFBDVUHUURUYEUUQNUUPGTVTUFVUHUVEUYIBEVUHUVAUYHUVDUUQNUUPGWTYOUF + UGYPZYSYTUUAUUBUVOUUOSEOUUPSGHZIZBPJZSUUPGHZUVKLZBEJZMZUVOUUCVULVUOVUKBUU + DVUNBEUWKVUMUVKUUPUUEVQUUHUUFUVNVUPASEUUQSQZUVJVULUVMVUOVUQUUSVUKBPVUQUUR + VUJUUQSUUPGTVTUFVUQUVLVUNBEVUQUVAVUMUVKUUQSUUPGWTYOUFUGYPUUGUUIUUJVMUUNUV + IMUYDUYKUVHXDUUNUYGUVIUYJUUNUYFBDUUNUYAUWKUYFDEUUPUTUYLVHXEUVIUYIBEUVIUYH + UVDUVCUYHCNDUVBNUUPGWTYPVSUUKUULVUIYSUUM $. $( Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005.) $) @@ -135418,27 +135418,27 @@ the expression make the whole thing evaluate to zero (on both sides), xrub $p |- ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. RR ( x < B -> E. y e. A x < y ) <-> A. x e. RR* ( x < B -> E. y e. A x < y ) ) ) $= ( vz cxr wcel wa clt wbr wrex wi cr wceq breq1 rexbidv cpnf cmnf c1 ax-mp - wss wral imbi12d cbvralv w3o elxr pm2.27 a1i pnfnlt notbid syl5ibr pm2.21 - cv wn syl6com ad2antlr a1dd cmin co peano2rem rspcv syl adantl id syl5com - mnflt mnfxr rexrd ssel2 adantlr xrlttr mp3an2i mpand reximdva 3syld ltpnf - ltm1 1re breq2 mpbiri rexr mp3an12 sylan9r syl5 xrltnr mtbiri pm2.21d a1d - mpani 3jaodan sylan2b imp syl5ibrcom 3jaod syl5bi ralimdv2 pm2.43d imim1i - com23 ex ralimi2 impbid1 ) CFUAZDFGZHZAUMZDIJZXFBUMZIJZBCKZLZAMUBZXKAFUBZ - XEXLXMXLEUMZDIJZXNXHIJZBCKZLZEMUBZXEXLXMLZXKXRAEMXFXNNZXGXOXJXQXFXNDIOYAX - IXPBCXFXNXHIOPUCUDXEXSXTXEXSHZXKXKAMFYBXFFGZXFMGZXKLZXKYCYDXFQNZXFRNZUEYB - YEXKLZXFUFYBYDYHYFYGYDYHLYBYDXKUGUHYBYFXKYEXDYFXKLXCXSYFXDXGUNZXKXDYIYFQD - IJZUNDUIYFXGYJXFQDIOUJUKXGXJULUOUPUQYBYGXKYEYBXKYGRDIJZRXHIJZBCKZLZXEXSYN - XDXCDMGZDQNZDRNZUEXSYNLZDUFXCYOYRYPYQXCYOHZXSYMYKYSXSDSURUSZDIJZYTXHIJZBC - KZLZUUCYMYOXSUUDLZXCYOYTMGZUUEDUTZXRUUDEYTMXNYTNZXOUUAXQUUCXNYTDIOUUHXPUU - BBCXNYTXHIOPUCVAVBVCYOUUDUUCLXCYOUUAUUDUUCDVQUUDVDVEVCYSUUBYLBCYSXHCGZHZR - YTIJZUUBYLUUJUUFUUKYOUUFXCUUIUUGUPZYTVFVBRFGZUUJYTFGXHFGZUUKUUBHYLLVGUUJY - TUULVHXCUUIUUNYOCFXHVIZVJRYTXHVKVLVMVNVOUQXCYPHZXSYMYKXSSDIJZSXHIJZBCKZLZ - UUPYMSMGZXSUUTLVRXRUUTESMXNSNZXOUUQXQUUSXNSDIOUVBXPUURBCXNSXHIOPUCVATYPUU - TUUSXCYMYPUUQUUTUUSYPUUQSQIJZUVAUVCVRSVPTDQSIVSVTUUTVDVEXCUURYLBCXCUUIHUU - NUURYLLUUOUUNRSIJZUURYLUVAUVDVRSVFTUUMSFGZUUNUVDUURHYLLVGUVAUVEVRSWATRSXH - VKWBWIVBVNWCWDUQXCYQHZYNXSUVFYKYMYQYKUNXCYQYKRRIJZUUMUVGUNVGRWETDRRIVSWFV - CWGWHWJWKWLYGXGYKXJYMXFRDIOYGXIYLBCXFRXHIOPUCWMUQWNWOWSWPWTWOWQXKXKAFMYDY - CXKXFWAWRXAXB $. + wss cv wral imbi12d cbvralvw w3o elxr pm2.27 a1i wn pnfnlt notbid syl5ibr + pm2.21 syl6com ad2antlr a1dd cmin peano2rem rspcv syl adantl ltm1 syl5com + co id mnflt mnfxr rexrd ssel2 adantlr xrlttr mp3an2i mpand reximdva 3syld + 1re ltpnf breq2 mpbiri rexr mp3an12 mpani sylan9r syl5 xrltnr pm2.21d a1d + mtbiri 3jaodan sylan2b imp syl5ibrcom 3jaod syl5bi com23 ralimdv2 pm2.43d + ex imim1i ralimi2 impbid1 ) CFUAZDFGZHZAUBZDIJZXFBUBZIJZBCKZLZAMUCZXKAFUC + ZXEXLXMXLEUBZDIJZXNXHIJZBCKZLZEMUCZXEXLXMLZXKXRAEMXFXNNZXGXOXJXQXFXNDIOYA + XIXPBCXFXNXHIOPUDUEXEXSXTXEXSHZXKXKAMFYBXFFGZXFMGZXKLZXKYCYDXFQNZXFRNZUFY + BYEXKLZXFUGYBYDYHYFYGYDYHLYBYDXKUHUIYBYFXKYEXDYFXKLXCXSYFXDXGUJZXKXDYIYFQ + DIJZUJDUKYFXGYJXFQDIOULUMXGXJUNUOUPUQYBYGXKYEYBXKYGRDIJZRXHIJZBCKZLZXEXSY + NXDXCDMGZDQNZDRNZUFXSYNLZDUGXCYOYRYPYQXCYOHZXSYMYKYSXSDSURVEZDIJZYTXHIJZB + CKZLZUUCYMYOXSUUDLZXCYOYTMGZUUEDUSZXRUUDEYTMXNYTNZXOUUAXQUUCXNYTDIOUUHXPU + UBBCXNYTXHIOPUDUTVAVBYOUUDUUCLXCYOUUAUUDUUCDVCUUDVFVDVBYSUUBYLBCYSXHCGZHZ + RYTIJZUUBYLUUJUUFUUKYOUUFXCUUIUUGUPZYTVGVARFGZUUJYTFGXHFGZUUKUUBHYLLVHUUJ + YTUULVIXCUUIUUNYOCFXHVJZVKRYTXHVLVMVNVOVPUQXCYPHZXSYMYKXSSDIJZSXHIJZBCKZL + ZUUPYMSMGZXSUUTLVQXRUUTESMXNSNZXOUUQXQUUSXNSDIOUVBXPUURBCXNSXHIOPUDUTTYPU + UTUUSXCYMYPUUQUUTUUSYPUUQSQIJZUVAUVCVQSVRTDQSIVSVTUUTVFVDXCUURYLBCXCUUIHU + UNUURYLLUUOUUNRSIJZUURYLUVAUVDVQSVGTUUMSFGZUUNUVDUURHYLLVHUVAUVEVQSWATRSX + HVLWBWCVAVOWDWEUQXCYQHZYNXSUVFYKYMYQYKUJXCYQYKRRIJZUUMUVGUJVHRWFTDRRIVSWI + VBWGWHWJWKWLYGXGYKXJYMXFRDIOYGXIYLBCXFRXHIOPUDWMUQWNWOWPWQWSWOWRXKXKAFMYD + YCXKXFWAWTXAXB $. $( The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) (Revised by Mario Carneiro, 21-Apr-2015.) $) @@ -136698,8 +136698,8 @@ the existence of its supremum (see ~ suprcl ). (Contributed by Paul 16-Nov-2013.) $) ioof $p |- (,) : ( RR* X. RR* ) --> ~P RR $= ( vx vz vy cv clt wbr wa cxr crab cr cpw wcel wral cxp cioo wf iooval wss - co ioossre ovex elpw mpbir syl6eqelr rgen2a df-ioo fmpo mpbi ) ADZBDZEFUJ - CDZEFGBHIZJKZLZCHMAHMHHNUMOPUNACHUIHLUKHLGULUIUKOSZUMBUIUKQUOUMLUOJRUIUKT + co ioossre ovex elpw mpbir syl6eqelr rgen2 df-ioo fmpo mpbi ) ADZBDZEFUJC + DZEFGBHIZJKZLZCHMAHMHHNUMOPUNACHHUIHLUKHLGULUIUKOSZUMBUIUKQUOUMLUOJRUIUKT UOJUIUKOUAUBUCUDUEACHHULUMOACBUFUGUH $. $( The set of closed intervals of extended reals maps to subsets of @@ -138414,14 +138414,14 @@ subset of a (possibly extended) finite sequence of integers. (Contributed -> ( A. j e. ( M ... N ) ph <-> A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph ) ) $= ( cz wcel cfz co wral cv cmin wsbc wi wa wb elfzelz syl wceq simpr sylan2 - w3a fzrev anassrs mpbid ex3 com23 ralrimdv nfv nfcv nfsbc1v nfral fzrev2i - rspsbc oveq2 sbceq1d rspcv cc zcnd nncan syl2an eqcomd sbceq1a sylibrd ex - zcn ralrimd 3ad2ant3 impbid ) EGHZFGHZDGHZUCZABEFIJZKZABDCLZMJZNZCDFMJZDE - MJZIJZKZVNVPVSCWBVNVQWBHZVPVSVKVLVMWDVPVSOZVKVLPZVMPZWDPZVRVOHZWEWHWDWIWG - WDUAWDWGVQGHZWDWIQZVQVTWARWFVMWJWKDVQEFUDUEUBUFABVRVOUOSUGUHUIVMVKWCVPOVL - VMWCABVOVMBUJVSBCWBBWBUKABVRULUMVMBLZVOHZWCAVMWMWCAOVMWMPZWCABDDWLMJZMJZN - ZAWNWOWBHWCWQODWLEFUNVSWQCWOWBVQWOTABVRWPVQWODMUPUQURSWNWLWPTAWQQWNWPWLVM - DUSHWLUSHWPWLTWMDVGWMWLWLEFRUTDWLVAVBVCABWPVDSVEVFUHVHVIVJ $. + w3a fzrev anassrs mpbid rspsbc ex3 com23 ralrimdv nfv nfcv nfsbc1v nfralw + fzrev2i oveq2 sbceq1d rspcv cc zcn nncan syl2an eqcomd sbceq1a sylibrd ex + zcnd ralrimd 3ad2ant3 impbid ) EGHZFGHZDGHZUCZABEFIJZKZABDCLZMJZNZCDFMJZD + EMJZIJZKZVNVPVSCWBVNVQWBHZVPVSVKVLVMWDVPVSOZVKVLPZVMPZWDPZVRVOHZWEWHWDWIW + GWDUAWDWGVQGHZWDWIQZVQVTWARWFVMWJWKDVQEFUDUEUBUFABVRVOUGSUHUIUJVMVKWCVPOV + LVMWCABVOVMBUKVSBCWBBWBULABVRUMUNVMBLZVOHZWCAVMWMWCAOVMWMPZWCABDDWLMJZMJZ + NZAWNWOWBHWCWQODWLEFUOVSWQCWOWBVQWOTABVRWPVQWODMUPUQURSWNWLWPTAWQQWNWPWLV + MDUSHWLUSHWPWLTWMDUTWMWLWLEFRVGDWLVAVBVCABWPVDSVEVFUIVHVIVJ $. $( Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) $) @@ -138450,18 +138450,18 @@ subset of a (possibly extended) finite sequence of integers. (Contributed -> ( A. j e. ( M ... N ) ph <-> A. k e. ( ( M + K ) ... ( N + K ) ) [. ( k - K ) / j ]. ph ) ) $= ( vx cz wcel cfz co wral cc0 cmin wsbc caddc wb cc wceq wa cv 0z fzrevral - w3a mp3an3 3adant3 zsubcl mpan syl3an 3com12 cvv ovex oveq2 sbcco3g ax-mp - ralbii zcn cneg df-neg oveq2i subneg addcom eqtrd syl5eqr 3adant2 oveq12d - id 3coml raleqdv elfzelz negsubdi2 syl2an sbceq1d ralbidva 3ad2ant3 bitrd - zcnd syl5bb 3bitrd ) EHIZFHIZDHIZUDZABEFJKLZABMGUAZNKZOZGMFNKZMENKZJKLZWG - GDCUAZNKZOZCDWINKZDWHNKZJKZLZABWKDNKZOZCEDPKZFDPKZJKZLZVTWAWDWJQZWBVTWAMH - IZXDUBABGMEFUCUEUFWAVTWBWJWQQZWAWHHIZVTWIHIZWBWBXFXEWAXGUBMFUGUHXEVTXHUBM - EUGUHWBVGWGGCDWHWIUCUIUJWQABMWLNKZOZCWPLZWCXCWMXJCWPWLUKIWMXJQDWKNULAGBWL - WFXIUKWEWLMNUMUNUOUPWCXKXJCXBLZXCWCXJCWPXBVTERIZWAFRIZWBDRIZWPXBSZEUQFUQD - UQZXOXMXNXPXOXMXNUDWNWTWOXAJXOXMWNWTSXNXOXMTZWNDEURZNKZWTXSWIDNEUSUTXRXTD - EPKWTDEVADEVBVCVDUFXOXNWOXASXMXOXNTZWODFURZNKZXAYBWHDNFUSUTYAYCDFPKXADFVA - DFVBVCVDVEVFVHUIVIWBVTXLXCQWAWBXJWSCXBWBWKXBIZTABXIWRWBXOWKRIZXIWRSYDXQYD - WKWKWTXAVJVQXOYETXIWLURWRWLUSDWKVKVDVLVMVNVOVPVRVS $. + w3a mp3an3 3adant3 zsubcl mpan id syl3an 3com12 ovex oveq2 sbcco3gw ax-mp + cvv ralbii cneg df-neg oveq2i subneg addcom eqtrd syl5eqr 3adant2 oveq12d + zcn 3coml raleqdv elfzelz zcnd negsubdi2 syl2an sbceq1d ralbidva 3ad2ant3 + bitrd syl5bb 3bitrd ) EHIZFHIZDHIZUDZABEFJKLZABMGUAZNKZOZGMFNKZMENKZJKLZW + GGDCUAZNKZOZCDWINKZDWHNKZJKZLZABWKDNKZOZCEDPKZFDPKZJKZLZVTWAWDWJQZWBVTWAM + HIZXDUBABGMEFUCUEUFWAVTWBWJWQQZWAWHHIZVTWIHIZWBWBXFXEWAXGUBMFUGUHXEVTXHUB + MEUGUHWBUIWGGCDWHWIUCUJUKWQABMWLNKZOZCWPLZWCXCWMXJCWPWLUPIWMXJQDWKNULAGBW + LWFXIUPWEWLMNUMUNUOUQWCXKXJCXBLZXCWCXJCWPXBVTERIZWAFRIZWBDRIZWPXBSZEVGFVG + DVGZXOXMXNXPXOXMXNUDWNWTWOXAJXOXMWNWTSXNXOXMTZWNDEURZNKZWTXSWIDNEUSUTXRXT + DEPKWTDEVADEVBVCVDUFXOXNWOXASXMXOXNTZWODFURZNKZXAYBWHDNFUSUTYAYCDFPKXADFV + ADFVBVCVDVEVFVHUJVIWBVTXLXCQWAWBXJWSCXBWBWKXBIZTABXIWRWBXOWKRIZXIWRSYDXQY + DWKWKWTXAVJVKXOYETXIWLURWRWLUSDWKVLVDVMVNVOVPVQVRVS $. $} $( Membership of an integer greater than 1 decreased by 1 in a 1-based finite @@ -142111,23 +142111,23 @@ The modulo (remainder) operation ( vy vz com cfv wceq cv wi wral wfn mpbir2an wcel wa clt wbr wn cuz wf c1 wf1o wf1 crn wss cvv caddc cmpt crdg cres frfnom fneq1i om2uzrani eqimssi co mpbir df-f wo cr wb cz om2uzuzi eluzelz syl zred lttri3 syl2an syl6bbr - ioran nnord ordtri3 con2bid om2uzlti ancoms orim12d sylbird sylbid rgen2a - word con1d dff13 dff1o5 ) HBUAIZCUDHWECUEZCUFZWEJWFHWECUBZFKZCIZGKZCIZJZW - IWKJZLZGHMFHMWHCHNZWGWEUGWPAUHAKUCUIUQUJZBUKHULZHNBWQUMHCWREUNURWGWEABCDE - UOZUPHWECUSOWOFGHWIHPZWKHPZQZWMWJWLRSZWLWJRSZUTZTZWNXBWMXCTXDTQZXFWTWJVAP + ioran word nnord ordtri3 con2bid ancoms orim12d sylbird con1d rgen2 dff13 + om2uzlti sylbid dff1o5 ) HBUAIZCUDHWECUEZCUFZWEJWFHWECUBZFKZCIZGKZCIZJZWI + WKJZLZGHMFHMWHCHNZWGWEUGWPAUHAKUCUIUQUJZBUKHULZHNBWQUMHCWREUNURWGWEABCDEU + OZUPHWECUSOWOFGHHWIHPZWKHPZQZWMWJWLRSZWLWJRSZUTZTZWNXBWMXCTXDTQZXFWTWJVAP WLVAPWMXGVBXAWTWJWTWJWEPWJVCPAWIBCDEVDBWJVEVFVGXAWLXAWLWEPWLVCPAWKBCDEVDB - WLVEVFVGWJWLVHVIXCXDVKVJXBWNXEXBWNTWIWKPZWKWIPZUTZXEXBWNXJWTWIWAWKWAWNXJT - VBXAWIVLWKVLWIWKVMVIVNXBXHXCXIXDAWIWKBCDEVOXAWTXIXDLAWKWIBCDEVOVPVQVRWBVS - VTFGHWECWCOWSHWECWDO $. + WLVEVFVGWJWLVHVIXCXDVKVJXBWNXEXBWNTWIWKPZWKWIPZUTZXEXBWNXJWTWIVLWKVLWNXJT + VBXAWIVMWKVMWIWKVNVIVOXBXHXCXIXDAWIWKBCDEWBXAWTXIXDLAWKWIBCDEWBVPVQVRVSWC + VTFGHWECWAOWSHWECWDO $. $( ` G ` (see ~ om2uz0i ) is an isomorphism from natural ordinals to upper integers. (Contributed by NM, 9-Oct-2008.) (Revised by Mario Carneiro, 13-Sep-2013.) $) om2uzisoi $p |- G Isom _E , < ( _om , ( ZZ>= ` C ) ) $= - ( vy vz com cuz cfv cep clt wiso wf1o cv wbr wb wral om2uzf1oi wcel epel - wa om2uzlt2i syl5bb rgen2a df-isom mpbir2an ) HBIJZKLCMHUHCNFOZGOZKPZUICJ - UJCJLPZQZGHRFHRABCDESUMFGHUKUIUJTUIHTUJHTUBULGUIUAAUIUJBCDEUCUDUEFGHUHKLC - UFUG $. + ( vy vz com cuz cfv cep clt wiso wf1o cv wbr wb wral om2uzf1oi wcel rgen2 + wa epel om2uzlt2i syl5bb df-isom mpbir2an ) HBIJZKLCMHUHCNFOZGOZKPZUICJUJ + CJLPZQZGHRFHRABCDESUMFGHHUKUIUJTUIHTUJHTUBULGUIUCAUIUJBCDEUDUEUAFGHUHKLCU + FUG $. $( An alternative definition of ` G ` in terms of ~ df-oi . (Contributed by Mario Carneiro, 2-Jun-2015.) $) @@ -142603,12 +142603,12 @@ equinumerous to omega (the set of finite ordinal numbers). (Contributed <-> E. s e. NN0 A. x e. NN0 ( s < x -> -. ph ) ) $= ( vy cn0 crab wss cfn wcel cv clt wbr wn wi wral wrex wb nfcv weq nfv nfn ssrab2 wnel ssnn0fi wsbc nnel nfsbc1v sbceq2a equcoms con2bid elrabf baib - wa syl5bb con4bid imbi2d ralbiia nfim breq2 imbi12d cbvral bitri rexbidva - a1i bitrd ax-mp ) ABEFZEGZVGHIZCJZBJZKLZAMZNZBEOZCEPZQABEUBVHVIVJDJZKLZVQ - VGUCZNZDEOZCEPVPDVGCUDVHWAVOCEWAVOQVHVJEIUMWAVRVMBVQUEZNZDEOVOVTWCDEVQEIZ - VSWBVRWDVSWBVSMVQVGIZWDWBMZVQVGUFWEWDWFAWFBVQEBVQRBERWBBVMBVQUGZUABDSWBAW - BVMQDBVMBVQUHZUIUJUKULUNUOUPUQWCVNDBEVRWBBVRBTWGURVNDTDBSVRVLWBVMVQVKVJKU - SWHUTVAVBVDVCVEVF $. + wa syl5bb con4bid imbi2d ralbiia breq2 imbi12d cbvralw bitri a1i rexbidva + nfim bitrd ax-mp ) ABEFZEGZVGHIZCJZBJZKLZAMZNZBEOZCEPZQABEUBVHVIVJDJZKLZV + QVGUCZNZDEOZCEPVPDVGCUDVHWAVOCEWAVOQVHVJEIUMWAVRVMBVQUEZNZDEOVOVTWCDEVQEI + ZVSWBVRWDVSWBVSMVQVGIZWDWBMZVQVGUFWEWDWFAWFBVQEBVQRBERWBBVMBVQUGZUABDSWBA + WBVMQDBVMBVQUHZUIUJUKULUNUOUPUQWCVNDBEVRWBBVRBTWGVDVNDTDBSVRVLWBVMVQVKVJK + URWHUSUTVAVBVCVEVF $. $} @@ -142724,20 +142724,20 @@ equinumerous to omega (the set of finite ordinal numbers). (Contributed ( vg c0 wceq csupp co wral cn0 wss wcel cc0 cfz wrex wn wa cv wo cmap cfn w3a cfsupp wbr wi 0nn0 a1i wb oveq2 sseq2d ralbidv adantl raleq mpbii 0ss ral0 sseq1 mpbiri ralimi jaoi rspcedvd 2a1d ciun cr clt csup simplr simpr - ioran oveq1 eqeq1d cbvralv notbii anbi2i bitri rexnal df-ne bicomi rexbii - wne sylbb1 simplbiim ad2antrr iunn0 sylib cbviunv eqid fsuppmapnn0fiublem - jca sylc nfv nfra1 nfor nfan ralbid neeq1i fsuppmapnn0fiub exp31 pm2.61i + wne ioran oveq1 eqeq1d cbvralvw notbii anbi2i rexnal bicomi rexbii sylbb1 + bitri df-ne simplbiim ad2antrr iunn0 sylib jca cbviunv fsuppmapnn0fiublem + eqid sylc nfv nfra1 nfor nfan ralbid neeq1i fsuppmapnn0fiub exp31 pm2.61i nfn ) HDIZBUAZFJKZHIZBDLZUBZDAMUCKNDUDOFEOUEZXEFUFUGZBDLZXFPCUAZQKZNZBDLZ CMRZUHUHXIXQXJXLXIXPXFPPQKZNZBDLZCPMPMOXIUIUJXMPIZXPXTUKXIYAXOXSBDYAXNXRX FXMPPQULUMUNUOXDXTXHXDXSBHLXTXSBUSXSBHDUPUQXGXSBDXGXSHXRNXRURXFHXRUTVAVBV - CVDVEXISZXJXLXQYBXJTZXLTZXPXFPGDGUAZFJKZVFZVGVHVIZQKZNZBDLZCYHMYDXJXLYGHW - CZTZYHMOYBXJXLVJZYDXLYLYCXLVKZYDYFHWCZGDRZYLYBYQXJXLYBXDSZYFHIZGDLZSZYQYB - YRXHSZTYRUUATXDXHVLZUUBUUAYRXHYTXGYSBGDXEYEIXFYFHXEYEFJVMZVNVOVPVQVRYSSZG - DRUUAYQYSGDVSUUEYPGDYPUUEYFHVTWAWBWDWEWFGDYFWGWHWLAYHYGBDEFGBDYFXFYEXEFJV - MWIZYHWJZWKWMYDXMYHIZTXOYJBDYDUUHBYCXLBYBXJBXIBXDXHBXDBWNXGBDWOWPXCXJBWNW + CVDVEXISZXJXLXQYBXJTZXLTZXPXFPGDGUAZFJKZVFZVGVHVIZQKZNZBDLZCYHMYDXJXLYGHV + LZTZYHMOYBXJXLVJZYDXLYLYCXLVKZYDYFHVLZGDRZYLYBYQXJXLYBXDSZYFHIZGDLZSZYQYB + YRXHSZTYRUUATXDXHVMZUUBUUAYRXHYTXGYSBGDXEYEIXFYFHXEYEFJVNZVOVPVQVRWCYSSZG + DRUUAYQYSGDVSUUEYPGDYPUUEYFHWDVTWAWBWEWFGDYFWGWHWIAYHYGBDEFGBDYFXFYEXEFJV + NWJZYHWLZWKWMYDXMYHIZTXOYJBDYDUUHBYCXLBYBXJBXIBXDXHBXDBWNXGBDWOWPXCXJBWNW QXKBDWOWQUUHBWNWQUUHXOYJUKYDUUHXNYIXFXMYHPQULUMUOWRYDXJYMYKYNYDXLYLYOYDXF - HWCZBDRZYLYBUUJXJXLYBYRUUBUUJUUCXGSZBDRUUBUUJXGBDVSUUKUUIBDUUIUUKXFHVTWAW - BWDWEWFUUJBDXFVFZHWCYLBDXFWGUULYGHBGDXFYFUUDWIWSVRWHWLAYHYGBDEFUUFUUGWTWM + HVLZBDRZYLYBUUJXJXLYBYRUUBUUJUUCXGSZBDRUUBUUJXGBDVSUUKUUIBDUUIUUKXFHWDVTW + AWBWEWFUUJBDXFVFZHVLYLBDXFWGUULYGHBGDXFYFUUDWJWSWCWHWIAYHYGBDEFUUFUUGWTWM VDXAXB $. $d M x $. $d R x $. $d V x $. $d Z x $. $d f x $. $d m x $. @@ -143387,21 +143387,21 @@ seq M ( .+ , F ) ) $= (Contributed by Mario Carneiro, 18-Jul-2014.) $) monoord2 $p |- ( ph -> ( F ` N ) <_ ( F ` M ) ) $= ( vn cfv cle wbr cneg cfz co cr wcel c1 wceq syl cv wa renegcld ffvelrnda - cmpt fmpttd cmin caddc wral ralrimiva fvoveq1 fveq2 breq12d cbvralv sylib - r19.21bi eleq1d adantr fzp1elp1 adantl cc cuz eluzelz zcnd ax-1cn sylancl - cz npcan oveq2d eleqtrd rspcdva fzssp1 sseqtrid sselda lenegd negeqd eqid - mpbid negex fvmpt 3brtr4d monoord eluzfz1 eluzfz2 3brtr3d mpbird ) AECJZD - CJZKLWHMZWGMZKLADBDENOZBUAZCJZMZUEZJZEWOJZWIWJKAIWODEFAWKPIUAZWOABWKWNPAW - LWKQUBWMGUCUFUDAWRDERUGOZNOZQZUBZWRCJZMZWRRUHOZCJZMZWRWOJZXEWOJZKXBXFXCKL - ZXDXGKLAXJIWTAWLRUHOCJZWMKLZBWTUIXJIWTUIAXLBWTHUJXLXJBIWTWLWRSZXKXFWMXCKW - LWRRCUHUKWLWRCULZUMUNUOUPXBXFXCXBWMPQZXFPQBWKXEWLXESZWMXFPWLXECULZUQAXOBW - KUIXAAXOBWKGUJZURZXBXEDWSRUHOZNOZWKXAXEYAQAWRDWSUSUTAYAWKSXAAXTEDNAEVAQRV - AQXTESAEAEDVBJQZEVGQFDEVCTVDVEERVHVFVIZURVJZVKXBXOXCPQBWKWRXMWMXCPXNUQXSA - WTWKWRAYAWTWKDWSVLYCVMVNZVKVOVRXBWRWKQXHXDSYEBWRWNXDWKWOXMWMXCXNVPWOVQZXC - VSVTTXBXEWKQXIXGSYDBXEWNXGWKWOXPWMXFXQVPYFXFVSVTTWAWBADWKQZWPWISAYBYGFDEW - CTZBDWNWIWKWOWLDSZWMWHWLDCULZVPYFWHVSVTTAEWKQZWQWJSAYBYKFDEWDTZBEWNWJWKWO - WLESZWMWGWLECULZVPYFWGVSVTTWEAWGWHAXOWGPQBWKEYMWMWGPYNUQXRYLVKAXOWHPQBWKD - YIWMWHPYJUQXRYHVKVOWF $. + cmpt fmpttd cmin caddc wral fvoveq1 fveq2 breq12d cbvralvw sylib r19.21bi + ralrimiva eleq1d adantr fzp1elp1 adantl cc cz eluzelz zcnd ax-1cn sylancl + cuz npcan oveq2d eleqtrd rspcdva fzssp1 sseqtrid sselda lenegd mpbid eqid + negeqd negex fvmpt 3brtr4d monoord eluzfz1 eluzfz2 3brtr3d mpbird ) AECJZ + DCJZKLWHMZWGMZKLADBDENOZBUAZCJZMZUEZJZEWOJZWIWJKAIWODEFAWKPIUAZWOABWKWNPA + WLWKQUBWMGUCUFUDAWRDERUGOZNOZQZUBZWRCJZMZWRRUHOZCJZMZWRWOJZXEWOJZKXBXFXCK + LZXDXGKLAXJIWTAWLRUHOCJZWMKLZBWTUIXJIWTUIAXLBWTHUPXLXJBIWTWLWRSZXKXFWMXCK + WLWRRCUHUJWLWRCUKZULUMUNUOXBXFXCXBWMPQZXFPQBWKXEWLXESZWMXFPWLXECUKZUQAXOB + WKUIXAAXOBWKGUPZURZXBXEDWSRUHOZNOZWKXAXEYAQAWRDWSUSUTAYAWKSXAAXTEDNAEVAQR + VAQXTESAEAEDVGJQZEVBQFDEVCTVDVEERVHVFVIZURVJZVKXBXOXCPQBWKWRXMWMXCPXNUQXS + AWTWKWRAYAWTWKDWSVLYCVMVNZVKVOVPXBWRWKQXHXDSYEBWRWNXDWKWOXMWMXCXNVRWOVQZX + CVSVTTXBXEWKQXIXGSYDBXEWNXGWKWOXPWMXFXQVRYFXFVSVTTWAWBADWKQZWPWISAYBYGFDE + WCTZBDWNWIWKWOWLDSZWMWHWLDCUKZVRYFWHVSVTTAEWKQZWQWJSAYBYKFDEWDTZBEWNWJWKW + OWLESZWMWGWLECUKZVRYFWGVSVTTWEAWGWHAXOWGPQBWKEYMWMWGPYNUQXRYLVKAXOWHPQBWK + DYIWMWHPYJUQXRYHVKVOWF $. $} ${ @@ -143827,7 +143827,7 @@ seq M ( .+ , F ) ) $= wa wi wcel c1 caddc oveq2 f1oeq23 syl2anc anbi12d eqeq12d imbi12d 2albidv wb feq2d fveq2 imbi2d weq cz f1of adantr elfz3 fvco3 syl2anr ffvelrn fzsn csn eleq2d elsni syl6bi syldan adantrr fveq2d eqtrd seq1 3eqtr4d alrimivv - imp ex f1oeq1 feq1 bi2anan9r coeq1 coeq2 sylan9eq seqeq3d fveq1d cbval2vv + imp ex f1oeq1 feq1 bi2anan9r coeq1 coeq2 sylan9eq seqeq3d fveq1d cbval2vw a1d simpl ccnv clt wbr cif simplll w3a simpllr wss syl simprl simprr eqid sylan simplr sylib seqf1olem2 exp31 syl5bir alrimdv syl5bi expcom a2d cfn uzind4 mpcom cvv wfn fvex fnmpti fzfi fvmpt seqfveq fnfi mp2an ovexd fex2 @@ -144243,14 +144243,14 @@ seq M ( .+ , F ) ) $= ( z e. A |-> ( seq M ( .+ , ( x e. B |-> X ) ) ` N ) ) ) $= ( vy cmpt cfv wcel nfcv vn cof cseq cv csb cfz co wa wceq wi nfv nffvmpt1 nfmpt nfeq weq eleq1w anbi2d fveq2 mpteq2dv eqeq12d imbi12d sselda adantr - nfim cvv mptexd eqid fvmpt2 syl2anc simpll simpr syl12anc mpteq2dva chvar - eqtr4d nfcsb1v csbeq1a fveq1d cbvmpt syl6eq seqof nfseq seqeq3d syl6eqr + nfim cvv mptexd eqid fvmpt2 syl2anc simpll simpr mpteq2dva eqtr4d chvarfv + syl12anc nfcsb1v csbeq1a fveq1d cbvmpt syl6eq seqof nfseq seqeq3d syl6eqr nffv ) AHFUBBECDKQZQZGUCRPDHFCPUDZBEKQZUEZGUCZRZQCDHFWIGUCZRZQAUAPDFWGWJG HILMAUAUDZGHUFUGZSZUHZWOWGRZCDWOWIRZQZPDWOWJRZQABUDZWPSZUHZXCWGRZCDXCWIRZ QZUIZUJWRWSXAUIZUJBUAWRXJBWRBUKBWSXABEWFWOULBCDWTBDTBEKWOULUMUNVDBUAUOZXE WRXIXJXKXDWQABUAWPUPUQXKXFWSXHXAXCWOWGURXKCDXGWTXCWOWIURUSUTVAXEXFWFXHXEX CESZWFVESXFWFUIAWPEXCNVBZXECDKIADISXDLVCVFBEWFVEWGWGVGVHVIXECDXGKXECUDDSZ - UHZXLKJSZXGKUIXEXLXNXMVCZXOAXLXNXPAXDXNVJXQXEXNVKOVLBEKJWIWIVGVHVIVMVOVNC + UHZXLKJSZXGKUIXEXLXNXMVCZXOAXLXNXPAXDXNVJXQXEXNVKOVOBEKJWIWIVGVHVIVLVMVNC PDWTXBPWTTCWOWJCWHWIVPZCWOTWECPUOZWOWIWJCWHWIVQZVRVSVTWACPDWNWLPWNTCHWKCF WJGCGTCFTXRWBCHTWEXSHWMWKXSWIWJFGXTWCVRVSWD $. $} @@ -146919,41 +146919,41 @@ notation is used by Donald Knuth for iterated exponentiation (_Science_ ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) ) $= ( vn cn wcel cexp co cmul c2 caddc cle wbr wa c1 wceq oveq2 oveq2d oveq1d - cc0 vm vj cn0 cfa cfv cv wral wi oveq1 oveq12d fveq2 breq12d cbvralv cmin - clt wo cr nnre 1re lelttric sylancl ancli andi sylib nnge1 letri3 biimpar - wb anassrs mpidan 1m1e0 syl6eq syl faclbnd4lem3 sylan2 a1d 1nn nnsub mpan - biimpa rspcv adantl jaodan faclbnd4lem2 3expa ralrimdva syl5bi expcom a2d - syld nnnn0 faclbnd3 nncn exp0d cc nn0cn expcl syl2an mulid2d eqtrd oveq2i - sq0 2cn exp0 ax-mp eqtri addid1d mpancom adantr 3brtr4d ralrimiva ralbidv - a1i imbi2d nn0indALT imp rspcva 3impb ) CEFZAUCFZBUCFZCAGHZBCGHZIHZJAJGHZ - GHZBBAKHZGHZIHZCUDUEZIHZLMZXTYANXSDUFZAGHZBYMGHZIHZYIYMUDUEZIHZLMZDEUGZYL - XTYAYTYAYMUAUFZGHZYOIHZJUUAJGHZGHZBBUUAKHZGHZIHZYQIHZLMZDEUGZUHYAYMTGHZYO - IHZJTJGHZGHZBBTKHZGHZIHZYQIHZLMZDEUGZUHYAYMUBUFZGHZYOIHZJUVBJGHZGHZBBUVBK - HZGHZIHZYQIHZLMZDEUGZUHYAYMUVBOKHZGHZYOIHZJUVMJGHZGHZBBUVMKHZGHZIHZYQIHZL - MZDEUGZUHYAYTUHUAUBAUVBUCFZYAUVLUWCYAUWDUVLUWCUHUVLUUAUVBGHZBUUAGHZIHZUVI - UUAUDUEZIHZLMZUAEUGZYAUWDNZUWCUVKUWJDUAEYMUUAPZUVDUWGUVJUWILUWMUVCUWEYOUW - FIYMUUAUVBGUIYMUUABGQUJUWMYQUWHUVIIYMUUAUDUKRULUMUWLUWKUWBDEUWLYMEFZNUWKY - MOUNHZUVBGHZBUWOGHZIHZUVIUWOUDUEZIHZLMZUWBUWNUWLUWNYMOLMZNZUWNOYMUOMZNZUP - ZUWKUXAUHZUWNUWNUXBUXDUPZNUXFUWNUXHUWNYMUQFZOUQFZUXHYMURZUSYMOUTVAVBUWNUX - BUXDVCVDUWLUXCUXGUXEUWLUXCNUXAUWKUXCUWLUWOTPZUXAUXCYMOPZUXLUWNUXBOYMLMZUX - MYMVEUWNUXBUXNUXMUWNUXMUXBUXNNZUWNUXIUXJUXMUXOVHUXKUSYMOVFVAVGVIVJUXMUWOO - OUNHTYMOOUNUIVKVLVMUVBBUWOVNVOVPUXEUXGUWLUXEUWOEFZUXGUWNUXDUXPOEFUWNUXDUX - PVHVQOYMVRVSVTUWJUXAUAUWOEUUAUWOPZUWGUWRUWIUWTLUXQUWEUWPUWFUWQIUUAUWOUVBG - UIUUAUWOBGQUJUXQUWHUWSUVIIUUAUWOUDUKRULWAVMWBWCVOYAUWDUWNUXAUWBUHUVBBYMWD - WEWJWFWGWHWIYAUUTDEYAUWNNZYOBBGHZYQIHZUUMUUSLUWNYAYMUCFZYOUXTLMYMWKZBYMWL - VOUXRUUMOYOIHZYOUWNUUMUYCPYAUWNUULOYOIUWNYMYMWMWNSWBUXRYOYABWOFZUYAYOWOFU - WNBWPZUYBBYMWQWRWSWTYAUUSUXTPUWNYAUURUXSYQIYAUUROUXSIHUXSYAUUOOUUQUXSIUUO - OPYAUUOJTGHZOUUNTJGXBXAJWOFUYFOPXCJXDXEXFXMYAUUPBBGYABUYEXGRUJYAUXSUYDYAU - XSWOFUYEBBWQXHWSWTSXIXJXKUUATPZUUKUVAYAUYGUUJUUTDEUYGUUCUUMUUIUUSLUYGUUBU - ULYOIUUATYMGQSUYGUUHUURYQIUYGUUEUUOUUGUUQIUYGUUDUUNJGUUATJGUIRUYGUUFUUPBG - UUATBKQRUJSULXLXNUUAUVBPZUUKUVLYAUYHUUJUVKDEUYHUUCUVDUUIUVJLUYHUUBUVCYOIU - UAUVBYMGQSUYHUUHUVIYQIUYHUUEUVFUUGUVHIUYHUUDUVEJGUUAUVBJGUIRUYHUUFUVGBGUU - AUVBBKQRUJSULXLXNUUAUVMPZUUKUWCYAUYIUUJUWBDEUYIUUCUVOUUIUWALUYIUUBUVNYOIU - UAUVMYMGQSUYIUUHUVTYQIUYIUUEUVQUUGUVSIUYIUUDUVPJGUUAUVMJGUIRUYIUUFUVRBGUU - AUVMBKQRUJSULXLXNUUAAPZUUKYTYAUYJUUJYSDEUYJUUCYPUUIYRLUYJUUBYNYOIUUAAYMGQ - SUYJUUHYIYQIUYJUUEYFUUGYHIUYJUUDYEJGUUAAJGUIRUYJUUFYGBGUUAABKQRUJSULXLXNX - OXPYSYLDCEYMCPZYPYDYRYKLUYKYNYBYOYCIYMCAGUIYMCBGQUJUYKYQYJYIIYMCUDUKRULXQ - VOXR $. + cc0 vm vj cn0 cfa cfv cv wral wi oveq1 oveq12d fveq2 breq12d cbvralvw clt + cmin wo cr nnre lelttric sylancl ancli andi sylib nnge1 wb letri3 biimpar + 1re anassrs mpidan 1m1e0 syl6eq syl faclbnd4lem3 sylan2 nnsub mpan biimpa + a1d 1nn rspcv adantl jaodan faclbnd4lem2 syld ralrimdva syl5bi expcom a2d + 3expa nnnn0 faclbnd3 exp0d cc nn0cn expcl syl2an mulid2d eqtrd sq0 oveq2i + nncn 2cn ax-mp eqtri a1i addid1d mpancom adantr 3brtr4d ralrimiva ralbidv + exp0 imbi2d nn0indALT imp rspcva 3impb ) CEFZAUCFZBUCFZCAGHZBCGHZIHZJAJGH + ZGHZBBAKHZGHZIHZCUDUEZIHZLMZXTYANXSDUFZAGHZBYMGHZIHZYIYMUDUEZIHZLMZDEUGZY + LXTYAYTYAYMUAUFZGHZYOIHZJUUAJGHZGHZBBUUAKHZGHZIHZYQIHZLMZDEUGZUHYAYMTGHZY + OIHZJTJGHZGHZBBTKHZGHZIHZYQIHZLMZDEUGZUHYAYMUBUFZGHZYOIHZJUVBJGHZGHZBBUVB + KHZGHZIHZYQIHZLMZDEUGZUHYAYMUVBOKHZGHZYOIHZJUVMJGHZGHZBBUVMKHZGHZIHZYQIHZ + LMZDEUGZUHYAYTUHUAUBAUVBUCFZYAUVLUWCYAUWDUVLUWCUHUVLUUAUVBGHZBUUAGHZIHZUV + IUUAUDUEZIHZLMZUAEUGZYAUWDNZUWCUVKUWJDUAEYMUUAPZUVDUWGUVJUWILUWMUVCUWEYOU + WFIYMUUAUVBGUIYMUUABGQUJUWMYQUWHUVIIYMUUAUDUKRULUMUWLUWKUWBDEUWLYMEFZNUWK + YMOUOHZUVBGHZBUWOGHZIHZUVIUWOUDUEZIHZLMZUWBUWNUWLUWNYMOLMZNZUWNOYMUNMZNZU + PZUWKUXAUHZUWNUWNUXBUXDUPZNUXFUWNUXHUWNYMUQFZOUQFZUXHYMURZVHYMOUSUTVAUWNU + XBUXDVBVCUWLUXCUXGUXEUWLUXCNUXAUWKUXCUWLUWOTPZUXAUXCYMOPZUXLUWNUXBOYMLMZU + XMYMVDUWNUXBUXNUXMUWNUXMUXBUXNNZUWNUXIUXJUXMUXOVEUXKVHYMOVFUTVGVIVJUXMUWO + OOUOHTYMOOUOUIVKVLVMUVBBUWOVNVOVSUXEUXGUWLUXEUWOEFZUXGUWNUXDUXPOEFUWNUXDU + XPVEVTOYMVPVQVRUWJUXAUAUWOEUUAUWOPZUWGUWRUWIUWTLUXQUWEUWPUWFUWQIUUAUWOUVB + GUIUUAUWOBGQUJUXQUWHUWSUVIIUUAUWOUDUKRULWAVMWBWCVOYAUWDUWNUXAUWBUHUVBBYMW + DWJWEWFWGWHWIYAUUTDEYAUWNNZYOBBGHZYQIHZUUMUUSLUWNYAYMUCFZYOUXTLMYMWKZBYMW + LVOUXRUUMOYOIHZYOUWNUUMUYCPYAUWNUULOYOIUWNYMYMXBWMSWBUXRYOYABWNFZUYAYOWNF + UWNBWOZUYBBYMWPWQWRWSYAUUSUXTPUWNYAUURUXSYQIYAUUROUXSIHUXSYAUUOOUUQUXSIUU + OOPYAUUOJTGHZOUUNTJGWTXAJWNFUYFOPXCJXMXDXEXFYAUUPBBGYABUYEXGRUJYAUXSUYDYA + UXSWNFUYEBBWPXHWRWSSXIXJXKUUATPZUUKUVAYAUYGUUJUUTDEUYGUUCUUMUUIUUSLUYGUUB + UULYOIUUATYMGQSUYGUUHUURYQIUYGUUEUUOUUGUUQIUYGUUDUUNJGUUATJGUIRUYGUUFUUPB + GUUATBKQRUJSULXLXNUUAUVBPZUUKUVLYAUYHUUJUVKDEUYHUUCUVDUUIUVJLUYHUUBUVCYOI + UUAUVBYMGQSUYHUUHUVIYQIUYHUUEUVFUUGUVHIUYHUUDUVEJGUUAUVBJGUIRUYHUUFUVGBGU + UAUVBBKQRUJSULXLXNUUAUVMPZUUKUWCYAUYIUUJUWBDEUYIUUCUVOUUIUWALUYIUUBUVNYOI + UUAUVMYMGQSUYIUUHUVTYQIUYIUUEUVQUUGUVSIUYIUUDUVPJGUUAUVMJGUIRUYIUUFUVRBGU + UAUVMBKQRUJSULXLXNUUAAPZUUKYTYAUYJUUJYSDEUYJUUCYPUUIYRLUYJUUBYNYOIUUAAYMG + QSUYJUUHYIYQIUYJUUEYFUUGYHIUYJUUDYEJGUUAAJGUIRUYJUUFYGBGUUAABKQRUJSULXLXN + XOXPYSYLDCEYMCPZYPYDYRYKLUYKYNYBYOYCIYMCAGUIYMCBGQUJUYKYQYJYIIYMCUDUKRULX + QVOXR $. $} $( Variant of ~ faclbnd5 providing a non-strict lower bound. (Contributed by @@ -147386,16 +147386,16 @@ notation is used by Donald Knuth for iterated exponentiation (_Science_ bccl $p |- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) e. NN0 ) $= ( vk vm cn0 wcel cv cbc co cz wral cc0 c1 wceq oveq1 eleq1d ralbidv oveq2 wa 0nn0 vn caddc cfz elfz1eq adantl bcn0 1nn0 eqeltri syl6eqel syl bcval3 - ax-mp wn mp3an1 pm2.61dan rgen cbvralv cmin bcpasc adantlr rspccva sylan2 - peano2zm nn0addcld adantll eqeltrrd ralrimiva ex syl5bi nn0ind sylan ) BE - FBCGZHIZEFZCJKZAJFBAHIZEFZDGZVLHIZEFZCJKLVLHIZEFZCJKUAGZVLHIZEFZCJKZWCMUB - IZVLHIZEFZCJKZVODUABVRLNZVTWBCJWKVSWAEVRLVLHOPQVRWCNZVTWECJWLVSWDEVRWCVLH - OPQVRWGNZVTWICJWMVSWHEVRWGVLHOPQVRBNZVTVNCJWNVSVMEVRBVLHOPQWBCJVLJFZVLLLU - CIFZWBWOWPSVLLNZWBWPWQWOVLLUDUEWQWALLHIZEVLLLHRWRMELEFZWRMNTLUFULUGUHUIUJ - WOWPUMZSWALEWSWOWTWALNTVLLUKUNTUIUOUPWFWCVRHIZEFZDJKZWCEFZWJWEXBCDJVLVRNW - DXAEVLVRWCHRPUQXDXCWJXDXCSZWICJXEWOSWDWCVLMURIZHIZUBIZWHEXDWOXHWHNXCVLWCU - SUTXCWOXHEFXDXCWOSWDXGXBWEDVLJVRVLNXAWDEVRVLWCHRPVAWOXCXFJFXGEFZVLVCXBXID - XFJVRXFNXAXGEVRXFWCHRPVAVBVDVEVFVGVHVIVJVNVQCAJVLANVMVPEVLABHRPVAVK $. + ax-mp mp3an1 pm2.61dan rgen cbvralvw cmin bcpasc adantlr rspccva peano2zm + wn sylan2 nn0addcld adantll eqeltrrd ralrimiva ex syl5bi nn0ind sylan ) B + EFBCGZHIZEFZCJKZAJFBAHIZEFZDGZVLHIZEFZCJKLVLHIZEFZCJKUAGZVLHIZEFZCJKZWCMU + BIZVLHIZEFZCJKZVODUABVRLNZVTWBCJWKVSWAEVRLVLHOPQVRWCNZVTWECJWLVSWDEVRWCVL + HOPQVRWGNZVTWICJWMVSWHEVRWGVLHOPQVRBNZVTVNCJWNVSVMEVRBVLHOPQWBCJVLJFZVLLL + UCIFZWBWOWPSVLLNZWBWPWQWOVLLUDUEWQWALLHIZEVLLLHRWRMELEFZWRMNTLUFULUGUHUIU + JWOWPVBZSWALEWSWOWTWALNTVLLUKUMTUIUNUOWFWCVRHIZEFZDJKZWCEFZWJWEXBCDJVLVRN + WDXAEVLVRWCHRPUPXDXCWJXDXCSZWICJXEWOSWDWCVLMUQIZHIZUBIZWHEXDWOXHWHNXCVLWC + URUSXCWOXHEFXDXCWOSWDXGXBWEDVLJVRVLNXAWDEVRVLWCHRPUTWOXCXFJFXGEFZVLVAXBXI + DXFJVRXFNXAXGEVRXFWCHRPUTVCVDVEVFVGVHVIVJVNVQCAJVLANVMVPEVLABHRPUTVK $. $( A binomial coefficient, in its standard domain, is a positive integer. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, @@ -148931,28 +148931,28 @@ are used instead of sets because their representation is shorter (and more hash0 a1i oveq12d cn0 0nn0 bcn0 ax-mp syl6eq pw0 eqcomd raleqi 0ex eqeq1d ralsn bitri sylibr rabid2 syl5reqr cvv hashsng eqtr4d adantl wn wa oveq1i bcval3 mp3an1 id 0z elfz3 syl6eqelr con3i notbid rabeq0 syl5eq rgen oveq2 - pm2.61dan eqeq2 rabbidv fveqeq2 simpll simplr simprr fveq2i eqeq2i ralbii - cbvrabv cbvralv simprl hashbclem expr ralrimdva syl5bi findcard2s rspccva - sylan ) BUCGBHIZDJZKLZAJZHIZXMMZABUDZNZHIZMZDOPZCOGXLCKLZXPCMZAXRNZHIZMZU - AJZHIZXMKLZXQAYHUDZNZHIZMZDOPTHIZXMKLZXQATUDZNZHIZMZDOPUBJZHIZXMKLZXQAUUA - UDZNZHIZMZDOPZUUAEJZUEUFZHIZXMKLZXQAUUJUDZNZHIZMZDOPZYBUAUBEBYHTMZYNYTDOU - URYJYPYMYSUURYIYOXMKYHTHUGUHUURYLYRHUURXQAYKYQYHTUIUJQRUKYHUUAMZYNUUGDOUU - SYJUUCYMUUFUUSYIUUBXMKYHUUAHUGUHUUSYLUUEHUUSXQAYKUUDYHUUAUIUJQRUKYHUUJMZY - NUUPDOUUTYJUULYMUUOUUTYIUUKXMKYHUUJHUGUHUUTYLUUNHUUTXQAYKUUMYHUUJUIUJQRUK - YHBMZYNYADOUVAYJXNYMXTUVAYIXLXMKYHBHUGUHUVAYLXSHUVAXQAYKXRYHBUIUJQRUKYTDO - XMOGZXMSSULLZGZYTUVDYTUVBUVDYPUMYSUVDYPSSKLZUMUVDYOSXMSKYOSMUVDUOUPXMSUNZ - UQSURGZUVEUMMUSSUTVAVBUVDYSTUEZHIZUMUVDYRUVHHUVDUVHYQYRVCUVDXQAYQPZYQYRMU - VDSXMMZUVJUVDXMSUVFVDUVJXQAUVHPUVKXQAYQUVHVCVEXQUVKATVFXOTMZXPSXMUVLXPYOS - XOTHUGUOVBVGZVHVIVJXQAYQVKVJVLQTVMGUVIUMMVFTVMVNVAVBVOVPUVBUVDVQZVRZYPSXM - KLZYSYOSXMKUOVSUVOUVPSYSUVGUVBUVNUVPSMUSXMSVTWAUVOYSYOSUVOYRTHUVOXQVQZAYQ - PZYRTMUVOUVKVQZUVRUVNUVSUVBUVKUVDUVKXMSUVCUVKWBSOGSUVCGWCSWDVAWEWFVPUVRUV - QAUVHPUVSUVQAYQUVHVCVEUVQUVSATVFUVLXQUVKUVMWGVHVIVJXQAYQWHVJQUOVBVOWIWLWJ - UUHUUBFJZKLZUUIHIUVTMZEUUDNZHIZMZFOPZUUAUCGZUUIUUAGVQZVRZUUQUUGUWEDFOXMUV - TMZUUCUWAUUFUWDXMUVTUUBKWKUWJUUEUWCHUWJUUEXPUVTMZAUUDNZUWCUWJXQUWKAUUDXMU - VTXPWMWNUWKUWBAEUUDXOUUIUVTHWOXBZVBQRXCUWIUWFUUPDOUWIUVBUWFUUPUWIUVBUWFVR - ZVRZAEUUAFXMUWGUWHUWNWPUWGUWHUWNWQUWOUWFUWAUWLHIZMZFOPUWIUVBUWFWRUWQUWEFO - UWPUWDUWAUWLUWCHUWMWSWTXAVJUWIUVBUWFXDXEXFXGXHXIYAYGDCOXMCMZXNYCXTYFXMCXL - KWKUWRXSYEHUWRXQYDAXRXMCXPWMWNQRXJXK $. + eqeq2 rabbidv fveqeq2 cbvrabv cbvralvw simpll simplr simprr fveq2i eqeq2i + pm2.61dan ralbii simprl hashbclem expr ralrimdva findcard2s rspccva sylan + syl5bi ) BUCGBHIZDJZKLZAJZHIZXMMZABUDZNZHIZMZDOPZCOGXLCKLZXPCMZAXRNZHIZMZ + UAJZHIZXMKLZXQAYHUDZNZHIZMZDOPTHIZXMKLZXQATUDZNZHIZMZDOPUBJZHIZXMKLZXQAUU + AUDZNZHIZMZDOPZUUAEJZUEUFZHIZXMKLZXQAUUJUDZNZHIZMZDOPZYBUAUBEBYHTMZYNYTDO + UURYJYPYMYSUURYIYOXMKYHTHUGUHUURYLYRHUURXQAYKYQYHTUIUJQRUKYHUUAMZYNUUGDOU + USYJUUCYMUUFUUSYIUUBXMKYHUUAHUGUHUUSYLUUEHUUSXQAYKUUDYHUUAUIUJQRUKYHUUJMZ + YNUUPDOUUTYJUULYMUUOUUTYIUUKXMKYHUUJHUGUHUUTYLUUNHUUTXQAYKUUMYHUUJUIUJQRU + KYHBMZYNYADOUVAYJXNYMXTUVAYIXLXMKYHBHUGUHUVAYLXSHUVAXQAYKXRYHBUIUJQRUKYTD + OXMOGZXMSSULLZGZYTUVDYTUVBUVDYPUMYSUVDYPSSKLZUMUVDYOSXMSKYOSMUVDUOUPXMSUN + ZUQSURGZUVEUMMUSSUTVAVBUVDYSTUEZHIZUMUVDYRUVHHUVDUVHYQYRVCUVDXQAYQPZYQYRM + UVDSXMMZUVJUVDXMSUVFVDUVJXQAUVHPUVKXQAYQUVHVCVEXQUVKATVFXOTMZXPSXMUVLXPYO + SXOTHUGUOVBVGZVHVIVJXQAYQVKVJVLQTVMGUVIUMMVFTVMVNVAVBVOVPUVBUVDVQZVRZYPSX + MKLZYSYOSXMKUOVSUVOUVPSYSUVGUVBUVNUVPSMUSXMSVTWAUVOYSYOSUVOYRTHUVOXQVQZAY + QPZYRTMUVOUVKVQZUVRUVNUVSUVBUVKUVDUVKXMSUVCUVKWBSOGSUVCGWCSWDVAWEWFVPUVRU + VQAUVHPUVSUVQAYQUVHVCVEUVQUVSATVFUVLXQUVKUVMWGVHVIVJXQAYQWHVJQUOVBVOWIXBW + JUUHUUBFJZKLZUUIHIUVTMZEUUDNZHIZMZFOPZUUAUCGZUUIUUAGVQZVRZUUQUUGUWEDFOXMU + VTMZUUCUWAUUFUWDXMUVTUUBKWKUWJUUEUWCHUWJUUEXPUVTMZAUUDNZUWCUWJXQUWKAUUDXM + UVTXPWLWMUWKUWBAEUUDXOUUIUVTHWNWOZVBQRWPUWIUWFUUPDOUWIUVBUWFUUPUWIUVBUWFV + RZVRZAEUUAFXMUWGUWHUWNWQUWGUWHUWNWRUWOUWFUWAUWLHIZMZFOPUWIUVBUWFWSUWQUWEF + OUWPUWDUWAUWLUWCHUWMWTXAXCVJUWIUVBUWFXDXEXFXGXKXHYAYGDCOXMCMZXNYCXTYFXMCX + LKWKUWRXSYEHUWRXQYDAXRXMCXPWLWMQRXIXJ $. $} ${ @@ -149926,7 +149926,7 @@ Proper unordered pairs and triples (sets of size 2 and 3) ( vx wsbc cfn wcel chash cfv cle wbr cn0 wi cv wceq wa wex dfclel cz nn0z wal mp1i ad2antlr wb breq2 eqcoms biimpcd adantr c1 caddc co eqeq1 anbi2d imp imbi1d 2albidv weq eqcom sylan2b a1i w3a simpl simpr sbceq1d sbceqbid - gen2 fveq2 eqeq2d anbi12d imbi12d cbval2vv cc0 nn0ge0 0red nn0re zre letr + gen2 fveq2 eqeq2d anbi12d imbi12d cbval2vw cc0 nn0ge0 0red nn0re zre letr cr syl3anc 0nn0 pm3.22 0z eluz1 mpbird eluznn0 sylancr ex syl6com pm2.43a cuz com14 com12 3adant1 clt nn0p1gt0 breqtrrd adantrl cvv hashgt0elex csn mp2b vex hashdifsnp1 syl5bi peano2nn0 ad2antrr simplrr simprlr jca spc2gv @@ -150685,11 +150685,11 @@ of an open range of nonnegative integers (of length equal to the length of elovmpowrd $p |- ( Z e. ( V O Y ) -> ( V e. _V /\ Y e. _V /\ Z e. Word V ) ) $= ( vx wcel cvv cv cword csb w3a crab cmpo wa adantr co wceq csbwrdg eqcomd - rabeqdv mpoeq3ia eqtri wrdexg eqeltrd elovmporab1 wb eleq2d 3expia sylbid - id 3impia syl ) HFGEUAKFLKZGLKZHJFJMNZOZKZPURUSHFNZKZPZADBCJUTEFGHEDBLLAC - DMZNZQZRDBLLACJVFUTOZQZRIDBLLVHVJVFLKZBMLKZSACVGVIVKVGVIUBVLVKVIVGJVFLUCU - DTUEUFUGURVALKUSURVAVCLJFLUCZFLUHUITUJURUSVBVEURUSSVBVDVEURVBVDUKUSURVAVC - HVMULTURUSVDVEVEUOUMUNUPUQ $. + rabeqdv mpoeq3ia eqtri wrdexg elovmporab1w wb eleq2d 3expia sylbid 3impia + eqeltrd id syl ) HFGEUAKFLKZGLKZHJFJMNZOZKZPURUSHFNZKZPZADBCJUTEFGHEDBLLA + CDMZNZQZRDBLLACJVFUTOZQZRIDBLLVHVJVFLKZBMLKZSACVGVIVKVGVIUBVLVKVIVGJVFLUC + UDTUEUFUGURVALKUSURVAVCLJFLUCZFLUHUOTUIURUSVBVEURUSSVBVDVEURVBVDUJUSURVAV + CHVMUKTURUSVDVEVEUPULUMUNUQ $. $} ${ @@ -152995,32 +152995,32 @@ computer programs (as last() or lastChar()), the terminology used for (Proof shortened by AV, 12-Oct-2022.) $) wrdind $p |- ( A e. Word B -> ta ) $= ( wcel wceq wi co vn vm cword cv chash cfv wral cn0 lencl cc0 caddc eqeq2 - c1 imbi1d ralbidv hasheq0 mpbiri syl6bi rgen fveqeq2 imbi12d cbvralv cmin - c0 wa cpfx clsw cs1 cconcat wsbc cfz simprl cfzo fzossfz nn0p1nn ad2antrr - cn simprr eqeltrd fzo0end syl sseldi pfxlen syl2anc oveq1d cc nn0cn pncan - ax-1cn sylancl 3eqtrd vex sbcie dfsbcq syl5bbr pfxcl ad2antrl rspcdva mpd - simplr wne cle wbr nnge1d wb wrdlenge1n0 mpbird lswcl sbceq1d s1eq oveq2d - oveq1 imbi2d 3imtr4g vtocl2ga cfn wrdfin hashnncl mpbid pfxlswccat eqcomd - ovex sbceq1a expr ralrimiva ex syl5bi nn0ind eqidd rspcv mp2d ) IJUCZQZFU - DZUEUFZIUEUFZRZASZFYLUGZYPYPRZEYMYPUHQYSJIUIYOUAUDZRZASZFYLUGYOUJRZASZFYL - UGYOUBUDZRZASZFYLUGZYOUUFUMUKTZRZASZFYLUGZYSUAUBYPUUAUJRZUUCUUEFYLUUNUUBU - UDAUUAUJYOULUNUOUUAUUFRZUUCUUHFYLUUOUUBUUGAUUAUUFYOULUNUOUUAUUJRZUUCUULFY - LUUPUUBUUKAUUAUUJYOULUNUOUUAYPRZUUCYRFYLUUQUUBYQAUUAYPYOULUNUOUUEFYLYNYLQ - ZUUDYNVDRZAYNYLUPUUSABOKUQURUSUUIGUDZUEUFUUFRZCSZGYLUGZUUFUHQZUUMUUHUVBFG - YLYNUUTRUUGUVAACYNUUTUUFUEUTLVAVBUVDUVCUUMUVDUVCVEZUULFYLUVEUURUUKAUVEUUR - UUKVEZVEZAAFYNYOUMVCTZVFTZYNVGUFZVHZVITZVJZUVGAFUVIVJZUVMUVGUVIUEUFZUUFRZ - UVNUVGUVOUVHUUJUMVCTZUUFUVGUURUVHUJYOVKTZQUVOUVHRUVEUURUUKVLZUVGUJYOVMTZU - VRUVHUJYOVNUVGYOVQQZUVHUVTQUVGYOUUJVQUVEUURUUKVRZUVDUUJVQQUVCUVFUUFVOVPVS - ZYOVTWAWBJYNUVHWCWDUVGYOUUJUMVCUWBWEUVGUUFWFQZUMWFQUVQUUFRUVDUWDUVCUVFUUF - WGVPWIUUFUMWHWJWKUVGUVBUVPUVNSGYLUVIUUTUVIRZUVAUVPCUVNUUTUVIUUFUEUTCAFUUT - VJZUWEUVNACFUUTGWLLWMZAFUUTUVIWNZWOVAUVDUVCUVFWTUURUVIYLQZUVEUUKJYNUVHWPW - QZWRWSUVGUWIUVJJQZUVNUVMSZUWJUVGUURYNVDXAZUWKUVSUVGUWMUMYOXBXCZUVGYOUWCXD - UURUWMUWNXEUVEUUKJYNXFWQXGJYNXHWDUWFAFUUTHUDZVHZVITZVJZSUVNAFUVIUWPVITZVJ - ZSUWLGHUVIUVJYLJUWEUWFUVNUWRUWTUWHUWEAFUWQUWSUUTUVIUWPVIXLXIVAUWOUVJRZUWT - UVMUVNUXAAFUWSUVLUXAUWPUVKUVIVIUWOUVJXJXKXIXMUUTYLQUWOJQVECDUWFUWRPUWGADF - UWQUUTUWPVIYBMWMXNXOWDWSUVGYNUVLRZAUVMXEUVGUURUWMUXBUVSUVGUWAUWMUWCUVGYNX - PQZUWAUWMXEUURUXCUVEUUKJYNXQWQYNXRWAXSUURUWMVEUVLYNJYNXTYAWDAFUVLYCWAXGYD - YEYFYGYHWAYMYPYIYRYTESFIYLYNIRYQYTAEYNIYPUEUTNVAYJYK $. + c1 imbi1d ralbidv c0 hasheq0 mpbiri rgen fveqeq2 imbi12d cbvralvw wa cmin + syl6bi cpfx clsw cs1 cconcat wsbc cfz simprl cfzo fzossfz simprr ad2antrr + cn nn0p1nn eqeltrd fzo0end syl sseldi pfxlen oveq1d cc nn0cn ax-1cn pncan + syl2anc sylancl 3eqtrd sbcie dfsbcq syl5bbr simplr pfxcl ad2antrl rspcdva + vex mpd wne cle wbr nnge1d wb wrdlenge1n0 mpbird lswcl oveq1 sbceq1d s1eq + oveq2d imbi2d ovex 3imtr4g vtocl2ga cfn wrdfin hashnncl pfxlswccat eqcomd + mpbid sbceq1a expr ralrimiva ex syl5bi nn0ind eqidd rspcv mp2d ) IJUCZQZF + UDZUEUFZIUEUFZRZASZFYLUGZYPYPRZEYMYPUHQYSJIUIYOUAUDZRZASZFYLUGYOUJRZASZFY + LUGYOUBUDZRZASZFYLUGZYOUUFUMUKTZRZASZFYLUGZYSUAUBYPUUAUJRZUUCUUEFYLUUNUUB + UUDAUUAUJYOULUNUOUUAUUFRZUUCUUHFYLUUOUUBUUGAUUAUUFYOULUNUOUUAUUJRZUUCUULF + YLUUPUUBUUKAUUAUUJYOULUNUOUUAYPRZUUCYRFYLUUQUUBYQAUUAYPYOULUNUOUUEFYLYNYL + QZUUDYNUPRZAYNYLUQUUSABOKURVEUSUUIGUDZUEUFUUFRZCSZGYLUGZUUFUHQZUUMUUHUVBF + GYLYNUUTRUUGUVAACYNUUTUUFUEUTLVAVBUVDUVCUUMUVDUVCVCZUULFYLUVEUURUUKAUVEUU + RUUKVCZVCZAAFYNYOUMVDTZVFTZYNVGUFZVHZVITZVJZUVGAFUVIVJZUVMUVGUVIUEUFZUUFR + ZUVNUVGUVOUVHUUJUMVDTZUUFUVGUURUVHUJYOVKTZQUVOUVHRUVEUURUUKVLZUVGUJYOVMTZ + UVRUVHUJYOVNUVGYOVQQZUVHUVTQUVGYOUUJVQUVEUURUUKVOZUVDUUJVQQUVCUVFUUFVRVPV + SZYOVTWAWBJYNUVHWCWIUVGYOUUJUMVDUWBWDUVGUUFWEQZUMWEQUVQUUFRUVDUWDUVCUVFUU + FWFVPWGUUFUMWHWJWKUVGUVBUVPUVNSGYLUVIUUTUVIRZUVAUVPCUVNUUTUVIUUFUEUTCAFUU + TVJZUWEUVNACFUUTGWSLWLZAFUUTUVIWMZWNVAUVDUVCUVFWOUURUVIYLQZUVEUUKJYNUVHWP + WQZWRWTUVGUWIUVJJQZUVNUVMSZUWJUVGUURYNUPXAZUWKUVSUVGUWMUMYOXBXCZUVGYOUWCX + DUURUWMUWNXEUVEUUKJYNXFWQXGJYNXHWIUWFAFUUTHUDZVHZVITZVJZSUVNAFUVIUWPVITZV + JZSUWLGHUVIUVJYLJUWEUWFUVNUWRUWTUWHUWEAFUWQUWSUUTUVIUWPVIXIXJVAUWOUVJRZUW + TUVMUVNUXAAFUWSUVLUXAUWPUVKUVIVIUWOUVJXKXLXJXMUUTYLQUWOJQVCCDUWFUWRPUWGAD + FUWQUUTUWPVIXNMWLXOXPWIWTUVGYNUVLRZAUVMXEUVGUURUWMUXBUVSUVGUWAUWMUWCUVGYN + XQQZUWAUWMXEUURUXCUVEUUKJYNXRWQYNXSWAYBUURUWMVCUVLYNJYNXTYAWIAFUVLYCWAXGY + DYEYFYGYHWAYMYPYIYRYTESFIYLYNIRYQYTAEYNIYPUEUTNVAYJYK $. $} ${ @@ -153049,68 +153049,68 @@ computer programs (as last() or lastChar()), the terminology used for syl2anc jca simprlr ad2antll simplr oveq1d cfz ad2antrr eqeltrd pfxlen cc oveq1 imp vex sbc2ie a1i simpr sbceq1d dfsbcq sbccom eqeq2d oveq2d imbi2d s1eq ovex cfn wrdfin hashnncl mpbid pfxlswccat eqcomd sbceq1a rspcv com24 - imp31 sylbid rgen2 cbvraldva cbvralv nn0p1nn jca32 adantlr simprl simprrl - fzossfz simprrr fzo0end sseldi oveq2 eleq12d 3eqtr4d nn0cn ax-1cn sylancl - cfzo pncan 3eqtrd expcom bicomi 3bitrd rspcdv rspcimdv syl3c syl6bb bitrd - sbcbidv simpll syl3anc 3imtr4g vtocl4ga sylc eqtr2 expr ralrimivva syl5bi - sylan9bb nn0ind 3ad2ant1 anbi1d ralbidv 3ad2ant2 eqidd com23 expd 3adant2 - mpd com34 mp2d ) LNUFZUGZMOUFZUGZLUHUIZMUHUIZUJZUKZGULZUHUIZUXAUJZUXEUWTU - JZUMZFUNZGUWPUOZUWTUWTUJZEUXCUXEJULZUHUIZUJZUXGUMZAUNZGUWPUOZJUWRUOZUXJUW - QUWSUXRUXBUWQUWTUPUGUXRNLUQUXNUXEUDULZUJZUMZAUNZGUWPUOJUWRUOUXNUXEVAUJZUM - ZAUNZGUWPUOJUWRUOUXNUXEUEULZUJZUMZAUNZGUWPUOZJUWRUOZUXNUXEUYFURUSUTZUJZUM - ZAUNZGUWPUOJUWRUOZUXRUDUEUWTUXSVAUJZUYBUYEJGUWRUWPUYQUYAUYDAUYQUXTUYCUXNU - XSVAUXEVBVCVDVEUDUEVFZUYBUYIJGUWRUWPUYRUYAUYHAUYRUXTUYGUXNUXSUYFUXEVBVCVD - VEUXSUYLUJZUYBUYOJGUWRUWPUYSUYAUYNAUYSUXTUYMUXNUXSUYLUXEVBVCVDVEUXSUWTUJZ - UYBUXPJGUWRUWPUYTUYAUXOAUYTUXTUXGUXNUXSUWTUXEVBVCVDVEUYEJGUWRUWPUXLUWRUGZ - UXDUWPUGZUMZUYCUXNAVUCUYCUXNAUNVUCUYCUMUXNVAUXMUJZAUYCUXNVUDVGVUCUXEVAUXM - VHVIVUAVUBUYCVUDAUNVUAVUDUYCVUBAVUAVUDUXLVMUJZUYCVUBAUNUNVUDUXMVAUJVUAVUE - VAUXMVJUXLUWRVKVLVUBUYCVUEAVUBUYCUXDVMUJZVUEAUNUXDUWPVKVUFVUEAVUFVUEUMABU - BQVNVOVPVQVPUUAUUBUUCVOVRUUDUYKHULZUHUIZKULZUHUIZUJZVUHUYFUJZUMZCUNZHUWPU - OZKUWRUOZUYFUPUGZUYPUYJVUOJKUWRJKVFZUYIVUNGHUWPGHVFZVURUYIVUNVGVUSVURUMZU - YHVUMACVUTUXNVUKUYGVULVUSVURUXEVUHUXMVUJUXDVUGUHVSUXLVUIUHVSVTVUSUYGVULVG - VURUXDVUGUYFUHWAWDWBRWCWQUUEUUFVUQVUPUYPVUQVUPUMZUYOJGUWRUWPVVAVUCUYNAVVA - VUCUYNUMZUMZAAJUXLUXMURWEUTZWFUTZUXLWGUIZWHZWIUTZWJZGUXDUXEURWEUTZWFUTZUX - DWGUIZWHZWIUTZWJZVVCVVEUWRUGZVVFOUGZUMZVVKUWPUGZVVLNUGZUMUMZAJVVEWJZGVVKW - JZVVKUHUIZVVEUHUIZUJZUMZVVOVUQVVBVWAVUPVUQVVBUMZVVRVVSVVTVWHVVPVVQVUCVVPV - UQUYNVUAVVPVUBOUXLVVDWKWDZWLVWHVUAUXLVMWMZVVQVUQVUAVUBUYNWNZVWHVWJURUXMWO - WPZVWHUXMVVBVUQUXMWRUGZUYNVUQVWMUNZVUCUYMUXNVWNUYMUXNUYLUXMUJZVWNUXEUYLUX - MVHVUQVWMVWOUYLWRUGZUYFUUGZVWMVWPVGUXMUYLUXMUYLWRWSWTXAVPXBVIXBXCVWHVUAVW - JVWLVGVWKOUXLXDXEXFOUXLXGXHXIVUCVVSVUQUYNVUBVVSVUANUXDVVJWKVIZWLVWHVUBUXD - VMWMZVVTVUQVUAVUBUYNXJZVWHVWSURUXEWOWPZVWHUXEVVBVUQUXEWRUGZUYMVUQVXBUNVUC - UXNVUQVXBUYMVWPVWQUXEUYLWRWSXAXKXBXCVWHVUBVWSVXAVGVWTNUXDXDXEXFNUXDXGXHUU - HUUIVVCVWCVWFVVCVUCVUPVWFVWDUYFUJZUMZVWCVVAVUCUYNUUJVUQVUPVVBXLVVCVWFVXCV - VCVVJVVDVWDVWEVVCUXEUXMURWEVVAVUCUXNUYMUUKXMVVCVUBVVJVAUXEXNUTZUGZVWDVVJU - JVVAVUAVUBUYNXJZVVCVAUXEUVBUTZVXEVVJVAUXEUULVVCVXBVVJVXHUGVVCUXEUYLWRVVAV - UCUXNUYMUUMZVUQVWPVUPVVBVWQXOZXPZUXEUUNXEUUOZNUXDVVJXQXHZVVCVUAVVDVAUXMXN - UTZUGZVWEVVDUJVVAVUAVUBUYNWNZVVCVXOVXFVXLUYNVXOVXFVGZVVAVUCUXNVXQUYMVXQUX - MUXEUXMUXEUJVVDVVJVXNVXEUXMUXEURWEXSUXMUXEVAXNUUPUUQWTWDXKXFOUXLVVDXQXHUU - RZVVCVWDVVJUYLURWEUTZUYFVXMVVCUXEUYLURWEVXIXMVVCUYFXRUGZURXRUGVXSUYFUJVUQ - VXTVUPVVBUYFUUSXOUUTUYFURUVCUVAUVDXIVUCVUOVXDVWCUNZKVVEUWRVWIVUCVUIVVEUJZ - UMZVUNVYAHVVKUWPVUCVVSVYBVWRWDVYCVUGVVKUJZUMZVUMVXDCVWCVYEVUKVWFVULVXCVYC - VYDVUKVWFVGZVYBVYDVYFUNVUCVYDVYBVYFVYDVYBVUHVWDVUJVWEVUGVVKUHVSVUIVVEUHVS - ZVTUVEVIXTVYDVULVXCVGVYCVUGVVKUYFUHWAVIWBVYECAJVUIWJZGVUGWJZVYHGVVKWJZVWC - CVYIVGVYEVYICACGJVUGVUIHYAZKYAZRYBUVFYCVYEVYHGVUGVVKVYCVYDYDYEVYCVYJVWCVG - ZVYDVYBVYMVUCVYBVYHVWBGVVKAJVUIVVEYFUVMVIWDUVGWCUVHUVIUVJVXRXIAGVUGWJZJVU - IWJZVUKUMZAGVUGIULZWHZWIUTZWJZJVUIPULZWHZWIUTZWJZUNVWBGVUGWJZVUHVWEUJZUMZ - VYTJVVEWUBWIUTZWJZUNZWUGVVIGVYSWJZUNZVWGVVOUNVWGVVIGVVKVYRWIUTZWJZUNKPHIV - VEVVFVVKVVLUWROUWPNVYBVYPWUGWUDWUIVYBVYOWUEVUKWUFVYBVYOVYNJVVEWJWUEVYNJVU - IVVEYFAJGVVEVUGYGUVKVYBVUJVWEVUHVYGYHWBVYBVYTJWUCWUHVUIVVEWUBWIXSYEWCWUAV - VFUJZWUJWUGVYTJVVHWJZUNWULWUOWUIWUPWUGWUOVYTJWUHVVHWUOWUBVVGVVEWIWUAVVFYK - YIYEYJWUOWUPWUKWUGWUPWUKVGWUOAJGVVHVYSYGYCYJUVLVYDWUGVWGWUKWUNVYDWUEVWCWU - FVWFVWBGVUGVVKYFVUGVVKVWEUHWAWBVYDVVIGVYSWUMVUGVVKVYRWIXSYEWCVYQVVLUJZWUN - VVOVWGWUQVVIGWUMVVNWUQVYRVVMVVKWIVYQVVLYKYIYEYJVUIUWRUGWUAOUGUMZVUGUWPUGV - YQNUGUMZUMZVUKVYOWUDWUTVUKVYOWUDUNWUTVUKUMZCDVYOWUDWVAWUSWURVUKCDUNWURWUS - VUKXLWURWUSVUKUVNWUTVUKYDUCUVOACJGVUIVUGVYLVYKVUSVURACVGRWQYBADJGWUCVYSVU - IWUBWIYLVUGVYRWIYLUXDVYSUJUXLWUCUJADVGSWQYBUVPVOVRUVQUVRVVCUXLVVHUJZUXDVV - NUJZAVVOVGVVCVUAVWJWVBVXPVVCVWMVWJVVCUXMUYLWRUYNUXMUYLUJVVAVUCUXEUXMUYLUV - SXKVXJXPVVCUXLYMUGZVWMVWJVGVUCWVDVVAUYNVUAWVDVUBOUXLYNWDWLUXLYOXEYPVUAVWJ - UMVVHUXLOUXLYQYRXHVVCVUBVWSWVCVXGVVCVXBVWSVXKVVCUXDYMUGZVXBVWSVGVUCWVEVVA - UYNVUBWVEVUANUXDYNVIWLUXDYOXEYPVUBVWSUMVVNUXDNUXDYQYRXHWVBAVVIWVCVVOAJVVH - YSVVIGVVNYSUWCXHXFUVTUWAVOUWBUWDXEUWEUWSUWQUXRUXJUNUXBUXQUXJJMUWRUXLMUJZU - XPUXIGUWPWVFUXOUXHAFWVFUXNUXFUXGWVFUXMUXAUXEUXLMUHVSYHUWFUAWCUWGYTUWHUWMU - XCUWTUWIUWQUXBUXJUXKEUNUNZUWSUWQUXBWVGUWQUXBUXKUXJEUWQUXBUXKUXJEUNUWQUXJU - XBUXKUMZEUXIWVHEUNGLUWPUXDLUJZUXHWVHFEWVIUXFUXBUXGUXKUXDLUXAUHWAUXDLUWTUH - WAWBTWCYTUWJUWKUWNXTUWLUWO $. + imp31 sylbid rgen2 cbvraldva cbvralvw nn0p1nn adantlr simprl simprrl cfzo + jca32 fzossfz simprrr fzo0end sseldi oveq2 eleq12d 3eqtr4d ax-1cn sylancl + nn0cn pncan 3eqtrd expcom bicomi sbcbidv 3bitrd rspcdv syl3c syl6bb bitrd + rspcimdv simpll syl3anc 3imtr4g vtocl4ga eqtr2 sylan9bb ralrimivva syl5bi + sylc expr nn0ind 3ad2ant1 anbi1d ralbidv 3ad2ant2 mpd eqidd com23 3adant2 + expd com34 mp2d ) LNUFZUGZMOUFZUGZLUHUIZMUHUIZUJZUKZGULZUHUIZUXAUJZUXEUWT + UJZUMZFUNZGUWPUOZUWTUWTUJZEUXCUXEJULZUHUIZUJZUXGUMZAUNZGUWPUOZJUWRUOZUXJU + WQUWSUXRUXBUWQUWTUPUGUXRNLUQUXNUXEUDULZUJZUMZAUNZGUWPUOJUWRUOUXNUXEVAUJZU + MZAUNZGUWPUOJUWRUOUXNUXEUEULZUJZUMZAUNZGUWPUOZJUWRUOZUXNUXEUYFURUSUTZUJZU + MZAUNZGUWPUOJUWRUOZUXRUDUEUWTUXSVAUJZUYBUYEJGUWRUWPUYQUYAUYDAUYQUXTUYCUXN + UXSVAUXEVBVCVDVEUDUEVFZUYBUYIJGUWRUWPUYRUYAUYHAUYRUXTUYGUXNUXSUYFUXEVBVCV + DVEUXSUYLUJZUYBUYOJGUWRUWPUYSUYAUYNAUYSUXTUYMUXNUXSUYLUXEVBVCVDVEUXSUWTUJ + ZUYBUXPJGUWRUWPUYTUYAUXOAUYTUXTUXGUXNUXSUWTUXEVBVCVDVEUYEJGUWRUWPUXLUWRUG + ZUXDUWPUGZUMZUYCUXNAVUCUYCUXNAUNVUCUYCUMUXNVAUXMUJZAUYCUXNVUDVGVUCUXEVAUX + MVHVIVUAVUBUYCVUDAUNVUAVUDUYCVUBAVUAVUDUXLVMUJZUYCVUBAUNUNVUDUXMVAUJVUAVU + EVAUXMVJUXLUWRVKVLVUBUYCVUEAVUBUYCUXDVMUJZVUEAUNUXDUWPVKVUFVUEAVUFVUEUMAB + UBQVNVOVPVQVPUUAUUBUUCVOVRUUDUYKHULZUHUIZKULZUHUIZUJZVUHUYFUJZUMZCUNZHUWP + UOZKUWRUOZUYFUPUGZUYPUYJVUOJKUWRJKVFZUYIVUNGHUWPGHVFZVURUYIVUNVGVUSVURUMZ + UYHVUMACVUTUXNVUKUYGVULVUSVURUXEVUHUXMVUJUXDVUGUHVSUXLVUIUHVSVTVUSUYGVULV + GVURUXDVUGUYFUHWAWDWBRWCWQUUEUUFVUQVUPUYPVUQVUPUMZUYOJGUWRUWPVVAVUCUYNAVV + AVUCUYNUMZUMZAAJUXLUXMURWEUTZWFUTZUXLWGUIZWHZWIUTZWJZGUXDUXEURWEUTZWFUTZU + XDWGUIZWHZWIUTZWJZVVCVVEUWRUGZVVFOUGZUMZVVKUWPUGZVVLNUGZUMUMZAJVVEWJZGVVK + WJZVVKUHUIZVVEUHUIZUJZUMZVVOVUQVVBVWAVUPVUQVVBUMZVVRVVSVVTVWHVVPVVQVUCVVP + VUQUYNVUAVVPVUBOUXLVVDWKWDZWLVWHVUAUXLVMWMZVVQVUQVUAVUBUYNWNZVWHVWJURUXMW + OWPZVWHUXMVVBVUQUXMWRUGZUYNVUQVWMUNZVUCUYMUXNVWNUYMUXNUYLUXMUJZVWNUXEUYLU + XMVHVUQVWMVWOUYLWRUGZUYFUUGZVWMVWPVGUXMUYLUXMUYLWRWSWTXAVPXBVIXBXCVWHVUAV + WJVWLVGVWKOUXLXDXEXFOUXLXGXHXIVUCVVSVUQUYNVUBVVSVUANUXDVVJWKVIZWLVWHVUBUX + DVMWMZVVTVUQVUAVUBUYNXJZVWHVWSURUXEWOWPZVWHUXEVVBVUQUXEWRUGZUYMVUQVXBUNVU + CUXNVUQVXBUYMVWPVWQUXEUYLWRWSXAXKXBXCVWHVUBVWSVXAVGVWTNUXDXDXEXFNUXDXGXHU + ULUUHVVCVWCVWFVVCVUCVUPVWFVWDUYFUJZUMZVWCVVAVUCUYNUUIVUQVUPVVBXLVVCVWFVXC + VVCVVJVVDVWDVWEVVCUXEUXMURWEVVAVUCUXNUYMUUJXMVVCVUBVVJVAUXEXNUTZUGZVWDVVJ + UJVVAVUAVUBUYNXJZVVCVAUXEUUKUTZVXEVVJVAUXEUUMVVCVXBVVJVXHUGVVCUXEUYLWRVVA + VUCUXNUYMUUNZVUQVWPVUPVVBVWQXOZXPZUXEUUOXEUUPZNUXDVVJXQXHZVVCVUAVVDVAUXMX + NUTZUGZVWEVVDUJVVAVUAVUBUYNWNZVVCVXOVXFVXLUYNVXOVXFVGZVVAVUCUXNVXQUYMVXQU + XMUXEUXMUXEUJVVDVVJVXNVXEUXMUXEURWEXSUXMUXEVAXNUUQUURWTWDXKXFOUXLVVDXQXHU + USZVVCVWDVVJUYLURWEUTZUYFVXMVVCUXEUYLURWEVXIXMVVCUYFXRUGZURXRUGVXSUYFUJVU + QVXTVUPVVBUYFUVBXOUUTUYFURUVCUVAUVDXIVUCVUOVXDVWCUNZKVVEUWRVWIVUCVUIVVEUJ + ZUMZVUNVYAHVVKUWPVUCVVSVYBVWRWDVYCVUGVVKUJZUMZVUMVXDCVWCVYEVUKVWFVULVXCVY + CVYDVUKVWFVGZVYBVYDVYFUNVUCVYDVYBVYFVYDVYBVUHVWDVUJVWEVUGVVKUHVSVUIVVEUHV + SZVTUVEVIXTVYDVULVXCVGVYCVUGVVKUYFUHWAVIWBVYECAJVUIWJZGVUGWJZVYHGVVKWJZVW + CCVYIVGVYEVYICACGJVUGVUIHYAZKYAZRYBUVFYCVYEVYHGVUGVVKVYCVYDYDYEVYCVYJVWCV + GZVYDVYBVYMVUCVYBVYHVWBGVVKAJVUIVVEYFUVGVIWDUVHWCUVIUVMUVJVXRXIAGVUGWJZJV + UIWJZVUKUMZAGVUGIULZWHZWIUTZWJZJVUIPULZWHZWIUTZWJZUNVWBGVUGWJZVUHVWEUJZUM + ZVYTJVVEWUBWIUTZWJZUNZWUGVVIGVYSWJZUNZVWGVVOUNVWGVVIGVVKVYRWIUTZWJZUNKPHI + VVEVVFVVKVVLUWROUWPNVYBVYPWUGWUDWUIVYBVYOWUEVUKWUFVYBVYOVYNJVVEWJWUEVYNJV + UIVVEYFAJGVVEVUGYGUVKVYBVUJVWEVUHVYGYHWBVYBVYTJWUCWUHVUIVVEWUBWIXSYEWCWUA + VVFUJZWUJWUGVYTJVVHWJZUNWULWUOWUIWUPWUGWUOVYTJWUHVVHWUOWUBVVGVVEWIWUAVVFY + KYIYEYJWUOWUPWUKWUGWUPWUKVGWUOAJGVVHVYSYGYCYJUVLVYDWUGVWGWUKWUNVYDWUEVWCW + UFVWFVWBGVUGVVKYFVUGVVKVWEUHWAWBVYDVVIGVYSWUMVUGVVKVYRWIXSYEWCVYQVVLUJZWU + NVVOVWGWUQVVIGWUMVVNWUQVYRVVMVVKWIVYQVVLYKYIYEYJVUIUWRUGWUAOUGUMZVUGUWPUG + VYQNUGUMZUMZVUKVYOWUDWUTVUKVYOWUDUNWUTVUKUMZCDVYOWUDWVAWUSWURVUKCDUNWURWU + SVUKXLWURWUSVUKUVNWUTVUKYDUCUVOACJGVUIVUGVYLVYKVUSVURACVGRWQYBADJGWUCVYSV + UIWUBWIYLVUGVYRWIYLUXDVYSUJUXLWUCUJADVGSWQYBUVPVOVRUVQUWBVVCUXLVVHUJZUXDV + VNUJZAVVOVGVVCVUAVWJWVBVXPVVCVWMVWJVVCUXMUYLWRUYNUXMUYLUJVVAVUCUXEUXMUYLU + VRXKVXJXPVVCUXLYMUGZVWMVWJVGVUCWVDVVAUYNVUAWVDVUBOUXLYNWDWLUXLYOXEYPVUAVW + JUMVVHUXLOUXLYQYRXHVVCVUBVWSWVCVXGVVCVXBVWSVXKVVCUXDYMUGZVXBVWSVGVUCWVEVV + AUYNVUBWVEVUANUXDYNVIWLUXDYOXEYPVUBVWSUMVVNUXDNUXDYQYRXHWVBAVVIWVCVVOAJVV + HYSVVIGVVNYSUVSXHXFUWCUVTVOUWAUWDXEUWEUWSUWQUXRUXJUNUXBUXQUXJJMUWRUXLMUJZ + UXPUXIGUWPWVFUXOUXHAFWVFUXNUXFUXGWVFUXMUXAUXEUXLMUHVSYHUWFUAWCUWGYTUWHUWI + UXCUWTUWJUWQUXBUXJUXKEUNUNZUWSUWQUXBWVGUWQUXBUXKUXJEUWQUXBUXKUXJEUNUWQUXJ + UXBUXKUMZEUXIWVHEUNGLUWPUXDLUJZUXHWVHFEWVIUXFUXBUXGUXKUXDLUXAUHWAUXDLUWTU + HWAWBTWCYTUWKUWMUWNXTUWLUWO $. $} @@ -153725,18 +153725,18 @@ computer programs (as last() or lastChar()), the terminology used for -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! x e. X W = ( x prefix ( # ` W ) ) ) ) $= ( vy vu cv wcel chash cfv co wceq wa wral cs1 cconcat cpfx weq cword wreu - c1 caddc wi eleq1w fveqeq2 anbi12d cbvralv wrex s1eq oveq2d eleq1d reu8nf - nfel2 nfv nfral nfan nfreu wb simprl simpl anim1i simplrr reuccatpfxs1lem - ad2antrr simp-4r syl3anc oveq1 s1cl anim12i pfxccat1 syl sylan9eqr eqcomd - ex impbid ralrimiva reu6i syl2anc exp31 rexlimd syl5bi sylan2b ) AIZCUAZJ - ZWEKLDKLZUCUDMZNZOZAEPDWFJZGIZWFJZWMKLWINZOZGEPZDBIZQZRMZEJZBCUBZDWEWHSMZ - NZAEUBZUEWKWPAGEAGTWGWNWJWOAGWFUFWEWMWIKUGUHUIXBXADHIZQZRMZEJZBHTUEHCPZOZ - BCUJWLWQOZXEXAXIDWEQZRMZEJBHACBXHEFUOBXNEFUOBATZWTXNEXOWSXMDRWRWEUKULUMAH - TZXNXHEXPXMXGDRWEXFUKULUMUNXLXKXEBCWLWQBWLBUPWPBGEFWPBUPUQURXDBAEFXDBUPUS - XLWRCJZXKXEXLXQOZXKOZXAXDWEWTNZUTZAEPXEXRXAXJVAXSYAAEXSWEEJZOZXDXTYCWLYBO - XJWQXDXTUEXSWLYBXLWLXQXKWLWQVBZVFVCXRXAXJYBVDWLWQXQXKYBVGGWRWECDEHVEVHYCX - TXDYCXTOXCDXTYCXCWTWHSMZDWEWTWHSVIYCWLWSWFJZOZYEDNXRYGXKYBXLWLXQYFYDWRCVJ - VKVFCDWSVLVMVNVOVPVQVRXDAEWTVSVTWAWBWCWD $. + c1 caddc wi eleq1w fveqeq2 anbi12d cbvralvw wrex nfel2 s1eq oveq2d eleq1d + reu8nf nfralw nfan nfreuw wb simprl simpl ad2antrr anim1i simplrr simp-4r + nfv reuccatpfxs1lem syl3anc s1cl anim12i pfxccat1 syl sylan9eqr eqcomd ex + oveq1 impbid ralrimiva reu6i syl2anc exp31 rexlimd syl5bi sylan2b ) AIZCU + AZJZWEKLDKLZUCUDMZNZOZAEPDWFJZGIZWFJZWMKLWINZOZGEPZDBIZQZRMZEJZBCUBZDWEWH + SMZNZAEUBZUEWKWPAGEAGTWGWNWJWOAGWFUFWEWMWIKUGUHUIXBXADHIZQZRMZEJZBHTUEHCP + ZOZBCUJWLWQOZXEXAXIDWEQZRMZEJBHACBXHEFUKBXNEFUKBATZWTXNEXOWSXMDRWRWEULUMU + NAHTZXNXHEXPXMXGDRWEXFULUMUNUOXLXKXEBCWLWQBWLBVFWPBGEFWPBVFUPUQXDBAEFXDBV + FURXLWRCJZXKXEXLXQOZXKOZXAXDWEWTNZUSZAEPXEXRXAXJUTXSYAAEXSWEEJZOZXDXTYCWL + YBOXJWQXDXTUEXSWLYBXLWLXQXKWLWQVAZVBVCXRXAXJYBVDWLWQXQXKYBVEGWRWECDEHVGVH + YCXTXDYCXTOXCDXTYCXCWTWHSMZDWEWTWHSVPYCWLWSWFJZOZYEDNXRYGXKYBXLWLXQYFYDWR + CVIVJVBCDWSVKVLVMVNVOVQVRXDAEWTVSVTWAWBWCWD $. $} ${ @@ -156446,8 +156446,8 @@ the symbol at any position is repeated at multiples of L (modulo the fveq1 fvmpt eqeqan12d cword chash cpr w3a fveqeq2 eqeq1d eleq1d 3anbi123d preq12d elrab2 co simpr1 eqcomd sylan9eq adantr simpr2 simpr wb fzo0to2pr cfzo oveq2 syl6eq raleqdv c0ex 1ex fveq2 eqeq12d syl6bb 3ad2ant1 ad3antlr - ralpr mpbir2and eqwrd ad2ant2r ex syl2anb sylbid rgen2a dff13 mpbir2an ) - CEGUCCEGUDMUEZGNZUAUEZGNZOZMUAUFZUGZUACUHMCUHABCDEFGHIJKLUIWTMUACWNCPZWPC + ralpr mpbir2and eqwrd ad2ant2r ex syl2anb sylbid rgen2 dff13 mpbir2an ) C + EGUCCEGUDMUEZGNZUAUEZGNZOZMUAUFZUGZUACUHMCUHABCDEFGHIJKLUIWTMUACCWNCPZWPC PZQWRRWNNZRWPNZOZWSXAXBWOXCWQXDBWNRBUEZNZXCCGRXFWNUKLRWNUJULBWPXGXDCGRXFW PUKLRWPUJULUMXAWNHUNZPZWNUONZSOZTWNNZDOZXLXCUPZIPZUQZQZWPXHPZWPUONZSOZTWP NZDOZYAXDUPZIPZUQZQZXEWSUGXBAUEZUONSOZTYGNZDOZYIRYGNZUPZIPZUQZXPAWNXHCAMU @@ -160665,17 +160665,17 @@ reflection about the origin (under the map ` x |-> -u x ` ). (Contributed ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) ) ) $= ( vx vy cr cv cle wbr wa wi wral wrex simpl imim2i breq1 imbi1d wcel ifcl - wss ralimi reximi simpr jca weq ralbidv cbvrexv anbi12i reeanv bitr4i cif - ancoms adantl r19.26 anim12 simplrl simplrr sselda maxle syl3anc ralimdva - wb syl5ibr syl5bir rspceaimv syl6an rexlimdvva syl5bi impbid2 ) CHUBZDIZE - IZJKZABLZMZECNZDHOZVOAMZECNZDHOZVOBMZECNZDHOZLZVSWBWEVRWADHVQVTECVPAVOABP - QUCUDVRWDDHVQWCECVPBVOABUEQUCUDUFWFFIZVNJKZAMZECNZGIZVNJKZBMZECNZLZGHOFHO - ZVLVSWFWJFHOZWNGHOZLWPWBWQWEWRWAWJDFHDFUGZVTWIECWSVOWHAVMWGVNJRSUHUIWDWND - GHDGUGZWCWMECWTVOWLBVMWKVNJRSUHUIUJWJWNFGHHUKULVLWOVSFGHHVLWGHTZWKHTZLZLZ - WGWKJKZWKWGUMZHTZWOXFVNJKZVPMZECNZVSXCXGVLXBXAXGXEWKWGHUAUNUOWOWIWMLZECNX - DXJWIWMECUPXDXKXIECXKXIXDVNCTZLZWHWLLZVPMWHAWLBUQXMXHXNVPXMXAXBVNHTXHXNVD - VLXAXBXLURVLXAXBXLUSXDCHVNVLXCPUTWGWKVNVAVBSVEVCVFVOXHVPDEXFHCVMXFVNJRVGV - HVIVJVK $. + wss ralimi reximi simpr jca ralbidv cbvrexvw anbi12i reeanv bitr4i ancoms + weq cif adantl r19.26 anim12 simplrl simplrr sselda maxle syl3anc syl5ibr + wb ralimdva syl5bir rspceaimv syl6an rexlimdvva syl5bi impbid2 ) CHUBZDIZ + EIZJKZABLZMZECNZDHOZVOAMZECNZDHOZVOBMZECNZDHOZLZVSWBWEVRWADHVQVTECVPAVOAB + PQUCUDVRWDDHVQWCECVPBVOABUEQUCUDUFWFFIZVNJKZAMZECNZGIZVNJKZBMZECNZLZGHOFH + OZVLVSWFWJFHOZWNGHOZLWPWBWQWEWRWAWJDFHDFUMZVTWIECWSVOWHAVMWGVNJRSUGUHWDWN + DGHDGUMZWCWMECWTVOWLBVMWKVNJRSUGUHUIWJWNFGHHUJUKVLWOVSFGHHVLWGHTZWKHTZLZL + ZWGWKJKZWKWGUNZHTZWOXFVNJKZVPMZECNZVSXCXGVLXBXAXGXEWKWGHUAULUOWOWIWMLZECN + XDXJWIWMECUPXDXKXIECXKXIXDVNCTZLZWHWLLZVPMWHAWLBUQXMXHXNVPXMXAXBVNHTXHXNV + DVLXAXBXLURVLXAXBXLUSXDCHVNVLXCPUTWGWKVNVAVBSVCVEVFVOXHVPDEXFHCVMXFVNJRVG + VHVIVJVK $. $} ${ @@ -160756,17 +160756,17 @@ reflection about the origin (under the map ` x |-> -u x ` ). (Contributed exp4a jca cfl c1 caddc co cif simpl flcl peano2zd zre reflcl peano2re syl ifcld max1 eluz2 syl3anbrc syl6eleqr impexp sseqtrrdi sselda simplr simpr wss uzss zred fllep1 max2 letrd eluzle syl5bir wceq raleqdv rspcev syl6an - ex fveq2 rexlimdva cbvrexv syl6ib impbid2 ) DHIZACBJZKLZMZBENZWQCJZOPZAQZ - CEMZBRNZWSXDBERWQEIZWSSWQRIZXDXFXGWSXGWQDKLZEDWQUAFUBUCXFWSXDXFAXCCWREXFX - AWRIZAQXAEIZXBAXFXJXBSZXIAXFXJXBXIXFXJSXIXBXFWQHIZXAHIZXIXBUDXJXLWQXHEDWQ - UEFUBXMXAXHEDXAUEFUBWQXAUFUGUHUIUJUNUKULUOUMWPXEACGJZKLZMZGENZWTWPXDXQBRW - PXGSZDWQUPLZUQURUSZOPZXTDUTZEIXDACYBKLZMZXQXRYBXHEXRWPYBHIZDYBOPZYBXHIZWP - XGVAZXRYAXTDHXRXSXGXSHIWPWQVBTVCYHVHZWPDRIZXTRIZYFXGDVDZXGXSRIYKWQVEXSVFV - GZDXTVIUGDYBVJVKZFVLXRXCACEYCXJXCQXKAQXRXAYCIZAQXJXBAVMXRYOXKAXRYOXKXRYOS - ZXJXBXRYCEXAXRYCXHEXRYGYCXHVRYNDYBVSVGFVNVOYPWQYBXAWPXGYOVPYPYBXRYEYOYIUC - VTYOXARIXRYBXAUATXRWQYBOPYOXRWQXTYBWPXGVQXGYKWPYMTXRYBYIVTXGWQXTOPWPWQWAT - WPYJYKXTYBOPXGYLYMDXTWBUGWCUCYOYBXAOPXRYBXAWDTWCUOWJUJWEUKXPYDGYBEXNYBWFA - CXOYCXNYBKWKWGWHWIWLXPWSGBEXNWQWFACXOWRXNWQKWKWGWMWNWO $. + ex fveq2 rexlimdva cbvrexvw syl6ib impbid2 ) DHIZACBJZKLZMZBENZWQCJZOPZAQ + ZCEMZBRNZWSXDBERWQEIZWSSWQRIZXDXFXGWSXGWQDKLZEDWQUAFUBUCXFWSXDXFAXCCWREXF + XAWRIZAQXAEIZXBAXFXJXBSZXIAXFXJXBXIXFXJSXIXBXFWQHIZXAHIZXIXBUDXJXLWQXHEDW + QUEFUBXMXAXHEDXAUEFUBWQXAUFUGUHUIUJUNUKULUOUMWPXEACGJZKLZMZGENZWTWPXDXQBR + WPXGSZDWQUPLZUQURUSZOPZXTDUTZEIXDACYBKLZMZXQXRYBXHEXRWPYBHIZDYBOPZYBXHIZW + PXGVAZXRYAXTDHXRXSXGXSHIWPWQVBTVCYHVHZWPDRIZXTRIZYFXGDVDZXGXSRIYKWQVEXSVF + VGZDXTVIUGDYBVJVKZFVLXRXCACEYCXJXCQXKAQXRXAYCIZAQXJXBAVMXRYOXKAXRYOXKXRYO + SZXJXBXRYCEXAXRYCXHEXRYGYCXHVRYNDYBVSVGFVNVOYPWQYBXAWPXGYOVPYPYBXRYEYOYIU + CVTYOXARIXRYBXAUATXRWQYBOPYOXRWQXTYBWPXGVQXGYKWPYMTXRYBYIVTXGWQXTOPWPWQWA + TWPYJYKXTYBOPXGYLYMDXTWBUGWCUCYOYBXAOPXRYBXAWDTWCUOWJUJWEUKXPYDGYBEXNYBWF + ACXOYCXNYBKWKWGWHWIWLXPWSGBEXNWQWFACXOWRXNWQKWKWGWMWNWO $. $} ${ @@ -160779,13 +160779,13 @@ reflection about the origin (under the map ` x |-> -u x ` ). (Contributed ( vn cr wss wcel wa cv cle wbr wi wral cpnf wrex simpr simplr wb cico cxr pnfxr icossre sylancl ssrexv syl cif ifcld max1 adantll elicopnf ad2antlr co mpbir2and simpllr simpll sselda maxle syl6bi imim1d ralimdva rspceaimv - syl3anc breq1 syl6an rexlimdva weq imbi1d ralbidv cbvrexv syl6ib impbid ) - BGHZCGIZJZDKZEKZLMZANZEBOZDCPUAUNZQZWADGQZVPWBGHZWCWDNVPVOPUBIWEVNVORUCCP - UDUEWADWBGUFUGVPWDFKZVRLMZANZEBOZFWBQZWCVPWAWJDGVPVQGIZJZCVQLMZVQCUHZWBIZ - WAWNVRLMZANZEBOWJWLWOWNGIZCWNLMZWLWMVQCGVPWKRVNVOWKSUIVOWKWSVNCVQUJUKVOWO - WRWSJTVNWKCWNULUMUOWLVTWQEBWLVRBIZJZWPVSAXAWPCVRLMZVSJZVSXAVOWKVRGIWPXCTV - NVOWKWTUPVPWKWTSWLBGVRVNVOWKUQURCVQVRUSVDXBVSRUTVAVBWGWPAFEWNWBBWFWNVRLVE - VCVFVGWIWAFDWBFDVHZWHVTEBXDWGVSAWFVQVRLVEVIVJVKVLVM $. + syl3anc breq1 syl6an rexlimdva weq imbi1d ralbidv cbvrexvw syl6ib impbid + ) BGHZCGIZJZDKZEKZLMZANZEBOZDCPUAUNZQZWADGQZVPWBGHZWCWDNVPVOPUBIWEVNVORUC + CPUDUEWADWBGUFUGVPWDFKZVRLMZANZEBOZFWBQZWCVPWAWJDGVPVQGIZJZCVQLMZVQCUHZWB + IZWAWNVRLMZANZEBOWJWLWOWNGIZCWNLMZWLWMVQCGVPWKRVNVOWKSUIVOWKWSVNCVQUJUKVO + WOWRWSJTVNWKCWNULUMUOWLVTWQEBWLVRBIZJZWPVSAXAWPCVRLMZVSJZVSXAVOWKVRGIWPXC + TVNVOWKWTUPVPWKWTSWLBGVRVNVOWKUQURCVQVRUSVDXBVSRUTVAVBWGWPAFEWNWBBWFWNVRL + VEVCVFVGWIWAFDWBFDVHZWHVTEBXDWGVSAWFVQVRLVEVIVJVKVLVM $. $} ${ @@ -160809,39 +160809,39 @@ reflection about the origin (under the map ` x |-> -u x ` ). (Contributed ( G ` ( ( F ` k ) D ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ta /\ A. m e. ( ZZ>= ` k ) ( G ` ( ( F ` k ) D ( F ` m ) ) ) < x ) ) ) $= - ( vz cv cfv co clt wbr wa cuz wral wrex crp weq anbi2d rexralbidv cbvralv - breq2 wcel c2 cdiv wi rphalfcl rspcv syl adantl ralimi r19.26 wb fvoveq1d - wceq fveq2 breq1d anbi12d biimpi a1i syl5bir expdimp cz sseli uzid rspcva - sylan adantll jctild simplll simplrr simplrl syl3anc cr simpllr syl122anc - simpr rpred sylbid expd impr anassrs expimpd ralimdv expr wss uzss ssralv - an32s sylan9 ralimdva ex com23 adantr mpdd sylan2 imdistanda 3imtr4g syld - reximdva ralrimdva syl5bi raleqbidv oveq2d fveq2d anim2i w3a 3expia ralbi - ad2antlr sylc syl5bb sylibd impbid ) AEIUBZKUCZHUBZKUCZGUDLUCZFUBZUEUFZUG - ZIYKUHUCZUIZHMUJZFUKUIZEYJJUBZKUCZGUDLUCZYNUEUFZJYIUHUCZUIZUGIYQUIZHMUJZF - UKUIZYTEYMUAUBZUEUFZUGZIYQUIHMUJZUAUKUIZAUUIYSUUMFUAUKFUAULZYPUULHIMYQUUO - YOUUKEYNUUJYMUEUPUMUNUOAUUNUUHFUKAYNUKUQZUGZUUNEYMYNURUSUDZUEUFZUGZIYQUIZ - HMUJZUUHUUPUUNUVBUTZAUUPUURUKUQUVCYNVAUUMUVBUAUURUKUUJUURVIZUULUUTHIMYQUV - DUUKUUSEUUJUURYMUEUPUMUNVBVCVDUUQUVAUUGHMUUQYKMUQZUGZEIYQUIZUUSIYQUIZUGUV - GUUFIYQUIZUGZUVAUUGUVFUVGUVHUVIUVGUVFBIYQUIZUVHUVIUTEBIYQOVEZUVFUVKUGZUVH - CDUUBYLGUDLUCZUURUEUFZUGZJYQUIZUGZUVIUVMUVHUVQCUVFUVKUVHUVQUVKUVHUGZBUUSU - GZIYQUIZUVFUVQBUUSIYQVFZUWAUVQUTUVFUWAUVQUVTUVPIJYQIJULZBDUUSUVOUWCYJUUBV - IBDVGYIUUAKVJZQVCUWCYMUVNUURUEUWCYJUUBYLLGUWDVHVKVLUOVMVNVOVPUVEUVKCUUQUV - EYKYQUQZUVKCUVEYKVQUQUWEMVQYKNVRYKVSVCZBCIYKYQIHULZYJYLVIBCVGYIYKKVJZPVCV - TZWAWBWCUVFUVKUVHUVRUVIUTZUVSUWAUVFUWJUWBUUQUWAUWJUTUVEUUQUVRUWAUVIUUQUVR - UWAUVIUTUUQUVRUGZUVTUUFIYQUWKYIYQUQZUGBUUSUUFUWKBUWLUUSUUFUTUWKBUGUUSUUDJ - YQUIZUWLUUFUWKBUUSUWMUUQUVTUVRUWMUUQUVTUGZCUVQUWMUWNCUGZUVPUUDJYQUWODUVOU - UDUWNCDUVOUUDUTZUUQCDUGZUVTUWPUUQUWQUGZBUUSUWPUWRBUGZUUSUVOUUDUWSUUSUVOUG - UUSYLUUBGUDZLUCZUURUEUFZUGZUUDUWSUVOUXBUUSUWSUVNUXAUURUEUWSADCUVNUXAVIAUU - PUWQBWDZUUQCDBWEZUUQCDBWFZSWGVKUMUWSABDCYNWHUQUXCUUDUTUXDUWRBWKUXEUXFUWSY - NAUUPUWQBWIWLTWJWMWNWOXCWPWQWRWOXCWSUWLUUEYQWTUWMUUFUTYKYIXAUUDJUUEYQXBVC - XDXCWQXEXFXGXHVOVPXIXJXKEUUSIYQVFEUUFIYQVFZXLXNXMXOXPAUUHYSFUKAUUGYRHMAUV - EUGUVJUVGYOIYQUIZUGZUUGYRUVEAUWEUVJUXIUTUWFAUWEUGZUVGUVIUXHUVGUXJUVKUVIUX - HUTUVLUXJUVKUGZUVIUXAYNUEUFZJYQUIZUXHUWEUVIUXMUTAUVKUUFUXMIYKYQUWGUUDUXLJ - UUEYQYIYKUHVJUWGUUCUXAYNUEUWGYJYLUUBLGUWHVHVKXQVBYDUXMYLYJGUDZLUCZYNUEUFZ - IYQUIZUXKUXHUXLUXPJIYQJIULZUXAUXOYNUEUXRUWTUXNLUXRUUBYJYLGUUAYIKVJXRXSVKU - OUXKUXPYOVGZIYQUIZUXQUXHVGUXKACUGZUVKUXTAUWEUVKUYAUWEUVKUGCAUWIXTWPUXJUVK - WKUYABUXSIYQACBUXSACBYAUXOYMYNUERVKYBWRYEUXPYOIYQYCVCYFYGXJXKXJUXGEYOIYQV - FXLXNWRYH $. + ( vz cv cfv co clt wbr wa cuz wral wrex crp weq breq2 rexralbidv cbvralvw + anbi2d wcel c2 cdiv wi rphalfcl wceq rspcv syl adantl ralimi r19.26 fveq2 + wb fvoveq1d breq1d anbi12d biimpi a1i syl5bir expdimp cz sseli uzid sylan + rspcva adantll jctild simplll simplrr simplrl syl3anc simpr simpllr rpred + cr syl122anc sylbid expd impr an32s anassrs expimpd ralimdv expr wss uzss + ssralv sylan9 ralimdva ex com23 adantr sylan2 imdistanda 3imtr4g reximdva + mpdd syld ralrimdva syl5bi raleqbidv ad2antlr oveq2d fveq2d anim2i 3expia + w3a sylc ralbi syl5bb sylibd impbid ) AEIUBZKUCZHUBZKUCZGUDLUCZFUBZUEUFZU + GZIYKUHUCZUIZHMUJZFUKUIZEYJJUBZKUCZGUDLUCZYNUEUFZJYIUHUCZUIZUGIYQUIZHMUJZ + FUKUIZYTEYMUAUBZUEUFZUGZIYQUIHMUJZUAUKUIZAUUIYSUUMFUAUKFUAULZYPUULHIMYQUU + OYOUUKEYNUUJYMUEUMUPUNUOAUUNUUHFUKAYNUKUQZUGZUUNEYMYNURUSUDZUEUFZUGZIYQUI + ZHMUJZUUHUUPUUNUVBUTZAUUPUURUKUQUVCYNVAUUMUVBUAUURUKUUJUURVBZUULUUTHIMYQU + VDUUKUUSEUUJUURYMUEUMUPUNVCVDVEUUQUVAUUGHMUUQYKMUQZUGZEIYQUIZUUSIYQUIZUGU + VGUUFIYQUIZUGZUVAUUGUVFUVGUVHUVIUVGUVFBIYQUIZUVHUVIUTEBIYQOVFZUVFUVKUGZUV + HCDUUBYLGUDLUCZUURUEUFZUGZJYQUIZUGZUVIUVMUVHUVQCUVFUVKUVHUVQUVKUVHUGZBUUS + UGZIYQUIZUVFUVQBUUSIYQVGZUWAUVQUTUVFUWAUVQUVTUVPIJYQIJULZBDUUSUVOUWCYJUUB + VBBDVIYIUUAKVHZQVDUWCYMUVNUURUEUWCYJUUBYLLGUWDVJVKVLUOVMVNVOVPUVEUVKCUUQU + VEYKYQUQZUVKCUVEYKVQUQUWEMVQYKNVRYKVSVDZBCIYKYQIHULZYJYLVBBCVIYIYKKVHZPVD + WAZVTWBWCUVFUVKUVHUVRUVIUTZUVSUWAUVFUWJUWBUUQUWAUWJUTUVEUUQUVRUWAUVIUUQUV + RUWAUVIUTUUQUVRUGZUVTUUFIYQUWKYIYQUQZUGBUUSUUFUWKBUWLUUSUUFUTUWKBUGUUSUUD + JYQUIZUWLUUFUWKBUUSUWMUUQUVTUVRUWMUUQUVTUGZCUVQUWMUWNCUGZUVPUUDJYQUWODUVO + UUDUWNCDUVOUUDUTZUUQCDUGZUVTUWPUUQUWQUGZBUUSUWPUWRBUGZUUSUVOUUDUWSUUSUVOU + GUUSYLUUBGUDZLUCZUURUEUFZUGZUUDUWSUVOUXBUUSUWSUVNUXAUURUEUWSADCUVNUXAVBAU + UPUWQBWDZUUQCDBWEZUUQCDBWFZSWGVKUPUWSABDCYNWKUQUXCUUDUTUXDUWRBWHUXEUXFUWS + YNAUUPUWQBWIWJTWLWMWNWOWPWQWRWSWOWPWTUWLUUEYQXAUWMUUFUTYKYIXBUUDJUUEYQXCV + DXDWPWRXEXFXGXHVOVPXMXIXJEUUSIYQVGEUUFIYQVGZXKXLXNXOXPAUUHYSFUKAUUGYRHMAU + VEUGUVJUVGYOIYQUIZUGZUUGYRUVEAUWEUVJUXIUTUWFAUWEUGZUVGUVIUXHUVGUXJUVKUVIU + XHUTUVLUXJUVKUGZUVIUXAYNUEUFZJYQUIZUXHUWEUVIUXMUTAUVKUUFUXMIYKYQUWGUUDUXL + JUUEYQYIYKUHVHUWGUUCUXAYNUEUWGYJYLUUBLGUWHVJVKXQVCXRUXMYLYJGUDZLUCZYNUEUF + ZIYQUIZUXKUXHUXLUXPJIYQJIULZUXAUXOYNUEUXRUWTUXNLUXRUUBYJYLGUUAYIKVHXSXTVK + UOUXKUXPYOVIZIYQUIZUXQUXHVIUXKACUGZUVKUXTAUWEUVKUYAUWEUVKUGCAUWIYAWQUXJUV + KWHUYABUXSIYQACBUXSACBYCUXOYMYNUERVKYBWSYDUXPYOIYQYEVDYFYGXIXJXIUXGEYOIYQ + VGXKXLWSYH $. $} ${ @@ -162285,14 +162285,14 @@ Superior limit (lim sup) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) $= ( vw wbr cc wcel cfv cmin cabs clt wral nfcv cmpt crli cv cle co wrex crp wi cr wa eqid fmpt sylib eqidd rlim biantrurd nfv nffvmpt1 nfov nffv nfbr - wf nfim breq2 imbrov2fvoveq cbvral fvmpt2 fvoveq1d breq1d imbi2d ralimiaa - wb ralbi 3syl syl5bb rexbidv ralbidv 3bitr2d ) ADEFUAZGUBLGMNZCUCZKUCZUDL - ZWBVSOZGPUEZQOZBUCZRLZUHZKESZCUIUFZBUGSZUJWLWADUCZUDLZFGPUEQOZWGRLZUHZDES - ZCUIUFZBUGSABCKEWDGVSAFMNZDESZEMVSVBHDEMFVSVSUKZULUMIAWBENUJWDUNUOAVTWLJU - PAWKWSBUGAWJWRCUIWJWNWMVSOZGPUEQOZWGRLZUHZDESZAWRWIXFKDEWCWHDWCDUQDWFWGRD - WEQDQTDWDGPDEFWBURDPTDGTUSUTDRTDWGTVAVCXFKUQWCWNWGRPQVSGWBWMWBWMWAUDVDVEV - FAXAXFWQVLZDESXGWRVLHWTXHDEWMENWTUJZXEWPWNXIXDWOWGRXIXCFGQPDEFMVSXBVGVHVI - VJVKXFWQDEVMVNVOVPVQVR $. + wf nfim breq2 imbrov2fvoveq cbvralw fvmpt2 fvoveq1d breq1d ralimiaa ralbi + wb imbi2d 3syl syl5bb rexbidv ralbidv 3bitr2d ) ADEFUAZGUBLGMNZCUCZKUCZUD + LZWBVSOZGPUEZQOZBUCZRLZUHZKESZCUIUFZBUGSZUJWLWADUCZUDLZFGPUEQOZWGRLZUHZDE + SZCUIUFZBUGSABCKEWDGVSAFMNZDESZEMVSVBHDEMFVSVSUKZULUMIAWBENUJWDUNUOAVTWLJ + UPAWKWSBUGAWJWRCUIWJWNWMVSOZGPUEQOZWGRLZUHZDESZAWRWIXFKDEWCWHDWCDUQDWFWGR + DWEQDQTDWDGPDEFWBURDPTDGTUSUTDRTDWGTVAVCXFKUQWCWNWGRPQVSGWBWMWBWMWAUDVDVE + VFAXAXFWQVLZDESXGWRVLHWTXHDEWMENWTUJZXEWPWNXIXDWOWGRXIXCFGQPDEFMVSXBVGVHV + IVMVJXFWQDEVKVNVOVPVQVR $. $( Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.) $) @@ -162591,13 +162591,13 @@ Superior limit (lim sup) ello1mpt $p |- ( ph -> ( ( x e. A |-> B ) e. <_O(1) <-> E. y e. RR E. m e. RR A. x e. A ( y <_ x -> B <_ m ) ) ) $= ( vz wcel cv cle wbr cfv wi wral cr wrex syl2anc nfv cmpt clo1 wss fmpttd - wf wb ello12 nffvmpt1 nfcv nfbr nfim breq2 fveq2 breq1d imbi12d cbvral wa - wceq simpr eqid fvmpt2 imbi2d ralbidva syl5bb 2rexbidv bitrd ) ABDEUAZUBJ - ZCKZIKZLMZVJVGNZFKZLMZOZIDPZFQRCQRZVIBKZLMZEVMLMZOZBDPZFQRCQRADQVGUEDQUCV - HVQUFABDEQHUDGCIDFVGUGSAVPWBCFQQVPVSVRVGNZVMLMZOZBDPAWBVOWEIBDVKVNBVKBTBV - LVMLBDEVJUHBLUIBVMUIUJUKWEITVJVRURZVKVSVNWDVJVRVILULWFVLWCVMLVJVRVGUMUNUO - UPAWEWABDAVRDJZUQZWDVTVSWHWCEVMLWHWGEQJWCEURAWGUSHBDEQVGVGUTVASUNVBVCVDVE - VF $. + wf ello12 nffvmpt1 nfcv nfbr nfim wceq breq2 fveq2 breq1d imbi12d cbvralw + wb wa simpr eqid fvmpt2 imbi2d ralbidva syl5bb 2rexbidv bitrd ) ABDEUAZUB + JZCKZIKZLMZVJVGNZFKZLMZOZIDPZFQRCQRZVIBKZLMZEVMLMZOZBDPZFQRCQRADQVGUEDQUC + VHVQUQABDEQHUDGCIDFVGUFSAVPWBCFQQVPVSVRVGNZVMLMZOZBDPAWBVOWEIBDVKVNBVKBTB + VLVMLBDEVJUGBLUHBVMUHUIUJWEITVJVRUKZVKVSVNWDVJVRVILULWFVLWCVMLVJVRVGUMUNU + OUPAWEWABDAVRDJZURZWDVTVSWHWCEVMLWHWGEQJWCEUKAWGUSHBDEQVGVGUTVASUNVBVCVDV + EVF $. ello1d.3 $e |- ( ph -> C e. RR ) $. $( Elementhood in the set of eventually upper bounded functions. @@ -163128,9 +163128,9 @@ Superior limit (lim sup) (Contributed by NM, 25-Dec-2005.) $) climeu $p |- ( F ~~> A -> E! x F ~~> x ) $= ( vy cli wbr cv wex wa weq wi wal weu wcel climcl breq2 spcegv mpcom nfv - cc climuni gen2 cbveu eu4 bitri sylanblrc ) CBEFZCDGZEFZDHZUICAGZEFZIDAJK - ZALDLZULAMZBTNUGUJBCOUIUGDBTUHBCEPQRUMDAUHUKCUAUBUOUIDMUJUNIULUIADULDSUIA - SUKUHCEPUCUIULDAUHUKCEPUDUEUF $. + cc climuni gen2 cbveuw eu4 bitri sylanblrc ) CBEFZCDGZEFZDHZUICAGZEFZIDAJ + KZALDLZULAMZBTNUGUJBCOUIUGDBTUHBCEPQRUMDAUHUKCUAUBUOUIDMUJUNIULUIADULDSUI + ASUKUHCEPUCUIULDAUHUKCEPUDUEUF $. $( An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.) $) @@ -163422,7 +163422,7 @@ Superior limit (lim sup) climmpt2 $p |- ( ph -> ( F ~~> A <-> ( n e. Z |-> ( F ` n ) ) ~~>r A ) ) $= ( vm cli wbr cv cfv wcel cc wral cmpt crli eqid climmpt syl2anc ralrimiva - cz weq fveq2 eleq1d cbvralv bitri sylib r19.21bi fmpttd rlimclim bitr4d + cz weq fveq2 eleq1d cbvralvw bitri sylib r19.21bi fmpttd rlimclim bitr4d wb ) AEBNOZDHDPZEQZUAZBNOZVBBUBOAFUGREGRUSVCURJKBDEVBFGHIVBUCUDUEABVBFHIJ ADHVASAVASRZDHACPZEQZSRZCHTZVDDHTZAVGCHLUFVHMPZEQZSRZMHTVIVGVLCMHCMUHVFVK SVEVJEUIUJUKVLVDMDHMDUHVKVASVJUTEUIUJUKULUMUNUOUPUQ $. @@ -163501,21 +163501,21 @@ seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 ) $= ( vr wcel cle wral cr cv wbr cmin co cabs cfv csb clt wi wrex ralrimiva wn wa adantr cc cdif crp cmpt crli rlimcl syl simpr eldifd nfcsb1v wceq nfel1 csbeq1a eleq1d rspc sylc rlimi ad2antrr rpred wss ad4ant14 sseldd - ad3antrrr subcld abscld nfcv nfral oveq2 fveq2d breq12d ralbidv fvoveq1 - nfbr breq2d rspcv lensymd imp nsyl nrexdv cxr csup cpnf cdm eqid dmmptd - id wb rlimss eqsstrrd ressxr syl6ss supxrunb1 mpbird r19.29 expcom mtod - r19.21bi condan ) AGHQZPUAZBUAZRUBZFGUCUDZUEUFZCGIUGZUHUBZUIZBESZPTUJAX - MULZUMZPBEFGXSHAFHQZBESYCAYEBEOUKUNYDGUOHUPZQZIUQQZCYFSZXSUQQZYDGUOHYDB - EFURZGUSUBZGUOQZAYLYCKUNZGYKUTVAZAYCVBVCZAYIYCAYHCYFMUKUNYHYJCGYFCXSUQC - GIVDZVFCUAZGVEZIXSUQCGIVGZVHVIVJZYNVKYDYBPTYDXNTQZUMZYBYAXPUMZBEUJZUUCU - UDBEUUCXOEQZUMZXTUUDUUGXSXRUUGXSYDYJUUBUUFUUAVLVMUUGXQUUGFGUUGHUOFAHUOV - NYCUUBUUFLVQAUUFYEYCUUBOVOZVPYDYMUUBUUFYOVLVRVSUUGYEXSDUAZGUCUDZUEUFZRU - BZDHSZXSXRRUBZUUHYDUUMUUBUUFYDYGIUUIYRUCUDZUEUFZRUBZDHSZCYFSZUUMYPAUUSY - CAUURCYFAYRYFQUMUUQDHNUKUKUNUURUUMCGYFUULCDHCHVTCXSUUKRYQCRVTCUUKVTWGWA - YSUUQUULDHYSIXSUUPUUKRYTYSUUOUUJUEYRGUUIUCWBWCWDWEVIVJVLUULUUNDFHUUIFVE - UUKXRXSRUUIFGUEUCWFWHWIVJWJYAXPXTYAWTWKWLWMUUCXPBEUJZYBUUEUIYDUUTPTAUUT - PTSZYCAUVAEWNUHWOWPVEZJAEWNVNUVAUVBXAAETWNAEYKWQZTABYKEFHYKWROWSAYLUVCT - VNKGYKXBVAXCXDXEPBEXFVAXGUNXKYBUUTUUEYAXPBEXHXIVAXJWMXL $. + ad3antrrr subcld abscld nfcv nfbr nfralw fveq2d breq12d ralbidv fvoveq1 + oveq2 breq2d rspcv lensymd id imp nsyl nrexdv cxr csup cpnf wb cdm eqid + dmmptd rlimss eqsstrrd ressxr syl6ss mpbird r19.21bi r19.29 expcom mtod + supxrunb1 condan ) AGHQZPUAZBUAZRUBZFGUCUDZUEUFZCGIUGZUHUBZUIZBESZPTUJA + XMULZUMZPBEFGXSHAFHQZBESYCAYEBEOUKUNYDGUOHUPZQZIUQQZCYFSZXSUQQZYDGUOHYD + BEFURZGUSUBZGUOQZAYLYCKUNZGYKUTVAZAYCVBVCZAYIYCAYHCYFMUKUNYHYJCGYFCXSUQ + CGIVDZVFCUAZGVEZIXSUQCGIVGZVHVIVJZYNVKYDYBPTYDXNTQZUMZYBYAXPUMZBEUJZUUC + UUDBEUUCXOEQZUMZXTUUDUUGXSXRUUGXSYDYJUUBUUFUUAVLVMUUGXQUUGFGUUGHUOFAHUO + VNYCUUBUUFLVQAUUFYEYCUUBOVOZVPYDYMUUBUUFYOVLVRVSUUGYEXSDUAZGUCUDZUEUFZR + UBZDHSZXSXRRUBZUUHYDUUMUUBUUFYDYGIUUIYRUCUDZUEUFZRUBZDHSZCYFSZUUMYPAUUS + YCAUURCYFAYRYFQUMUUQDHNUKUKUNUURUUMCGYFUULCDHCHVTCXSUUKRYQCRVTCUUKVTWAW + BYSUUQUULDHYSIXSUUPUUKRYTYSUUOUUJUEYRGUUIUCWGWCWDWEVIVJVLUULUUNDFHUUIFV + EUUKXRXSRUUIFGUEUCWFWHWIVJWJYAXPXTYAWKWLWMWNUUCXPBEUJZYBUUEUIYDUUTPTAUU + TPTSZYCAUVAEWOUHWPWQVEZJAEWOVNUVAUVBWRAETWOAEYKWSZTABYKEFHYKWTOXAAYLUVC + TVNKGYKXBVAXCXDXEPBEXKVAXFUNXGYBUUTUUEYAXPBEXHXIVAXJWNXL $. $} ${ @@ -163671,12 +163671,12 @@ seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 ) $= bounded function. (Contributed by Mario Carneiro, 12-May-2016.) $) o1compt $p |- ( ph -> ( F o. ( y e. B |-> C ) ) e. O(1) ) $= ( vz cv cr wcel cle wbr wi cmpt fmpttd wa cfv wral wrex nfv nfcv nffvmpt1 - nfbr nfim wceq breq2 fveq2 breq2d imbi12d cbvral simpr eqid fvmpt2 imbi2d - wb syl2anc ralbidva syl5bb rexbidv adantr mpbird o1co ) ABNDEGHCEFUAZIJAC - EFDKUBLAGOZPQZUCBOZNOZRSZVKVNVJUDZRSZTZNEUEZBPUFZVMCOZRSZVKFRSZTZCEUEZBPU - FZMAVTWFVBVLAVSWEBPVSWBVKWAVJUDZRSZTZCEUEAWEVRWINCEVOVQCVOCUGCVKVPRCVKUHC - RUHCEFVNUIUJUKWINUGVNWAULZVOWBVQWHVNWAVMRUMWJVPWGVKRVNWAVJUNUOUPUQAWIWDCE - AWAEQZUCZWHWCWBWLWGFVKRWLWKFDQWGFULAWKURKCEFDVJVJUSUTVCUOVAVDVEVFVGVHVI + wb nfbr nfim wceq breq2 fveq2 breq2d imbi12d cbvralw simpr fvmpt2 syl2anc + eqid imbi2d ralbidva syl5bb rexbidv adantr mpbird o1co ) ABNDEGHCEFUAZIJA + CEFDKUBLAGOZPQZUCBOZNOZRSZVKVNVJUDZRSZTZNEUEZBPUFZVMCOZRSZVKFRSZTZCEUEZBP + UFZMAVTWFUJVLAVSWEBPVSWBVKWAVJUDZRSZTZCEUEAWEVRWINCEVOVQCVOCUGCVKVPRCVKUH + CRUHCEFVNUIUKULWINUGVNWAUMZVOWBVQWHVNWAVMRUNWJVPWGVKRVNWAVJUOUPUQURAWIWDC + EAWAEQZUCZWHWCWBWLWGFVKRWLWKFDQWGFUMAWKUSKCEFDVJVJVBUTVAUPVCVDVEVFVGVHVI $. $} @@ -165415,44 +165415,44 @@ seq N ( + , F ) e. dom ~~> ) ) $= ( vm cle wbr cmin co cr wcel adantr vn cv cfv cabs wi wral clsp c3 cmul clt wa cxr caddc cmnf cvv wf wss reex ssex syl a1i fex2 limsupcl simprl syl3anc ffvelrnd rpred readdcld mnfxr resubcld rexrd mnfltd fss sylancl - ressxr csup cpnf wceq wrex sseldd breq2 imbrov2fvoveq cbvralv ffvelrnda - simprr sylib recnd abscld ltle syl2anc absdifled sylibd imim2d ralimdva - simpl syl6 breq1 rspceaimv limsupbnd2 xrltletrd adantrr simplrr rspcdva - mpd ltled simprd expr ralrimiva limsupbnd1 xrre syl22anc c2 2re remulcl - mpbid sylancr abssubd 2timesd oveq2d subsub4d eqtr4d lesubaddd lesub1dd - 3re mpbird eqbrtrd letrd leadd1dd addassd breqtrd mpbir2and crp ltmul1d - 2lt3 mpbii lelttrd sylibr jca imbi2d rexralbidv reximddv ) AEUBZFUBZNOZ - UUCGUCZUUBGUCZPQUDUCZDUJOZUEZFCUFZGUGUCZRSZUUDUUEUUKPQUDUCUHDUIQZUJOUEZ - FCUFZUKECAUUBCSZUUJUKZUKZUULUUOUURUUKULSZUUFDUMQZRSZUNUUKUJOUUKUUTNOZUU - LAUUSUUQAGUOSZUUSACRGUPZCUOSZRUOSZUVCIACRUQZUVEHCRURUSUTUVFAURVACRGUOUO - VBVEGUOVCUTTZUURUUFDUURCRUUBGAUVDUUQITZAUUPUUJVDZVFZADRSZUUQADLVGTZVHZU - URUNUUFDPQZUUKUNULSUURVIVAUURUVOUURUUFDUVKUVMVJZVKZUVHUURUVOUVPVLUURUVO - CMUAGAUVGUUQHTZACULGUPZUUQAUVDRULUQUVSIVOCRULGVMVNTZUVQACULUJVPVQVRUUQJ - TUURUUBRSZUUBMUBZNOZUVOUWBGUCZNOZUEZMCUFZUAUBZUWBNOZUWEUEMCUFUARVSUURCR - UUBUVRUVJVTZUURUWCUWDUUFPQZUDUCZDUJOZUEZMCUFZUWGUURUUJUWOAUUPUUJWEUUIUW - NFMCUUDUWCDUJPUDGUUFUUCUWBUUCUWBUUBNWAZWBZWCWFUURUWNUWFMCUURUWBCSZUKZUW - MUWEUWCUWSUWMUWEUWDUUTNOZUKZUWEUWSUWMUWLDNOZUXAUWSUWLRSZUVLUWMUXBUEUWSU - WKUWSUWKUWSUWDUUFUURCRUWBGUVIWDZUURUUFRSZUWRUVKTZVJWGWHZUURUVLUWRUVMTZU - WLDWIWJUWSUWDUUFDUXDUXFUXHWKWLUWEUWTWOZWPWMWNXDUWIUWCUWEUAMUUBRCUWHUUBU - WBNWQZWRWJWSZWTUURUUTCMUAGUVRUVTUURUUTUVNVKUURUWAUWCUWTUEZMCUFUWIUWTUEM - CUFUARVSUWJUURUXLMCUURUWRUWCUWTUURUWRUWCUKZUKZUWEUWTUXNUXBUXAUXNUWLDUUR - UWRUXCUWCUXGXAUURUVLUXMUVMTZUXNUWCUWMUURUWRUWCWEUXNUUIUWNFCUWBUWQAUUPUU - JUXMXBUURUWRUWCVDXCXDXEUXNUWDUUFDUURUWRUWDRSUWCUXDXAZUURUXEUXMUVKTZUXOW - KXOZXFZXGXHUWIUWCUWTUAMUUBRCUXJWRWJXIZUUKUUTXJXKZUURUWCUWDUUKPQZUDUCZUU - MUJOZUEZMCUFUUOUURUYEMCUURUWRUWCUYDUXNUYCXLDUIQZUUMUXNUYBUXNUYBUXNUWDUU - KUXPUURUULUXMUYATZVJWGWHUXNXLRSZUVLUYFRSXMUXOXLDXNXPZUXNUHRSZUVLUUMRSYD - UXOUHDXNXPUXNUYCUUKUWDPQUDUCZUYFNUXNUWDUUKUXNUWDUXPWGZUXNUUKUYGWGXQUXNU - YKUYFNOUWDUYFPQZUUKNOUUKUWDUYFUMQZNOUXNUYMUVOUUKUXNUWDUYFUXPUYIVJUURUVO - RSUXMUVPTUYGUXNUYMUWDDPQZDPQZUVONUXNUYMUWDDDUMQZPQUYPUXNUYFUYQUWDPUXNDU - XNDUXOWGZXRZXSUXNUWDDDUYLUYRUYRXTYAUXNUYOUUFDUXNUWDDUXPUXOVJUXQUXOUXNUY - OUUFNOUWTUXSUXNUWDDUUFUXPUXOUXQYBYEYCYFUURUVOUUKNOUXMUXKTYGUXNUUKUUTUYN - UYGUURUVAUXMUVNTUXNUWDUYFUXPUYIVHUURUVBUXMUXTTUXNUUTUWDDUMQZDUMQZUYNNUX - NUUFUYTDUXQUXNUWDDUXPUXOVHUXOUXNUWEUUFUYTNOUXNUXAUWEUXRUXIUTUXNUUFDUWDU - XQUXOUXPYBXOYHUXNVUAUWDUYQUMQUYNUXNUWDDDUYLUYRUYRYIUXNUYFUYQUWDUMUYSXSY - AYJYGUXNUUKUWDUYFUYGUXPUYIWKYKYFUXNXLUHUJOUYFUUMUJOYNUXNXLUHDUYHUXNXMVA - UYJUXNYDVAUURDYLSZUXMAVUBUUQLTTYMYOYPXGXHUUNUYEFMCUUDUWCUUMUJPUDGUUKUUC - UWBUWPWBWCYQYRAUUDUUGBUBZUJOZUEZFCUFECVSUUJECVSBYLDVUCDVRZVUEUUIEFCCVUF - VUDUUHUUDVUCDUUGUJWAYSYTKLXCUUA $. + ressxr csup cpnf wceq sseldd simprr breq2 imbrov2fvoveq sylib ffvelrnda + wrex cbvralvw recnd abscld ltle syl2anc absdifled sylibd simpl ralimdva + imim2d mpd breq1 rspceaimv limsupbnd2 xrltletrd adantrr simplrr rspcdva + syl6 ltled mpbid simprd expr ralrimiva limsupbnd1 xrre syl22anc remulcl + 2re sylancr 3re abssubd 2timesd oveq2d subsub4d eqtr4d lesubaddd mpbird + c2 lesub1dd eqbrtrd leadd1dd addassd breqtrd mpbir2and 2lt3 crp ltmul1d + letrd mpbii lelttrd sylibr jca imbi2d rexralbidv reximddv ) AEUBZFUBZNO + ZUUCGUCZUUBGUCZPQUDUCZDUJOZUEZFCUFZGUGUCZRSZUUDUUEUUKPQUDUCUHDUIQZUJOUE + ZFCUFZUKECAUUBCSZUUJUKZUKZUULUUOUURUUKULSZUUFDUMQZRSZUNUUKUJOUUKUUTNOZU + ULAUUSUUQAGUOSZUUSACRGUPZCUOSZRUOSZUVCIACRUQZUVEHCRURUSUTUVFAURVACRGUOU + OVBVEGUOVCUTTZUURUUFDUURCRUUBGAUVDUUQITZAUUPUUJVDZVFZADRSZUUQADLVGTZVHZ + UURUNUUFDPQZUUKUNULSUURVIVAUURUVOUURUUFDUVKUVMVJZVKZUVHUURUVOUVPVLUURUV + OCMUAGAUVGUUQHTZACULGUPZUUQAUVDRULUQUVSIVOCRULGVMVNTZUVQACULUJVPVQVRUUQ + JTUURUUBRSZUUBMUBZNOZUVOUWBGUCZNOZUEZMCUFZUAUBZUWBNOZUWEUEMCUFUARWEUURC + RUUBUVRUVJVSZUURUWCUWDUUFPQZUDUCZDUJOZUEZMCUFZUWGUURUUJUWOAUUPUUJVTUUIU + WNFMCUUDUWCDUJPUDGUUFUUCUWBUUCUWBUUBNWAZWBZWFWCUURUWNUWFMCUURUWBCSZUKZU + WMUWEUWCUWSUWMUWEUWDUUTNOZUKZUWEUWSUWMUWLDNOZUXAUWSUWLRSZUVLUWMUXBUEUWS + UWKUWSUWKUWSUWDUUFUURCRUWBGUVIWDZUURUUFRSZUWRUVKTZVJWGWHZUURUVLUWRUVMTZ + UWLDWIWJUWSUWDUUFDUXDUXFUXHWKWLUWEUWTWMZXDWOWNWPUWIUWCUWEUAMUUBRCUWHUUB + UWBNWQZWRWJWSZWTUURUUTCMUAGUVRUVTUURUUTUVNVKUURUWAUWCUWTUEZMCUFUWIUWTUE + MCUFUARWEUWJUURUXLMCUURUWRUWCUWTUURUWRUWCUKZUKZUWEUWTUXNUXBUXAUXNUWLDUU + RUWRUXCUWCUXGXAUURUVLUXMUVMTZUXNUWCUWMUURUWRUWCVTUXNUUIUWNFCUWBUWQAUUPU + UJUXMXBUURUWRUWCVDXCWPXEUXNUWDUUFDUURUWRUWDRSUWCUXDXAZUURUXEUXMUVKTZUXO + WKXFZXGZXHXIUWIUWCUWTUAMUUBRCUXJWRWJXJZUUKUUTXKXLZUURUWCUWDUUKPQZUDUCZU + UMUJOZUEZMCUFUUOUURUYEMCUURUWRUWCUYDUXNUYCYDDUIQZUUMUXNUYBUXNUYBUXNUWDU + UKUXPUURUULUXMUYATZVJWGWHUXNYDRSZUVLUYFRSXNUXOYDDXMXOZUXNUHRSZUVLUUMRSX + PUXOUHDXMXOUXNUYCUUKUWDPQUDUCZUYFNUXNUWDUUKUXNUWDUXPWGZUXNUUKUYGWGXQUXN + UYKUYFNOUWDUYFPQZUUKNOUUKUWDUYFUMQZNOUXNUYMUVOUUKUXNUWDUYFUXPUYIVJUURUV + ORSUXMUVPTUYGUXNUYMUWDDPQZDPQZUVONUXNUYMUWDDDUMQZPQUYPUXNUYFUYQUWDPUXND + UXNDUXOWGZXRZXSUXNUWDDDUYLUYRUYRXTYAUXNUYOUUFDUXNUWDDUXPUXOVJUXQUXOUXNU + YOUUFNOUWTUXSUXNUWDDUUFUXPUXOUXQYBYCYEYFUURUVOUUKNOUXMUXKTYNUXNUUKUUTUY + NUYGUURUVAUXMUVNTUXNUWDUYFUXPUYIVHUURUVBUXMUXTTUXNUUTUWDDUMQZDUMQZUYNNU + XNUUFUYTDUXQUXNUWDDUXPUXOVHUXOUXNUWEUUFUYTNOUXNUXAUWEUXRUXIUTUXNUUFDUWD + UXQUXOUXPYBXFYGUXNVUAUWDUYQUMQUYNUXNUWDDDUYLUYRUYRYHUXNUYFUYQUWDUMUYSXS + YAYIYNUXNUUKUWDUYFUYGUXPUYIWKYJYFUXNYDUHUJOUYFUUMUJOYKUXNYDUHDUYHUXNXNV + AUYJUXNXPVAUURDYLSZUXMAVUBUUQLTTYMYOYPXHXIUUNUYEFMCUUDUWCUUMUJPUDGUUKUU + CUWBUWPWBWFYQYRAUUDUUGBUBZUJOZUEZFCUFECWEUUJECWEBYLDVUCDVRZVUEUUIEFCCVU + FVUDUUHUUDVUCDUUGUJWAYSYTKLXCUUA $. $} $( A Cauchy sequence of real numbers converges to its limit supremum. The @@ -165562,26 +165562,26 @@ seq N ( + , F ) e. dom ~~> ) ) $= ( vn vi vm cfv wcel cmin wa wral crp cv cr co cabs clt wbr cuz wrex cli cdm c0 wne c1 1rp ne0ii r19.2z sylancr ralimi cmpt clsp eqid simprr weq simpl fveq2 eleq1d rspccva fmpttd oveq2d fveq2d breq1d anbi2d raleqbidv - sylan cc cbvrexv fvoveq1d anbi12d cbvralv recn anim1i reximi syl adantr - sylbi cau4 ad2antrl mpbid simpr wceq uztrn2 fvex fvmpt oveq12d ralimdva - syl5ibr reximia caurcvg eluzelz eleq2s cbvmptv climmpt syl2anc releldmi - wb cz mpbird climrel expr syl5 rexlimdva rexlimdvw mpd ) ADUAZEOZUBPZXO - CUAZEOZQUCZUDOZBUAZUEUFZRZDXQUGOZSZCHUHZBTUHZEUIUJPZATUKULYFBTSZYGUMTUN - UOKYFBTUPUQAYFYHBTAYEYHCHYEXPDYDSZAXQHPZRYHYCXPDYDXPYBVDURAYKYJYHAYKYJR - ZRZELYDLUAZEOZUSZUTOZUIUFZYHYMYRYPYQUIUFZYMBMNYPXQYDYDVAZYMLYDYOUBYMYJY - NYDPYOUBPZAYKYJVBXPUUADYNYDDLVCXOYOUBXNYNEVEVFVGVNVHYMMUAZEOZVOPZUUCNUA - ZEOZQUCZUDOZYAUEUFZRZMUUEUGOZSZNYDUHZBTSZUUBYPOZUUEYPOZQUCZUDOZYAUEUFZM - UUKSZNYDUHZBTSYMUULNHUHZBTSZUUNAUVCYLAYIUVCKYFUVBBTYFXPXOUUFQUCZUDOZYAU - EUFZRZDUUKSZNHUHUVBYEUVHCNHCNVCZYCUVGDYDUUKXQUUEUGVEUVIYBUVFXPUVIXTUVEY - AUEUVIXSUVDUDUVIXRUUFXOQXQUUEEVEVIVJVKVLVMVPUVHUULNHUVHUUCUBPZUUIRZMUUK - SUULUVGUVKDMUUKDMVCZXPUVJUVFUUIUVLXOUUCUBXNUUBEVEZVFUVLUVEUUHYAUEUVLXOU - UCUUFUDQUVMVQVKVRVSUVKUUJMUUKUVJUUDUUIUUCVTWAURWEWBWEURWCWDYKUVCUUNXEAY - JBNMEFXQYDHIYTWFWGWHUUMUVABTUULUUTNYDUUEYDPZUUJUUSMUUKUUJUUSUVNUUBUUKPZ - RZUUIUUDUUIWIUVPUURUUHYAUEUVPUUQUUGUDUVPUUOUUCUUPUUFQUVPUUBYDPUUOUUCWJX - QUUBUUEYDYTWKLUUBYOUUCYDYPYNUUBEVEYPVAZUUBEWLWMWCUVNUUPUUFWJUVOLUUEYOUU - FYDYPYNUUEEVEUVQUUEEWLWMWDWNVJVKWPWOWQURWCWRYMXQXFPZEGPZYRYSXEYKUVRAYJU - VRXQFUGOHFXQWSIWTWGAUVSYLJWDYQDEYPXQGYDYTLDYDYOXOYNXNEVEXAXBXCXGEYQUIXH - XDWCXIXJXKXLXM $. + sylan cbvrexvw fvoveq1d anbi12d cbvralvw anim1i sylbi reximi syl adantr + cc recn wb cau4 ad2antrl mpbid simpr wceq uztrn2 fvmpt oveq12d ralimdva + fvex syl5ibr reximia caurcvg cz eluzelz cbvmptv climmpt syl2anc climrel + eleq2s mpbird releldmi expr syl5 rexlimdva rexlimdvw mpd ) ADUAZEOZUBPZ + XOCUAZEOZQUCZUDOZBUAZUEUFZRZDXQUGOZSZCHUHZBTUHZEUIUJPZATUKULYFBTSZYGUMT + UNUOKYFBTUPUQAYFYHBTAYEYHCHYEXPDYDSZAXQHPZRYHYCXPDYDXPYBVDURAYKYJYHAYKY + JRZRZELYDLUAZEOZUSZUTOZUIUFZYHYMYRYPYQUIUFZYMBMNYPXQYDYDVAZYMLYDYOUBYMY + JYNYDPYOUBPZAYKYJVBXPUUADYNYDDLVCXOYOUBXNYNEVEVFVGVNVHYMMUAZEOZWDPZUUCN + UAZEOZQUCZUDOZYAUEUFZRZMUUEUGOZSZNYDUHZBTSZUUBYPOZUUEYPOZQUCZUDOZYAUEUF + ZMUUKSZNYDUHZBTSYMUULNHUHZBTSZUUNAUVCYLAYIUVCKYFUVBBTYFXPXOUUFQUCZUDOZY + AUEUFZRZDUUKSZNHUHUVBYEUVHCNHCNVCZYCUVGDYDUUKXQUUEUGVEUVIYBUVFXPUVIXTUV + EYAUEUVIXSUVDUDUVIXRUUFXOQXQUUEEVEVIVJVKVLVMVOUVHUULNHUVHUUCUBPZUUIRZMU + UKSUULUVGUVKDMUUKDMVCZXPUVJUVFUUIUVLXOUUCUBXNUUBEVEZVFUVLUVEUUHYAUEUVLX + OUUCUUFUDQUVMVPVKVQVRUVKUUJMUUKUVJUUDUUIUUCWEVSURVTWAVTURWBWCYKUVCUUNWF + AYJBNMEFXQYDHIYTWGWHWIUUMUVABTUULUUTNYDUUEYDPZUUJUUSMUUKUUJUUSUVNUUBUUK + PZRZUUIUUDUUIWJUVPUURUUHYAUEUVPUUQUUGUDUVPUUOUUCUUPUUFQUVPUUBYDPUUOUUCW + KXQUUBUUEYDYTWLLUUBYOUUCYDYPYNUUBEVEYPVAZUUBEWPWMWBUVNUUPUUFWKUVOLUUEYO + UUFYDYPYNUUEEVEUVQUUEEWPWMWCWNVJVKWQWOWRURWBWSYMXQWTPZEGPZYRYSWFYKUVRAY + JUVRXQFUGOHFXQXAIXFWHAUVSYLJWCYQDEYPXQGYDYTLDYDYOXOYNXNEVEXBXCXDXGEYQUI + XEXHWBXIXJXKXLXM $. $} caucvg.2 $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) $. @@ -165622,26 +165622,26 @@ seq N ( + , F ) e. dom ~~> ) ) $= ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) ) $= ( vn vm vi wcel wa cv cfv cuz wral wrex clt crp vy cz cc cli cmin co cabs cdm wbr cop wex eldm2g ibi df-br c1 simpll eqidd simpr climi simpl ralimi - 1rp a1i reximi syl ex syl5bir exlimdv syl5 wi wb wceq weq raleqdv cbvrexv - fveq2 rspcdva eluzelz eleq2s climcau sylan r19.29uz ralimdv mpan9 adantll - an32s simplrr eleq1d rspccva fvoveq1d breq1d cbvralv adantl oveq2d fveq2d - eqid sylib raleqbidv breq2 rexralbidv syl5bb caucvg adantlll impbida cau4 - ad2antrl bitr4d rexlimdvaa pm5.21ndd ) EUBLZDFLZMZCNZDOZUCLZCINZPOZQZIGRZ - DUDUHZLZXOXNBNZDOZUEUFUGOZANZSUIZMZCYBPOZQZBGRZATQZYADJNZUJUDLZJUKZXLXSYA - YNJDUDXTULUMXLYMXSJYMDYLUDUIZXLXSDYLUDUNXLYOXSXLYOMZXOXNYLUEUFUGOUOSUIZMZ - CXQQZIGRXSYPYLXNUOICDEGHXJXKYOUPUOTLZYPVBVCYPXMGLMXNUQXLYOURUSYSXRIGYRXOC - XQXOYQUTVAVDVEVFVGVHVIYKXSVJXLYKXOCYHQZBGRZXSATUOUUBXSVKYEUOVLUUAXRBIGBIV - MXOCYHXQYBXPPVPVNVOVCYJUUBATYIUUABGYGXOCYHXOYFUTVAVDVAYTYKVBVCVQVCXLXRYAY - KVKIGXLXPGLZXRMZMZYAYIBXQRZATQZYKUUEYAUUGUUDYAUUGXLUUCYAXRUUGUUCYAMYFCYHQ - ZBXQRZATQZXRUUGUUCXPUBLZYAUUJUUKXPEPOGEXPVRHVSABCDXPXQXQWPZVTWAXRUUIUUFAT - XRUUIUUFXOYFBCXPXQUULWBVFWCWDWFWEXKUUDUUGYAXJXKUUDMZUUGMZUAKJDXPFXQUULUUN - XRYLXQLYLDOZUCLZXKUUCXRUUGWGXOUUPCYLXQCJVMZXNUUOUCXMYLDVPZWHWIWAUUNUUOYCU - EUFZUGOZYESUIZJYHQZBXQRZATQZUUOKNZDOZUEUFZUGOZUANZSUIZJUVEPOZQKXQRZUATQUU - GUVDUUMUUFUVCATYIUVBBXQYIUUHUVBYGYFCYHXOYFURVAYFUVACJYHUUQYDUUTYESUUQXNUU - OYCUGUEUURWJWKWLWQVDVAWMUVCUVLAUATUVCUVHYESUIZJUVKQZKXQRAUAVMZUVLUVBUVNBK - XQBKVMZUVAUVMJYHUVKYBUVEPVPUVPUUTUVHYESUVPUUSUVGUGUVPYCUVFUUOUEYBUVEDVPWN - WOWKWRVOUVOUVMUVJKJXQUVKYEUVIUVHSWSWTXAWLWQXKUUDUUGUPXBXCXDUUCYKUUGVKXLXR - ABCDEXPXQGHUULXEXFXGXHXI $. + 1rp a1i reximi syl ex syl5bir exlimdv syl5 wi wceq fveq2 raleqdv cbvrexvw + wb rspcdva eluzelz eleq2s eqid climcau sylan r19.29uz ralimdv mpan9 an32s + weq adantll simplrr eleq1d rspccva fvoveq1d breq1d cbvralvw adantl oveq2d + sylib fveq2d raleqbidv rexralbidv syl5bb caucvg adantlll impbida ad2antrl + breq2 cau4 bitr4d rexlimdvaa pm5.21ndd ) EUBLZDFLZMZCNZDOZUCLZCINZPOZQZIG + RZDUDUHZLZXOXNBNZDOZUEUFUGOZANZSUIZMZCYBPOZQZBGRZATQZYADJNZUJUDLZJUKZXLXS + YAYNJDUDXTULUMXLYMXSJYMDYLUDUIZXLXSDYLUDUNXLYOXSXLYOMZXOXNYLUEUFUGOUOSUIZ + MZCXQQZIGRXSYPYLXNUOICDEGHXJXKYOUPUOTLZYPVBVCYPXMGLMXNUQXLYOURUSYSXRIGYRX + OCXQXOYQUTVAVDVEVFVGVHVIYKXSVJXLYKXOCYHQZBGRZXSATUOUUBXSVOYEUOVKUUAXRBIGB + IWFXOCYHXQYBXPPVLVMVNVCYJUUBATYIUUABGYGXOCYHXOYFUTVAVDVAYTYKVBVCVPVCXLXRY + AYKVOIGXLXPGLZXRMZMZYAYIBXQRZATQZYKUUEYAUUGUUDYAUUGXLUUCYAXRUUGUUCYAMYFCY + HQZBXQRZATQZXRUUGUUCXPUBLZYAUUJUUKXPEPOGEXPVQHVRABCDXPXQXQVSZVTWAXRUUIUUF + ATXRUUIUUFXOYFBCXPXQUULWBVFWCWDWEWGXKUUDUUGYAXJXKUUDMZUUGMZUAKJDXPFXQUULU + UNXRYLXQLYLDOZUCLZXKUUCXRUUGWHXOUUPCYLXQCJWFZXNUUOUCXMYLDVLZWIWJWAUUNUUOY + CUEUFZUGOZYESUIZJYHQZBXQRZATQZUUOKNZDOZUEUFZUGOZUANZSUIZJUVEPOZQKXQRZUATQ + UUGUVDUUMUUFUVCATYIUVBBXQYIUUHUVBYGYFCYHXOYFURVAYFUVACJYHUUQYDUUTYESUUQXN + UUOYCUGUEUURWKWLWMWPVDVAWNUVCUVLAUATUVCUVHYESUIZJUVKQZKXQRAUAWFZUVLUVBUVN + BKXQBKWFZUVAUVMJYHUVKYBUVEPVLUVPUUTUVHYESUVPUUSUVGUGUVPYCUVFUUOUEYBUVEDVL + WOWQWLWRVNUVOUVMUVJKJXQUVKYEUVIUVHSXEWSWTWMWPXKUUDUUGUPXAXBXCUUCYKUUGVOXL + XRABCDEXPXQGHUULXFXDXGXHXI $. serf0.2 $e |- ( ph -> M e. ZZ ) $. serf0.3 $e |- ( ph -> F e. V ) $. @@ -165993,7 +165993,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ nfsum1 $p |- F/_ k sum_ k e. A B $= ( vm vn vx vf cv cfv caddc cz csb cc0 cmpt cseq cli c1 cn nfcv csu cuz wa wss wcel cif wbr wrex cfz co wf1o wceq wex wo cio nfss nfcri nfcsb1v nfif - df-sum nfmpt nfseq nfbr nfan nfrex nff1o nffv nfeq2 nfex nfiota nfcxfr + df-sum nfmpt nfseq nfbr nfan nfrex nff1o nffv nfeq2 nfex nfiotaw nfcxfr nfor ) CABCUAAEIZUBJZUDZKFLFIZAUEZCVPBMZNUFZOZVMPZGIZQUGZUCZELUHZRVMUIUJZ AHIZUKZWBVMKFSCVPWGJZBMZOZRPZJZULZUCZHUMZESUHZUNZGUOGABHCEFUTWRCGWEWQCWDC ELCLTZVOWCCCAVNDCVNTUPCWAWBQCKVTVMCVMTZCKTZCFLVSWSVQCVRNCFADUQCVPBURCNTUS @@ -166091,15 +166091,15 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ (Revised by Mario Carneiro, 13-Jun-2019.) $) cbvsum $p |- sum_ j e. A B = sum_ k e. A C $= ( vm vn vx vf cv caddc cz cn wceq wtru cuz cfv wss wcel csb cc0 cif cli - cmpt cseq wbr wa wrex c1 cfz co wf1o wex wo cio csu cbvcsb a1i mpteq2dv - ifeq1d seqeq3d mptru breq1i anbi2i rexbii fveq1i eqeq2i orbi12i iotabii - exbii df-sum 3eqtr4i ) AKOZUAUBUCZPLQLOZAUDZDVTBUEZUFUGZUIZVRUJZMOZUHUK - ZULZKQUMZUNVRUOUPANOZUQZWFVRPLRDVTWJUBZBUEZUIZUNUJZUBZSZULZNURZKRUMZUSZ - MUTVSPLQWAEVTCUEZUFUGZUIZVRUJZWFUHUKZULZKQUMZWKWFVRPLREWLCUEZUIZUNUJZUB - ZSZULZNURZKRUMZUSZMUTABDVAACEVAXAXQMWIXHWTXPWHXGKQWGXFVSWEXEWFUHWEXESTW - DXDPVRTLQWCXCTWAWBXBUFWBXBSTDEVTBCIJFVBVCVEVDVFVGVHVIVJWSXOKRWRXNNWQXMW - KWPXLWFVRWOXKWOXKSTWNXJPUNTLRWMXIWMXISTDEWLBCIJFVBVCVDVFVGVKVLVIVOVJVMV - NMABNDKLVPMACNEKLVPVQ $. + cmpt cseq wbr wa wrex c1 cfz co wf1o wex wo cio cbvcsbw ifeq1d mpteq2dv + csu a1i seqeq3d mptru breq1i anbi2i rexbii fveq1i exbii orbi12i iotabii + eqeq2i df-sum 3eqtr4i ) AKOZUAUBUCZPLQLOZAUDZDVTBUEZUFUGZUIZVRUJZMOZUHU + KZULZKQUMZUNVRUOUPANOZUQZWFVRPLRDVTWJUBZBUEZUIZUNUJZUBZSZULZNURZKRUMZUS + ZMUTVSPLQWAEVTCUEZUFUGZUIZVRUJZWFUHUKZULZKQUMZWKWFVRPLREWLCUEZUIZUNUJZU + BZSZULZNURZKRUMZUSZMUTABDVDACEVDXAXQMWIXHWTXPWHXGKQWGXFVSWEXEWFUHWEXEST + WDXDPVRTLQWCXCTWAWBXBUFWBXBSTDEVTBCIJFVAVEVBVCVFVGVHVIVJWSXOKRWRXNNWQXM + WKWPXLWFVRWOXKWOXKSTWNXJPUNTLRWMXIWMXISTDEWLBCIJFVAVEVCVFVGVKVOVIVLVJVM + VNMABNDKLVPMACNEKLVPVQ $. $} $d A j k $. $d B k $. $d C j $. @@ -166397,20 +166397,20 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) ) $= ( cv cfv wa cz wcel clt vj vg cuz wss caddc cseq cli wbr wrex c1 cfz wf1o - co wceq wex cn wi fveq2 sseq2d seqeq1 breq1d anbi12d cbvrexv simplrr wiso - chash wor cfn simplrl uzssz zssre sstri syl6ss ltso soss mpisyl fzfi ovex - cr cen f1oen ad2antll ensymd enfii sylancr fz1iso syl2anc csb cc ad5ant15 - cmpt eqid simprll simpllr simprlr summolem2a expr exlimdv climuni anassrs - simprr mpd eqeq2 syl5ibrcom expimpd rexlimdva r19.29an sylan2b ) DHOZUCPZ - UDZUEJXIUFZBOZUGUHZQZHRUIADUAOZUCPZUDZUEJXPUFZXMUGUHZQZUARUIUJXIUKUMZDFOZ - ULZCOZXIUEKUJUFPZUNZQZFUOZHUPUIXMYEUNZUQZXOYAHUARXIXPUNZXKXRXNXTYLXJXQDXI - XPUCURUSYLXLXSXMUGUEJXIXPUTVAVBVCAYAYKUARAXPRSZQZYAQZYIYJHUPYOXIUPSZQZYHY - JFYQYDYGYJYQYDQYJYGXMYFUNZYOYPYDYRYOYPYDQZQZXTXSYFUGUHZYRYNXRXTYSVDYTUJDV - FPUKUMDTTUBOZVEZUBUOZUUAYTDTVGZDVHSZUUDYTDVSUDVSTVGUUEYTDXQVSYNXRXTYSVIXQ - RVSXPVJVKVLVMVNDVSTVOVPYTYBVHSDYBVTUHUUFUJXIVQYTYBDYDYBDVTUHYOYPYBDYCUJXI - UKVRWAWBWCDYBWDWEDTUBWFWGYTUUCUUAUBYOYSUUCUUAYOYSUUCQZQDEFGIJKIUPGIOUUBPE - WHWKZUUBXPXILAGODSEWISYMYAUUGMWJNUUHWLYOYPYDUUCWMAYMYAUUGWNYNXRXTUUGVIYOY - PYDUUCWOYOYSUUCXAWPWQWRXBXMYFXSWSWGWTYEYFXMXCXDXEWRXFXGXH $. + co wceq wex cn wi fveq2 sseq2d seqeq1 anbi12d cbvrexvw simplrr chash wiso + breq1d wor cfn simplrl uzssz zssre sstri syl6ss ltso soss mpisyl cen fzfi + ovex f1oen ad2antll ensymd enfii sylancr fz1iso syl2anc csb cmpt ad5ant15 + cr cc eqid simprll simpllr simprlr simprr summolem2a expr exlimdv climuni + mpd anassrs eqeq2 syl5ibrcom expimpd rexlimdva r19.29an sylan2b ) DHOZUCP + ZUDZUEJXIUFZBOZUGUHZQZHRUIADUAOZUCPZUDZUEJXPUFZXMUGUHZQZUARUIUJXIUKUMZDFO + ZULZCOZXIUEKUJUFPZUNZQZFUOZHUPUIXMYEUNZUQZXOYAHUARXIXPUNZXKXRXNXTYLXJXQDX + IXPUCURUSYLXLXSXMUGUEJXIXPUTVFVAVBAYAYKUARAXPRSZQZYAQZYIYJHUPYOXIUPSZQZYH + YJFYQYDYGYJYQYDQYJYGXMYFUNZYOYPYDYRYOYPYDQZQZXTXSYFUGUHZYRYNXRXTYSVCYTUJD + VDPUKUMDTTUBOZVEZUBUOZUUAYTDTVGZDVHSZUUDYTDWJUDWJTVGUUEYTDXQWJYNXRXTYSVIX + QRWJXPVJVKVLVMVNDWJTVOVPYTYBVHSDYBVQUHUUFUJXIVRYTYBDYDYBDVQUHYOYPYBDYCUJX + IUKVSVTWAWBDYBWCWDDTUBWEWFYTUUCUUAUBYOYSUUCUUAYOYSUUCQZQDEFGIJKIUPGIOUUBP + EWGWHZUUBXPXILAGODSEWKSYMYAUUGMWINUUHWLYOYPYDUUCWMAYMYAUUGWNYNXRXTUUGVIYO + YPYDUUCWOYOYSUUCWPWQWRWSXAXMYFXSWTWFXBYEYFXMXCXDXEWSXFXGXH $. $( A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) $) @@ -166419,34 +166419,34 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) ) $= ( vy cv cfv wa cz wrex cn vg vj cuz wss caddc cseq cli wbr c1 cfz co wf1o - wceq wex wo weq wal wmo fveq2 sseq2d seqeq1 breq1d anbi12d cbvrexv reeanv - wi wcel simprlr cc ad4ant14 simplrl simplrr simprll simprrl sumrb simprrr - mpbid climuni syl2anc rexlimdvv syl5bir expdimp syl5bi jaod equcom syl6ib - exp31 summolem2 impancom oveq2 f1oeq2d eqeq2d exbidv f1oeq1 fveq1 csbeq1d - csb cmpt mpteq2dv syl5eq seqeq3d fveq1d cbvexvw syl6bb exdistrv an4 eqtri - cbvmptv simplr simprl simprr summolem3 eqeq12 syl5ibrcom expimpd exlimdvv - rexlimdvva jaodan alrimivv breq2 anbi2d rexbidv eqeq1 orbi12d mo4 sylibr + wceq wex wo weq wi wal fveq2 sseq2d seqeq1 breq1d anbi12d cbvrexvw reeanv + wcel simprlr ad4ant14 simplrl simplrr simprll simprrl sumrb mpbid simprrr + wmo climuni syl2anc exp31 rexlimdvv syl5bir expdimp syl5bi summolem2 jaod + cc equcom syl6ib impancom cmpt oveq2 f1oeq2d eqeq2d exbidv f1oeq1 csbeq1d + csb fveq1 mpteq2dv syl5eq seqeq3d fveq1d cbvexvw syl6bb an4 cbvmptv eqtri + exdistrv simplr simprl simprr summolem3 eqeq12 syl5ibrcom exlimdvv jaodan + expimpd rexlimdvva alrimivv breq2 anbi2d rexbidv eqeq1 orbi12d mo4 sylibr ) ACGOZUCPZUDZUEIYGUFZBOZUGUHZQZGRSZUIYGUJUKZCEOZULZYKYGUEJUIUFZPZUMZQZEU - NZGTSZUOZYIYJNOZUGUHZQZGRSZYQUUEYSUMZQZEUNZGTSZUOZQBNUPZVFZNUQBUQUUDBURAU - UOBNAUUDUUMUUNAYNUUMUUNVFUUCAYNQZUUHUUNUULUUHCHOZUCPZUDZUEIUUQUFZUUEUGUHZ + NZGTSZUOZYIYJNOZUGUHZQZGRSZYQUUEYSUMZQZEUNZGTSZUOZQBNUPZUQZNURBURUUDBVPAU + UOBNAUUDUUMUUNAYNUUMUUNUQUUCAYNQZUUHUUNUULUUHCHOZUCPZUDZUEIUUQUFZUUEUGUHZ QZHRSZUUPUUNUUGUVBGHRGHUPZYIUUSUUFUVAUVDYHUURCYGUUQUCUSUTUVDYJUUTUUEUGUEI - YGUUQVAVBVCVDAYNUVCUUNYNUVCQYMUVBQZHRSGRSAUUNYMUVBGHRRVEAUVEUUNGHRRAYGRVG - ZUUQRVGZQZUVEUUNAUVHQZUVEQZUUTYKUGUHZUVAUUNUVJYLUVKUVIYIYLUVBVHUVJCDYKFIY - GUUQKAFOCVGZDVIVGZUVHUVELVJAUVFUVGUVEVKAUVFUVGUVEVLUVIYIYLUVBVMUVIYMUUSUV - AVNVOVQUVIYMUUSUVAVPYKUUEUUTVRVSWGVTWAWBWCABNCDEFGHIJKLMWHWDAUUCQZUUHUUNU - ULAUUHUUCUUNAUUHQUUCNBUPUUNANBCDEFGHIJKLMWHNBWEWFWIUULUIUUQUJUKZCUAOZULZU - UEUUQUEHTFUUQUVPPZDWQZWRZUIUFZPZUMZQZUAUNZHTSZUVNUUNUUKUWEGHTUVDUUKUVOCYP - ULZUUEUUQYRPZUMZQZEUNUWEUVDUUJUWJEUVDYQUWGUUIUWIUVDYOUVOCYPYGUUQUIUJWJWKU - VDYSUWHUUEYGUUQYRUSWLVCWMUWJUWDEUAEUAUPZUWGUVQUWIUWCUVOCYPUVPWNUWKUWHUWBU - UEUWKUUQYRUWAUWKJUVTUEUIUWKJHTFUUQYPPZDWQZWRZUVTMUWKHTUWMUVSUWKFUWLUVRDUU - QYPUVPWOWPWSWTXAXBWLVCXCXDVDAUUCUWFUUNUUCUWFQUUBUWEQZHTSGTSAUUNUUBUWEGHTT - VEAUWOUUNGHTTUWOUUAUWDQZUAUNEUNAYGTVGUUQTVGQZQZUUNUUAUWDEUAXEUWRUWPUUNEUA - UWPYQUVQQZYTUWCQZQUWRUUNYQYTUVQUWCXFUWRUWSUWTUUNUWRUWSQZUUNUWTYSUWBUMUXAC - DEFUBIJUVTUVPYGUUQKAUVLUVMUWQUWSLVJJUWNUBTFUBOZYPPZDWQZWRMHUBTUWMUXDHUBUP - ZFUWLUXCDUUQUXBYPUSWPXHXGHUBTUVSFUXBUVPPZDWQUXEFUVRUXFDUUQUXBUVPUSWPXHAUW - QUWSXIUWRYQUVQXJUWRYQUVQXKXLYKYSUUEUWBXMXNXOWCXPWAXQWAWBWCWDXRXOXSUUDUUMB + YGUUQVAVBVCVDAYNUVCUUNYNUVCQYMUVBQZHRSGRSAUUNYMUVBGHRRVEAUVEUUNGHRRAYGRVF + ZUUQRVFZQZUVEUUNAUVHQZUVEQZUUTYKUGUHZUVAUUNUVJYLUVKUVIYIYLUVBVGUVJCDYKFIY + GUUQKAFOCVFZDWFVFZUVHUVELVHAUVFUVGUVEVIAUVFUVGUVEVJUVIYIYLUVBVKUVIYMUUSUV + AVLVMVNUVIYMUUSUVAVOYKUUEUUTVQVRVSVTWAWBWCABNCDEFGHIJKLMWDWEAUUCQZUUHUUNU + ULAUUHUUCUUNAUUHQUUCNBUPUUNANBCDEFGHIJKLMWDNBWGWHWIUULUIUUQUJUKZCUAOZULZU + UEUUQUEHTFUUQUVPPZDWQZWJZUIUFZPZUMZQZUAUNZHTSZUVNUUNUUKUWEGHTUVDUUKUVOCYP + ULZUUEUUQYRPZUMZQZEUNUWEUVDUUJUWJEUVDYQUWGUUIUWIUVDYOUVOCYPYGUUQUIUJWKWLU + VDYSUWHUUEYGUUQYRUSWMVCWNUWJUWDEUAEUAUPZUWGUVQUWIUWCUVOCYPUVPWOUWKUWHUWBU + UEUWKUUQYRUWAUWKJUVTUEUIUWKJHTFUUQYPPZDWQZWJZUVTMUWKHTUWMUVSUWKFUWLUVRDUU + QYPUVPWRWPWSWTXAXBWMVCXCXDVDAUUCUWFUUNUUCUWFQUUBUWEQZHTSGTSAUUNUUBUWEGHTT + VEAUWOUUNGHTTUWOUUAUWDQZUAUNEUNAYGTVFUUQTVFQZQZUUNUUAUWDEUAXHUWRUWPUUNEUA + UWPYQUVQQZYTUWCQZQUWRUUNYQYTUVQUWCXEUWRUWSUWTUUNUWRUWSQZUUNUWTYSUWBUMUXAC + DEFUBIJUVTUVPYGUUQKAUVLUVMUWQUWSLVHJUWNUBTFUBOZYPPZDWQZWJMHUBTUWMUXDHUBUP + ZFUWLUXCDUUQUXBYPUSWPXFXGHUBTUVSFUXBUVPPZDWQUXEFUVRUXFDUUQUXBUVPUSWPXFAUW + QUWSXIUWRYQUVQXJUWRYQUVQXKXLYKYSUUEUWBXMXNXQWCXOWAXRWAWBWCWEXPXQXSUUDUUMB NUUNYNUUHUUCUULUUNYMUUGGRUUNYLUUFYIYKUUEYJUGXTYAYBUUNUUBUUKGTUUNUUAUUJEUU - NYTUUIYQYKUUEYSYCYAWMYBYDYEYF $. + NYTUUIYQYKUUEYSYCYAWNYBYDYEYF $. $} ${ @@ -166467,34 +166467,34 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ nfel1 syl5 mpan9 simplr ad2antrr simpr syl6sseq sumrb expimpd rexlimdva biimpd chash clt wiso wor cr uzssz eqsstri zssre sstri ltso soss mpisyl cfn mp2 cen fzfi f1oen adantl ensymd enfii sylancr fz1iso syl2anc fveq2 - ovex csbeq1d csbco syl6eqr eqid simprl simprr summolem2a expr mpd breq2 - exlimdv syl5ibrcom jaod adantr sseq2d seqeq1 breq1d anbi12d rspcev orcd - syl12anc ex impbid cvv sseldi nfcv syl6eleqr eqeq12d sylc syl6eqelr nfv - nfeq2 fvex nfif cbvmpt eqcomi fvmpts eqtr4d seqfeq bitrd iotabidv df-fv - df-sum 3eqtr4g ) ABUAOZUFPZUGZUHMQMOZBRZDUVBCUIZUJULZUKZUUSUMZUBOZSUNZT - ZUAQUOZUPUUSUQURZBUCOZUSZUVHUUSUHMUTDUVBUVMPZCUIZUKZUPUMPZVAZTZUCVBZUAU - TUOZVCZUBVDUHEFUMZUVHSUNZUBVDBCDVEUWDSPAUWCUWEUBAUWCUHUVFFUMZUVHSUNZUWE - AUWCUWGAUVKUWGUWBAUVJUWGUAQAUUSQRZTZUVAUVIUWGUWIUVATZUVIUWGUWJBDNOZCUIZ - UVHNUVFUUSFMNQUVEUWKBRZUWLUJULMNVHUVCUWMUVDUWLUJMNBVFDUVBUWKCVIVGVJZUWJ - AUWMUWLVKRZAUWHUVAVLACVKRZDBVMUWMUWOAUWPDBLVNUWPUWODUWKBDUWLVKDUWKCVOVS - DNVHCUWLVKDUWKCVPVQVRVTZWAAUWHUVAWBAFQRZUWHUVAIWCUWIUVAWDABFUFPZUGZUWHU - VAABGUWSJHWEZWCWFWIWGWHAUWAUWGUAUTAUUSUTRZTZUVTUWGUCUXCUVNUVSUWGUXCUVNT - ZUWGUVSUWFUVRSUNZUXDUPBWJPUQURBWKWKUDOZWLZUDVBZUXEUXDBWKWMZBXBRZUXHUXDB - GUGZGWKWMZUXIAUXKUXBUVNJWCGWNUGWNWKWMUXLGQWNGUWSQHFWOZWPWQWRWSGWNWKWTXC - BGWKWTXAUXDUVLXBRBUVLXDUNUXJUPUUSXEUXDUVLBUVNUVLBXDUNUXCUVLBUVMUPUUSUQX - NXFXGXHBUVLXIXJBWKUDXKXLUXDUXGUXEUDUXCUVNUXGUXEUXCUVNUXGTZTZBUWLUCNUEUV - FUVQUEUTNUEOZUXFPUWLUIUKZUXFFUUSUWNUXOAUWMUWOAUXBUXNVLUWQWAMUEUTUVPNUXP - UVMPZUWLUIZMUEVHZUVPDUXRCUIUXSUXTDUVOUXRCUVBUXPUVMXMXODNUXRCXPXQVJUXQXR - AUXBUXNWBAUWRUXBUXNIWCAUWTUXBUXNUXAWCUXCUVNUXGXSUXCUVNUXGXTYAYBYEYCUVHU - VRUWFSYDYFWGYEWHYGAUWGUWCAUWGTZUVKUWBUYAUWRUWTUWGUVKAUWRUWGIYHAUWTUWGUX - AYHAUWGWDUVJUWTUWGTUAFQUUSFVAZUVAUWTUVIUWGUYBUUTUWSBUUSFUFXMYIUYBUVGUWF - UVHSUHUVFUUSFYJYKYLYMYOYNYPYQAUWFUWDUVHSAUHUEUVFEFIAUXPUWSRZTZUXPUVFPZD - UXPDOZBRZCUJULZUIZUXPEPZUYDUXPQRUYIYRRUYEUYIVAUYDUWSQUXPUXMAUYCWDZYSUYD - UYIUYJYRUYDUXPGRUYFEPZUYHVAZDGVMZUYJUYIVAZUYDUXPUWSGUYKHUUAAUYNUYCAUYMD - GKVNYHUYMUYODUXPGDUYJUYIDUXPUYHVOUUFDUEVHUYLUYJUYHUYIUYFUXPEXMDUXPUYHVP - UUBVRUUCZUXPEUUGUUDDUXPUYHQUVFYRDQUYHUKUVFDMQUYHUVEMUYHYTUVCDUVDUJUVCDU - UEDUVBCVODUJYTUUHDMVHUYGUVCCUVDUJDMBVFDUVBCVPVGUUIUUJUUKXLUYPUULUUMYKUU - NUUOUBBCUCDUAMUUQUBUWDSUUPUUR $. + ovex csbeq1d csbcow syl6eqr eqid simprl simprr summolem2a exlimdv breq2 + expr mpd syl5ibrcom adantr sseq2d seqeq1 breq1d anbi12d rspcev syl12anc + jaod orcd ex impbid cvv sseldi nfcv syl6eleqr nfeq2 sylc fvex syl6eqelr + nfv nfif cbvmpt eqcomi fvmpts eqtr4d seqfeq bitrd iotabidv df-sum df-fv + eqeq12d 3eqtr4g ) ABUAOZUFPZUGZUHMQMOZBRZDUVBCUIZUJULZUKZUUSUMZUBOZSUNZ + TZUAQUOZUPUUSUQURZBUCOZUSZUVHUUSUHMUTDUVBUVMPZCUIZUKZUPUMPZVAZTZUCVBZUA + UTUOZVCZUBVDUHEFUMZUVHSUNZUBVDBCDVEUWDSPAUWCUWEUBAUWCUHUVFFUMZUVHSUNZUW + EAUWCUWGAUVKUWGUWBAUVJUWGUAQAUUSQRZTZUVAUVIUWGUWIUVATZUVIUWGUWJBDNOZCUI + ZUVHNUVFUUSFMNQUVEUWKBRZUWLUJULMNVHUVCUWMUVDUWLUJMNBVFDUVBUWKCVIVGVJZUW + JAUWMUWLVKRZAUWHUVAVLACVKRZDBVMUWMUWOAUWPDBLVNUWPUWODUWKBDUWLVKDUWKCVOV + SDNVHCUWLVKDUWKCVPVQVRVTZWAAUWHUVAWBAFQRZUWHUVAIWCUWIUVAWDABFUFPZUGZUWH + UVAABGUWSJHWEZWCWFWIWGWHAUWAUWGUAUTAUUSUTRZTZUVTUWGUCUXCUVNUVSUWGUXCUVN + TZUWGUVSUWFUVRSUNZUXDUPBWJPUQURBWKWKUDOZWLZUDVBZUXEUXDBWKWMZBXBRZUXHUXD + BGUGZGWKWMZUXIAUXKUXBUVNJWCGWNUGWNWKWMUXLGQWNGUWSQHFWOZWPWQWRWSGWNWKWTX + CBGWKWTXAUXDUVLXBRBUVLXDUNUXJUPUUSXEUXDUVLBUVNUVLBXDUNUXCUVLBUVMUPUUSUQ + XNXFXGXHBUVLXIXJBWKUDXKXLUXDUXGUXEUDUXCUVNUXGUXEUXCUVNUXGTZTZBUWLUCNUEU + VFUVQUEUTNUEOZUXFPUWLUIUKZUXFFUUSUWNUXOAUWMUWOAUXBUXNVLUWQWAMUEUTUVPNUX + PUVMPZUWLUIZMUEVHZUVPDUXRCUIUXSUXTDUVOUXRCUVBUXPUVMXMXODNUXRCXPXQVJUXQX + RAUXBUXNWBAUWRUXBUXNIWCAUWTUXBUXNUXAWCUXCUVNUXGXSUXCUVNUXGXTYAYDYBYEUVH + UVRUWFSYCYFWGYBWHYNAUWGUWCAUWGTZUVKUWBUYAUWRUWTUWGUVKAUWRUWGIYGAUWTUWGU + XAYGAUWGWDUVJUWTUWGTUAFQUUSFVAZUVAUWTUVIUWGUYBUUTUWSBUUSFUFXMYHUYBUVGUW + FUVHSUHUVFUUSFYIYJYKYLYMYOYPYQAUWFUWDUVHSAUHUEUVFEFIAUXPUWSRZTZUXPUVFPZ + DUXPDOZBRZCUJULZUIZUXPEPZUYDUXPQRUYIYRRUYEUYIVAUYDUWSQUXPUXMAUYCWDZYSUY + DUYIUYJYRUYDUXPGRUYFEPZUYHVAZDGVMZUYJUYIVAZUYDUXPUWSGUYKHUUAAUYNUYCAUYM + DGKVNYGUYMUYODUXPGDUYJUYIDUXPUYHVOUUBDUEVHUYLUYJUYHUYIUYFUXPEXMDUXPUYHV + PUUQVRUUCZUXPEUUDUUEDUXPUYHQUVFYRDQUYHUKUVFDMQUYHUVEMUYHYTUVCDUVDUJUVCD + UUFDUVBCVODUJYTUUGDMVHUYGUVCCUVDUJDMBVFDUVBCVPVGUUHUUIUUJXLUYPUUKUULYJU + UMUUNUBBCUCDUAMUUOUBUWDSUUPUUR $. $} isum.3 $e |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B ) $. @@ -166521,30 +166521,30 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ ( vm cfv wcel c1 cn wceq vx vf vj vi csu cv cuz wss caddc cz csb cc0 cmpt cif cseq cli wbr wa wrex cfz co wf1o wex wo cio df-sum cvv fvex wb wmo wi eleq1w csbeq1 ifbieq1d cbvmptv wral ralrimiva nfcsb1v csbeq1a eleq1d rspc - cc nfel1 mpan9 fveq2 csbeq1d csbco syl6eqr summo wf f1of syl ovex sylancl - fex nnuz syl6eleq elfznn syl6eqelr fvmpt2 syl2an2 eqtr4d nffvmpt1 eqeq12d - eqid nfeq2 seqfveq jca f1oeq1 fveq1 syl6eq mpteq2dv seqeq3d fveq1d eqeq2d - csbie anbi12d elabd oveq2 f1oeq2d exbidv rspcev syl2anc olcd breq2 anbi2d - rexbidv eqeq1 orbi12d mpanl1 ancom2s syl5ibrcom impbid adantr iota5 mpan2 - moi2 expr syl5eq ) ABCEUEBOUFZUGPUHZUIFUJFUFZBQZEUUBCUKZULUNZUMZYTUOZUAUF - ZUPUQZURZOUJUSZRYTUTVAZBUBUFZVBZUUHYTUIFSEUUBUUMPZCUKZUMZRUOZPZTZURZUBVCZ - OSUSZVDZUAVEZIUIHRUOZPZUABCUBEOFVFAUVGVGQZUVEUVGTIUVFVHZAUVDUAUVGVGAUVDUU - HUVGTZVIUVHAUVDUVJAUVDUAVJZUUAUUGUVGUPUQZURZOUJUSZUUNUVGUUSTZURZUBVCZOSUS - ZVDZUVDUVJVKAUABEUCUFZCUKZUBUCOUDUUFUUQFUCUJUUEUVTBQZUWAULUNUUBUVTTUUCUWB - UUDUWAULFUCBVLEUUBUVTCVMVNVOACWBQZEBVPUWBUWAWBQZAUWCEBMVQUWCUWDEUVTBEUWAW - BEUVTCVRWCEUFZUVTTCUWAWBEUVTCVSVTWAWDFUDSUUPUCUDUFZUUMPZUWAUKZUUBUWFTZUUP - EUWGCUKUWHUWIEUUOUWGCUUBUWFUUMWEWFEUCUWGCWGWHVOWIAUVRUVNAISQRIUTVAZBUUMVB - ZUVGIUURPZTZURZUBVCZUVRKAUWNUWJBGVBZUVGIUIFSDUMZRUOZPZTZURUBGAUWJBGWJZUWJ - VGQGVGQAUWPUXALUWJBGWKWLRIUTWMUWJBVGGWOWNAUWPUWTLAUIEHUWQRIAISRUGPKWPWQAU - UBHPZUUBUWQPZTZFUWJVPUWEUWJQUWEHPZUWEUWQPZTZAUXDFUWJAUUBUWJQZURZUXBDUXCNU - XHUUBSQADVGQUXCDTUUBIWRUXIDUXBVGNUUBHVHWSFSDVGUWQUWQXEWTXAXBVQUXDUXGFUWEU - WJFUXEUXFFSDUWEXCXFUUBUWETUXBUXEUXCUXFUUBUWEHWEUUBUWEUWQWEXDWAWDXGXHUUMGT - ZUWKUWPUWMUWTUWJBUUMGXIUXJUWLUWSUVGUXJIUURUWRUXJUUQUWQUIRUXJFSUUPDUXJUUPE - UUBGPZCUKDUXJEUUOUXKCUUBUUMGXJWFEUXKCDUUBGVHJXPXKXLXMXNXOXQXRUVQUWOOISYTI - TZUVPUWNUBUXLUUNUWKUVOUWMUXLUULUWJBUUMYTIRUTXSXTUXLUUSUWLUVGYTIUURWEXOXQY - AYBYCYDZUVKUVSUVDUVJUVKUVDUVSUVJUVHUVKUVDUVSURUVJUVIUVDUVSUAUVGVGUVJUUKUV - NUVCUVRUVJUUJUVMOUJUVJUUIUVLUUAUUHUVGUUGUPYEYFYGUVJUVBUVQOSUVJUVAUVPUBUVJ - UUTUVOUUNUUHUVGUUSYHYFYAYGYIZYQYJYKYRYCAUVDUVJUVSUXMUXNYLYMYNYOYPYS $. + cc nfel1 mpan9 fveq2 csbeq1d csbcow syl6eqr summo wf f1of syl fex sylancl + ovex nnuz syl6eleq elfznn syl6eqelr fvmpt2 syl2an2 nffvmpt1 nfeq2 eqeq12d + eqid eqtr4d seqfveq jca f1oeq1 fveq1 csbie syl6eq mpteq2dv seqeq3d fveq1d + eqeq2d anbi12d elabd oveq2 f1oeq2d exbidv rspcev syl2anc olcd breq2 eqeq1 + anbi2d rexbidv orbi12d moi2 mpanl1 ancom2s syl5ibrcom impbid adantr iota5 + expr mpan2 syl5eq ) ABCEUEBOUFZUGPUHZUIFUJFUFZBQZEUUBCUKZULUNZUMZYTUOZUAU + FZUPUQZURZOUJUSZRYTUTVAZBUBUFZVBZUUHYTUIFSEUUBUUMPZCUKZUMZRUOZPZTZURZUBVC + ZOSUSZVDZUAVEZIUIHRUOZPZUABCUBEOFVFAUVGVGQZUVEUVGTIUVFVHZAUVDUAUVGVGAUVDU + UHUVGTZVIUVHAUVDUVJAUVDUAVJZUUAUUGUVGUPUQZURZOUJUSZUUNUVGUUSTZURZUBVCZOSU + SZVDZUVDUVJVKAUABEUCUFZCUKZUBUCOUDUUFUUQFUCUJUUEUVTBQZUWAULUNUUBUVTTUUCUW + BUUDUWAULFUCBVLEUUBUVTCVMVNVOACWBQZEBVPUWBUWAWBQZAUWCEBMVQUWCUWDEUVTBEUWA + WBEUVTCVRWCEUFZUVTTCUWAWBEUVTCVSVTWAWDFUDSUUPUCUDUFZUUMPZUWAUKZUUBUWFTZUU + PEUWGCUKUWHUWIEUUOUWGCUUBUWFUUMWEWFEUCUWGCWGWHVOWIAUVRUVNAISQRIUTVAZBUUMV + BZUVGIUURPZTZURZUBVCZUVRKAUWNUWJBGVBZUVGIUIFSDUMZRUOZPZTZURUBGAUWJBGWJZUW + JVGQGVGQAUWPUXALUWJBGWKWLRIUTWOUWJBVGGWMWNAUWPUWTLAUIEHUWQRIAISRUGPKWPWQA + UUBHPZUUBUWQPZTZFUWJVPUWEUWJQUWEHPZUWEUWQPZTZAUXDFUWJAUUBUWJQZURZUXBDUXCN + UXHUUBSQADVGQUXCDTUUBIWRUXIDUXBVGNUUBHVHWSFSDVGUWQUWQXEWTXAXFVQUXDUXGFUWE + UWJFUXEUXFFSDUWEXBXCUUBUWETUXBUXEUXCUXFUUBUWEHWEUUBUWEUWQWEXDWAWDXGXHUUMG + TZUWKUWPUWMUWTUWJBUUMGXIUXJUWLUWSUVGUXJIUURUWRUXJUUQUWQUIRUXJFSUUPDUXJUUP + EUUBGPZCUKDUXJEUUOUXKCUUBUUMGXJWFEUXKCDUUBGVHJXKXLXMXNXOXPXQXRUVQUWOOISYT + ITZUVPUWNUBUXLUUNUWKUVOUWMUXLUULUWJBUUMYTIRUTXSXTUXLUUSUWLUVGYTIUURWEXPXQ + YAYBYCYDZUVKUVSUVDUVJUVKUVDUVSUVJUVHUVKUVDUVSURUVJUVIUVDUVSUAUVGVGUVJUUKU + VNUVCUVRUVJUUJUVMOUJUVJUUIUVLUUAUUHUVGUUGUPYEYGYHUVJUVBUVQOSUVJUVAUVPUBUV + JUUTUVOUUNUUHUVGUUSYFYGYAYHYIZYJYKYLYQYCAUVDUVJUVSUXMUXNYMYNYOYPYRYS $. $} $( Any sum over the empty set is zero. (Contributed by Mario Carneiro, @@ -166957,12 +166957,12 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ fsumsplitf $p |- ( ph -> sum_ k e. U C = ( sum_ k e. A C + sum_ k e. B C ) ) $= ( vj csu cv csb caddc wceq cbvsumi wcel cc co nfcv nfcsb1v csbeq1a a1i wa - wi nfv nfan nfel1 nfim eleq1w anbi2d eleq1d imbi12d chvar fsumsplit csbco - csbid eqtri syl6eq oveq12i 3eqtrd ) AEDFMZEFLNZDOZLMZBVFLMZCVFLMZPUAZBDFM - ZCDFMZPUAZVDVGQAEDVFFLLDUBZFVEDUCZFVEDUDZRUEABCVFELHIJAFNZESZUFZDTSZUGAVE - ESZUFZVFTSZUGFLWBWCFAWAFGWAFUHUIFVFTVOUJUKVQVEQZVSWBVTWCWDVRWAAFLEULUMWDD - VFTVPUNUOKUPUQVJVMQAVHVKVIVLPBVFDLFVOVNVEVQQVFLVQVFOZDLVQVFUDWEFVQDODFLVQ - DURFDUSUTVAZRCVFDLFVOVNWFRVBUEVC $. + nfv nfan nfel1 nfim eleq1w anbi2d eleq1d imbi12d chvarfv fsumsplit csbcow + wi csbid eqtri syl6eq oveq12i 3eqtrd ) AEDFMZEFLNZDOZLMZBVFLMZCVFLMZPUAZB + DFMZCDFMZPUAZVDVGQAEDVFFLLDUBZFVEDUCZFVEDUDZRUEABCVFELHIJAFNZESZUFZDTSZUR + AVEESZUFZVFTSZURFLWBWCFAWAFGWAFUGUHFVFTVOUIUJVQVEQZVSWBVTWCWDVRWAAFLEUKUL + WDDVFTVPUMUNKUOUPVJVMQAVHVKVIVLPBVFDLFVOVNVEVQQVFLVQVFOZDLVQVFUDWEFVQDODF + LVQDUQFDUSUTVAZRCVFDLFVOVNWFRVBUEVC $. $} ${