diff --git a/changes-set.txt b/changes-set.txt index ee1a9cde67..13aa655ffa 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -92,6 +92,10 @@ make a github issue.) DONE: Date Old New Notes + 7-Jan-25 rhmdvdsr [same] Moved from TA's mathbox to main set.mm + 7-Jan-25 rhmopp [same] Moved from TA's mathbox to main set.mm + 7-Jan-25 elrhmunit [same] Moved from TA's mathbox to main set.mm + 7-Jan-25 rhmunitinv [same] Moved from TA's mathbox to main set.mm 7-Jan-25 ringi ringdilem 5-Jan-25 nfrexd nfrexdw consistent with nfraldw 5-Jan-25 nfrex nfrexw consistent with nfralw @@ -281,7 +285,7 @@ Date Old New Notes 26-Jun-24 rp-imass resssxp moved from RP's mathbox to main set.mm 26-Jun-24 sscon34b [same] moved from RP's mathbox to main set.mm 26-Jun-24 rcompleq [same] moved from RP's mathbox to main set.mm -26-Jun-24 funresd [same] moved from GS's mathbox to main set.mm +26-Jun-24 funresd [same] moved from GS's mathbox to main set.mmisCyclic_of_subgroup_isDomain 26-Jun-24 cmnmndd [same] moved from SN's mathbox to main set.mm 26-Jun-24 syl6req eqtr2di compare to eqtr2i or eqtr2d 16-Jun-24 syl6eqr eqtr4di compare to eqtr4i or eqtr4d diff --git a/set.mm b/set.mm index 39bf91b21e..4ce473946d 100644 --- a/set.mm +++ b/set.mm @@ -254130,6 +254130,82 @@ irreducible elements (see ~ df-irred ). (Contributed by Mario Carneiro, $} + ${ + $d c y A $. $d c y B $. $d c y F $. $d c R $. $d c y S $. $d c X $. + $d c .|| $. + rhmdvdsr.x $e |- X = ( Base ` R ) $. + rhmdvdsr.m $e |- .|| = ( ||r ` R ) $. + rhmdvdsr.n $e |- ./ = ( ||r ` S ) $. + $( A ring homomorphism preserves the divisibility relation. (Contributed + by Thierry Arnoux, 22-Oct-2017.) $) + rhmdvdsr $p |- ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) + /\ A .|| B ) -> ( F ` A ) ./ ( F ` B ) ) $= + ( vy vc co wcel wa cfv wceq wrex syl2anc crh w3a wbr cbs cv simpl1 simpl2 + cmulr eqid rhmf ffvelcdmda simpll1 ralrimiva adantr rhmmul syl3anc dvdsr2 + wral simpr biimpac r19.29 simpl fveq2d eqtr3d reximi syl eqeq1d rexlimivw + oveq1 rspcev dvdsr sylanbrc ) GEFUANOZAHOZBHOZUBZABCUCZPZAGQZFUDQZOZLUEZV + SFUHQZNZBGQZRZLVTSZVSWEDUCVRVMVNWAVMVNVOVQUFVMVNVOVQUGZVMHVTAGHVTEFGIVTUI + ZUJZUKTVRMUEZGQZVTOZWLVSWCNZWERZPZMHSZWGVRWMMHURWOMHSZWQVRWMMHVRWKHOZPZVM + WSWMVMVNVOVQWSULZVRWSUSZVMHVTWKGWJUKTUMVRWKAEUHQZNZGQZWNRZMHURZXDBRZMHSZW + RVRXFMHWTVMWSVNXFXAXBVRVNWSWHUNWKAEFXCWCGHIXCUIZWCUIZUOUPUMVRVQVNXIVPVQUS + WHVNVQXIMHCEXCABIJXJUQUTTXGXIPXFXHPZMHSWRXFXHMHVAXLWOMHXLXEWNWEXFXHVBXLXD + BGXFXHUSVCVDVEVFTWMWOMHVATWPWGMHWFWOLWLVTWBWLRWDWNWEWBWLVSWCVIVGVJVHVFLVT + DFWCVSWEWIKXKVKVL $. + $} + + ${ + $d x y F $. $d x y R $. $d x y S $. + $( A ring homomorphism is also a ring homomorphism for the opposite rings. + (Contributed by Thierry Arnoux, 27-Oct-2017.) $) + rhmopp $p |- ( F e. ( R RingHom S ) + -> F e. ( ( oppR ` R ) RingHom ( oppR ` S ) ) ) $= + ( vx vy co wcel coppr cfv cbs cmulr cur eqid opprringb sylib oppr1 eqcomi + crg cv wa rhmrcl1 rhmrcl2 rhm1 wceq simpl simprr opprbas eleqtrrdi simprl + crh rhmmul syl3anc opprmul fveq2i 3eqtr4g cgrp wf cplusg wral ringgrp syl + cghm rhmf rhmghm ad2antrr simplr simpr ghmlin ralrimiva jca jca31 oppradd + isghm sylibr isrhm2d ) CABUJFGZDEAHIZJIZVQBHIZVQKIZVSKIZVQLIZCVSLIZVRMWBM + WCMVTMZWAMZVPARGVQRGZABCUAAVQVQMZNOZVPBRGVSRGZABCUBBVSVSMZNOZABWBCWCALIZW + BAWLVQWGWLMPQBLIZWCBWMVSWJWMMPQUCVPDSZVRGZESZVRGZTZTZWPWNAKIZFZCIZWPCIZWN + CIZBKIZFZWNWPVTFZCIXDXCWAFWSVPWPAJIZGZWNXHGZXBXFUDVPWRUEWSWPVRXHVPWOWQUFX + HAVQWGXHMZUGZUHWSWNVRXHVPWOWQUIXLUHWPWNABWTXECXHXKWTMZXEMZUKULXGXACXHAVTW + TVQWNWPXKXMWGWDUMUNBJIZBWAXEVSXDXCXOMZXNWJWEUMUOVPVQUPGZVSUPGZTXHXOCUQZWN + WPAURIZFCIXDXCBURIZFUDZEXHUSZDXHUSZTZTCVQVSVBFGVPXQXRYEVPWFXQWHVQUTVAVPWI + XRWKVSUTVAVPXSYDXHXOABCXKXPVCVPYCDXHVPXJTZYBEXHYFXITCABVBFGZXJXIYBVPYGXJX + IABCVDVEVPXJXIVFYFXIVGXTYAABWNCWPXHXKXTMZYAMZVHULVIVIVJVKEDXTYAVQVSCXHXOX + LXOBVSWJXPUGXTAVQWGYHVLYABVSWJYIVLVMVNVO $. + $} + + $( Ring homomorphisms preserve unit elements. (Contributed by Thierry + Arnoux, 23-Oct-2017.) $) + elrhmunit $p |- ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) + -> ( F ` A ) e. ( Unit ` S ) ) $= + ( crh co wcel cui cfv wa cur cdsr wbr coppr isunit rhmdvdsr syl31anc adantr + eqid wb cbs simpl unitss simpr sselid crg rhmrcl1 ringidcl 3syl simpld rhm1 + sylib breq2d mpbid rhmopp simprd opprbas sylanbrc ) DBCEFGZABHIZGZJZADIZCKI + ZCLIZMZVCVDCNIZLIZMZVCCHIZGVBVCBKIZDIZVEMZVFVBUSABUAIZGZVKVNGZAVKBLIZMZVMUS + VAUBZVBUTVNAVNBUTVNSZUTSZUCUSVAUDZUEZVBUSBUFGVPVSBCDUGVNBVKVTVKSZUHUIZVBVRA + VKBNIZLIZMZVBVAVRWHJWBVQBWFUTVKWGAWAWDVQSZWFSZWGSZOULZUJAVKVQVEBCDVNVTWIVES + ZPQUSVMVFTVAUSVLVDVCVEBCVKDVDWDVDSZUKZUMRUNVBVCVLVHMZVIVBDWFVGEFGZVOVPWHWPU + SWQVABCDUORWCWEVBVRWHWLUPAVKWGVHWFVGDVNVNBWFWJVTUQWKVHSZPQUSWPVITVAUSVLVDVC + VHWOUMRUNVECVGVJVDVHVCVJSWNWMVGSWROUR $. + + $( Ring homomorphisms preserve the inverse of unit elements. (Contributed by + Thierry Arnoux, 23-Oct-2017.) $) + rhmunitinv $p |- ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) + -> ( F ` ( ( invr ` R ) ` A ) ) = ( ( invr ` S ) ` ( F ` A ) ) ) $= + ( co wcel cui cfv cinvr cmulr wceq cur eqid unitlinv sylan unitinvcl sselid + crg adantr elrhmunit crh rhmrcl1 fveq2d cbs simpl unitss simpr syl3anc rhm1 + wa rhmmul 3eqtr3d rhmrcl2 syl2anc eqtr4d cmgp cress cgrp unitgrp syl syldan + unitgrpbas cvv cplusg fvex mgpplusg ressplusg ax-mp grprcan syl13anc mpbid + wb ) DBCUAEFZABGHZFZUJZABIHZHZDHZADHZCJHZEZVTCIHZHZVTWAEZKZVSWDKZVPWBCLHZWE + VPVRABJHZEZDHZBLHZDHZWBWHVPWJWLDVMBRFZVOWJWLKBCDUBZBWIVNWLVQAVNMZVQMZWIMZWL + MZNOUCVPVMVRBUDHZFAWTFWKWBKVMVOUEVPVNWTVRWTBVNWTMZWPUFZVMWNVOVRVNFZWOBVNVQA + WPWQPOZQVPVNWTAXBVMVOUGQVRABCWIWADWTXAWRWAMZUKUHVMWMWHKVOBCWLDWHWSWHMZUISUL + VPCRFZVTCGHZFZWEWHKVMXGVOBCDUMZSZABCDTZCWAXHWHWCVTXHMZWCMZXEXFNUNUOVPCUPHZX + HUQEZURFZVSXHFZWDXHFZXIWFWGVLVMXQVOVMXGXQXJCXHXPXMXPMZUSUTSVMVOXCXRXDVRBCDT + VAVPXGXIXSXKXLCXHWCVTXMXNPUNXLXHWAXPVSWDVTCXHXPXMXTVBXHVCFWAXPVDHKCGVEXHWAX + OXPVCXTCWAXOXOMXEVFVGVHVIVJVK $. + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# Division rings and fields @@ -485305,65 +485381,6 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) - ${ - $d c y A $. $d c y B $. $d c y F $. $d c R $. $d c y S $. $d c X $. - $d c .|| $. - rhmdvdsr.x $e |- X = ( Base ` R ) $. - rhmdvdsr.m $e |- .|| = ( ||r ` R ) $. - rhmdvdsr.n $e |- ./ = ( ||r ` S ) $. - $( A ring homomorphism preserves the divisibility relation. (Contributed - by Thierry Arnoux, 22-Oct-2017.) $) - rhmdvdsr $p |- ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) - /\ A .|| B ) -> ( F ` A ) ./ ( F ` B ) ) $= - ( vy vc co wcel wa cfv wceq wrex syl2anc crh w3a wbr cbs cv simpl1 simpl2 - cmulr eqid rhmf ffvelcdmda simpll1 ralrimiva adantr rhmmul syl3anc dvdsr2 - wral simpr biimpac r19.29 simpl fveq2d eqtr3d reximi syl eqeq1d rexlimivw - oveq1 rspcev dvdsr sylanbrc ) GEFUANOZAHOZBHOZUBZABCUCZPZAGQZFUDQZOZLUEZV - SFUHQZNZBGQZRZLVTSZVSWEDUCVRVMVNWAVMVNVOVQUFVMVNVOVQUGZVMHVTAGHVTEFGIVTUI - ZUJZUKTVRMUEZGQZVTOZWLVSWCNZWERZPZMHSZWGVRWMMHURWOMHSZWQVRWMMHVRWKHOZPZVM - WSWMVMVNVOVQWSULZVRWSUSZVMHVTWKGWJUKTUMVRWKAEUHQZNZGQZWNRZMHURZXDBRZMHSZW - RVRXFMHWTVMWSVNXFXAXBVRVNWSWHUNWKAEFXCWCGHIXCUIZWCUIZUOUPUMVRVQVNXIVPVQUS - WHVNVQXIMHCEXCABIJXJUQUTTXGXIPXFXHPZMHSWRXFXHMHVAXLWOMHXLXEWNWEXFXHVBXLXD - BGXFXHUSVCVDVEVFTWMWOMHVATWPWGMHWFWOLWLVTWBWLRWDWNWEWBWLVSWCVIVGVJVHVFLVT - DFWCVSWEWIKXKVKVL $. - $} - - ${ - $d x y F $. $d x y R $. $d x y S $. - $( A ring homomorphism is also a ring homomorphism for the opposite rings. - (Contributed by Thierry Arnoux, 27-Oct-2017.) $) - rhmopp $p |- ( F e. ( R RingHom S ) - -> F e. ( ( oppR ` R ) RingHom ( oppR ` S ) ) ) $= - ( vx vy co wcel coppr cfv cbs cmulr cur eqid opprringb sylib oppr1 eqcomi - crg cv wa rhmrcl1 rhmrcl2 rhm1 wceq simpl simprr opprbas eleqtrrdi simprl - crh rhmmul syl3anc opprmul fveq2i 3eqtr4g cgrp wf cplusg wral ringgrp syl - cghm rhmf rhmghm ad2antrr simplr simpr ghmlin ralrimiva jca jca31 oppradd - isghm sylibr isrhm2d ) CABUJFGZDEAHIZJIZVQBHIZVQKIZVSKIZVQLIZCVSLIZVRMWBM - WCMVTMZWAMZVPARGVQRGZABCUAAVQVQMZNOZVPBRGVSRGZABCUBBVSVSMZNOZABWBCWCALIZW - BAWLVQWGWLMPQBLIZWCBWMVSWJWMMPQUCVPDSZVRGZESZVRGZTZTZWPWNAKIZFZCIZWPCIZWN - CIZBKIZFZWNWPVTFZCIXDXCWAFWSVPWPAJIZGZWNXHGZXBXFUDVPWRUEWSWPVRXHVPWOWQUFX - HAVQWGXHMZUGZUHWSWNVRXHVPWOWQUIXLUHWPWNABWTXECXHXKWTMZXEMZUKULXGXACXHAVTW - TVQWNWPXKXMWGWDUMUNBJIZBWAXEVSXDXCXOMZXNWJWEUMUOVPVQUPGZVSUPGZTXHXOCUQZWN - WPAURIZFCIXDXCBURIZFUDZEXHUSZDXHUSZTZTCVQVSVBFGVPXQXRYEVPWFXQWHVQUTVAVPWI - XRWKVSUTVAVPXSYDXHXOABCXKXPVCVPYCDXHVPXJTZYBEXHYFXITCABVBFGZXJXIYBVPYGXJX - IABCVDVEVPXJXIVFYFXIVGXTYAABWNCWPXHXKXTMZYAMZVHULVIVIVJVKEDXTYAVQVSCXHXOX - LXOBVSWJXPUGXTAVQWGYHVLYABVSWJYIVLVMVNVO $. - $} - - $( Ring homomorphisms preserve unit elements. (Contributed by Thierry - Arnoux, 23-Oct-2017.) $) - elrhmunit $p |- ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) - -> ( F ` A ) e. ( Unit ` S ) ) $= - ( crh co wcel cui cfv wa cur cdsr wbr coppr isunit rhmdvdsr syl31anc adantr - eqid wb cbs simpl unitss simpr sselid crg rhmrcl1 ringidcl 3syl simpld rhm1 - sylib breq2d mpbid rhmopp simprd opprbas sylanbrc ) DBCEFGZABHIZGZJZADIZCKI - ZCLIZMZVCVDCNIZLIZMZVCCHIZGVBVCBKIZDIZVEMZVFVBUSABUAIZGZVKVNGZAVKBLIZMZVMUS - VAUBZVBUTVNAVNBUTVNSZUTSZUCUSVAUDZUEZVBUSBUFGVPVSBCDUGVNBVKVTVKSZUHUIZVBVRA - VKBNIZLIZMZVBVAVRWHJWBVQBWFUTVKWGAWAWDVQSZWFSZWGSZOULZUJAVKVQVEBCDVNVTWIVES - ZPQUSVMVFTVAUSVLVDVCVEBCVKDVDWDVDSZUKZUMRUNVBVCVLVHMZVIVBDWFVGEFGZVOVPWHWPU - SWQVABCDUORWCWEVBVRWHWLUPAVKWGVHWFVGDVNVNBWFWJVTUQWKVHSZPQUSWPVITVAUSVLVDVC - VHWOUMRUNVECVGVJVDVHVCVJSWNWMVGSWROUR $. - $( @{ rhmdvr.u @e |- U = ( Unit ` R ) @. @@ -485398,23 +485415,6 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a GIUOVLJWGEFILWGTZUPUNWCUQVCVGVIVKURVCVGVIVKUSWGDFVQHVPVHVJWHKMWEUTVAVB $. $} - $( Ring homomorphisms preserve the inverse of unit elements. (Contributed by - Thierry Arnoux, 23-Oct-2017.) $) - rhmunitinv $p |- ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) - -> ( F ` ( ( invr ` R ) ` A ) ) = ( ( invr ` S ) ` ( F ` A ) ) ) $= - ( co wcel cui cfv cinvr cmulr wceq cur eqid unitlinv sylan unitinvcl sselid - crg adantr elrhmunit crh rhmrcl1 fveq2d cbs simpl unitss simpr syl3anc rhm1 - wa rhmmul 3eqtr3d rhmrcl2 syl2anc eqtr4d cmgp cress cgrp unitgrp syl syldan - unitgrpbas cvv cplusg fvex mgpplusg ressplusg ax-mp grprcan syl13anc mpbid - wb ) DBCUAEFZABGHZFZUJZABIHZHZDHZADHZCJHZEZVTCIHZHZVTWAEZKZVSWDKZVPWBCLHZWE - VPVRABJHZEZDHZBLHZDHZWBWHVPWJWLDVMBRFZVOWJWLKBCDUBZBWIVNWLVQAVNMZVQMZWIMZWL - MZNOUCVPVMVRBUDHZFAWTFWKWBKVMVOUEVPVNWTVRWTBVNWTMZWPUFZVMWNVOVRVNFZWOBVNVQA - WPWQPOZQVPVNWTAXBVMVOUGQVRABCWIWADWTXAWRWAMZUKUHVMWMWHKVOBCWLDWHWSWHMZUISUL - VPCRFZVTCGHZFZWEWHKVMXGVOBCDUMZSZABCDTZCWAXHWHWCVTXHMZWCMZXEXFNUNUOVPCUPHZX - HUQEZURFZVSXHFZWDXHFZXIWFWGVLVMXQVOVMXGXQXJCXHXPXMXPMZUSUTSVMVOXCXRXDVRBCDT - VAVPXGXIXSXKXLCXHWCVTXMXNPUNXLXHWAXPVSWDVTCXHXPXMXTVBXHVCFWAXPVDHKCGVEXHWAX - OXPVCXTCWAXOXOMXEVFVGVHVIVJVK $. - $( @{ rhmuntghm.1 @e |- G = ( ( mulGrp ` R ) |`s ( Unit ` R ) ) @. @@ -652900,6 +652900,161 @@ fixed reference functional determined by this vector (corresponding to IEXKFXPVNAXGBWQHCIEXKFXPVOVPVQ $. $} + ${ + $d A a b $. $d F a b $. $d a b ph $. + fldhmf1.1 $e |- ( ph -> K e. Field ) $. + fldhmf1.2 $e |- ( ph -> L e. Field ) $. + fldhmf1.3 $e |- ( ph -> F e. ( K RingHom L ) ) $. + fldhmf1.4 $e |- A = ( Base ` K ) $. + fldhmf1.5 $e |- B = ( Base ` L ) $. + $( A field homomorphism is injective. This follows immediately from the + definition of the ring homomorphism that sends the multiplicative + identity to the multiplicative identity. (Contributed by metakunt, + 7-Jan-2025.) $) + fldhmf1 $p |- ( ph -> F : A -1-1-> B ) $= + ( wne cfv wa co wcel syl wceq eqid syl2anc va vb wf wral wf1 crh rhmf c0g + cv wi cur cminusg cplusg cinvr cmulr cghm ad4antr rhmghm simp-4r cgrp cdr + cfield isfld simpld drnggrp simpllr grpinvcl ghmlin syl3anc ghminv oveq2d + ccrg sylib simpr oveq1d crg ad3antrrr drngring ringgrpd ffvelcdmd grprinv + adantr eqtrd grpcl grpinvinv simplr necomd eqnetrd wb grpinvid2 necon3bid + cui w3a jca drngunit mpbird rhmunitinv elrhmunit unitinvcl biimpd eqeltrd + mpd ringlz eqcomd simprd crngringd unitcl eqcomi eleqtrdi rhmmul unitrinv + cbs fveq2d rhm1 3eqtrd drngunz neneqd pm2.65da neqned ex ralrimiva dff14a + mpbid sylibr ) ABCDUCZUAUIZUBUIZLZYFDMZYGDMZLZUJZUBBUDZUABUDZNBCDUEAYEYNA + DEFUFOPZYEIBCEFDJKUGZQAYMUABAYFBPZNZYLUBBYRYGBPZNZYHYKYTYHNZYIYJUUAYIYJRZ + FUHMZFUKMZRUUAUUBNZUUCYFYGEULMZMZEUMMZOZDMZUUIEUNMZMZDMZFUOMZOZUUIUULEUOM + ZOZDMZUUDUUEUUOUUCUUEUUOUUCUUMUUNOZUUCUUEUUJUUCUUMUUNUUEUUJYIUUGDMZFUMMZO + ZUUCUUEDEFUPOPZYQUUGBPZUUJUVBRUUEYOUVCAYOYQYSYHUUBIUQZEFDURQZAYQYSYHUUBUS + ZUUEEUTPZYSUVDUUEEVAPZUVHAUVIYQYSYHUUBAUVIEVLPZAEVBPUVIUVJNGEVCVMZVDUQZEV + EQZYRYSYHUUBVFZBEUUFYGJUUFSZVGTZUUHUVAEFYFDUUGBJUUHSZUVASZVHVIUUEUVBYIYJF + ULMZMZUVAOZUUCUUEUUTUVTYIUVAUUEUVCYSUUTUVTRUVFUVNBEFDUUFUVSYGJUVOUVSSZVJT + VKUUEUWAYJUVTUVAOZUUCUUEYIYJUVTUVAUUAUUBVNVOUUEFUTPYJCPUWCUUCRUUEFUUEFVAP + ZFVPPZUUAUWDUUBUUAUWDFVLPZUUAFVBPZUWDUWFNAUWGYQYSYHHVQFVCVMVDZWBZFVRQZVSU + UEBCYGDUUEYOYEUVEYPQUVNVTCUVAFUVSYJUUCKUVRUUCSZUWBWATWCWCWCVOUUEUWEUUMCPZ + NUUSUUCRUUEUWEUWLUWJUUEUUMUUJFUNMZMZCUUEYOUUIEWLMZPZUUMUWNRUVEUUEUWPUUIBP + ZUUIEUHMZLZNZUUEUWQUWSUUEUVHYQUVDUWQUVMUVGUVPBUUHEYFUUGJUVQWDVIZUUEUUGUUF + MZYFLZUWSUUEUXBYGYFUUEUVHYSUXBYGRUVMUVNBEUUFYGJUVOWETUUEYFYGYTYHUUBWFWGWH + UUEUVHUVDYQUXCUWSWIUVMUVPUVGUVHUVDYQWMUXBYFUUIUWRBUUHEUUFUUGYFUWRJUVQUWRS + ZUVOWJWKVIYCWNUUEUVIUWPUWTWIUVLBEUWOUUIUWRJUWOSZUXDWOQWPZUUIEFDWQTUUEUWNC + PZUWNUUCLZUUEUWNFWLMZPZUXGUXHNZUUEUWEUUJUXIPZUXJUWJUUEYOUWPUXLUVEUXFUUIEF + DWRTFUXIUWMUUJUXISZUWMSWSTUUEUXJUXKUUEUWDUXJUXKWIUWICFUXIUWNUUCKUXMUWKWOQ + WTXBVDXAWNCFUUNUUMUUCKUUNSZUWKXCQWCXDUUEUURUUOUUEYOUWQUULBPZUURUUORUVEUXA + UUEUULUWOPZUXOUUEEVPPZUWPUXPAUXQYQYSYHUUBAEAUVIUVJUVKXEXFUQUXFEUWOUUKUUIU + XEUUKSZWSTUXPUULEXLMZBUXSEUWOUULUXSSUXEXGBUXSJXHXIQUUIUULEFUUPUUNDBJUUPSZ + UXNXJVIXDUUEUUREUKMZDMZUUDUUEUUQUYADUUEUXQUWPUUQUYARUUEUVIUXQUVLEVRQUXFEU + UPUWOUYAUUKUUIUXEUXRUXTUYASZXKTXMUUEYOUYBUUDRUVEEFUYADUUDUYCUUDSZXNQWCXOU + UEUUCUUDUUAUUCUUDLUUBUUAUUDUUCUUAUWDUUDUUCLUWHFUUDUUCUWKUYDXPQWGWBXQXRXSX + TYAYAWNUAUBBCDYBYD $. + $} + + ${ + $d N a k l $. $d P a k l $. $d a ph $. + aks6d1c2p1.1 $e |- ( ph -> N e. NN ) $. + aks6d1c2p1.2 $e |- ( ph -> P e. Prime ) $. + aks6d1c2p1.3 $e |- ( ph -> P || N ) $. + aks6d1c2p1.4 $e |- E = ( k e. NN0 , l e. NN0 |-> + ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) $. + $( In the AKS-theorem the subset defined by ` E ` takes values in the + positive integers. (Contributed by metakunt, 7-Jan-2025.) $) + aks6d1c2p1 $p |- ( ph -> E : ( NN0 X. NN0 ) --> NN ) $= + ( va cn0 cv cfv cexp co cmul cn wcel syl cxp c1st cdiv c2nd cprime adantr + wa prmnn simpr xp1st nnexpcld cdvds wbr wb nndivdvds mpbid xp2nd nnmulcld + jca cmpo cmpt cop wceq vex op1std oveq2d op2ndd mpompt eqcomi eqtri fmptd + oveq12d ) AKLLUAZBKMZUBNZOPZEBUCPZVNUDNZOPZQPZRDAVNVMSZUGZVPVSWBBVOABRSZW + AABUESWCHBUHTZUFWBWAVOLSAWAUIZVNLLUJTUKWBVQVRAVQRSZWAABEULUMZWFIAERSZWCUG + WGWFUNAWHWCGWDUSEBUOTUPUFWBWAVRLSWEVNLLUQTUKURDCFLLBCMZOPZVQFMZOPZQPZUTZK + VMVTVAZJWOWNCFKLLVTWMVNWIWKVBVCZVPWJVSWLQWPVOWIBOWIWKVNCVDZFVDZVEVFWPVRWK + VQOWIWKVNWQWRVGVFVLVHVIVJVK $. + $} + + ${ + $d E a b c d $. $d N k l $. $d N p $. $d P k l $. $d P p $. $d Q p $. + $d a b c d k l ph $. $d a b c d p ph $. + aks6d1c2p2.1 $e |- ( ph -> N e. NN ) $. + aks6d1c2p2.2 $e |- ( ph -> P e. Prime ) $. + aks6d1c2p2.3 $e |- ( ph -> P || N ) $. + aks6d1c2p2.4 $e |- E = ( k e. NN0 , l e. NN0 |-> + ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) $. + aks6d1c2p2.5 $e |- ( ph -> Q e. Prime ) $. + aks6d1c2p2.6 $e |- ( ph -> Q || N ) $. + aks6d1c2p2.7 $e |- ( ph -> P =/= Q ) $. + $( Injective condition for countability argument assuming that ` N ` is not + a prime power. (Contributed by metakunt, 7-Jan-2025.) $) + aks6d1c2p2 $p |- ( ph -> E : ( NN0 X. NN0 ) -1-1-> NN ) $= + ( cn0 co wceq wa wcel syl va vb vc vd vp cxp cn wf cv wral wf1 aks6d1c2p1 + wi wn wne cexp cdiv cmul neneq orcd simpr neneqd olcd jaoi anim1ci adantl + wo neqne pm2.61dan impbii orcom bitri ianor bicomi cpc cprime wrex oveq1d + ad5antr neeq12d caddc cc0 0cnd cdvds wbr prmnn jca nndivdvds mpbid adantr + ad2antrr simp-4r nnexpcld pccld nn0cnd simplr simp-5l nncnd nnne0d eqcomd + wb divcan2d breq2d cz nnzd euclemma syl3anc biimpd mpd c1 necom mpbi 1red + imbi2i mpbird ad4antr simpllr nn0zd 3jca pcexp 3netr3d prmdvdsexpr zexpcl + w3a pceq0 expne0d pcmul rspcedvd pcidlem simprl oveq2d biidd nnnn0d bitrd + nnmulcld a1i simprr oveq12d ovmpod ralrimiva prmgt1 ltned sylib dvdsprime + clt necomd pm4.56 syl2anc mtbird pcelnn mulcan2d necon3bid cq nnq divne0d + orcnd addneintrd con3d divcld simp-5r addneintr2d eqidd jaodan necon3abid + mtod pc11 notbid rexnal necon3bbid rexbidv sylan2br ex con4d f1opr sylibr + cmpo ) AOOUFZUGEUHZUAUIZUBUIZEPZUCUIZUDUIZEPZQZUVSUWBQZUVTUWCQZRZUMZUDOUJ + ZUCOUJZUBOUJZUAOUJZRUVQUGEUKAUVRUWMABDEFGHIJKULAUWLUAOAUVSOSZRZUWKUBOUWOU + VTOSZRZUWJUCOUWQUWBOSZRZUWIUDOUWSUWCOSZRZUWHUWEUXAUWHUNZUWEUNUXAUXBRZUWAU + WDUXCUWAUWDUOZBUVSUPPZFBUQPZUVTUPPZURPZBUWBUPPZUXFUWCUPPZURPZUOZUXBUXAUVT + UWCUOZUWGUVSUWBUOZRZVGZUXLUXPUWFUNZUWGUNZVGZUXBUXPUXRUXQVGZUXSUXPUXTUXMUX + TUXOUXMUXRUXQUVTUWCUSUTUXOUXQUXRUXOUVSUWBUWGUXNVAZVBVCVDUXRUXPUXQUXRUXMUX + OUVTUWCVHUTZUXQUWGUXPUXQUWGRUXOUXMUXQUXNUWGUVSUWBVHVEVCUXRUXPUXQUYBVFVIVD + VJUXRUXQVKVLUXBUXSUWFUWGVMVNVLUXAUXPRUXLUEUIZUXHVOPZUYCUXKVOPZUOZUEVPVQZU + XAUXMUYGUXOUXAUXMRZUYFCUXHVOPZCUXKVOPZUOUECVPACVPSZUWNUWPUWRUWTUXMLVSZUYH + UYCCQZRZUYDUYIUYEUYJUYNUYCCUXHVOUYHUYMVAZVRUYNUYCCUXKVOUYOVRVTUYHCUXEVOPZ + CUXGVOPZWAPZCUXIVOPZCUXJVOPZWAPZUYIUYJUYHWBUYQWAPZWBUYTWAPZUYRVUAUYHWBUYQ + UYTUYHWCUYHUYQUYHCUXGUYLUYHUXFUVTUXAUXFUGSZUXMUWQVUDUWRUWTUWOVUDUWPAVUDUW + NABFWDWEZVUDJAFUGSZBUGSZRVUEVUDXAAVUFVUGHABVPSZVUGIBWFZTZWGFBWHTWIZWJWJZW + KZWJZUWOUWPUWRUWTUXMWLZWMWNWOUYHUYTUYHCUXJUYLUYHUXFUWCVUNUWSUWTUXMWPZWMWN + WOUYHUVTCUXFVOPZURPZUWCVUQURPZUYQUYTUYHVURVUSUOUXMUXAUXMVAUYHVURVUSUVTUWC + UYHUVTUWCVUQUYHUVTVUOWOUYHUWCVUPWOUYHVUQUYHCUXFUYLVUNWNWOUYHVUQUYHAVUQUGS + ZAUWNUWPUWRUWTUXMWQAVUTCUXFWDWEZACBWDWEZVVAACBUXFURPZWDWEZVVBVVAVGZACFWDW + EVVDMAFVVCCWDAVVCFAFBAFHWRABVUJWRABVUJWSXBWTXCWIAVVDVVEAUYKBXDSZUXFXDSZVV + DVVEXALABVUJXEAUXFVUKXECBUXFXFXGXHXIAVVBCBQZCXJQZVGZAVVHUNZVVIUNZRVVJUNAV + VKVVLACBABCUOZUMACBUOZUMNVVMVVNABCXKXNXLVBZACXJAXJCAXJCAXMAUYKXJCUUEWELCU + UATUUBUUFVBWGVVHVVIUUGUUCAVUHCUGSZVVBVVJXAIAUYKVVPLCWFTBCUUDUUHUUIUUPAUYK + VUDRVUTVVAXAAUYKVUDLVUKWGCUXFUUJTXOTWSUUKUULXOUYHUYQVURUXAUYQVURQZUXMUXAU + YKUXFUUMSZUXFWBUOZRZUVTXDSZYDVVQUXAUYKVVTVWAAUYKUWNUWPUWRUWTLXPZUXAVVRVVS + UXAVUDVVRVUMUXFUUNTUXAFBUXAFAVUFUWNUWPUWRUWTHXPZWRZUXABUWQVUGUWRUWTUWOVUG + UWPAVUGUWNVUJWJWJZWKZWRZUXAFVWCWSUXABVWFWSZUUOZWGZUXAUVTUWOUWPUWRUWTXQZXR + ZXSUXFCUVTXTTWJWTUYHUYTVUSUXAUYTVUSQZUXMUXAUYKVVTUWCXDSZYDVWMUXAUYKVVTVWN + VWBVWJUXAUWCUWSUWTVAZXRXSUXFCUWCXTTWJWTYAUUQUXAVUBUYRQUXMUXAWBUYPUYQWAUXA + UYPWBUXAUYPWBQZCUXEWDWEZUNZUXAVVKVWRAVVKUWNUWPUWRUWTVVOXPZUXAVWQVVHUXAUYK + VUHUWNVWQVVHUMVWBAVUHUWNUWPUWRUWTIXPZAUWNUWPUWRUWTWLZCBUVSYBXGUURXIUXAUYK + UXEUGSZRVWPVWRXAUXAUYKVXBVWBUWQVXBUWRUWTUWQBUVSVWEAUWNUWPWPWMZWKWGCUXEYET + XOWTVRWJUXAVUCVUAQUXMUXAWBUYSUYTWAUXAUYSWBUXAUYSWBQZCUXIWDWEZUNZUXAVXEVVH + VWSUXAUYKVUHUWRVXEVVHUMVWBVWTUWQUWRUWTWPZCBUWBYBXGUVEUXAUYKUXIUGSZRVXDVXF + XAUXAUYKVXHVWBUXABUWBVWFVXGWMZWGCUXIYETXOWTVRWJYAUYHUYIUYRUXAUYIUYRQZUXMU + XAUYKUXEXDSZUXEWBUOZRZUXGXDSZUXGWBUOZRZYDVXJUXAUYKVXMVXPVWBUXAVXKVXLUXAVV + FUWNRVXKUXAVVFUWNUXABVWFXEVXAWGBUVSYCTUXABUVSVWGVWHUXAUVSVXAXRYFWGZUXAVXN + VXOUXAVVGUWPRVXNUXAVVGUWPUXAUXFVUMXEVWKWGUXFUVTYCTUXAUXFUVTUXAFBVWDVWGVWH + UUSVWIVWLYFWGZXSUXEUXGCYGTWJWTUYHUYJVUAUXAUYJVUAQZUXMUXAUYKUXIXDSZUXIWBUO + ZRZUXJXDSZUXJWBUOZRZYDVXSUXAUYKVYBVYEVWBUXAVXTVYAUXAUXIVXIXEUXAUXIVXIWSWG + ZUXAVYCVYDUXAUXJUXAUXFUWCVUMVWOWMZXEUXAUXJVYGWSWGZXSUXIUXJCYGTWJWTYAYHUXA + UXORZUYFBUXHVOPZBUXKVOPZUOUEBVPAVUHUWNUWPUWRUWTUXOIVSVYIUYCBQZRZUYDVYJUYE + VYKVYMUYCBUXHVOVYIVYLVAZVRVYMUYCBUXKVOVYNVRVTVYIBUXEVOPZBUXGVOPZWAPZBUXIV + OPZBUXJVOPZWAPZVYJVYKVYIVYQVYRVYPWAPVYQVYTVYIVYOVYRVYPVYIVYOVYIBUXEUXAVUH + UXOVWTWJZVYIBUVSVYIVUHVUGWUAVUITZAUWNUWPUWRUWTUXOUUTZWMWNWOVYIVYRVYIBUXIW + UAVYIBUWBWUBUWQUWRUWTUXOXQZWMWNWOVYIVYPVYIBUXGWUAVYIUXFUVTUXAVUDUXOVUMWJU + WOUWPUWRUWTUXOWLWMWNWOVYIUVSUWBVYOVYRUXOUXNUXAUYAVFVYIVYOUVSVYIVUHUWNRVYO + UVSQVYIVUHUWNWUAWUCWGUVSBYITWTVYIVYRUWBVYIVUHUWRRVYRUWBQVYIVUHUWRWUAWUDWG + UWBBYITWTYAUVAVYIVYQUVBVYIVYPVYSVYRWAVYIUXGUXJBVOVYIUVTUWCUXFUPUXAUWGUXNY + JYKYKYKYAUXAVYQVYJQUXOUXAVYJVYQUXAVUHVXMVXPYDVYJVYQQUXAVUHVXMVXPVWTVXQVXR + XSUXEUXGBYGTWTWJUXAVYTVYKQZUXOUXAVUHVYBVYEYDZWUEUXAVUHVYBVYEVWTVYFVYHXSWU + FVYKVYTUXIUXJBYGWTTWJYAYHUVCUXAUXLUYGXAUXPUXAUXLUYDUYEQZUNZUEVPVQZUYGUXAU + XLWUGUEVPUJZUNZWUIUXAUXLUXHUXKQZUNWUKUXAWULUXHUXKUXAWULYLUVDUXAWULWUJUXAU + XHOSZUXKOSZRWULWUJXAUXAWUMWUNUXAUXHUWSUXHUGSZUWTUWQWUOUWRUWQUXEUXGVXCUWQU + XFUVTVULUWOUWPVAWMYOWJWJZYMUXAUXKUXAUXIUXJVXIVYGYOZYMWGUXHUXKUEUVFTUVGYNW + UKWUIXAUXAWUIWUKWUGUEVPUVHVNYPYNUXAWUHUYFUEVPUXAWUGUYDUYEUXAWUGYLUVIUVJYN + WJXOUVKUXAUXDUXLXAUXBUXAUWAUXHUWDUXKUXADGUVSUVTOOBDUIZUPPZUXFGUIZUPPZURPZ + UXHEUGEDGOOWVBUVPQUXAKYPZUXAWURUVSQZWUTUVTQZRRZWUSUXEWVAUXGURWVFWURUVSBUP + UXAWVDWVEYJYKWVFWUTUVTUXFUPUXAWVDWVEYQYKYRVXAVWKWUPYSUXADGUWBUWCOOWVBUXKE + UGWVCUXAWURUWBQZWUTUWCQZRRZWUSUXIWVAUXJURWVIWURUWBBUPUXAWVGWVHYJYKWVIWUTU + WCUXFUPUXAWVGWVHYQYKYRVXGVWOWUQYSVTWJXOVBUVLUVMYTYTYTYTWGUDUCOOUGEUBUAUVN + UVO $. + $} + ${ $( The value of 5 choose 2. (Contributed by metakunt, 8-Jun-2024.) $) 5bc2eq10 $p |- ( 5 _C 2 ) = ; 1 0 $=