diff --git a/changes-set.txt b/changes-set.txt index caca3a3a27..617c359239 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -99,6 +99,8 @@ make a github issue.) DONE: Date Old New Notes +24-Aug-24 dvdspw dvdsexp2im moved from SF's mathbox to main set.mm +24-Aug-24 pdivsq prmdvdssq moved from SF's mathbox to main set.mm 24-Aug-24 dvdstrd [same] moved from MKU's mathbox to main set.mm 23-Aug-24 qred [same] moved from GS's mathbox to main set.mm 20-Aug-24 uzssre [same] moved from GS's mathbox to main set.mm diff --git a/set.mm b/set.mm index 5675cf195a..91e05bf10f 100644 --- a/set.mm +++ b/set.mm @@ -179299,6 +179299,23 @@ infinite descent (here implemented by strong induction). This is SWOVSWTRURAVTWBUSUTWOWCWPAJWOVSVAGWCWPNXAVSVCVDPVEVFVGVHVI $. $} + ${ + $d K m $. $d M m $. $d N m $. + $( Exponentiation law for divisibility. (Contributed by Scott Fenton, + 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) $) + dvdsexp2im $p |- ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) + -> ( K || M -> K || ( M ^ N ) ) ) $= + ( vm cz wcel cn w3a cdvds wbr cv cmul wceq cexp adantr zexpcl syl2anc zcn + co cc wrex wb divides 3adant3 wa simpl1 cn0 nnnn0 3ad2ant3 zmulcld simpl3 + simpr iddvdsexp dvdsmul2 dvdstrd adantl 3ad2ant1 breqtrrd oveq1 syl5ibcom + mulexpd breq2d rexlimdva sylbid ) AEFZBEFZCGFZHZABIJZDKZALSZBMZDEUAZABCNS + ZIJZVEVFVIVMUBVGDABUCUDVHVLVODEVHVJEFZUEZAVKCNSZIJVLVOVQAVJCNSZACNSZLSZVR + IVQAVTWAVEVFVGVPUFZVQVECUGFZVTEFZWBVHWCVPVGVEWCVFCUHUIOZACPQZVQVSVTVQVPWC + VSEFZVHVPULWEVJCPQZWFUJVQVEVGAVTIJWBVEVFVGVPUKACUMQVQWGWDVTWAIJWHWFVSVTUN + QUOVQVJACVPVJTFVHVJRUPVHATFZVPVEVFWIVGARUQOWEVAURVLVRVNAIVKBCNUSVBUTVCVD + $. + $} + $( A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) $) dvdsexp $p |- ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> @@ -186035,6 +186052,23 @@ being prime ( ` Prime = { p e. NN | ... ` ), but even if ` p e. NN0 ` was ZIJZVCLVGVIATIJZVCVGVHTAIVGBVGBUSBMEURBUDUEUFUGSURVJVCLUSURVJVCAUKUHUIUJVFV BVIVCVFVAVHAICNBGULSUMUNUOUPUQ $. + $( Condition for a prime dividing a square. (Contributed by Scott Fenton, + 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened + by SN, 21-Aug-2024.) $) + prmdvdssq $p |- ( ( P e. Prime /\ M e. ZZ ) + -> ( P || M <-> P || ( M ^ 2 ) ) ) $= + ( cprime wcel cz wa c2 cexp co cdvds wbr cn wb 2nn prmdvdsexp mp3an3 bicomd + ) ACDZBEDZFABGHIJKZABJKZRSGLDTUAMNBAGOPQ $. + + $( Obsolete version of ~ prmdvdssq as of 21-Aug-2024. (Contributed by Scott + Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + prmdvdssqOLD $p |- ( ( P e. Prime /\ M e. ZZ ) + -> ( P || M <-> P || ( M ^ 2 ) ) ) $= + ( cprime wcel cz wa c2 cexp co cdvds wbr cmul wb zcn sqvald breq2d euclemma + adantl wo 3anidm23 oridm syl6bb bitr2d ) ACDZBEDZFZABGHIZJKZABBLIZJKZABJKZU + EUHUJMUDUEUGUIAJUEBBNOPRUFUJUKUKSZUKUDUEUJULMABBQTUKUAUBUC $. + $( Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.) $) prmexpb $p |- ( ( ( P e. Prime /\ Q e. Prime ) /\ ( M e. NN /\ N e. NN ) ) -> @@ -186136,7 +186170,7 @@ being prime ( ` Prime = { p e. NN | ... ` ), but even if ` p e. NN0 ` was $d ph i p $. $d A i p $. $d B i p $. ncoprmgcdne1bgd.a $e |- ( ph -> A e. NN ) $. ncoprmgcdne1bgd.b $e |- ( ph -> B e. NN ) $. - $( Two positive integers are coprime iff no prime divides both integers. + $( Two positive integers are not coprime iff a prime divides both integers. General, deduction version of ~ ncoprmgcdne1b . (Contributed by SN, 24-Aug-2024.) $) ncoprmgcdne1bgd $p |- ( ph -> ( E. p e. Prime ( p || A /\ p || B ) @@ -523489,40 +523523,6 @@ Real and complex numbers (cont.) =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) - $( Condition for a prime dividing a square. (Contributed by Scott Fenton, - 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened - by SN, 21-Aug-2024.) $) - pdivsq $p |- ( ( P e. Prime /\ M e. ZZ ) - -> ( P || M <-> P || ( M ^ 2 ) ) ) $= - ( cprime wcel cz wa c2 cexp co cdvds wbr cn wb 2nn prmdvdsexp mp3an3 bicomd - ) ACDZBEDZFABGHIJKZABJKZRSGLDTUAMNBAGOPQ $. - - $( Obsolete version of ~ pdivsq as of 21-Aug-2024. (Contributed by Scott - Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) - (Proof modification is discouraged.) (New usage is discouraged.) $) - pdivsqOLD $p |- ( ( P e. Prime /\ M e. ZZ ) - -> ( P || M <-> P || ( M ^ 2 ) ) ) $= - ( cprime wcel cz wa c2 cexp co cdvds wbr cmul wb zcn sqvald breq2d euclemma - adantl wo 3anidm23 oridm syl6bb bitr2d ) ACDZBEDZFZABGHIZJKZABBLIZJKZABJKZU - EUHUJMUDUEUGUIAJUEBBNOPRUFUJUKUKSZUKUDUEUJULMABBQTUKUAUBUC $. - - ${ - $d K m $. $d M m $. $d N m $. - $( Exponentiation law for divisibility. (Contributed by Scott Fenton, - 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) $) - dvdspw $p |- ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) - -> ( K || M -> K || ( M ^ N ) ) ) $= - ( vm cz wcel cn w3a cdvds wbr cv cmul wceq cexp adantr zexpcl syl2anc zcn - co cc wrex wb divides 3adant3 wa simpl1 cn0 nnnn0 3ad2ant3 zmulcld simpl3 - simpr iddvdsexp dvdsmul2 dvdstrd adantl 3ad2ant1 breqtrrd oveq1 syl5ibcom - mulexpd breq2d rexlimdva sylbid ) AEFZBEFZCGFZHZABIJZDKZALSZBMZDEUAZABCNS - ZIJZVEVFVIVMUBVGDABUCUDVHVLVODEVHVJEFZUEZAVKCNSZIJVLVOVQAVJCNSZACNSZLSZVR - IVQAVTWAVEVFVGVPUFZVQVECUGFZVTEFZWBVHWCVPVGVEWCVFCUHUIOZACPQZVQVSVTVQVPWC - VSEFZVHVPULWEVJCPQZWFUJVQVEVGAVTIJWBVEVFVGVPUKACUMQVQWGWDVTWAIJWHWFVSVTUN - QUOVQVJACVPVJTFVHVJRUPVHATFZVPVEVFWIVGARUQOWEVAURVLVRVNAIVKBCNUSVBUTVCVD - $. - $} - $( Swap the second and third arguments of a gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) $) gcd32 $p |- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> @@ -648133,29 +648133,46 @@ standardize vectors to a length (norm) of one, but such definitions require ) -> ( M gcd N ) = 1 ) $= ( vi cn wcel c2 cexp co wceq cdvds wbr wa wi nnzd cz w3a caddc cgcd c1 wn wral simp3l simp11 simp12 coprmgcdb syl2anc mpbird simplr pythagtriplem11 - cv cmin simprl ad2antrr 2nn a1i dvdspw syl3anc mpd simprr pythagtriplem13 - wb nnsqcld dvds2subd pythagtriplem15 breqtrrd 2z nnmulcld pythagtriplem16 - cmul dvdsmultr2d jca ex imim1d ralimdva mpbid ) AIJZBIJZCIJZUAZAKLMBKLMUB - MCKLMNZABUCMUDNZKAOPUEZQZUAZHUOZDOPZWJEOPZQZWJUDNZRZHIUFZDEUCMUDNZWIWJAOP - ZWJBOPZQZWNRZHIUFZWPWIXBWFWDWEWFWGUGWIWAWBXBWFVFWAWBWCWEWHUHWAWBWCWEWHUIA - BHUJUKULWIXAWOHIWIWJIJZQZWMWTWNXDWMWTXDWMQZWRWSXEWJDKLMZEKLMZUPMZAOXEWJXF - XGXEWJWIXCWMUMSZXEWKWJXFOPZXDWKWLUQXEWJTJZDTJKIJZWKXJRXIXEDWIDIJZXCWMABCD - FUNZURZSZXLXEUSUTZWJDKVAVBVCXEWLWJXGOPZXDWKWLVDZXEXKETJXLWLXRRXIXEEWIEIJZ - XCWMABCEGVEZURZSZXQWJEKVAVBVCXEXFXEDXOVGSXEXGXEEYBVGSVHWIAXHNXCWMABCDEFGV - IURVJXEWJKDEVNMZVNMZBOXEWJKYDXIKTJXEVKUTXEYDXEDEXOYBVLSXEWJDEXIXPYCXSVOVO - WIBYENXCWMABCDEFGVMURVJVPVQVRVSVCWIXMXTWPWQVFXNYADEHUJUKVT $. + cv wb cmin simprl ad2antrr 2nn a1i dvdsexp2im syl3anc mpd pythagtriplem13 + simprr nnsqcld dvds2subd pythagtriplem15 breqtrrd 2z nnmulcld dvdsmultr2d + cmul pythagtriplem16 jca ex imim1d ralimdva mpbid ) AIJZBIJZCIJZUAZAKLMBK + LMUBMCKLMNZABUCMUDNZKAOPUEZQZUAZHUOZDOPZWJEOPZQZWJUDNZRZHIUFZDEUCMUDNZWIW + JAOPZWJBOPZQZWNRZHIUFZWPWIXBWFWDWEWFWGUGWIWAWBXBWFUPWAWBWCWEWHUHWAWBWCWEW + HUIABHUJUKULWIXAWOHIWIWJIJZQZWMWTWNXDWMWTXDWMQZWRWSXEWJDKLMZEKLMZUQMZAOXE + WJXFXGXEWJWIXCWMUMSZXEWKWJXFOPZXDWKWLURXEWJTJZDTJKIJZWKXJRXIXEDWIDIJZXCWM + ABCDFUNZUSZSZXLXEUTVAZWJDKVBVCVDXEWLWJXGOPZXDWKWLVFZXEXKETJXLWLXRRXIXEEWI + EIJZXCWMABCEGVEZUSZSZXQWJEKVBVCVDXEXFXEDXOVGSXEXGXEEYBVGSVHWIAXHNXCWMABCD + EFGVIUSVJXEWJKDEVNMZVNMZBOXEWJKYDXIKTJXEVKVAXEYDXEDEXOYBVLSXEWJDEXIXPYCXS + VMVMWIBYENXCWMABCDEFGVOUSVJVPVQVRVSVDWIXMXTWPWQUPXNYADEHUJUKVT $. $} ${ + $d ph p $. $d M p $. $d R p $. $d S p $. flt4lem5elem.m $e |- ( ph -> M e. NN ) $. flt4lem5elem.r $e |- ( ph -> R e. NN ) $. flt4lem5elem.s $e |- ( ph -> S e. NN ) $. flt4lem5elem.1 $e |- ( ph -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) ) $. flt4lem5elem.2 $e |- ( ph -> ( R gcd S ) = 1 ) $. - $( Powerless version of ~ fltaccoprm and ~ fltbccoprm . - TempNoteSN: will need coprmgcdb with ` A. i e. Prime ` $) + $( Version of ~ fltaccoprm and ~ fltbccoprm where ` M ` is not squared. + This can be proved in general for any polynomial in three variables: + using ~ ncoprmgcdne1bgd , ~ dvds2addd , and ~ prmdvdsexp , we can show + that if two variables are coprime, the third is also coprime to the two. + (Contributed by SN, 24-Aug-2024.) $) flt4lem5elem $p |- ( ph -> ( ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) ) $= - ? $. + ( vp co c1 cdvds wbr wa cprime wcel cz nnzd ad2antrr cgcd wceq cv wrex wn + ncoprmgcdne1bgd necon2bbid mpbid simprl c2 cexp cmin simplr syl simprr wb + prmz prmdvdssq syl2anc nnsqcld dvds2subd cc nncnd mvrladdd breqtrd mpbird + caddc jca ex reximdva mtod mvrraddd ) ABDUAKZLUBZCDUAKZLUBZAVNJUCZBMNZVQD + MNZOZJPUDZUEAWAVRVQCMNZOZJPUDZABCUAKZLUBWDUEIAWDWELABCJFGUFUGUHZAVTWCJPAV + QPQZOZVTWCWHVTOZVRWBWHVRVSUIZWIWBVQCUJUKKZMNZWIVQDBUJUKKZULKWKMWIVQDWMWIW + GVQRQZAWGVTUMZVQUQZUNWHVRVSUOWIVRVQWMMNZWJWIWGBRQZVRWQUPZWOAWRWGVTABFSZTV + QBURZUSUHADRQZWGVTADESZTAWMRQWGVTAWMABFUTZSTVAWIDWMWKAWMVBQZWGVTAWMXDVCZT + AWKVBQZWGVTAWKACGUTZVCZTADWMWKVGKUBZWGVTHTVDVEWIWGCRQZWBWLUPZWOAXKWGVTACG + SZTVQCURZUSVFVHVIVJVKAWAVMLABDJFEUFUGVFAVPWBVSOZJPUDZUEAXPWDWFAXOWCJPWHXO + WCWHXOOZVRWBXQVRWQXQVQDWKULKWMMXQVQDWKXQWGWNAWGXOUMZWPUNWHWBVSUOXQWBWLWHW + BVSUIZXQWGXKXLXRAXKWGXOXMTXNUSUHAXBWGXOXCTAWKRQWGXOAWKXHSTVAXQDWMWKAXEWGX + OXFTAXGWGXOXITAXJWGXOHTVLVEXQWGWRWSXRAWRWGXOWTTXAUSVFXSVHVIVJVKAXPVOLACDJ + GEUFUGVFVH $. $} ${ @@ -648178,105 +648195,102 @@ standardize vectors to a length (norm) of one, but such definitions require (Contributed by SN, 22-Aug-2024.) $) flt4lem5a $p |- ( ph -> ( ( A ^ 2 ) + ( N ^ 2 ) ) = ( M ^ 2 ) ) $= ( c2 co cexp cn wcel w3a caddc wceq cgcd c1 cdvds wn wa nnsqcld cprime cz - wbr wb 2prm nnzd pdivsq sylancr mtbid wi 2nn a1i rplpwr syl3anc mpd nncnd - c4 flt4lem oveq12d eqtr3d pythagtriplem11 pythagtriplem13 pythagtriplem15 - flt4lem1 syl cmin mvrlsubd ) ABSUATZGSUATZHSUATZAWAAGAVTUBUCCSUATZUBUCDUB - UCZUDVTSUATZWCSUATZUETZDSUATZUFVTWCUGTUHUFSVTUIUOZUJUKUDZGUBUCAVTWCDABMUL - ACNULOASBUIUOZWIPASUMUCBUNUCWKWIUPUQABMURSBUSUTVAABDUGTUHUFZVTDUGTUHUFZQA - BUBUCWDSUBUCZWLWMVBMOWNAVCVDBDSVEVFVGABVIUATZCVIUATZUETWGWHAWOWEWPWFUEABA - BMVHVJACACNVHVJVKRVLVPZVTWCDGIVMVQULVHAWBAHAWJHUBUCWQVTWCDHJVNVQULVHAWJVT - WAWBVRTUFWQVTWCDGHIJVOVQVS $. + wbr wb 2prm nnzd prmdvdssq sylancr mtbid wi 2nn a1i rplpwr syl3anc mpd c4 + nncnd flt4lem oveq12d eqtr3d flt4lem1 pythagtriplem11 syl pythagtriplem13 + cmin pythagtriplem15 mvrlsubd ) ABSUATZGSUATZHSUATZAWAAGAVTUBUCCSUATZUBUC + DUBUCZUDVTSUATZWCSUATZUETZDSUATZUFVTWCUGTUHUFSVTUIUOZUJUKUDZGUBUCAVTWCDAB + MULACNULOASBUIUOZWIPASUMUCBUNUCWKWIUPUQABMURSBUSUTVAABDUGTUHUFZVTDUGTUHUF + ZQABUBUCWDSUBUCZWLWMVBMOWNAVCVDBDSVEVFVGABVHUATZCVHUATZUETWGWHAWOWEWPWFUE + ABABMVIVJACACNVIVJVKRVLVMZVTWCDGIVNVOULVIAWBAHAWJHUBUCWQVTWCDHJVPVOULVIAW + JVTWAWBVQTUFWQVTWCDGHIJVRVOVS $. $( Part 2 of Equation 1 of ~ https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html . (Contributed by SN, 22-Aug-2024.) $) flt4lem5b $p |- ( ph -> ( 2 x. ( M x. N ) ) = ( B ^ 2 ) ) $= ( c2 co cexp cmul cn wcel w3a caddc wceq cgcd c1 cdvds wbr nnsqcld cprime - wn wa cz wb 2prm pdivsq sylancr mtbid wi 2nn a1i rplpwr syl3anc mpd nncnd - nnzd c4 flt4lem oveq12d eqtr3d flt4lem1 pythagtriplem16 syl eqcomd ) ACSU - ATZSGHUBTUBTZABSUATZUCUDVRUCUDDUCUDZUEVTSUATZVRSUATZUFTZDSUATZUGVTVRUHTUI - UGSVTUJUKZUNUOUEVRVSUGAVTVRDABMULACNULOASBUJUKZWFPASUMUDBUPUDWGWFUQURABMV - ISBUSUTVAABDUHTUIUGZVTDUHTUIUGZQABUCUDWASUCUDZWHWIVBMOWJAVCVDBDSVEVFVGABV - JUATZCVJUATZUFTWDWEAWKWBWLWCUFABABMVHVKACACNVHVKVLRVMVNVTVRDGHIJVOVPVQ $. + wn wa cz wb 2prm prmdvdssq sylancr mtbid wi 2nn a1i rplpwr syl3anc mpd c4 + nnzd nncnd flt4lem oveq12d eqtr3d flt4lem1 pythagtriplem16 syl eqcomd ) A + CSUATZSGHUBTUBTZABSUATZUCUDVRUCUDDUCUDZUEVTSUATZVRSUATZUFTZDSUATZUGVTVRUH + TUIUGSVTUJUKZUNUOUEVRVSUGAVTVRDABMULACNULOASBUJUKZWFPASUMUDBUPUDWGWFUQURA + BMVISBUSUTVAABDUHTUIUGZVTDUHTUIUGZQABUCUDWASUCUDZWHWIVBMOWJAVCVDBDSVEVFVG + ABVHUATZCVHUATZUFTWDWEAWKWBWLWCUFABABMVJVKACACNVJVKVLRVMVNVTVRDGHIJVOVPVQ + $. $( Part 2 of Equation 2 of ~ https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html . (Contributed by SN, 22-Aug-2024.) $) flt4lem5c $p |- ( ph -> N = ( 2 x. ( R x. S ) ) ) $= ( c2 co cn wcel cexp caddc wceq cgcd c1 cdvds wbr cmul w3a nnsqcld cprime - wn wa cz wb 2prm pdivsq sylancr mtbid wi 2nn a1i rplpwr syl3anc mpd nncnd - nnzd c4 flt4lem eqtr3d flt4lem1 pythagtriplem13 pythagtriplem11 flt4lem5a - oveq12d syl syl2anc flt4lem5 addcomd fltabcoprm pythagtriplem16 syl312anc - gcdcom eqtrd ) ABUAUBZHUAUBZGUAUBZBSUCTZHSUCTZUDTZGSUCTZUEBHUFTZUGUESBUHU - IZUNHSEFUJTUJTUEMAWJUAUBCSUCTZUAUBDUAUBZUKWJSUCTZWPSUCTZUDTZDSUCTZUEWJWPU - FTUGUESWJUHUIZUNUOUKZWHAWJWPDABMULZACNULOAWOXBPASUMUBBUPUBZWOXBUQURABMVIZ - SBUSUTVAABDUFTUGUEZWJDUFTUGUEZQAWGWQSUAUBZXGXHVBMOXIAVCVDBDSVEVFVGABVJUCT - ZCVJUCTZUDTWTXAAXJWRXKWSUDABABMVHVKACACNVHVKVQRVLVMZWJWPDHJVNVRZAXCWIXLWJ - WPDGIVOVRZABCDEFGHIJKLMNOPQRVPZAWNHBUFTZUGAXEHUPUBZWNXPUEXFAHXMVIZBHWEVSA - HBGXMMXNAHGUFTZGHUFTZUGAXQGUPUBXSXTUEXRAGXNVIHGWEVSAXCXTUGUEXLWJWPDGHIJVT - VRWFAWKWJUDTWLWMAWKWJAWKAHXMULVHAWJXDVHWAXOWFWBWFPBHGEFKLWCWD $. + wn wa cz wb 2prm prmdvdssq sylancr mtbid wi 2nn a1i rplpwr syl3anc mpd c4 + nncnd flt4lem oveq12d eqtr3d flt4lem1 pythagtriplem13 syl pythagtriplem11 + nnzd flt4lem5a gcdcom syl2anc flt4lem5 addcomd fltabcoprm pythagtriplem16 + eqtrd syl312anc ) ABUAUBZHUAUBZGUAUBZBSUCTZHSUCTZUDTZGSUCTZUEBHUFTZUGUESB + UHUIZUNHSEFUJTUJTUEMAWJUAUBCSUCTZUAUBDUAUBZUKWJSUCTZWPSUCTZUDTZDSUCTZUEWJ + WPUFTUGUESWJUHUIZUNUOUKZWHAWJWPDABMULZACNULOAWOXBPASUMUBBUPUBZWOXBUQURABM + VQZSBUSUTVAABDUFTUGUEZWJDUFTUGUEZQAWGWQSUAUBZXGXHVBMOXIAVCVDBDSVEVFVGABVH + UCTZCVHUCTZUDTWTXAAXJWRXKWSUDABABMVIVJACACNVIVJVKRVLVMZWJWPDHJVNVOZAXCWIX + LWJWPDGIVPVOZABCDEFGHIJKLMNOPQRVRZAWNHBUFTZUGAXEHUPUBZWNXPUEXFAHXMVQZBHVS + VTAHBGXMMXNAHGUFTZGHUFTZUGAXQGUPUBXSXTUEXRAGXNVQHGVSVTAXCXTUGUEXLWJWPDGHI + JWAVOWEAWKWJUDTWLWMAWKWJAWKAHXMULVIAWJXDVIWBXOWEWCWEPBHGEFKLWDWF $. $( Part 3 of Equation 2 of ~ https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html . (Contributed by SN, 23-Aug-2024.) $) flt4lem5d $p |- ( ph -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) ) $= ( c2 co cn wcel cexp caddc wceq cgcd c1 cdvds wbr wn wa nnsqcld cprime cz - w3a wb 2prm nnzd pdivsq sylancr mtbid wi 2nn a1i rplpwr syl3anc mpd nncnd - flt4lem oveq12d eqtr3d flt4lem1 pythagtriplem13 pythagtriplem11 flt4lem5a - c4 syl gcdcom syl2anc flt4lem5 eqtrd fltabcoprm pythagtriplem17 syl312anc - addcomd ) ABUAUBZHUAUBZGUAUBZBSUCTZHSUCTZUDTZGSUCTZUEBHUFTZUGUESBUHUIZUJG - ESUCTFSUCTUDTUEMAWIUAUBCSUCTZUAUBDUAUBZUOWISUCTZWOSUCTZUDTZDSUCTZUEWIWOUF - TUGUESWIUHUIZUJUKUOZWGAWIWODABMULZACNULOAWNXAPASUMUBBUNUBZWNXAUPUQABMURZS - BUSUTVAABDUFTUGUEZWIDUFTUGUEZQAWFWPSUAUBZXFXGVBMOXHAVCVDBDSVEVFVGABVPUCTZ - CVPUCTZUDTWSWTAXIWQXJWRUDABABMVHVIACACNVHVIVJRVKVLZWIWODHJVMVQZAXBWHXKWIW - ODGIVNVQZABCDEFGHIJKLMNOPQRVOZAWMHBUFTZUGAXDHUNUBZWMXOUEXEAHXLURZBHVRVSAH - BGXLMXMAHGUFTZGHUFTZUGAXPGUNUBXRXSUEXQAGXMURHGVRVSAXBXSUGUEXKWIWODGHIJVTV - QWAAWJWIUDTWKWLAWJWIAWJAHXLULVHAWIXCVHWEXNWAWBWAPBHGEFKLWCWD $. - - $( Satisfy the hypotheses of ~ flt4lem4 . (Contributed by SN, - 23-Aug-2024.) $) + w3a wb 2prm nnzd prmdvdssq sylancr mtbid wi 2nn a1i rplpwr syl3anc mpd c4 + nncnd flt4lem oveq12d eqtr3d flt4lem1 pythagtriplem13 syl pythagtriplem11 + flt4lem5a gcdcom syl2anc flt4lem5 eqtrd addcomd pythagtriplem17 syl312anc + fltabcoprm ) ABUAUBZHUAUBZGUAUBZBSUCTZHSUCTZUDTZGSUCTZUEBHUFTZUGUESBUHUIZ + UJGESUCTFSUCTUDTUEMAWIUAUBCSUCTZUAUBDUAUBZUOWISUCTZWOSUCTZUDTZDSUCTZUEWIW + OUFTUGUESWIUHUIZUJUKUOZWGAWIWODABMULZACNULOAWNXAPASUMUBBUNUBZWNXAUPUQABMU + RZSBUSUTVAABDUFTUGUEZWIDUFTUGUEZQAWFWPSUAUBZXFXGVBMOXHAVCVDBDSVEVFVGABVHU + CTZCVHUCTZUDTWSWTAXIWQXJWRUDABABMVIVJACACNVIVJVKRVLVMZWIWODHJVNVOZAXBWHXK + WIWODGIVPVOZABCDEFGHIJKLMNOPQRVQZAWMHBUFTZUGAXDHUNUBZWMXOUEXEAHXLURZBHVRV + SAHBGXLMXMAHGUFTZGHUFTZUGAXPGUNUBXRXSUEXQAGXMURHGVRVSAXBXSUGUEXKWIWODGHIJ + VTVOWAAWJWIUDTWKWLAWJWIAWJAHXLULVIAWIXCVIWBXNWAWEWAPBHGEFKLWCWD $. + + $( Satisfy the hypotheses of ~ flt4lem4 . EDITORIAL: This is not + minimized! (Contributed by SN, 23-Aug-2024.) $) flt4lem5e $p |- ( ph -> ( ( ( R gcd S ) = 1 /\ ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) /\ ( R e. NN /\ S e. NN /\ M e. NN ) /\ ( ( M x. ( R x. S ) ) = ( ( B / 2 ) ^ 2 ) /\ ( B / 2 ) e. NN ) ) ) $= - ( co c2 vi cgcd c1 wceq w3a cn wcel cmul cdiv cexp wa caddc cdvds nnsqcld - wbr wn cprime cz wb 2prm nnzd pdivsq sylancr mtbid 2nn a1i rplpwr syl3anc + ( co c2 cgcd c1 wceq w3a cn wcel cmul cdiv cexp wa caddc cdvds wn nnsqcld + wbr cprime cz wb 2prm nnzd prmdvdssq sylancr mtbid 2nn a1i rplpwr syl3anc wi mpd c4 flt4lem oveq12d eqtr3d flt4lem1 pythagtriplem13 pythagtriplem11 - nncnd syl flt4lem5a gcdcom syl2anc flt4lem5 eqtrd fltabcoprm syl312anc cv - addcomd wral coprmgcdb mpbird simprl jca ex imim1d ralimdv mpbid 3jca sq2 - cc 4cn eqeltri nnmulcld cc0 wne 4ne0 eqnetri 2cn sqvali oveq1i 2cnd mul4d - flt4lem5c eqcomd eqeltrd oveq2d 3eqtrd syl5eq mvllmuld 2ne0 sqdivd eqtr4d - mulassd flt4lem5b eqeltrrd cq znq sylancl nngt0d nnred halfpos2 posqsqznn - clt cr ) AEFUBSUCUDZEGUBSUCUDZFGUBSUCUDZUEEUFUGZFUFUGZGUFUGZUEGEFUHSZUHSZ - CTUISZTUJSZUDZUUCUFUGZUKAYOYPYQABUFUGZHUFUGZYTBTUJSZHTUJSZULSZGTUJSZUDZBH - UBSZUCUDZTBUMUOZUPZYOMAUUIUFUGCTUJSZUFUGDUFUGZUEUUITUJSZUURTUJSZULSZDTUJS - ZUDUUIUURUBSUCUDTUUIUMUOZUPUKUEZUUHAUUIUURDABMUNZACNUNOAUUPUVDPATUQUGBURU - GZUUPUVDUSUTABMVAZTBVBVCVDABDUBSUCUDZUUIDUBSUCUDZQAUUGUUSTUFUGZUVIUVJVIMO - UVKAVEVFBDTVGVHVJABVKUJSZCVKUJSZULSUVBUVCAUVLUUTUVMUVAULABABMVRVLACACNVRZ - VLVMRVNVOZUUIUURDHJVPVSZAUVEYTUVOUUIUURDGIVQVSZABCDEFGHIJKLMNOPQRVTZAUUNH - BUBSZUCAUVGHURUGZUUNUVSUDUVHAHUVPVAZBHWAWBAHBGUVPMUVQAHGUBSZGHUBSZUCAUVTG - URUGUWBUWCUDUWAAGUVQVAHGWAWBAUVEUWCUCUDUVOUUIUURDGHIJWCVSWDAUUJUUIULSUUKU - ULAUUJUUIAUUJAHUVPUNVRAUUIUVFVRWHUVRWDWEWDZPBHGEFKLWCWFZAUAWGZEUMUOZUWFGU - MUOZUKZUWFUCUDZVIZUAUFWIZYPAUWGUWFFUMUOZUKZUWJVIZUAUFWIZUWLAUWPYOUWEAYRYS - UWPYOUSAUUGUUHYTUUMUUOUUQYRMUVPUVQUVRUWDPBHGEKVQWFZAUUGUUHYTUUMUUOUUQYSMU - VPUVQUVRUWDPBHGFLVPWFZEFUAWJWBWKZAUWOUWKUAUFAUWIUWNUWJAUWIUWNAUWIUKUWGUWM - AUWGUWHWL?WMWNWOWPVJAYRYTUWLYPUSUWQUVQEGUAWJWBWQAUWMUWHUKZUWJVIZUAUFWIZYQ - AUWPUXBUWSAUWOUXAUAUFAUWTUWNUWJAUWTUWNAUWTUKUWGUWM?AUWMUWHWLWMWNWOWPVJAYS - YTUXBYQUSUWRUVQFGUAWJWBWQWRAYRYSYTUWQUWRUVQWRAUUEUUFAUUBUURTTUJSZUISUUDAU - XCUUBUURUXCWTUGAUXCVKWTWSXAXBVFAUUBAGUUAUVQAEFUWQUWRXCZXCZVRUXCXDXEAUXCVK - XDWSXFXGVFAUXCUUBUHSTTUHSZUUBUHSZUURUXCUXFUUBUHTXHXIXJAUXGTGUHSTUUAUHSZUH - SZTGHUHSZUHSZUURATTGUUAAXKZUXLAGUVQVRZAUUAUXDVRXLAUXITGUXHUHSZUHSUXKATGUX - HUXLUXMAUXHAUXHHUFAHUXHABCDEFGHIJKLMNOPQRXMXNZUVPXOVRYCAUXNUXJTUHAUXHHGUH - UXOXPXPWDABCDEFGHIJKLMNOPQRYDXQXRXSACTUVNUXLTXDXEAXTVFYAYBZAUUCAUUBUUDURU - XPAUUBUXEVAYEACURUGUVKUUCYFUGACNVAVECTYGYHAXDCYMUOZXDUUCYMUOZACNYIACYNUGU - XQUXRUSACNYJCYKVSWQYLWMWR $. + nncnd flt4lem5a gcdcom syl2anc flt4lem5 eqtrd addcomd syl312anc flt4lem5d + syl fltabcoprm flt4lem5elem jca 3anass sylibr cc sq2 4cn eqeltri nnmulcld + 3jca cc0 wne 4ne0 eqnetri 2cn sqvali oveq1i 2cnd flt4lem5c eqcomd eqeltrd + mul4d oveq2d flt4lem5b 3eqtrd syl5eq mvllmuld 2ne0 sqdivd eqtr4d eqeltrrd + mulassd cq znq sylancl clt nngt0d cr nnred halfpos2 mpbid posqsqznn ) AEF + UASUBUCZEGUASUBUCZFGUASUBUCZUDZEUEUFZFUEUFZGUEUFZUDGEFUGSZUGSZCTUHSZTUISZ + UCZYSUEUFZUJAYJYKYLUJZUJYMAYJUUCABUEUFZHUEUFZYPBTUISZHTUISZUKSZGTUISZUCZB + HUASZUBUCZTBULUOZUMZYJMAUUFUEUFCTUISZUEUFDUEUFZUDUUFTUISZUUOTUISZUKSZDTUI + SZUCUUFUUOUASUBUCTUUFULUOZUMUJUDZUUEAUUFUUODABMUNZACNUNOAUUMUVAPATUPUFBUQ + UFZUUMUVAURUSABMUTZTBVAVBVCABDUASUBUCZUUFDUASUBUCZQAUUDUUPTUEUFZUVFUVGVHM + OUVHAVDVEBDTVFVGVIABVJUISZCVJUISZUKSUUSUUTAUVIUUQUVJUURUKABABMVQVKACACNVQ + ZVKVLRVMVNZUUFUUODHJVOWFZAUVBYPUVLUUFUUODGIVPWFZABCDEFGHIJKLMNOPQRVRZAUUK + HBUASZUBAUVDHUQUFZUUKUVPUCUVEAHUVMUTZBHVSVTAHBGUVMMUVNAHGUASZGHUASZUBAUVQ + GUQUFUVSUVTUCUVRAGUVNUTHGVSVTAUVBUVTUBUCUVLUUFUUODGHIJWAWFWBAUUGUUFUKSUUH + UUIAUUGUUFAUUGAHUVMUNVQAUUFUVCVQWCUVOWBWGWBZPBHGEFKLWAWDZAEFGUVNAUUDUUEYP + UUJUULUUNYNMUVMUVNUVOUWAPBHGEKVPWDZAUUDUUEYPUUJUULUUNYOMUVMUVNUVOUWAPBHGF + LVOWDZABCDEFGHIJKLMNOPQRWEUWBWHWIYJYKYLWJWKAYNYOYPUWCUWDUVNWQAUUAUUBAYRUU + OTTUISZUHSYTAUWEYRUUOUWEWLUFAUWEVJWLWMWNWOVEAYRAGYQUVNAEFUWCUWDWPZWPZVQUW + EWRWSAUWEVJWRWMWTXAVEAUWEYRUGSTTUGSZYRUGSZUUOUWEUWHYRUGTXBXCXDAUWITGUGSTY + QUGSZUGSZTGHUGSZUGSZUUOATTGYQAXEZUWNAGUVNVQZAYQUWFVQXIAUWKTGUWJUGSZUGSUWM + ATGUWJUWNUWOAUWJAUWJHUEAHUWJABCDEFGHIJKLMNOPQRXFXGZUVMXHVQXSAUWPUWLTUGAUW + JHGUGUWQXJXJWBABCDEFGHIJKLMNOPQRXKXLXMXNACTUVKUWNTWRWSAXOVEXPXQZAYSAYRYTU + QUWRAYRUWGUTXRACUQUFUVHYSXTUFACNUTVDCTYAYBAWRCYCUOZWRYSYCUOZACNYDACYEUFUW + SUWTURACNYFCYGWFYHYIWIWQ $. $( Final equation of ~ https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html . (Contributed by SN, 23-Aug-2024.) $) flt4lem5f $p |- ( ph -> ( ( M gcd ( B / 2 ) ) ^ 2 ) = ( ( ( R gcd ( B / 2 ) ) ^ 4 ) + ( ( S gcd ( B / 2 ) ) ^ 4 ) ) ) $= - ? $. + ( ) ? $. $} ${