diff --git a/iset.mm b/iset.mm index fbf4a10fb6..718c084ae4 100644 --- a/iset.mm +++ b/iset.mm @@ -50859,10 +50859,10 @@ We use their notation ("onto" under the arrow). (Contributed by NM, CAFZGCDHZDIZFZUABFZSDAJTUCABDKACDLMSUCUDNTSUBBUAABDOPQR $. ${ - ffvrni.1 $e |- F : A --> B $. + ffvelcdmi.1 $e |- F : A --> B $. $( A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.) $) - ffvelrni $p |- ( C e. A -> ( F ` C ) e. B ) $= + ffvelcdmi $p |- ( C e. A -> ( F ` C ) e. B ) $= ( wf wcel cfv ffvelcdm mpan ) ABDFCAGCDHBGEABCDIJ $. $} @@ -112255,20 +112255,20 @@ This definition (in terms of ` U. ` and ` ~<_ ` ) is not taken directly omgadd $p |- ( ( A e. _om /\ B e. _om ) -> ( G ` ( A +o B ) ) = ( ( G ` A ) + ( G ` B ) ) ) $= ( com wcel coa co cfv caddc wceq wi c0 oveq2 fveq2d oveq2d cc0 cn0 c1 0zd - vn vz cv csuc fveq2 eqeq12d imbi2d wf1o wf frechashgf1o f1of ax-mp nn0cnd - ffvelrni addid1d frec2uz0d 3eqtr4rd w3a wa nnasuc nnacl frec2uzsucd eqtrd - nna0 3adant3 3ad2ant1 3ad2ant2 1cnd addassd oveq1 3ad2ant3 3eqtr4d 3expia - cc id expcom a2d finds impcom ) CFGBFGZBCHIZDJZBDJZCDJZKIZLZWABUBUDZHIZDJ - ZWDWHDJZKIZLZMWABNHIZDJZWDNDJZKIZLZMWABUCUDZHIZDJZWDWSDJZKIZLZMWABWSUEZHI - ZDJZWDXEDJZKIZLZMWAWGMUBUCCWHNLZWMWRWAXKWJWOWLWQXKWIWNDWHNBHOPXKWKWPWDKWH - NDUFQUGUHWHWSLZWMXDWAXLWJXAWLXCXLWIWTDWHWSBHOPXLWKXBWDKWHWSDUFQUGUHWHXELZ - WMXJWAXMWJXGWLXIXMWIXFDWHXEBHOPXMWKXHWDKWHXEDUFQUGUHWHCLZWMWGWAXNWJWCWLWF - XNWIWBDWHCBHOPXNWKWEWDKWHCDUFQUGUHWAWDRKIWDWQWOWAWDWAWDFSBDFSDUIFSDUJADEU - KFSDULUMZUOUNZUPWAWPRWDKWAARDWAUAEUQQWAWNBDBVEPURWSFGZWAXDXJWAXQXDXJMWAXQ - XDXJWAXQXDUSZXGXATKIZXIWAXQXGXSLXDWAXQUTZXGWTUEZDJXSXTXFYADBWSVAPXTAWTRDX - TUAEBWSVBVCVDVFXRXCTKIZWDXBTKIZKIZXSXIXRWDXBTWAXQWDVOGXDXPVGXQWAXBVOGXDXQ - XBFSWSDXOUOUNVHXRVIVJXDWAXSYBLXQXAXCTKVKVLXQWAXIYDLXDXQXHYCWDKXQAWSRDXQUA - EXQVPVCQVHVMVDVNVQVRVSVT $. + vn vz cv csuc fveq2 eqeq12d imbi2d wf1o frechashgf1o f1of ax-mp ffvelcdmi + wf nn0cnd addid1d frec2uz0d nna0 3eqtr4rd w3a wa nnasuc nnacl frec2uzsucd + eqtrd 3adant3 cc 3ad2ant1 3ad2ant2 1cnd addassd oveq1 3ad2ant3 id 3eqtr4d + 3expia expcom a2d finds impcom ) CFGBFGZBCHIZDJZBDJZCDJZKIZLZWABUBUDZHIZD + JZWDWHDJZKIZLZMWABNHIZDJZWDNDJZKIZLZMWABUCUDZHIZDJZWDWSDJZKIZLZMWABWSUEZH + IZDJZWDXEDJZKIZLZMWAWGMUBUCCWHNLZWMWRWAXKWJWOWLWQXKWIWNDWHNBHOPXKWKWPWDKW + HNDUFQUGUHWHWSLZWMXDWAXLWJXAWLXCXLWIWTDWHWSBHOPXLWKXBWDKWHWSDUFQUGUHWHXEL + ZWMXJWAXMWJXGWLXIXMWIXFDWHXEBHOPXMWKXHWDKWHXEDUFQUGUHWHCLZWMWGWAXNWJWCWLW + FXNWIWBDWHCBHOPXNWKWEWDKWHCDUFQUGUHWAWDRKIWDWQWOWAWDWAWDFSBDFSDUIFSDUNADE + UJFSDUKULZUMUOZUPWAWPRWDKWAARDWAUAEUQQWAWNBDBURPUSWSFGZWAXDXJWAXQXDXJMWAX + QXDXJWAXQXDUTZXGXATKIZXIWAXQXGXSLXDWAXQVAZXGWTUEZDJXSXTXFYADBWSVBPXTAWTRD + XTUAEBWSVCVDVEVFXRXCTKIZWDXBTKIZKIZXSXIXRWDXBTWAXQWDVGGXDXPVHXQWAXBVGGXDX + QXBFSWSDXOUMUOVIXRVJVKXDWAXSYBLXQXAXCTKVLVMXQWAXIYDLXDXQXHYCWDKXQAWSRDXQU + AEXQVNVDQVIVOVEVPVQVRVSVT $. $} ${ @@ -113399,7 +113399,7 @@ a function (ordinarily on a subset of ` CC ` ) and produces a new (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) $) cjcl $p |- ( A e. CC -> ( * ` A ) e. CC ) $= - ( cc ccj cjf ffvelrni ) BBACDE $. + ( cc ccj cjf ffvelcdmi ) BBACDE $. $( The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) $) @@ -118725,11 +118725,11 @@ A Cauchy sequence (as defined here, which has a rate of convergence 31-Jan-2014.) $) climmpt $p |- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> G ~~> A ) ) $= - ( vm cz wcel wa cvv simpr cv cfv cuz syl eqeltrid cmpt cpw uzf ffvelrni - elex mptexg adantr simpl wceq fvexg adantll fveq2 fvmptg syl2anc eqcomd - climeq ) EKLZCFLZMZAJCDEFNGHUQUROUQDNLURUQDBGBPZCQZUAZNIUQGNLVBNLUQGERQ - ZNHUQVCKUBZLVCNLKVDERUCUDVCVDUESTBGVANUFSTUGUQURUHUSJPZGLZMZVEDQZVECQZV - GVFVINLZVHVIUIUSVFOURVFVJUQVECFGUJUKBVEVAVIGNDUTVECULIUMUNUOUP $. + ( vm cz wcel wa cvv simpr cv cfv cuz syl eqeltrid cmpt ffvelcdmi mptexg + cpw uzf elex adantr simpl wceq fvexg adantll fveq2 fvmptg eqcomd climeq + syl2anc ) EKLZCFLZMZAJCDEFNGHUQUROUQDNLURUQDBGBPZCQZUAZNIUQGNLVBNLUQGER + QZNHUQVCKUDZLVCNLKVDERUEUBVCVDUFSTBGVANUCSTUGUQURUHUSJPZGLZMZVEDQZVECQZ + VGVFVINLZVHVIUIUSVFOURVFVJUQVECFGUJUKBVEVAVIGNDUTVECULIUMUPUNUO $. $} $d k G $. @@ -119083,12 +119083,12 @@ seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 ) $= ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) ) $= ( cc wcel cv crp wa cmin co cabs cfv clt wbr wi cr wral wrex simpr simpll - cle syl2anc ffvelrni syl subcld abscld rpre ad2antlr lelttr syl3anc mpand - ralrimiva weq breq2 imbi1d ralbidv rspcev ) DHIZAJZKIZLZVDCJZDMNZOPZVCQRZ - VFEPZDEPZMNZOPZVCQRZSZCHUAZVHBJZQRZVNSZCHUAZBKUBVBVDUCVEVOCHVEVFHIZLZVMVH - UERZVIVNWBWAVBWCVEWAUCZVBVDWAUDZGUFWBVMTIVHTIVCTIZWCVILVNSWBVLWBVJVKWBWAV - JHIWDHHVFEFUGUHWBVBVKHIWEHHDEFUGUHUIUJWBVGWBVFDWDWEUIUJVDWFVBWAVCUKULVMVH - VCUMUNUOUPVTVPBVCKBAUQZVSVOCHWGVRVIVNVQVCVHQURUSUTVAUF $. + cle syl2anc ffvelcdmi syl subcld abscld ad2antlr lelttr syl3anc ralrimiva + rpre mpand weq breq2 imbi1d ralbidv rspcev ) DHIZAJZKIZLZVDCJZDMNZOPZVCQR + ZVFEPZDEPZMNZOPZVCQRZSZCHUAZVHBJZQRZVNSZCHUAZBKUBVBVDUCVEVOCHVEVFHIZLZVMV + HUERZVIVNWBWAVBWCVEWAUCZVBVDWAUDZGUFWBVMTIVHTIVCTIZWCVILVNSWBVLWBVJVKWBWA + VJHIWDHHVFEFUGUHWBVBVKHIWEHHDEFUGUHUIUJWBVGWBVFDWDWEUIUJVDWFVBWAVCUOUKVMV + HVCULUMUPUNVTVPBVCKBAUQZVSVOCHWGVRVIVNVQVCVHQURUSUTVAUF $. $} ${ @@ -119150,10 +119150,10 @@ seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 ) $= $( The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.) $) climcn1lem $p |- ( ph -> G ~~> ( H ` A ) ) $= - ( cc cli wbr wcel climcl syl cv cfv ffvelrni adantl crp cmin co cabs wi - clt wral wrex sylan climcn1 ) ABCDEUAFIGHJKLMPAGEUBUCEUAUDZNEGUEUFZDUGZ - UAUDVCIUHZUAUDAUAUAVCIRUIUJNOAVABUGZUKUDVCEULUMUNUHCUGUPUCVDEIUHULUMUNU - HVEUPUCUODUAUQCUKURVBSUSQTUT $. + ( cc cli wbr wcel climcl syl cv cfv ffvelcdmi adantl crp cmin co clt wi + cabs wral wrex sylan climcn1 ) ABCDEUAFIGHJKLMPAGEUBUCEUAUDZNEGUEUFZDUG + ZUAUDVCIUHZUAUDAUAUAVCIRUIUJNOAVABUGZUKUDVCEULUMUPUHCUGUNUCVDEIUHULUMUP + UHVEUNUCUODUAUQCUKURVBSUSQTUT $. $} ${ @@ -122524,30 +122524,30 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) fsumrelem $p |- ( ph -> ( F ` sum_ k e. A B ) = sum_ k e. A ( F ` B ) ) $= ( csu cfv wceq sumeq1 cc0 caddc co cc wcel vw vu csn cun fveq2d eqeq12d - vv cv 0cn ffvelrni ax-mp addid1i fvoveq1 fveq2 oveq1d oveq2 00id eqtrdi - c0 oveq2d vtocl2ga mp2an eqtr2i addcani mpbi sum0 fveq2i 3eqtr4i a1i wa - cfn wss csb cvv nfv nfcsb1v simplr simprr eldifbd simplll simprl sselda - cdif vex syl2anc csbeq1a wral ralrimiva ad2antrr nfel1 eleq1d rspc sylc - eldifad fsumsplitsn adantr fsumcl simpr 3eqtrd nfcv nffv wf ffvelrnd ex - eqtr4d findcard2sd ) AUAUHZEFLZGMZXGEGMZFLZNUSEFLZGMZUSXJFLZNZUBUHZEFLZ - GMZXPXJFLZNZXPUGUHZUCUDZEFLZGMZYBXJFLZNZDEFLZGMZDXJFLZNUAUBUGDXGUSNZXIX - MXKXNYJXHXLGXGUSEFOUEXGUSXJFOUFXGXPNZXIXRXKXSYKXHXQGXGXPEFOUEXGXPXJFOUF - XGYBNZXIYDXKYEYLXHYCGXGYBEFOUEXGYBXJFOUFXGDNZXIYHXKYIYMXHYGGXGDEFOUEXGD - XJFOUFXOAPGMZPXMXNYNYNQRZYNPQRZNYNPNYPYNYOYNPSTZYNSTUISSPGJUJUKZULYQYQY - NYONZUIUIBUHZCUHZQRGMZYTGMZUUAGMZQRZNZPUUAQRZGMZYNUUDQRZNYSBCPPSSYTPNZU - UBUUHUUEUUIYTPUUAGQUMUUJUUCYNUUDQYTPGUNUOUFUUAPNZUUHYNUUIYOUUKUUGPGUUKU - UGPPQRPUUAPPQUPUQURUEUUKUUDYNYNQUUAPGUNUTUFKVAVBVCYNYNPYRYRUIVDVEXLPGEF - VFVGXJFVFVHVIAXPVKTZVJZXPDVLZYADXPWCTZVJZVJZXTYFUUQXTVJZYDXSFYAEVMZGMZQ - RZYEUURYDXQUUSQRZGMZXRUUTQRZUVAUURYCUVBGUUQYCUVBNXTUUQXPYAEUUSFVNUUQFVO - ZFYAEVPZAUULUUPVQZYAVNTUUQUGWDVIZUUQYADXPUUMUUNUUOVRZVSZUUQFUHZXPTZVJZA - UVKDTESTZAUULUUPUVLVTUUQXPDUVKUUMUUNUUOWAWBIWEZFYAEWFZUUQYADTUVNFDWGZUU - SSTZUUQYADXPUVIWNAUVQUULUUPAUVNFDIWHWIUVNUVRFYADFUUSSUVFWJUVKYANZEUUSSU - VPWKWLWMZWOWPUEUURXQSTZUVRUVCUVDNZUUQUWAXTUUQXPEFUVGUVOWQWPUUQUVRXTUVTW - PUUFXQUUAQRZGMZXRUUDQRZNUWBBCXQUUSSSYTXQNZUUBUWDUUEUWEYTXQUUAGQUMUWFUUC - XRUUDQYTXQGUNUOUFUUAUUSNZUWDUVCUWEUVDUWGUWCUVBGUUAUUSXQQUPUEUWGUUDUUTXR - QUUAUUSGUNUTUFKVAWEUURXRXSUUTQUUQXTWRUOWSUUQYEUVANXTUUQXPYAXJUUTFVNUVEF - UUSGFGWTUVFXAUVGUVHUVJUVMSSEGSSGXBZUVMJVIUVOXCUVSEUUSGUVPUEUUQSSUUSGUWH - UUQJVIUVTXCWOWPXEXDHXF $. + vv cv c0 ffvelcdmi ax-mp addid1i fvoveq1 fveq2 oveq1d oveq2 00id eqtrdi + 0cn oveq2d vtocl2ga mp2an eqtr2i addcani mpbi fveq2i 3eqtr4i a1i cfn wa + wss csb cvv nfv nfcsb1v simplr vex simprr eldifbd simplll simprl sselda + sum0 cdif syl2anc csbeq1a wral eldifad ralrimiva nfel1 eleq1d rspc sylc + ad2antrr fsumsplitsn adantr fsumcl simpr 3eqtrd nfcv wf ffvelrnd eqtr4d + nffv ex findcard2sd ) AUAUHZEFLZGMZXGEGMZFLZNUIEFLZGMZUIXJFLZNZUBUHZEFL + ZGMZXPXJFLZNZXPUGUHZUCUDZEFLZGMZYBXJFLZNZDEFLZGMZDXJFLZNUAUBUGDXGUINZXI + XMXKXNYJXHXLGXGUIEFOUEXGUIXJFOUFXGXPNZXIXRXKXSYKXHXQGXGXPEFOUEXGXPXJFOU + FXGYBNZXIYDXKYEYLXHYCGXGYBEFOUEXGYBXJFOUFXGDNZXIYHXKYIYMXHYGGXGDEFOUEXG + DXJFOUFXOAPGMZPXMXNYNYNQRZYNPQRZNYNPNYPYNYOYNPSTZYNSTUSSSPGJUJUKZULYQYQ + YNYONZUSUSBUHZCUHZQRGMZYTGMZUUAGMZQRZNZPUUAQRZGMZYNUUDQRZNYSBCPPSSYTPNZ + UUBUUHUUEUUIYTPUUAGQUMUUJUUCYNUUDQYTPGUNUOUFUUAPNZUUHYNUUIYOUUKUUGPGUUK + UUGPPQRPUUAPPQUPUQURUEUUKUUDYNYNQUUAPGUNUTUFKVAVBVCYNYNPYRYRUSVDVEXLPGE + FWCVFXJFWCVGVHAXPVITZVJZXPDVKZYADXPWDTZVJZVJZXTYFUUQXTVJZYDXSFYAEVLZGMZ + QRZYEUURYDXQUUSQRZGMZXRUUTQRZUVAUURYCUVBGUUQYCUVBNXTUUQXPYAEUUSFVMUUQFV + NZFYAEVOZAUULUUPVPZYAVMTUUQUGVQVHZUUQYADXPUUMUUNUUOVRZVSZUUQFUHZXPTZVJZ + AUVKDTESTZAUULUUPUVLVTUUQXPDUVKUUMUUNUUOWAWBIWEZFYAEWFZUUQYADTUVNFDWGZU + USSTZUUQYADXPUVIWHAUVQUULUUPAUVNFDIWIWNUVNUVRFYADFUUSSUVFWJUVKYANZEUUSS + UVPWKWLWMZWOWPUEUURXQSTZUVRUVCUVDNZUUQUWAXTUUQXPEFUVGUVOWQWPUUQUVRXTUVT + WPUUFXQUUAQRZGMZXRUUDQRZNUWBBCXQUUSSSYTXQNZUUBUWDUUEUWEYTXQUUAGQUMUWFUU + CXRUUDQYTXQGUNUOUFUUAUUSNZUWDUVCUWEUVDUWGUWCUVBGUUAUUSXQQUPUEUWGUUDUUTX + RQUUAUUSGUNUTUFKVAWEUURXRXSUUTQUUQXTWRUOWSUUQYEUVANXTUUQXPYAXJUUTFVMUVE + FUUSGFGWTUVFXDUVGUVHUVJUVMSSEGSSGXAZUVMJVHUVOXBUVSEUUSGUVPUEUUQSSUUSGUW + HUUQJVHUVTXBWOWPXCXEHXF $. $} $( The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) @@ -127224,7 +127224,7 @@ seq n ( x. , $( Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) $) efcl $p |- ( A e. CC -> ( exp ` A ) e. CC ) $= - ( cc ce eff ffvelrni ) BBACDE $. + ( cc ce eff ffvelcdmi ) BBACDE $. $} ${ @@ -127901,12 +127901,12 @@ seq n ( x. , $( Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) $) sincl $p |- ( A e. CC -> ( sin ` A ) e. CC ) $= - ( cc csin sinf ffvelrni ) BBACDE $. + ( cc csin sinf ffvelcdmi ) BBACDE $. $( Closure of the cosine function with a complex argument. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) $) coscl $p |- ( A e. CC -> ( cos ` A ) e. CC ) $= - ( cc ccos cosf ffvelrni ) BBACDE $. + ( cc ccos cosf ffvelcdmi ) BBACDE $. ${ $d x A $. @@ -132999,18 +132999,18 @@ integers has a least element (schema form). (Contributed by NM, ` N ` is the value of ` C ` for the initial state ` A ` . (Contributed by Paul Chapman, 22-Jun-2011.) $) algcvg $p |- ( A e. S -> ( C ` ( R ` N ) ) = 0 ) $= - ( wcel cfv cc0 cn0 wf wceq fvco3 clt vk ccom nn0uz 0zd a1i algrf ffvelrni - id eqeltrid syl2anc fco sylancr sylancl ialgr0 fveq2d eqtrd eqtr4id cv wa - 0nn0 wne wbr c1 caddc co wi ffvelrnda 2fveq3 neeq1d fveq2 breq12d imbi12d - vtoclga syl peano2nn0 syl2an algrp1 sylan 3imtr4d nn0seqcvgd eqtr3d ) BEM - ZGCDUBZNZGDNCNZOWBPEDQZGPMWDWERWBBDEFOPUCIWBUDZWBUHZEEFQWBHUEZUFZWBGBCNZP - LEPBCJUGUIPEGCDSUJWBUAWCGWBEPCQWFPPWCQJWJPEPCDUKULWBGWKOWCNZLWBWLODNZCNZW - KWBWFOPMWLWNRWJUTPEOCDSUMWBWMBCWBBDEFOPUCIWGWHWIUNUOUPUQWBUAURZPMZUSZWODN - ZFNZCNZOVAZWTWRCNZTVBZWOVCVDVEZWCNZOVAXEWOWCNZTVBWQWREMXAXCVFZWBPEWODWJVG - AURZFNCNZOVAZXIXHCNZTVBZVFXGAWREXHWRRZXJXAXLXCXMXIWTOXHWRCFVHZVIXMXIWTXKX - BTXNXHWRCVJVKVLKVMVNWQXEWTOWQXEXDDNZCNZWTWBWFXDPMXEXPRWPWJWOVOPEXDCDSVPWQ - XOWSCWBBDEFWOOPUCIWGWHWIVQUOUPZVIWQXEWTXFXBTXQWBWFWPXFXBRWJPEWOCDSVRVKVSV - TWA $. + ( wcel cfv cc0 cn0 wf wceq fvco3 clt vk ccom nn0uz 0zd id algrf ffvelcdmi + a1i eqeltrid syl2anc fco sylancr 0nn0 sylancl ialgr0 fveq2d eqtrd eqtr4id + cv wa wne wbr c1 caddc co ffvelrnda 2fveq3 neeq1d breq12d imbi12d vtoclga + wi fveq2 syl peano2nn0 syl2an algrp1 sylan 3imtr4d nn0seqcvgd eqtr3d ) BE + MZGCDUBZNZGDNCNZOWBPEDQZGPMWDWERWBBDEFOPUCIWBUDZWBUEZEEFQWBHUHZUFZWBGBCNZ + PLEPBCJUGUIPEGCDSUJWBUAWCGWBEPCQWFPPWCQJWJPEPCDUKULWBGWKOWCNZLWBWLODNZCNZ + WKWBWFOPMWLWNRWJUMPEOCDSUNWBWMBCWBBDEFOPUCIWGWHWIUOUPUQURWBUAUSZPMZUTZWOD + NZFNZCNZOVAZWTWRCNZTVBZWOVCVDVEZWCNZOVAXEWOWCNZTVBWQWREMXAXCVLZWBPEWODWJV + FAUSZFNCNZOVAZXIXHCNZTVBZVLXGAWREXHWRRZXJXAXLXCXMXIWTOXHWRCFVGZVHXMXIWTXK + XBTXNXHWRCVMVIVJKVKVNWQXEWTOWQXEXDDNZCNZWTWBWFXDPMXEXPRWPWJWOVOPEXDCDSVPW + QXOWSCWBBDEFWOOPUCIWGWHWIVQUPUQZVHWQXEWTXFXBTXQWBWFWPXFXBRWJPEWOCDSVRVIVS + VTWA $. $} $( Lemma for ~ algcvgb . (Contributed by Paul Chapman, 31-Mar-2011.) $) @@ -133043,7 +133043,7 @@ integers has a least element (schema form). (Contributed by NM, ( ( ( C ` ( F ` X ) ) =/= 0 -> ( C ` ( F ` X ) ) < ( C ` X ) ) <-> ( ( ( C ` X ) =/= 0 -> ( C ` ( F ` X ) ) < ( C ` X ) ) /\ ( ( C ` X ) = 0 -> ( C ` ( F ` X ) ) = 0 ) ) ) ) $= - ( wcel cfv cn0 cc0 wne clt wbr wi wceq wa wb ffvelrni syl algcvgblem + ( wcel cfv cn0 cc0 wne clt wbr wi wceq wa wb ffvelcdmi syl algcvgblem syl2anc ) DBGZDAHZIGDCHZAHZIGZUEJKUEUCLMZNUCJKUGNUCJOUEJONPQBIDAFRUBUDBGU FBBDCERBIUDAFRSUCUETUA $. $} @@ -133061,24 +133061,24 @@ integers has a least element (schema form). (Contributed by NM, (Contributed by Paul Chapman, 22-Jun-2011.) $) algcvga $p |- ( A e. S -> ( K e. ( ZZ>= ` N ) -> ( C ` ( R ` K ) ) = 0 ) ) $= - ( wcel cn0 cfv cc0 wceq wi wbr vm vk cuz ffvelrni eqeltrid cz nn0z cle wa - eluz1 cv c1 caddc co 2fveq3 eqeq1d imbi2d algcvg a1i w3a nn0ge0 adantr cr - nn0re zre letr mp3an1 syl2an mpand elnn0z simplbi2 adantl syld sylan impr - 0re expcom 3adant1 ancld nn0uz 0zd id wf algrf ffvelrnda wne neeq1d fveq2 - clt breq12d imbi12d vtoclga algcvgb simpr syl6bi mpd syl fveqeq2d sylibrd - algrp1 syl6 a2d uzind 3expib sylbid com3r ) BENZHONZGHUCPNZGDPCPZQRZSXGHB - CPOMEOBCKUDUEZXHXIXGXKXHHUFNZXIXGXKSZSHUGXMXIGUFNZHGUHTZUIXNHGUJXMXOXPXNX - GUAUKZDPCPZQRZSXGHDPCPZQRZSZXGUBUKZDPZCPZQRZSXGYCULUMUNZDPZCPZQRZSXNUAUBH - GXQHRZXSYAXGYKXRXTQXQHCDUOUPUQXQYCRZXSYFXGYLXRYEQXQYCCDUOUPUQXQYGRZXSYJXG - YMXRYIQXQYGCDUOUPUQXQGRZXSXKXGYNXRXJQXQGCDUOUPUQYBXMABCDEFHIJKLMURUSXMYCU - FNZHYCUHTZUTZXGYFYJYQXGXGYCONZUIZYFYJSYQXGYRYOYPXGYRSXMXGYOYPUIYRXGYOYPYR - XGXHYOYPYRSXLXHYOUIZYPQYCUHTZYRYTQHUHTZYPUUAXHUUBYOHVAVBXHHVCNZYCVCNZUUBY - PUIUUASZYOHVDYCVEQVCNUUCUUDUUEVPQHYCVFVGVHVIYOUUAYRSXHYRYOUUAYCVJVKVLVMVN - VOVQVRVSYSYFYDFPZCPZQRZYJYSYDENZYFUUHSZXGOEYCDXGBDEFQOVTJXGWAZXGWBZEEFWCX - GIUSZWDWEUUIUUGQWFZUUGYEWITZSZUUJAUKZFPCPZQWFZUURUUQCPZWITZSUUPAYDEUUQYDR - ZUUSUUNUVAUUOUVBUURUUGQUUQYDCFUOZWGUVBUURUUGUUTYEWIUVCUUQYDCWHWJWKLWLUUIU - UPYEQWFUUOSZUUJUIUUJCEFYDIKWMUVDUUJWNWOWPWQYSYHUUFQCXGBDEFYCQOVTJUUKUULUU - MWTWRWSXAXBXCXDXEWQXFWP $. + ( wcel cn0 cfv cc0 wceq wi wbr vm vk cuz ffvelcdmi eqeltrid cz nn0z eluz1 + cle wa cv c1 caddc co 2fveq3 eqeq1d imbi2d algcvg a1i nn0ge0 adantr nn0re + w3a cr zre 0re letr mp3an1 syl2an mpand elnn0z simplbi2 adantl syld sylan + expcom 3adant1 ancld nn0uz 0zd id wf algrf ffvelrnda wne clt neeq1d fveq2 + impr breq12d imbi12d vtoclga algcvgb simpr syl6bi mpd syl algrp1 fveqeq2d + sylibrd syl6 a2d uzind 3expib sylbid com3r ) BENZHONZGHUCPNZGDPCPZQRZSXGH + BCPOMEOBCKUDUEZXHXIXGXKXHHUFNZXIXGXKSZSHUGXMXIGUFNZHGUITZUJXNHGUHXMXOXPXN + XGUAUKZDPCPZQRZSXGHDPCPZQRZSZXGUBUKZDPZCPZQRZSXGYCULUMUNZDPZCPZQRZSXNUAUB + HGXQHRZXSYAXGYKXRXTQXQHCDUOUPUQXQYCRZXSYFXGYLXRYEQXQYCCDUOUPUQXQYGRZXSYJX + GYMXRYIQXQYGCDUOUPUQXQGRZXSXKXGYNXRXJQXQGCDUOUPUQYBXMABCDEFHIJKLMURUSXMYC + UFNZHYCUITZVCZXGYFYJYQXGXGYCONZUJZYFYJSYQXGYRYOYPXGYRSXMXGYOYPUJYRXGYOYPY + RXGXHYOYPYRSXLXHYOUJZYPQYCUITZYRYTQHUITZYPUUAXHUUBYOHUTVAXHHVDNZYCVDNZUUB + YPUJUUASZYOHVBYCVEQVDNUUCUUDUUEVFQHYCVGVHVIVJYOUUAYRSXHYRYOUUAYCVKVLVMVNV + OWIVPVQVRYSYFYDFPZCPZQRZYJYSYDENZYFUUHSZXGOEYCDXGBDEFQOVSJXGVTZXGWAZEEFWB + XGIUSZWCWDUUIUUGQWEZUUGYEWFTZSZUUJAUKZFPCPZQWEZUURUUQCPZWFTZSUUPAYDEUUQYD + RZUUSUUNUVAUUOUVBUURUUGQUUQYDCFUOZWGUVBUURUUGUUTYEWFUVCUUQYDCWHWJWKLWLUUI + UUPYEQWEUUOSZUUJUJUUJCEFYDIKWMUVDUUJWNWOWPWQYSYHUUFQCXGBDEFYCQOVSJUUKUULU + UMWRWSWTXAXBXCXDXEWQXFWP $. $d K z $. $d N z $. algfx.6 $e |- ( z e. S -> ( ( C ` z ) = 0 -> ( F ` z ) = z ) ) $. @@ -133086,20 +133086,20 @@ integers has a least element (schema form). (Contributed by NM, ` 0 ` , ` F ` remains fixed after ` N ` steps. (Contributed by Paul Chapman, 22-Jun-2011.) $) algfx $p |- ( A e. S -> ( K e. ( ZZ>= ` N ) -> ( R ` K ) = ( R ` N ) ) ) $= - ( wcel cfv wceq wi cn0 wa vm vk cz cuz ffvelrni eqeltrid nn0zd cv cle wbr - crab uzval eleq2d pm5.32i c1 caddc fveqeq2 imbi2d eqidd a1i eluznn0 sylan - co cc0 nn0uz 0zd id algrp1 syldan algrf ffvelrnda algcvga eqeq12d imbi12d - wf imp fveq2 vtoclga eqtrd eqeq1d biimprd expcom adantl sylbir a2d uzind3 - sylc sylbi ex com3r mpd ) BEOZHUCOZGHUDPZOZGDPHDPZQZRWLHWLHBCPSMESBCKUEUF - ZUGWMWOWLWQWMWOWLWQRZWMWOTWMGHAUHZUIUJAUCUKZOZTWSWMWOXBWMWNXAGAHULZUMUNWL - UAUHZDPWPQZRWLWPWPQZRZWLUBUHZDPZWPQZRWLXHUOUPVCZDPZWPQZRWSUAAUBHGXDHQXEXF - WLXDHWPDUQURXDXHQXEXJWLXDXHWPDUQURXDXKQXEXMWLXDXKWPDUQURXDGQXEWQWLXDGWPDU - QURXGWMWLWPUSUTWMXHXAOZTZWLXJXMXOWMXHWNOZTWLXJXMRZRZWMXPXNWMWNXAXHXCUMUNX - PXRWMWLXPXQWLXPTZXMXJXSXLXIWPXSXLXIFPZXIWLXPXHSOZXLXTQWLHSOXPYAWRXHHVAVBZ - WLBDEFXHVDSVEJWLVFZWLVGZEEFVOWLIUTZVHVIXSXIEOZXICPVDQZXTXIQZWLXPYAYFYBWLS - EXHDWLBDEFVDSVEJYCYDYEVJVKVIWLXPYGABCDEFXHHIJKLMVLVPWTCPVDQZWTFPZWTQZRYGY - HRAXIEWTXIQZYIYGYKYHWTXIVDCUQYLYJXTWTXIWTXIFVQYLVGVMVNNVRWGVSVTWAWBWCWDWE - WFWHWIWJWK $. + ( wcel cfv wceq wi cn0 wa vm vk cuz ffvelcdmi eqeltrid nn0zd cle wbr crab + cz cv uzval eleq2d pm5.32i c1 caddc co fveqeq2 imbi2d eqidd eluznn0 sylan + a1i cc0 nn0uz 0zd id wf algrp1 syldan algrf ffvelrnda algcvga imp eqeq12d + fveq2 imbi12d vtoclga sylc eqeq1d biimprd expcom adantl sylbir a2d uzind3 + eqtrd sylbi ex com3r mpd ) BEOZHUJOZGHUCPZOZGDPHDPZQZRWLHWLHBCPSMESBCKUDU + EZUFWMWOWLWQWMWOWLWQRZWMWOTWMGHAUKZUGUHAUJUIZOZTWSWMWOXBWMWNXAGAHULZUMUNW + LUAUKZDPWPQZRWLWPWPQZRZWLUBUKZDPZWPQZRWLXHUOUPUQZDPZWPQZRWSUAAUBHGXDHQXEX + FWLXDHWPDURUSXDXHQXEXJWLXDXHWPDURUSXDXKQXEXMWLXDXKWPDURUSXDGQXEWQWLXDGWPD + URUSXGWMWLWPUTVCWMXHXAOZTZWLXJXMXOWMXHWNOZTWLXJXMRZRZWMXPXNWMWNXAXHXCUMUN + XPXRWMWLXPXQWLXPTZXMXJXSXLXIWPXSXLXIFPZXIWLXPXHSOZXLXTQWLHSOXPYAWRXHHVAVB + ZWLBDEFXHVDSVEJWLVFZWLVGZEEFVHWLIVCZVIVJXSXIEOZXICPVDQZXTXIQZWLXPYAYFYBWL + SEXHDWLBDEFVDSVEJYCYDYEVKVLVJWLXPYGABCDEFXHHIJKLMVMVNWTCPVDQZWTFPZWTQZRYG + YHRAXIEWTXIQZYIYGYKYHWTXIVDCURYLYJXTWTXIWTXIFVPYLVGVOVQNVRVSWGVTWAWBWCWDW + EWFWHWIWJWK $. $} @@ -133197,13 +133197,13 @@ integers has a least element (schema form). (Contributed by NM, ( K e. ( ZZ>= ` N ) -> ( 2nd ` ( R ` K ) ) = 0 ) ) $= ( vz cn0 wcel cuz cfv c2nd cc0 wceq fvres clt cxp wa cres xp2nd eluznn0 eqeltrid sylan nn0uz 0zd id wf eucalgf a1i algrf ffvelrnda syldan simpl - syl eqtr4di fveq2d eleq2d biimpar f2ndres wne eucalglt ffvelrni breq12d - cv wbr neeq1d 3imtr4d eqid algcvga sylc eqtr3d ex ) CLLUAZMZFGNOZMZFDOZ - POZQRVRVTUBZWAPVQUCZOZWBQWCWAVQMZWEWBRVRVTFLMZWFVRGLMVTWGVRGCPOZLJCLLUD - UFFGUEUGVRLVQFDVRCDVQEQLUHIVRUIVRUJVQVQEUKVRABEHULZUMUNUOUPWAVQPSURWCVR - FCWDOZNOZMZWEQRVRVTUQVRWLVTVRWKVSFVRWJGNVRWJWHGCVQPSJUSUTVAVBKCWDDVQEFW - JWIILLVCKVHZVQMZWMEOZPOZQVDWPWMPOZTVIWOWDOZQVDWRWMWDOZTVIABEWMHVEWNWRWP - QWNWOVQMWRWPRVQVQWMEWIVFWOVQPSURZVJWNWRWPWSWQTWTWMVQPSVGVKWJVLVMVNVOVP + syl eqtr4di fveq2d eleq2d biimpar f2ndres cv wne wbr eucalglt ffvelcdmi + neeq1d breq12d 3imtr4d eqid algcvga sylc eqtr3d ex ) CLLUAZMZFGNOZMZFDO + ZPOZQRVRVTUBZWAPVQUCZOZWBQWCWAVQMZWEWBRVRVTFLMZWFVRGLMVTWGVRGCPOZLJCLLU + DUFFGUEUGVRLVQFDVRCDVQEQLUHIVRUIVRUJVQVQEUKVRABEHULZUMUNUOUPWAVQPSURWCV + RFCWDOZNOZMZWEQRVRVTUQVRWLVTVRWKVSFVRWJGNVRWJWHGCVQPSJUSUTVAVBKCWDDVQEF + WJWIILLVCKVDZVQMZWMEOZPOZQVEWPWMPOZTVFWOWDOZQVEWRWMWDOZTVFABEWMHVGWNWRW + PQWNWOVQMWRWPRVQVQWMEWIVHWOVQPSURZVIWNWRWPWSWQTWTWMVQPSVJVKWJVLVMVNVOVP $. $} @@ -133223,16 +133223,16 @@ integers has a least element (schema form). (Contributed by NM, ( cn0 wcel cfv cgcd cc0 c2nd wceq syl fveq2d fvres vz wa c1st co cop wf nn0uz cxp 0zd opelxpi eqeltrid eucalgf algrf ffvelcdm sylancom 1st2nd2 df-ov fveq2i a1i eqtr4di op2ndg eqtrid cuz cz xp2nd uzid eqid eucalgcvga mpd eqtr3d oveq2d - nn0zd xp1st nn0gcdid0 3syl 3eqtrrd cres cv eucalginv ffvelrni 3eqtr4d sylancl - alginv 0nn0 3eqtr3d ialgr0 eqtrdi 3eqtrd ) FKLZGKLZUBZGDMZUCMZWLNMZODMZNMZFGN - UDZWKWNWMWLPMZNUDZWMONUDZWMWKWNWMWRUEZNMWSWKWLXANWKWLKKUHZLZWLXAQWIWJKXBDUFZX - CWKCDXBEOKUGIWKUIZWKCFGUEZXBJFGKKUJUKZXBXBEUFWKABEHULZUSZUMZKXBGDUNUOZWLKKUPR - SWMWRNUQUTWKWROWMNWKCPMZDMZPMZWROWKXMWLPWKXLGDWKXLXFPMGCXFPJURFGKKVAVBSSWKCXB - LZXNOQZXGXOXLXLVCMLZXPXOXLVDLXQXOXLCKKVEVLXLVFRABCDEXLXLHIXLVGVHVIRVJVKWKXCWM - KLWTWMQXKWLKKVMWMVNVOVPWKWLNXBVQZMZWOXRMZWNWPWIWJXOXSXTQXGUACDXBEXRGIXHUAVRZX - BLZYAEMZNMZYANMYCXRMZYAXRMABEYAHVSYBYCXBLYEYDQXBXBYAEXHVTYCXBNTRYAXBNTWAWCUOW - KXCXSWNQXKWLXBNTRWKWOXBLZXTWPQWKXDOKLYFXJWDKXBODUNWBWOXBNTRWEWKWPXFNMWQWKWOXF - NWKWOCXFWKCDXBEOKUGIXEXGXIWFJWGSFGNUQUTWH $. + nn0zd xp1st nn0gcdid0 3syl 3eqtrrd cres cv eucalginv ffvelcdmi 3eqtr4d alginv + 0nn0 sylancl 3eqtr3d ialgr0 eqtrdi 3eqtrd ) FKLZGKLZUBZGDMZUCMZWLNMZODMZNMZFG + NUDZWKWNWMWLPMZNUDZWMONUDZWMWKWNWMWRUEZNMWSWKWLXANWKWLKKUHZLZWLXAQWIWJKXBDUFZ + XCWKCDXBEOKUGIWKUIZWKCFGUEZXBJFGKKUJUKZXBXBEUFWKABEHULZUSZUMZKXBGDUNUOZWLKKUP + RSWMWRNUQUTWKWROWMNWKCPMZDMZPMZWROWKXMWLPWKXLGDWKXLXFPMGCXFPJURFGKKVAVBSSWKCX + BLZXNOQZXGXOXLXLVCMLZXPXOXLVDLXQXOXLCKKVEVLXLVFRABCDEXLXLHIXLVGVHVIRVJVKWKXCW + MKLWTWMQXKWLKKVMWMVNVOVPWKWLNXBVQZMZWOXRMZWNWPWIWJXOXSXTQXGUACDXBEXRGIXHUAVRZ + XBLZYAEMZNMZYANMYCXRMZYAXRMABEYAHVSYBYCXBLYEYDQXBXBYAEXHVTYCXBNTRYAXBNTWAWBUO + WKXCXSWNQXKWLXBNTRWKWOXBLZXTWPQWKXDOKLYFXJWCKXBODUNWDWOXBNTRWEWKWPXFNMWQWKWOX + FNWKWOCXFWKCDXBEOKUGIXEXGXIWFJWGSFGNUQUTWH $. $} @@ -135336,28 +135336,28 @@ infinite descent (here implemented by strong induction). (Contributed power of two. (Contributed by Jim Kingdon, 17-Nov-2021.) $) sqpweven $p |- ( A e. NN -> 2 || ( 2nd ` ( `' F ` ( A ^ 2 ) ) ) ) $= ( cn wcel c2 cfv cmul co cexp cdvds wbr cn0 syl wceq ccnv c2nd cxp wf1o - cz wf oddpwdc f1ocnv f1of ffvelrni xp2nd nn0zd 2nn a1i dvdsmul2 syl2anc - mp2b nnzd c1st cop wn xp1st breq2 notbid elrab2 simplbi nnsqcld simprbi - cv cprime wb 2prm w3a euclemma oridm bitrdi mp3an2i mtbird nncnd sqvald + cz oddpwdc f1ocnv f1of mp2b ffvelcdmi xp2nd nn0zd 2nn a1i nnzd dvdsmul2 + wf syl2anc c1st wn xp1st cv breq2 notbid elrab2 simplbi nnsqcld simprbi + cop cprime wb 2prm wo euclemma oridm bitrdi mp3an2i mtbird nncnd sqvald breq2d sylanbrc nnnn0d nn0mulcld opelxp expmuld nnexpcld nnmulcld oveq2 - oveq1d ovmpog syl3anc f1ocnvfv2 mpan 1st2nd2 fveq2d df-ov eqtr4di eqtrd - wo eqtr3d sqmuld 3eqtr4rd eqtr2di wi f1ocnvfv sylc op2ndg breqtrrd ) DI - JZKDEUAZLZUBLZKMNZDKONZXKLZUBLZPXJXMUEJKUEJKXNPQXJXMXJXLFRUCZJZXMRJZIXR - DXKXRIEUDZIXRXKUDIXRXKUFABCEFGHUGZXRIEUHIXRXKUIUQUJZXLFRUKSZULXJKKIJXJU - MUNZURXMKUOUPXJXQXLUSLZKONZXNUTZUBLZXNXJXPYHUBXJYHXRJZYHELZXOTZXPYHTZXJ - YGFJZXNRJZYJXJYGIJKYGPQZVAZYNXJYFXJYFFJZYFIJZXJXSYRYCXLFRVBSZYRYSKYFPQZ - VAZKCVIZPQZVAZUUBCYFIFUUCYFTUUDUUAUUCYFKPVCVDGVEZVFSZVGZXJYPKYFYFMNZPQZ - XJUUJUUAXJYRUUBYTYRYSUUBUUFVHSKVJJZXJYFUEJZUULUUJUUAVKVLXJYFUUGURZUUMUU - KUULUULVMUUJUUAUUAWTUUAKYFYFVNUUAVOVPVQVRXJYGUUIKPXJYFXJYFUUGVSZVTWAVRU - UEYQCYGIFUUCYGTUUDYPUUCYGKPVCVDGVEWBZXJXMKYDXJKYEWCZWDZYGXNFRWEWBXJXOYG - XNENZYKXJKXNONZYGMNZKXMONZKONZYGMNZUURXOXJUUSUVBYGMXJKXMKXJKYEVSUUPYDWF - WJXJYNYOUUTIJUURUUTTUUOUUQXJUUSYGXJKXNYEUUQWGUUHWHABYGXNFRKBVIZONZAVIZM - NZUUTEUVEYGMNIUVFYGUVEMWIUVDXNTUVEUUSYGMUVDXNKOWIWJHWKWLXJXOUVAYFMNZKON - UVCXJDUVHKOXJDYFXMENZUVHXJDYFXMUTZELZUVIXJXLELZDUVKYAXJUVLDTYBXRIDEWMWN - XJXLUVJEXJXSXLUVJTYCXLFRWOSWPXAYFXMEWQWRXJYRXTUVHIJUVIUVHTYTYDXJUVAYFXJ - KXMYEYDWGZUUGWHABYFXMFRUVGUVHEUVEYFMNIUVFYFUVEMWIUVDXMTUVEUVAYFMUVDXMKO - WIWJHWKWLWSWJXJUVAYFXJUVAUVMVSUUNXBWSXCYGXNEWQXDYAYJYLYMXEYBXRIYHXOEXFW - NXGWPXJYNYOYIXNTUUOUUQYGXNFRXHUPWSXI $. + w3a oveq1d ovmpog syl3anc f1ocnvfv2 1st2nd2 fveq2d eqtr3d df-ov eqtr4di + mpan eqtrd sqmuld 3eqtr4rd eqtr2di wi f1ocnvfv sylc op2ndg breqtrrd ) D + IJZKDEUAZLZUBLZKMNZDKONZXKLZUBLZPXJXMUEJKUEJKXNPQXJXMXJXLFRUCZJZXMRJZIX + RDXKXRIEUDZIXRXKUDIXRXKUQABCEFGHUFZXRIEUGIXRXKUHUIUJZXLFRUKSZULXJKKIJXJ + UMUNZUOXMKUPURXJXQXLUSLZKONZXNVIZUBLZXNXJXPYHUBXJYHXRJZYHELZXOTZXPYHTZX + JYGFJZXNRJZYJXJYGIJKYGPQZUTZYNXJYFXJYFFJZYFIJZXJXSYRYCXLFRVASZYRYSKYFPQ + ZUTZKCVBZPQZUTZUUBCYFIFUUCYFTUUDUUAUUCYFKPVCVDGVEZVFSZVGZXJYPKYFYFMNZPQ + ZXJUUJUUAXJYRUUBYTYRYSUUBUUFVHSKVJJZXJYFUEJZUULUUJUUAVKVLXJYFUUGUOZUUMU + UKUULUULWJUUJUUAUUAVMUUAKYFYFVNUUAVOVPVQVRXJYGUUIKPXJYFXJYFUUGVSZVTWAVR + UUEYQCYGIFUUCYGTUUDYPUUCYGKPVCVDGVEWBZXJXMKYDXJKYEWCZWDZYGXNFRWEWBXJXOY + GXNENZYKXJKXNONZYGMNZKXMONZKONZYGMNZUURXOXJUUSUVBYGMXJKXMKXJKYEVSUUPYDW + FWKXJYNYOUUTIJUURUUTTUUOUUQXJUUSYGXJKXNYEUUQWGUUHWHABYGXNFRKBVBZONZAVBZ + MNZUUTEUVEYGMNIUVFYGUVEMWIUVDXNTUVEUUSYGMUVDXNKOWIWKHWLWMXJXOUVAYFMNZKO + NUVCXJDUVHKOXJDYFXMENZUVHXJDYFXMVIZELZUVIXJXLELZDUVKYAXJUVLDTYBXRIDEWNW + TXJXLUVJEXJXSXLUVJTYCXLFRWOSWPWQYFXMEWRWSXJYRXTUVHIJUVIUVHTYTYDXJUVAYFX + JKXMYEYDWGZUUGWHABYFXMFRUVGUVHEUVEYFMNIUVFYFUVEMWIUVDXMTUVEUVAYFMUVDXMK + OWIWKHWLWMXAWKXJUVAYFXJUVAUVMVSUUNXBXAXCYGXNEWRXDYAYJYLYMXEYBXRIYHXOEXF + WTXGWPXJYNYOYIXNTUUOUUQYGXNFRXHURXAXI $. $} ${ @@ -135367,34 +135367,34 @@ infinite descent (here implemented by strong induction). (Contributed 2sqpwodd $p |- ( A e. NN -> -. 2 || ( 2nd ` ( `' F ` ( 2 x. ( A ^ 2 ) ) ) ) ) $= ( cn wcel c2 cexp co cmul cfv cdvds wbr cn0 syl wceq ccnv c2nd c1 caddc - cz wn cxp wf1o wf oddpwdc f1ocnv f1of mp2b ffvelrni xp2nd nn0zd 2nn a1i - nnzd zmulcld dvdsmul2 syl2anc oddp1even biimprd con2d sylc cop xp1st cv - c1st breq2 notbid elrab2 simplbi nnsqcld simprbi cprime wb w3a euclemma - 2prm wo oridm bitrdi mp3an2i mtbird nncnd sqvald breq2d sylanbrc nnnn0d - nn0mulcld peano2nn0 opelxp expp1d expcld mulcomd oveq2d 3eqtrd nnexpcld - expmuld oveq1d nnmulcld oveq2 ovmpog syl3anc mpan 1st2nd2 fveq2d eqtr3d - f1ocnvfv2 df-ov eqtr4di eqtrd sqmuld cc eqeltrrd mulassd eqtr4d eqtr2di - 3eqtr4rd wi f1ocnvfv op2ndg ) DIJZKKDKLMZNMZEUAZOZUBOZPQKDYHOZUBOZKNMZU - CUDMZPQZYEYMUEJZKYMPQZYOUFYEYLKYEYLYEYKFRUGZJZYLRJZIYRDYHYRIEUHZIYRYHUH - IYRYHUIABCEFGHUJZYRIEUKIYRYHULUMUNZYKFRUOSZUPZYEKKIJYEUQURZUSZUTYEYLUEJ - KUEJYQUUEUUGYLKVAVBYPYOYQYPYQUFYOYMVCVDVEVFYEYJYNKPYEYJYKVJOZKLMZYNVGZU - BOZYNYEYIUUJUBYEUUJYRJZUUJEOZYGTZYIUUJTZYEUUIFJZYNRJZUULYEUUIIJKUUIPQZU - FZUUPYEUUHYEUUHFJZUUHIJZYEYSUUTUUCYKFRVHSZUUTUVAKUUHPQZUFZKCVIZPQZUFZUV - DCUUHIFUVEUUHTUVFUVCUVEUUHKPVKVLGVMZVNSZVOZYEUURKUUHUUHNMZPQZYEUVLUVCYE - UUTUVDUVBUUTUVAUVDUVHVPSKVQJZYEUUHUEJZUVNUVLUVCVRWAYEUUHUVIUSZUVOUVMUVN - UVNVSUVLUVCUVCWBUVCKUUHUUHVTUVCWCWDWEWFYEUUIUVKKPYEUUHYEUUHUVIWGZWHWIWF - UVGUUSCUUIIFUVEUUITUVFUURUVEUUIKPVKVLGVMWJZYEYMRJUUQYEYLKUUDYEKUUFWKZWL - ZYMWMSZUUIYNFRWNWJYEYGUUIYNEMZUUMYEKYNLMZUUINMZKKYLLMZKLMZNMZUUINMZUWAY - GYEUWBUWFUUINYEUWBKYMLMZKNMKUWHNMUWFYEKYMYEKUUFWGZUVSWOYEUWHKYEKYMUWIUV - SWPZUWIWQYEUWHUWEKNYEKYLKUWIUVRUUDXAZWRWSXBYEUUPUUQUWCIJUWAUWCTUVQUVTYE - UWBUUIYEKYNUUFUVTWTUVJXCABUUIYNFRKBVIZLMZAVIZNMZUWCEUWMUUINMIUWNUUIUWMN - XDUWLYNTUWMUWBUUINUWLYNKLXDXBHXEXFYEYGKUWEUUINMZNMUWGYEYFUWPKNYEYFUWDUU - HNMZKLMUWPYEDUWQKLYEDUUHYLEMZUWQYEDUUHYLVGZEOZUWRYEYKEOZDUWTUUAYEUXADTU - UBYRIDEXKXGYEYKUWSEYEYSYKUWSTUUCYKFRXHSXIXJUUHYLEXLXMYEUUTYTUWQIJUWRUWQ - TUVBUUDYEUWDUUHYEKYLUUFUUDWTZUVIXCABUUHYLFRUWOUWQEUWMUUHNMIUWNUUHUWMNXD - UWLYLTUWMUWDUUHNUWLYLKLXDXBHXEXFXNXBYEUWDUUHYEUWDUXBWGUVPXOXNWRYEKUWEUU - IUWIYEUWHUWEXPUWKUWJXQYEUUIUVJWGXRXSYAUUIYNEXLXTUUAUULUUNUUOYBUUBYRIUUJ - YGEYCXGVFXIYEUUPUUQUUKYNTUVQUVTUUIYNFRYDVBXNWIWF $. + cz wn cxp wf1o wf oddpwdc f1ocnv f1of mp2b ffvelcdmi xp2nd 2nn a1i nnzd + nn0zd zmulcld dvdsmul2 syl2anc oddp1even biimprd con2d sylc c1st cop cv + xp1st breq2 notbid elrab2 simplbi nnsqcld simprbi cprime wb 2prm w3a wo + euclemma oridm bitrdi mp3an2i mtbird nncnd sylanbrc nn0mulcld peano2nn0 + sqvald breq2d nnnn0d opelxp expp1d expcld mulcomd expmuld oveq2d 3eqtrd + oveq1d nnexpcld nnmulcld ovmpog syl3anc f1ocnvfv2 1st2nd2 fveq2d eqtr3d + oveq2 mpan df-ov eqtr4di eqtrd sqmuld eqeltrrd mulassd 3eqtr4rd eqtr2di + cc eqtr4d wi f1ocnvfv op2ndg ) DIJZKKDKLMZNMZEUAZOZUBOZPQKDYHOZUBOZKNMZ + UCUDMZPQZYEYMUEJZKYMPQZYOUFYEYLKYEYLYEYKFRUGZJZYLRJZIYRDYHYRIEUHZIYRYHU + HIYRYHUIABCEFGHUJZYRIEUKIYRYHULUMUNZYKFRUOSZUSZYEKKIJYEUPUQZURZUTYEYLUE + JKUEJYQUUEUUGYLKVAVBYPYOYQYPYQUFYOYMVCVDVEVFYEYJYNKPYEYJYKVGOZKLMZYNVHZ + UBOZYNYEYIUUJUBYEUUJYRJZUUJEOZYGTZYIUUJTZYEUUIFJZYNRJZUULYEUUIIJKUUIPQZ + UFZUUPYEUUHYEUUHFJZUUHIJZYEYSUUTUUCYKFRVJSZUUTUVAKUUHPQZUFZKCVIZPQZUFZU + VDCUUHIFUVEUUHTUVFUVCUVEUUHKPVKVLGVMZVNSZVOZYEUURKUUHUUHNMZPQZYEUVLUVCY + EUUTUVDUVBUUTUVAUVDUVHVPSKVQJZYEUUHUEJZUVNUVLUVCVRVSYEUUHUVIURZUVOUVMUV + NUVNVTUVLUVCUVCWAUVCKUUHUUHWBUVCWCWDWEWFYEUUIUVKKPYEUUHYEUUHUVIWGZWKWLW + FUVGUUSCUUIIFUVEUUITUVFUURUVEUUIKPVKVLGVMWHZYEYMRJUUQYEYLKUUDYEKUUFWMZW + IZYMWJSZUUIYNFRWNWHYEYGUUIYNEMZUUMYEKYNLMZUUINMZKKYLLMZKLMZNMZUUINMZUWA + YGYEUWBUWFUUINYEUWBKYMLMZKNMKUWHNMUWFYEKYMYEKUUFWGZUVSWOYEUWHKYEKYMUWIU + VSWPZUWIWQYEUWHUWEKNYEKYLKUWIUVRUUDWRZWSWTXAYEUUPUUQUWCIJUWAUWCTUVQUVTY + EUWBUUIYEKYNUUFUVTXBUVJXCABUUIYNFRKBVIZLMZAVIZNMZUWCEUWMUUINMIUWNUUIUWM + NXJUWLYNTUWMUWBUUINUWLYNKLXJXAHXDXEYEYGKUWEUUINMZNMUWGYEYFUWPKNYEYFUWDU + UHNMZKLMUWPYEDUWQKLYEDUUHYLEMZUWQYEDUUHYLVHZEOZUWRYEYKEOZDUWTUUAYEUXADT + UUBYRIDEXFXKYEYKUWSEYEYSYKUWSTUUCYKFRXGSXHXIUUHYLEXLXMYEUUTYTUWQIJUWRUW + QTUVBUUDYEUWDUUHYEKYLUUFUUDXBZUVIXCABUUHYLFRUWOUWQEUWMUUHNMIUWNUUHUWMNX + JUWLYLTUWMUWDUUHNUWLYLKLXJXAHXDXEXNXAYEUWDUUHYEUWDUXBWGUVPXOXNWSYEKUWEU + UIUWIYEUWHUWEXTUWKUWJXPYEUUIUVJWGXQYAXRUUIYNEXLXSUUAUULUUNUUOYBUUBYRIUU + JYGEYCXKVFXHYEUUPUUQUUKYNTUVQUVTUUIYNFRYDVBXNWLWF $. $} $} @@ -140658,34 +140658,34 @@ with complex numbers (gaussian integers) instead, so that we only have cima csn cun cif cmpo c0 cmin ccnv cmpt cseq ciun wfo wf1o frechashgf1o c1 f1ofo ax-mp a1i foco syl2anc wne csuc wral wrex wa cfz oveq2 raleqdv rexbidv adantr wf f1of simpr ffvelrnd rspcdva f1ocnv mp2b simprl neeq2d - fveq2 simplrr cle wbr ad2antrr peano2 syl ffvelrni caddc clt frec2uzltd - elnn 0zd mpd frec2uzsucd breqtrd nn0leltp1 mpbird fznn0 mpbir2and fvco3 - wb sylancr f1ocnvfv2 fveq2d eqtrd 3netr4d ralrimiva neeq1d rexlimddv id - ralbidv rspcev dmeq opeq1d uneq12d ifeq12d imaeq2 eleq12d opeq2d uneq2d - sneqd ifbieq2d cbvmpov eqeq1 fvoveq1 cbvmptv eqid cbviunv ennnfonelemen - ) ABCDUAUBUCUDHIUHZUEUFDNUIUJZNUFOZUUBPZUUBUUDUMZQZUEOZUUHUUHUKZUUEULZU - NZUOZUPZUQZUUNUERUUHSTZURUUHVGUSUJIUTZPZUPZVAZSVBZUUSUGRUGOZUUTPZVCIJAR - DHVDNRIVDZNDUUBVDKUVCANRIVEZUVCBIMVFZNRIVHVIVJNRDHIVKVLAUCOZUUBPZUBOZUU - BPZVMZUBUDOZVNZVOZUCNVPZUDNAUVKNQZVQZFOZHPZEOZHPZVMZESUVKIPZVRUJZVOZUVN - FRUVPUWAESGOZVRUJZVOZFRVPZUWDFRVPGRUWBUWEUWBTZUWGUWDFRUWIUWAEUWFUWCUWEU - WBSVRVSVTWAAUWHGRVOUVOLWBUVPNRUVKINRIWCZUVPUVDUWJUVENRIWDVIZVJAUVOWEZWF - ZWGUVPUVQRQZUWDVQZVQZUVQUUPPZNQZUWQUUBPZUVIVMZUBUVLVOZUVNUWPRNUVQUUPRNU - UPWCZUWPUVDRNUUPVEUXBUVENRIWHRNUUPWDWIVJUVPUWNUWDWJZWFZUWPUWTUBUVLUWPUV - HUVLQZVQZUVRUVHIPZHPZUWSUVIUXFUWAUVRUXHVMEUWCUXGUVSUXGTUVTUXHUVRUVSUXGH - WLWKUVPUWNUWDUXEWMUXFUXGUWCQZUXGRQZUXGUWBWNWOZUXFUVHNQZUXJUXFUXEUVLNQZU - XLUWPUXEWEZUXFUVOUXMUVPUVOUWOUXEUWLWPZUVKWQWRZUVHUVLXCVLZNRUVHIUWKWSWRZ - UXFUXKUXGUWBVGWTUJZXAWOZUXFUXGUVLIPZUXSXAUXFUXEUXGUYAXAWOUXNUXFBUVHUVLS - IUXFXDZMUXQUXPXBXEUXFBUVKSIUYBMUXOXFXGUXFUXJUWBRQZUXKUXTXMUXRUVPUYCUWOU - XEUWMWPZUXGUWBXHVLXIUXFUYCUXIUXJUXKVQXMUYDUXGUWBXJWRXKWGUXFUWSUWQIPZHPZ - UVRUXFUWJUWRUWSUYFTUWKUWPUWRUXEUXDWBNRUWQHIXLXNUXFUYEUVQHUXFUVDUWNUYEUV - QTUVEUWPUWNUXEUXCWBNRUVQIXOXNXPXQUXFUWJUXLUVIUXHTUWKUXQNRUVHHIXLXNXRXSU - VMUXAUCUWQNUVFUWQTZUVJUWTUBUVLUYGUVGUWSUVIUVFUWQUUBWLXTYCYDVLYAXSUEUFBC - UUCNUUMCOZUUBPZUUBUYHUMZQZBOZUYLUYLUKZUYIULZUNZUOZUPUUGUYLUYLUYMUUEULZU - NZUOZUPUUHUYLTZUUGUUHUYLUULUYSUYTYBZUYTUUHUYLUUKUYRVUAUYTUUJUYQUYTUUIUY - MUUEUUHUYLYEYFYMYGYHUUDUYHTZUUGUYKUYSUYPUYLVUBUUEUYIUUFUYJUUDUYHUUBWLZU - UDUYHUUBYIYJVUBUYRUYOUYLVUBUYQUYNVUBUUEUYIUYMVUCYKYMYLYNYOMUEBRUURUYLST - ZURUYLVGUSUJUUPPZUPUYTUUOVUDUUQVUEURUUHUYLSYPUUHUYLVGUUPUSYQYNYRUUTYSUG - UARUVBUAOZUUTPUVAVUFUUTWLYTUUA $. + fveq2 simplrr cle wbr ad2antrr peano2 syl elnn ffvelcdmi clt frec2uzltd + caddc 0zd frec2uzsucd breqtrd wb nn0leltp1 mpbird fznn0 mpbir2and fvco3 + mpd sylancr f1ocnvfv2 fveq2d 3netr4d ralrimiva neeq1d ralbidv rexlimddv + eqtrd rspcev id dmeq opeq1d sneqd uneq12d ifeq12d imaeq2 eleq12d opeq2d + uneq2d ifbieq2d cbvmpov eqeq1 fvoveq1 cbvmptv eqid cbviunv + ennnfonelemen ) ABCDUAUBUCUDHIUHZUEUFDNUIUJZNUFOZUUBPZUUBUUDUMZQZUEOZUU + HUUHUKZUUEULZUNZUOZUPZUQZUUNUERUUHSTZURUUHVGUSUJIUTZPZUPZVAZSVBZUUSUGRU + GOZUUTPZVCIJARDHVDNRIVDZNDUUBVDKUVCANRIVEZUVCBIMVFZNRIVHVIVJNRDHIVKVLAU + COZUUBPZUBOZUUBPZVMZUBUDOZVNZVOZUCNVPZUDNAUVKNQZVQZFOZHPZEOZHPZVMZESUVK + IPZVRUJZVOZUVNFRUVPUWAESGOZVRUJZVOZFRVPZUWDFRVPGRUWBUWEUWBTZUWGUWDFRUWI + UWAEUWFUWCUWEUWBSVRVSVTWAAUWHGRVOUVOLWBUVPNRUVKINRIWCZUVPUVDUWJUVENRIWD + VIZVJAUVOWEZWFZWGUVPUVQRQZUWDVQZVQZUVQUUPPZNQZUWQUUBPZUVIVMZUBUVLVOZUVN + UWPRNUVQUUPRNUUPWCZUWPUVDRNUUPVEUXBUVENRIWHRNUUPWDWIVJUVPUWNUWDWJZWFZUW + PUWTUBUVLUWPUVHUVLQZVQZUVRUVHIPZHPZUWSUVIUXFUWAUVRUXHVMEUWCUXGUVSUXGTUV + TUXHUVRUVSUXGHWLWKUVPUWNUWDUXEWMUXFUXGUWCQZUXGRQZUXGUWBWNWOZUXFUVHNQZUX + JUXFUXEUVLNQZUXLUWPUXEWEZUXFUVOUXMUVPUVOUWOUXEUWLWPZUVKWQWRZUVHUVLWSVLZ + NRUVHIUWKWTWRZUXFUXKUXGUWBVGXCUJZXAWOZUXFUXGUVLIPZUXSXAUXFUXEUXGUYAXAWO + UXNUXFBUVHUVLSIUXFXDZMUXQUXPXBXMUXFBUVKSIUYBMUXOXEXFUXFUXJUWBRQZUXKUXTX + GUXRUVPUYCUWOUXEUWMWPZUXGUWBXHVLXIUXFUYCUXIUXJUXKVQXGUYDUXGUWBXJWRXKWGU + XFUWSUWQIPZHPZUVRUXFUWJUWRUWSUYFTUWKUWPUWRUXEUXDWBNRUWQHIXLXNUXFUYEUVQH + UXFUVDUWNUYEUVQTUVEUWPUWNUXEUXCWBNRUVQIXOXNXPYBUXFUWJUXLUVIUXHTUWKUXQNR + UVHHIXLXNXQXRUVMUXAUCUWQNUVFUWQTZUVJUWTUBUVLUYGUVGUWSUVIUVFUWQUUBWLXSXT + YCVLYAXRUEUFBCUUCNUUMCOZUUBPZUUBUYHUMZQZBOZUYLUYLUKZUYIULZUNZUOZUPUUGUY + LUYLUYMUUEULZUNZUOZUPUUHUYLTZUUGUUHUYLUULUYSUYTYDZUYTUUHUYLUUKUYRVUAUYT + UUJUYQUYTUUIUYMUUEUUHUYLYEYFYGYHYIUUDUYHTZUUGUYKUYSUYPUYLVUBUUEUYIUUFUY + JUUDUYHUUBWLZUUDUYHUUBYJYKVUBUYRUYOUYLVUBUYQUYNVUBUUEUYIUYMVUCYLYGYMYNY + OMUEBRUURUYLSTZURUYLVGUSUJUUPPZUPUYTUUOVUDUUQVUEURUUHUYLSYPUUHUYLVGUUPU + SYQYNYRUUTYSUGUARUVBUAOZUUTPUVAVUFUUTWLYTUUA $. $} ${ @@ -158870,8 +158870,8 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is $( Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) $) relogcl $p |- ( A e. RR+ -> ( log ` A ) e. RR ) $= - ( crp wcel clog cres cr fvres wf1o wf relogf1o f1of ax-mp ffvelrni eqeltrrd - cfv ) ABCADBEZOADOFABDGBFAPBFPHBFPIJBFPKLMN $. + ( crp wcel clog cres cfv cr fvres wf1o wf relogf1o ax-mp ffvelcdmi eqeltrrd + f1of ) ABCADBEZFADFGABDHBGAPBGPIBGPJKBGPOLMN $. $( Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) $) @@ -167529,12 +167529,12 @@ C_ if ( A. k e. suc J ( Q ` ( i e. _om $( Lemma for ~ nninfomni . (Contributed by Jim Kingdon, 10-Aug-2022.) $) nninfomnilem $p |- NN+oo e. Omni $= ( vp vr xnninf wcel cv cfv c0 wceq c1o wral wo c2o cvv syl wrex cmap co - comni wb nninfex isomnimap ax-mp cpr elmapi nninfself ffvelrni ffvelrnd - df2o3 eleqtrdi elpri wi fveqeq2 rspcev ex wa simpl nninfsel orim12d mpd - simpr mprgbir ) IUDJZGKZHKZLZMNZGIUAZVKONGIPZQZHRIUBUCZISJVHVOHVPPUEUFG - IHSUGUHVJVPJZVJDLZVJLZMNZVSONZQZVOVQVSMOUIZJWBVQVSRWCVQIRVRVJVJRIUJVPIV - JDABCDEFUKULZUMUNUOVSMOUPTVQVTVMWAVNVQVRIJZVTVMUQWDWEVTVMVLVTGVRIVIVRMV - JURUSUTTVQWAVNVQWAVAVJABCDEGFVQWAVBVQWAVFVCUTVDVEVG $. + comni wb nninfex isomnimap ax-mp cpr nninfself ffvelcdmi ffvelrnd df2o3 + elmapi eleqtrdi elpri wi fveqeq2 rspcev ex simpl simpr nninfsel orim12d + wa mpd mprgbir ) IUDJZGKZHKZLZMNZGIUAZVKONGIPZQZHRIUBUCZISJVHVOHVPPUEUF + GIHSUGUHVJVPJZVJDLZVJLZMNZVSONZQZVOVQVSMOUIZJWBVQVSRWCVQIRVRVJVJRIUNVPI + VJDABCDEFUJUKZULUMUOVSMOUPTVQVTVMWAVNVQVRIJZVTVMUQWDWEVTVMVLVTGVRIVIVRM + VJURUSUTTVQWAVNVQWAVEVJABCDEGFVQWAVAVQWAVBVCUTVDVFVG $. $} $}