From 10f7dabe35f29b1f2317501e0e02aefdc92bc119 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 14 Nov 2024 13:08:27 -0800 Subject: [PATCH] Add partial 2sq development in iset.mm (#4388) * Add 2sqlem1 to iset.mm Stated as in set.mm. The proof is similar to the set.mm proof but needs some intuitionizing. * copy 2sqlem2 from set.mm to iset.mm * copy mul2sq from set.mm to iset.mm * Add 2sqlem3 to iset.mm Stated as in set.mm. The proof needs a small amount of intuitionizing but is only slightly changed from the set.mm proof. * copy 2sqlem4 from set.mm to iset.mm * copy 2sqlem5 from set.mm to iset.mm * copy 2sqlem6 from set.mm to iset.mm * Add 2sqlem7 to iset.mm Stated as in set.mm. The proof needs a small amount of intuitionizing but is basically the set.mm proof. * Add 2sqlem8a to iset.mm Stated as in set.mm. The proof needs a small amount of intuitionizing but is basically the set.mm proof. * Add 2sqlem8 to iset.mm Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof. * Add 2sqlem9 to iset.mm Stated as in set.mm. The proof needs a little bit of intuitionizing but is basically the set.mm proof. * Add 2sqlem10 to iset.mm Stated as in set.mm. The proof needs a little bit of intuitionizing but is basically the set.mm proof. * Adjust 2sq comments in iset.mm Add 2sqlem11 and 2sq to mmil.html Don't refer to 2sq in comments because we haven't proved it yet. --- iset.mm | 387 ++++++++++++++++++++++++++++++++++++++++++++++++++ mmil.raw.html | 12 ++ 2 files changed, 399 insertions(+) diff --git a/iset.mm b/iset.mm index 46febfd198..ae879ef0cb 100644 --- a/iset.mm +++ b/iset.mm @@ -157958,6 +157958,393 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + All primes 4n+1 are the sum of two squares +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + ${ + $d a b n p q w x y z $. $d a m x y z A $. $d x C $. $d p q u v x y ph $. + $d a b m p x y B $. $d a b p u v x y z M $. $d a b m n p q u v x y z S $. + $d x D $. $d a p x y z E $. $d p q u v x y z N $. $d a b m n x y Y $. + $d a p x y z F $. $d n p q x y P $. + 2sq.1 $e |- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) ) $. + $( Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) $) + 2sqlem1 $p |- ( A e. S <-> E. x e. Z[i] A = ( ( abs ` x ) ^ 2 ) ) $= + ( wcel cgz cv cabs cfv c2 cexp co cmpt crn wceq wrex eleq2i cc wb cbvmptv + fveq2 oveq1d elrnmptg gzcn abscld recnd sqcld mprg bitri ) CDFCBGBHZIJZKL + MZNZOZFZCAHZIJZKLMZPAGQZDUOCERUSSFUPUTTAGAGUSCUNSBAGUMUSUKUQPULURKLUKUQIU + BUCUAUDUQGFZURVAURVAUQUQUEUFUGUHUIUJ $. + + $( Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) $) + 2sqlem2 $p |- ( A e. S <-> E. x e. ZZ E. y e. ZZ + A = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) $= + ( vz wcel cv c2 cexp co caddc wceq cz wrex cfv cgz cc oveq1d cabs 2sqlem1 + cre cim elgz simp2bi simp3bi gzcn absvalsq2d oveq1 eqeq2d rspc2ev syl3anc + oveq2d eqeq1 2rexbidv syl5ibrcom rexlimiv sylbi wa cmul gzreim zcn ax-icn + ci mulcl sylancr addcl syl2an zre crre crim oveq12d eqtr2d fveq2 rspceeqv + cr syl2anc sylibr eleq1 rexlimivv impbii ) DEHZDAIZJKLZBIZJKLZMLZNZBOPAOP + ZWCDGIZUAQZJKLZNZGRPWJGCDEFUBWNWJGRWKRHZWJWNWMWHNZBOPAOPZWOWKUCQZOHZWKUDQ + ZOHZWMWRJKLZWTJKLZMLZNZWQWOWKSHZWSXAWKUEZUFWOXFWSXAXGUGWOWKWKUHUIWPXEWMXB + WGMLZNABWRWTOOWDWRNZWHXHWMXIWEXBWGMWDWRJKUJTUKWFWTNZXHXDWMXJWGXCXBMWFWTJK + UJUNUKULUMWNWIWPABOODWMWHUOUPUQURUSWIWCABOOWDOHZWFOHZUTZWCWIWHEHZXMWHWMNG + RPZXNXMWDVEWFVALZMLZRHWHXQUAQZJKLZNXOWDWFVBXMXSXQUCQZJKLZXQUDQZJKLZMLWHXM + XQXKWDSHXPSHZXQSHXLWDVCXLVESHWFSHYDVDWFVCVEWFVFVGWDXPVHVIUIXMYAWEYCWGMXMX + TWDJKXKWDVQHZWFVQHZXTWDNXLWDVJZWFVJZWDWFVKVITXMYBWFJKXKYEYFYBWFNXLYGYHWDW + FVLVITVMVNGXQRWMXSWHWKXQNWLXRJKWKXQUAVOTVPVRGCWHEFUBVSDWHEVTUQWAWB $. + + $( Fibonacci's identity (actually due to Diophantus). The product of two + sums of two squares is also a sum of two squares. We can take advantage + of Gaussian integers here to trivialize the proof. (Contributed by + Mario Carneiro, 19-Jun-2015.) $) + mul2sq $p |- ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S ) $= + ( vx vy vz wcel cv cabs cfv c2 cexp co wceq cgz wrex cmul cc 2sqlem1 gzcn + wa reeanv gzmulcl absmul syl2an oveq1d abscld recnd sqmul eqtr2d rspceeqv + fveq2 syl2anc sylibr oveq12 eleq1d syl5ibrcom rexlimivv sylbir syl2anb ) + BDIBFJZKLZMNOZPZFQRZCGJZKLZMNOZPZGQRZBCSOZDIZCDIFABDEUAGACDEUAVGVLUCVFVKU + CZGQRFQRVNVFVKFGQQUDVOVNFGQQVCQIZVHQIZUCZVNVOVEVJSOZDIZVRVSHJZKLZMNOZPHQR + ZVTVRVCVHSOZQIVSWEKLZMNOZPWDVCVHUEVRWGVDVISOZMNOZVSVRWFWHMNVPVCTIVHTIWFWH + PVQVCUBZVHUBZVCVHUFUGUHVPVDTIVITIWIVSPVQVPVDVPVCWJUIUJVQVIVQVHWKUIUJVDVIU + KUGULHWEQWCWGVSWAWEPWBWFMNWAWEKUNUHUMUOHAVSDEUAUPVOVMVSDBVECVJSUQURUSUTVA + VB $. + + ${ + 2sqlem5.1 $e |- ( ph -> N e. NN ) $. + 2sqlem5.2 $e |- ( ph -> P e. Prime ) $. + ${ + 2sqlem4.3 $e |- ( ph -> A e. ZZ ) $. + 2sqlem4.4 $e |- ( ph -> B e. ZZ ) $. + 2sqlem4.5 $e |- ( ph -> C e. ZZ ) $. + 2sqlem4.6 $e |- ( ph -> D e. ZZ ) $. + 2sqlem4.7 $e |- ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) ) $. + 2sqlem4.8 $e |- ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) ) $. + ${ + 2sqlem4.9 $e |- ( ph -> P || ( ( C x. B ) + ( A x. D ) ) ) $. + $( Lemma for ~ 2sqlem5 . (Contributed by Mario Carneiro, + 20-Jun-2015.) $) + 2sqlem3 $p |- ( ph -> N e. S ) $= + ( co vx cv cabs cfv c2 cexp wceq cgz wrex wcel ci cmul caddc cc cre + cdiv cz cim gzreim syl2anc gzmulcl syl cprime cn prmnn nncnd nnap0d + gzcn divclapd nnred redivapd cdvds prmz zsqcl nnzd zmulcld dvdsmul2 + sqvald breqtrrd dvdstrd abscld recnd sqmuld zred crred oveq1d crimd + oveq12d absvalsq2d 3eqtr4d mulassd 3eqtrd absmuld elgz simp2bi zcnd + wbr oveq2d simp3bi addcomd breqtrd wb mulcld mulcomd immuld 2nn a1i + eqtrd prmdvdsexp syl3anc dvdsadd2b syl112anc mpbid cc0 wne dvdsval2 + mpbird nnne0d eqeltrd imdivapd syl3anbrc absdivapd nn0ge0d sqdivapd + nnnn0d absidd nnsqcld divcanap4d 3eqtrrd rspceeqv 2sqlem1 sylibr + fveq2 ) AIUAUBZUCUDZUEUFTZUGUAUHUIZIHUJACUKDULTUMTZEUKFULTUMTZULTZG + UPTZUHUJZIUUAUCUDZUEUFTZUGYQAUUAUNUJUUAUOUDZUQUJUUAURUDZUQUJUUBAYTG + AYTUHUJZYTUNUJZAYRUHUJZYSUHUJZUUGACUQUJDUQUJUUIMNCDUSUTZAEUQUJFUQUJ + UUJOPEFUSUTZYRYSVAUTZYTVHVBZAGAGVCUJZGVDUJLGVEVBZVFZAGUUPVGZVIAUUEY + TUOUDZGUPTZUQAGYTAGUUPVJZUUNUURVKAGUUSVLWQZUUTUQUJZAGUUSUEUFTZVLWQZ + UVBAUVEGYTURUDZUEUFTZUVDUMTZVLWQZAGYTUCUDZUEUFTZUVHVLAGIGUEUFTZULTZ + UVKVLAGUVLUVMAUUOGUQUJZLGVMVBZAUVNUVLUQUJZUVOGVNVBZAIUVLAIKVOZUVQVP + AGGGULTZUVLVLAUVNUVNGUVSVLWQUVOUVOGGVQUTAGUUQVRZVSAIUQUJUVPUVLUVMVL + WQUVRUVQIUVLVQUTVTAYRUCUDZYSUCUDZULTZUEUFTZIUVSULTZUVKUVMAUWDUWAUEU + FTZUWBUEUFTZULTIGULTZGULTUWEAUWAUWBAUWAAYRAUUIYRUNUJUUKYRVHVBZWAWBA + UWBAYSAUUJYSUNUJUULYSVHVBZWAWBWCAUWFUWHUWGGULAYRUOUDZUEUFTZYRURUDZU + EUFTZUMTCUEUFTZDUEUFTZUMTUWFUWHAUWLUWOUWNUWPUMAUWKCUEUFACDACMWDZADN + WDZWEZWFAUWMDUEUFACDUWQUWRWGZWFWHAYRUWIWIQWJAYSUOUDZUEUFTZYSURUDZUE + UFTZUMTEUEUFTZFUEUFTZUMTUWGGAUXBUXEUXDUXFUMAUXAEUEUFAEFAEOWDZAFPWDZ + WEZWFAUXCFUEUFAEFUXGUXHWGZWFWHAYSUWJWIRWJWHAIGGAIKVFZUUQUUQWKWLAUVJ + UWCUEUFAYRYSUWIUWJWMWFAUVLUVSIULUVTWRWJZVSAUVKUVDUVGUMTUVHAYTUUNWIA + UVDUVGAUVDAUUSUQUJZUVDUQUJZAUUGUXMUUMUUGUUHUXMUVFUQUJZYTWNZWOVBZUUS + VNVBZWPAUVGAUXOUVGUQUJZAUUGUXOUUMUUGUUHUXMUXOUXPWSVBZUVFVNVBZWPWTXH + XAAUVNUXNUXSGUVGVLWQZUVEUVIXBUVOUXRUYAAUYBGUVFVLWQZAGCFULTZDEULTZUM + TZUVFVLAGEDULTZUYDUMTZUYFVLSAUYHUYDUYGUMTUYFAUYGUYDAEDAEOWPZADNWPZX + CACFACMWPAFPWPXCWTAUYGUYEUYDUMAEDUYIUYJXDWRXHXAAUVFUWKUXCULTZUWMUXA + ULTZUMTUYFAYRYSUWIUWJXEAUYKUYDUYLUYEUMAUWKCUXCFULUWSUXJWHAUWMDUXAEU + LUWTUXIWHWHXHVSZAUUOUXOUEVDUJZUYBUYCXBLUXTUYNAXFXGZUVFGUEXIXJXQGUVD + UVGXKXLXQAUUOUXMUYNUVEUVBXBLUXQUYOUUSGUEXIXJXMAUVNGXNXOZUXMUVBUVCXB + UVOAGUUPXRZUXQGUUSXPXJXMXSAUUFUVFGUPTZUQAGYTUVAUUNUURXTAUYCUYRUQUJZ + UYMAUVNUYPUXOUYCUYSXBUVOUYQUXTGUVFXPXJXMXSUUAWNYAAUUDUVJGUPTZUEUFTU + VKUVLUPTZIAUUCUYTUEUFAUUCUVJGUCUDZUPTUYTAYTGUUNUUQUURYBAVUBGUVJUPAG + UVAAGAGUUPYEYCYFWRXHWFAUVJGAUVJAYTUUNWAWBUUQUURYDAVUAUVMUVLUPTIAUVK + UVMUVLUPUXLWFAIUVLUXKAUVLAGUUPYGZVFAUVLVUCVGYHXHYIUAUUAUHYPUUDIYNUU + AUGYOUUCUEUFYNUUAUCYMWFYJUTUABIHJYKYL $. + $} + + $( Lemma for ~ 2sqlem5 . (Contributed by Mario Carneiro, + 20-Jun-2015.) $) + 2sqlem4 $p |- ( ph -> N e. S ) $= + ( cmul co caddc cdvds wbr wcel cmin wa cn adantr cprime cz cexp simpr + c2 wceq 2sqlem3 cneg znegcld cc zcnd sqneg syl oveq1d eqtr4d mulneg1d + oveq2d zmulcld negsubd eqtrd breq2d biimpar wo zsqcl zsubcld dvdsmul1 + prmz syl2anc sqcld pnpcand sqmuld oveq12d adddid nncnd mulcomd eqtr3d + mul12d adddird subdid subsq breqtrd wb zaddcld euclemma syl3anc mpbid + nnzd mpjaodan ) AGEDSTZCFSTZUATZUBUCZIHUDGWQWRUETZUBUCZAWTUFBCDEFGHIJ + AIUGUDZWTKUHAGUIUDZWTLUHACUJUDZWTMUHADUJUDZWTNUHAEUJUDZWTOUHAFUJUDZWT + PUHAIGSTZCUMUKTZDUMUKTZUATZUNWTQUHAGEUMUKTZFUMUKTZUATZUNZWTRUHAWTULUO + AXBUFBCUPZDEFGHIJAXCXBKUHAXDXBLUHAXQUJUDXBACMUQUHAXFXBNUHAXGXBOUHAXHX + BPUHAXIXQUMUKTZXKUATZUNXBAXIXLXSQAXRXJXKUAACURUDXRXJUNACMUSZCUTVAVBVC + UHAXPXBRUHAGWQXQFSTZUATZUBUCXBAYBXAGUBAYBWQWRUPZUATXAAYAYCWQUAACFXTAF + PUSZVDVEAWQWRAWQAEDONVFZUSZAWRACFMPVFZUSZVGVHVIVJUOAGWSXASTZUBUCZWTXB + VKZAGGXMISTZXJUETZSTZYIUBAGUJUDZYMUJUDGYNUBUCAXDYOLGVOVAZAYLXJAXMIAXG + XMUJUDOEVLVAZAIKWOVFZAXEXJUJUDMCVLVAZVMGYMVNVPAWQUMUKTZWRUMUKTZUETZYN + YIAECSTZUMUKTZYTUATZUUDUUAUATZUETZUUBYNAUUDYTUUAAUUCAUUCAECOMVFUSVQAW + QYFVQAWRYHVQVRAUUGGYLSTZGXJSTZUETYNAUUEUUHUUFUUIUEAUUEXMXLSTZUUHAUUEX + MXJSTZXMXKSTZUATUUJAUUDUUKYTUULUAAECAEOUSZXTVSZAEDUUMADNUSZVSVTAXMXJX + KAEUUMVQZAXJYSUSZADUUOVQWAVCAUUJXMGISTZSTUUHAXLUURXMSAXIXLUURQAIGAIKW + BZAGYPUSZWCWDVEAXMGIUUPUUTUUSWEVHVHAUUFXOXJSTZUUIAUUFUUKXNXJSTZUATUVA + AUUDUUKUUAUVBUAUUNAUUAXJXNSTUVBACFXTYDVSAXJXNUUQAFYDVQZWCVHVTAXMXNXJA + XMYQUSUVCUUQWFVCAGXOXJSRVBVCVTAGYLXJUUTAYLYRUSUUQWGVCWDAWQURUDWRURUDU + UBYIUNYFYHWQWRWHVPWDWIAXDWSUJUDXAUJUDYJYKWJLAWQWRYEYGWKAWQWRYEYGVMGWS + XAWLWMWNWP $. + $} + + 2sqlem5.3 $e |- ( ph -> ( N x. P ) e. S ) $. + 2sqlem5.4 $e |- ( ph -> P e. S ) $. + $( Lemma for 2sq . If a number that is a sum of two squares is divisible + by a prime that is a sum of two squares, then the quotient is a sum of + two squares. (Contributed by Mario Carneiro, 20-Jun-2015.) $) + 2sqlem5 $p |- ( ph -> N e. S ) $= + ( vp vq vx vy cv co cz wrex wcel wa cexp caddc wceq cmul 2sqlem2 reeanv + c2 sylib cprime simplrr simprlr simplrl simprll simprrr simprrl 2sqlem4 + cn ad2antrr expr rexlimdvva syl5bir mp2and ) ACKOZUGUAPLOZUGUAPUBPUCZLQ + RZKQRZECUDPZMOZUGUAPNOZUGUAPUBPUCZNQRZMQRZEDSZACDSVGJKLBCDFUEUHAVHDSVMI + MNBVHDFUEUHVGVMTVFVLTZMQRKQRAVNVFVLKMQQUFAVOVNKMQQVOVEVKTZNQRLQRAVCQSZV + IQSZTZTZVNVEVKLNQQUFVTVPVNLNQQVTVDQSZVJQSZTZVPVNVTWCVPTZTBVIVJVCVDCDEFA + EUQSVSWDGURACUISVSWDHURAVQVRWDUJVTWAWBVPUKAVQVRWDULVTWAWBVPUMVTWCVEVKUN + VTWCVEVKUOUPUSUTVAUTVAVB $. + $} + + ${ + 2sqlem6.1 $e |- ( ph -> A e. NN ) $. + 2sqlem6.2 $e |- ( ph -> B e. NN ) $. + 2sqlem6.3 $e |- ( ph -> A. p e. Prime ( p || B -> p e. S ) ) $. + 2sqlem6.4 $e |- ( ph -> ( A x. B ) e. S ) $. + $( Lemma for 2sq . If a number that is a sum of two squares is divisible + by a number whose prime divisors are all sums of two squares, then the + quotient is a sum of two squares. (Contributed by Mario Carneiro, + 20-Jun-2015.) $) + 2sqlem6 $p |- ( ph -> A e. S ) $= + ( vm cn wcel cmul wi wral cdvds cprime wa vx vy vz vn cv co wbr c1 wceq + breq2 imbi1d ralbidv oveq2 eleq1d imbi12d nncn mulid1d biimpd a1i breq1 + rgen eleq1 rspcv cz prmz iddvds syl simprl simpll simprr simplr 2sqlem5 + expr ralrimiva ex embantd syld c2 cuz cfv anim12 wo wb eluzelz ad2antrr + simpr ad2antlr euclemma syl3anc jaob bitrdi ralbidva r19.26 cbvralvw cc + biimpa oveq1 adantl uzssz zsscn sstri sselid w3a mulass eqtr3d nnmulcld + mul32 eluz2nn sylc sylbird imim1d ralimdva sylan2b expimpd com23 prmind + syl5 syl3c ) ACMNLUEZDOUFZENZXSENZPZLMQZCDOUFZENZCENZHADMNFUEZDRUGZYHEN + ZPZFSQZYDIJYHUAUEZRUGZYJPZFSQZXSYMOUFZENZYBPZLMQZPYHUHRUGZYJPZFSQZXSUHO + UFZENZYBPZLMQZPYHUBUEZRUGZYJPZFSQZXSUUHOUFZENZYBPZLMQZPZYHUCUEZRUGZYJPZ + FSQZXSUUQOUFZENZYBPZLMQZPZYHUUHUUQOUFZRUGZYJPZFSQZXSUVFOUFZENZYBPZLMQZP + ZYLYDPUAUBUCDYMUHUIZYPUUCYTUUGUVOYOUUBFSUVOYNUUAYJYMUHYHRUJUKULUVOYSUUF + LMUVOYRUUEYBUVOYQUUDEYMUHXSOUMUNUKULUOYMUUHUIZYPUUKYTUUOUVPYOUUJFSUVPYN + UUIYJYMUUHYHRUJUKULUVPYSUUNLMUVPYRUUMYBUVPYQUULEYMUUHXSOUMUNUKULUOYMUUQ + UIZYPUUTYTUVDUVQYOUUSFSUVQYNUURYJYMUUQYHRUJUKULUVQYSUVCLMUVQYRUVBYBUVQY + QUVAEYMUUQXSOUMUNUKULUOYMUVFUIZYPUVIYTUVMUVRYOUVHFSUVRYNUVGYJYMUVFYHRUJ + UKULUVRYSUVLLMUVRYRUVKYBUVRYQUVJEYMUVFXSOUMUNUKULUOYMDUIZYPYLYTYDUVSYOY + KFSUVSYNYIYJYMDYHRUJUKULUVSYSYCLMUVSYRYAYBUVSYQXTEYMDXSOUMUNUKULUOUUGUU + CUUFLMXSMNZUUEYBUVTUUDXSEUVTXSXSUPZUQUNURVAUSYMSNZYPYMYMRUGZYMENZPZYTYO + UWEFYMSYHYMUIYNUWCYJUWDYHYMYMRUTYHYMEVBUOVCUWBUWCUWDYTUWBYMVDNUWCYMVEYM + VFVGUWBUWDYTUWBUWDTZYSLMUWFUVTYRYBUWFUVTYRTZTBYMEXSGUWFUVTYRVHUWBUWDUWG + VIUWFUVTYRVJUWBUWDUWGVKVLVMVNVOVPVQUUPUVETUUKUUTTZUUOUVDTZPZUUHVRVSVTZN + ZUUQUWKNZTZUVNUUKUUOUUTUVDWAUWNUVIUWJUVMUWNUVIUWJUVMPUWNUVITZUWHUWIUVMU + WNUVIUWHUWNUVIUUJUUSTZFSQUWHUWNUVHUWPFSUWNYHSNZTZUVHUUIUURWBZYJPUWPUWRU + VGUWSYJUWRUWQUUHVDNZUUQVDNZUVGUWSWCUWNUWQWFUWLUWTUWMUWQVRUUHWDWEUWMUXAU + WLUWQVRUUQWDWGYHUUHUUQWHWIUKUUIYJUURWJWKWLUUJUUSFSWMWKWPUWOUUOUVDUVMUUO + UWOUDUEZUUHOUFZENZUXBENZPZUDMQZUVDUVMPUUNUXFLUDMXSUXBUIZUUMUXDYBUXEUXHU + ULUXCEXSUXBUUHOWQUNXSUXBEVBUOWNUWOUXGTZUVCUVLLMUXIUVTTZUVKUVBYBUXJUVKUV + AUUHOUFZENZUVBUXJUXKUVJEUXJXSWONZUUHWONZUUQWONZUXKUVJUIUVTUXMUXIUWAWRUX + JUWKWOUUHUWKVDWOVRWSWTXAZUWOUWLUXGUVTUWLUWMUVIVIWEXBUXJUWKWOUUQUXPUWOUW + MUXGUVTUWLUWMUVIVKWEZXBUXMUXNUXOXCUULUUQOUFUXKUVJXSUUHUUQXGXSUUHUUQXDXE + WIUNUXJUVAMNUXGUXLUVBPZUXJXSUUQUXIUVTWFUXJUWMUUQMNUXQUUQXHVGXFUWOUXGUVT + VKUXFUXRUDUVAMUXBUVAUIZUXDUXLUXEUVBUXSUXCUXKEUXBUVAUUHOWQUNUXBUVAEVBUOV + CXIXJXKXLXMXNVPVOXOXQXPXIKYCYFYGPLCMXSCUIZYAYFYBYGUXTXTYEEXSCDOWQUNXSCE + VBUOVCXR $. + $} + + 2sqlem7.2 $e |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ + z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) } $. + $( Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) $) + 2sqlem7 $p |- Y C_ ( S i^i NN ) $= + ( cv co c1 wceq wa cz wrex cn wcel cc0 wb cn0 cgcd c2 caddc cab cin simpr + cexp reximi 2sqlem2 sylibr wn 1ne0 gcdeq0 adantr eqeq1d bitr3d necon3bbid + wne mpbiri cle wbr zsqcl2 ad2antrr nn0red nn0ge0d ad2antlr add20 syl22anc + cr cc zcn sqeq0 bi2anan9 syl2anc bitrd mtbird nn0addcl syl2an elnn0 sylib + wo ecased eleq1 syl5ibrcom expimpd rexlimivv elind abssi eqsstri ) FAIZBI + ZUAJZKLZCIZWJUBUGJZWKUBUGJZUCJZLZMZBNOZANOZCUDEPUEZHXACXBXAEPWNXAWRBNOZAN + OWNEQWTXCANWSWRBNWMWRUFUHUHABDWNEGUIUJWSWNPQZABNNWJNQZWKNQZMZWMWRXDXGWMMZ + XDWRWQPQZXHXIWQRLZXHXJWJRLZWKRLZMZXHXMUKKRURULXHXMKRXHWLRLZXMKRLXGXNXMSWM + WJWKUMUNXHWLKRXGWMUFUOUPUQUSXHXJWORLZWPRLZMZXMXHWOVIQRWOUTVAWPVIQRWPUTVAX + JXQSXHWOXEWOTQZXFWMWJVBZVCZVDXHWOXTVEXHWPXFWPTQZXEWMWKVBZVFZVDXHWPYCVEWOW + PVGVHXHWJVJQZWKVJQZXQXMSXEYDXFWMWJVKVCXFYEXEWMWKVKVFYDXOXKYEXPXLWJVLWKVLV + MVNVOVPXHWQTQZXIXJWAXGYFWMXEXRYAYFXFXSYBWOWPVQVRUNWQVSVTWBWNWQPWCWDWEWFWG + WHWI $. + + ${ + 2sqlem9.5 $e |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) + A. a e. Y ( b || a -> b e. S ) ) $. + 2sqlem9.7 $e |- ( ph -> M || N ) $. + ${ + 2sqlem8.n $e |- ( ph -> N e. NN ) $. + 2sqlem8.m $e |- ( ph -> M e. ( ZZ>= ` 2 ) ) $. + 2sqlem8.1 $e |- ( ph -> A e. ZZ ) $. + 2sqlem8.2 $e |- ( ph -> B e. ZZ ) $. + 2sqlem8.3 $e |- ( ph -> ( A gcd B ) = 1 ) $. + 2sqlem8.4 $e |- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) ) $. + 2sqlem8.c $e |- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) ) $. + 2sqlem8.d $e |- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) ) $. + $( Lemma for ~ 2sqlem8 . (Contributed by Mario Carneiro, + 4-Jun-2016.) $) + 2sqlem8a $p |- ( ph -> ( C gcd D ) e. NN ) $= + ( cz wcel cc0 wceq wa wn cgcd co cn cmin cdiv c1 wne c2 cuz cfv sylib + eluz2b3 simpld 4sqlem5 cexp simprd cle cdvds simpr 4sqlem9 ex eluzelz + wbr wb syl dvdssq syl2anc sylibrd wi 1ne0 eqnetrd neneqd gcdeq0 mtbid + a1i dvdslegcd syl31anc syl2and breq2d nnle1eq1 sylibd necon3ad mpd cc + bitrd zcnd sqeq0 anbi12d gcdn0cl syl21anc ) AHUHUIZIUHUIZHUJUKZIUJUKZ + ULZUMHIUNUOUPUIAXDFHUQUOKURUOUHUIAFHKUBAKUPUIZKUSUTZAKVAVBVCUIZXIXJUL + UAKVEVDZVFZUFVGVFZAXEGIUQUOKURUOUHUIAGIKUCXMUGVGVFZAHVAVHUOUJUKZIVAVH + UOUJUKZULZXHAXJXRUMAXIXJXLVIAXRKUSAXRKFGUNUOZVJVPZKUSUKZAXPKFVKVPZXQK + GVKVPZXTAXPKVAVHUOZFVAVHUOVKVPZYBAXPYEAXPFHKUBXMUFAXPVLVMVNAKUHUIZFUH + UIZYBYEVQAXKYFUAVAKVOVRZUBKFVSVTWAAXQYDGVAVHUOVKVPZYCAXQYIAXQGIKUCXMU + GAXQVLVMVNAYFGUHUIZYCYIVQYHUCKGVSVTWAAYFYGYJFUJUKGUJUKULZUMYBYCULXTWB + YHUBUCAXSUJUKZYKAXSUJAXSUSUJUDUSUJUTAWCWHWDWEAYGYJYLYKVQUBUCFGWFVTWGK + FGWIWJWKAXTKUSVJVPZYAAXSUSKVJUDWLAXIYMYAVQXMKWMVRWRWNWOWPAXPXFXQXGAHW + QUIXPXFVQAHXNWSHWTVRAIWQUIXQXGVQAIXOWSIWTVRXAWGHIXBXC $. + + 2sqlem8.e $e |- E = ( C / ( C gcd D ) ) $. + 2sqlem8.f $e |- F = ( D / ( C gcd D ) ) $. + $( Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015.) $) + 2sqlem8 $p |- ( ph -> M e. S ) $= + ( vp c2 cexp co caddc cdiv cn c1 wne cuz cfv wa eluz2b3 simpld cz cc0 + wcel clt wbr cdvds cgcd cmul wceq cmin syl nnzd 4sqlem5 zsqcl zsubcld + 4sqlem8 oveq1d zcnd eqtrd breqtrrd dvdssub2 syl31anc mpbid cn0 zsqcl2 + nn0cnd gcddvds syl2anc nnne0d dvdsval2 syl3anc eqeltrid simprd sqmuld + wb oveq2i nnap0d divcanap2d syl5eq eqtr3d oveq12d gcdcld nn0zd mpbird + cle dvdstrd wn wi a1i mp2and breqtrd nn0red readdcld nnred sstri wrex + mpd oveq1 eqeq1d eqeq2d anbi12d syl112anc sselid nngt0d wral ad2antrl + cv cprime adantr zred cr rehalfcld nnsqcld 4sqlem7 letrd sylib adddid + eluzelz zaddcld dvds2addd addsub4d gcdcomd 1ne0 eqnetrd neneqd gcdeq0 + 2sqlem8a mtbid dvdslegcd simpr necon3ai gcdn0cl syl21anc nnle1eq1 2nn + rplpwr nn0addcld coprmdvds 2sqlem7 inss2 1cnd mulid1d mulgcd 3eqtr2rd + cin mulcanapad eqidd oveq2 oveq2d rspc2ev eqeq1 anbi2d elab2g divgt0d + 2rexbidv elnnz sylanbrc cfz prmnn peano2zm simprr prmz dvdsle nn0ge0d + 1red nnge1d lemul1ad mulid2d 3brtr3d le2addd recnd 2halvesd crp nnrpd + rphalflt lelttrd sqvald ltdivmul zltlem1 mpbir2and jca dvdsmul2 breq1 + fznn eleq1w imbi12d breq2 imbi1d rspc2v syl3c ralrimiva inss1 eqeltrd + expr 2sqlem6 ) AEMKUMUNUOZLUMUNUOZUPUOZMUQUOZJULRAMURVHZMUSUTZAMUMVAV + BVHZUYEUYFVCUCMVDUUAVEZAUYDVFVHZVGUYDVIVJUYDURVHZAMUYCVKVJZUYIAMHIVLU + OZUMUNUOZUYCVMUOZVKVJZMUYMVLUOZUSVNZUYKAMHUMUNUOZIUMUNUOZUPUOZUYNVKAM + NVKVJZMUYTVKVJZUAAMVFVHZNVFVHUYTVFVHMNUYTVOUOZVKVJVUAVUBWTAUYGVUCUCUM + MUUCVPZANUBVQAUYRUYSAHVFVHZUYRVFVHAVUFFHVOUOZMUQUOVFVHZAFHMUDUYHUHVRZ + VEZHVSVPZAIVFVHZUYSVFVHAVULGIVOUOZMUQUOVFVHZAGIMUEUYHUIVRZVEZIVSVPZUU + DAMFUMUNUOZUYRVOUOZGUMUNUOZUYSVOUOZUPUOZVUDVKAMVUSVVAVUEAVURUYRAFVFVH + ZVURVFVHUDFVSVPZVUKVTAVUTUYSAGVFVHZVUTVFVHUEGVSVPZVUQVTAFHMUDUYHUHWAA + GIMUEUYHUIWAUUEAVUDVURVUTUPUOZUYTVOUOVVBANVVGUYTVOUGWBAVURVUTUYRUYSAV + URVVDWCAVUTVVFWCAUYRVUKWCAUYSVUQWCUUFWDWEMNUYTWFWGWHAUYNUYMUYAVMUOZUY + MUYBVMUOZUPUOUYTAUYMUYAUYBAUYMAUYLVFVHZUYMWIVHAUYLABCDEFGHIJMNOPQRSTU + AUBUCUDUEUFUGUHUIUULZVQZUYLWJVPWKAUYAAKVFVHZUYAWIVHAKHUYLUQUOZVFUJAUY + LHVKVJZVVNVFVHZAVVOUYLIVKVJZAVUFVULVVOVVQVCVUJVUPHIWLWMZVEZAVVJUYLVGU + TZVUFVVOVVPWTVVLAUYLVVKWNZVUJUYLHWOWPWHWQZKWJVPZWKAUYBALVFVHZUYBWIVHA + LIUYLUQUOZVFUKAVVQVWEVFVHZAVVOVVQVVRWRZAVVJVVTVULVVQVWFWTVVLVWAVUPUYL + IWOWPWHWQZLWJVPZWKUUBAVVHUYRVVIUYSUPAUYLKVMUOZUMUNUOVVHUYRAUYLKAUYLVV + LWCZAKVWBWCWSAVWJHUMUNAVWJUYLVVNVMUOHKVVNUYLVMUJXAAHUYLAHVUJWCVWKAUYL + VVKXBZXCXDZWBXEAUYLLVMUOZUMUNUOVVIUYSAUYLLVWKALVWHWCWSAVWNIUMUNAVWNUY + LVWEVMUOILVWEUYLVMUKXAAIUYLAIVUPWCVWKVWLXCXDZWBXEXFWDZWEAUYPUYMMVLUOZ + USAMUYMVUEAVVJUYMVFVHZVVLUYLVSVPZUUGAUYLMVLUOZUSVNZVWQUSVNZAVWTUSXJVJ + ZVXAAVWTFGVLUOZUSXJAVWTFVKVJZVWTGVKVJZVWTVXDXJVJZAVXEVWTHVKVJZAVWTUYL + HAVWTAUYLMVVLVUEXGXHZVVLVUJAVWTUYLVKVJZVWTMVKVJZAVVJVUCVXJVXKVCVVLVUE + UYLMWLWMZVEZVVSXKAVWTVFVHZVVCVUFVWTVUGVKVJVXEVXHWTVXIUDVUJAVWTMVUGVXI + VUEAFHUDVUJVTZAVXJVXKVXLWRZAMVUGVKVJZVUHAVUFVUHVUIWRAVUCMVGUTZVUGVFVH + VXQVUHWTVUEAMUYHWNZVXOMVUGWOWPXIXKVWTFHWFWGXIAVXFVWTIVKVJZAVWTUYLIVXI + VVLVUPVXMVWGXKAVXNVVEVULVWTVUMVKVJVXFVXTWTVXIUEVUPAVWTMVUMVXIVUEAGIUE + VUPVTZVXPAMVUMVKVJZVUNAVULVUNVUOWRAVUCVXRVUMVFVHVYBVUNWTVUEVXSVYAMVUM + WOWPXIXKVWTGIWFWGXIAVXNVVCVVEFVGVNGVGVNVCZXLVXEVXFVCVXGXMVXIUDUEAVXDV + GVNZVYCAVXDVGAVXDUSVGUFUSVGUTAUUHXNUUIUUJAVVCVVEVYDVYCWTUDUEFGUUKWMUU + MVWTFGUUNWGXOUFXPAVWTURVHZVXCVXAWTAVVJVUCUYLVGVNZMVGVNZVCZXLZVYEVVLVU + EAVXRVYIVXSVYHMVGVYFVYGUUOUUPVPUYLMUUQUURVWTUUSVPWHAUYLURVHUYEUMURVHZ + VXAVXBXMVVKUYHVYJAUUTXNUYLMUMUVAWPYBWDAVUCVWRUYCVFVHZUYOUYQVCUYKXMVUE + VWSAUYCAUYAUYBVWCVWIUVBZXHZMUYMUYCUVCWPXOAVUCVXRVYKUYKUYIWTVUEVXSVYMM + UYCWOWPWHZAUYCMAUYAUYBAUYAVWCXQAUYBVWIXQXRZAMUYHXSZAUYCAOURUYCOJURUVJ + ZURBCDEJORSUVDZJURUVEXTAUYCOVHZBYLZCYLZVLUOZUSVNZUYCVYTUMUNUOZWUAUMUN + UOZUPUOZVNZVCZCVFYABVFYAZAVVMVWDKLVLUOZUSVNZUYCUYCVNZWUIVWBVWHAWUJUSU + YLAWUJAKLVWBVWHXGWKAUVFVWKVWLAUYLUSVMUOUYLVWJVWNVLUOZUYLWUJVMUOZAUYLV + WKUVGAVWJHVWNIVLVWMVWOXFAUYLWIVHVVMVWDWUMWUNVNAHIVUJVUPXGVWBVWHUYLKLU + VHWPUVIUVKAUYCUVLWUHWUKWULVCKWUAVLUOZUSVNZUYCUYAWUEUPUOZVNZVCBCKLVFVF + VYTKVNZWUCWUPWUGWURWUSWUBWUOUSVYTKWUAVLYCYDWUSWUFWUQUYCWUSWUDUYAWUEUP + VYTKUMUNYCWBYEYFWUALVNZWUPWUKWURWULWUTWUOWUJUSWUALKVLUVMYDWUTWUQUYCUY + CWUTWUEUYBUYAUPWUALUMUNYCUVNYEYFUVOYGAUYCWIVHVYSWUIWTVYLWUCDYLZWUFVNZ + VCZCVFYABVFYAWUIDUYCOWIWVAUYCVNZWVCWUHBCVFVFWVDWVBWUGWUCWVAUYCWUFUVPU + VQUVTSUVRVPXIZYHYIAMUYHYIZUVSUYDUWAUWBZAULYLZUYDVKVJZWVHJVHZXMULYMAWV + HYMVHZWVIWVJAWVKWVIVCZVCZWVHUSMUSVOUOZUWCUOZVHZVYSVCQYLZPYLZVKVJZWVQJ + VHZXMZPOYJQWVOYJZWVHUYCVKVJZWVJWVMWVPVYSWVMWVPWVHURVHZWVHWVNXJVJZWVKW + WDAWVIWVHUWDYKZWVMWVHUYDWVNWVMWVHWWFXSWVMUYDAUYIWVLVYNYNZYOAWVNYPVHWV + LAWVNAVUCWVNVFVHZVUEMUWEVPZYOYNWVMWVIWVHUYDXJVJZAWVKWVIUWFZWVMWVHVFVH + ZUYJWVIWWJXMWVKWWLAWVIWVHUWGYKZAUYJWVLWVGYNWVHUYDUWHWMYBAUYDWVNXJVJZW + VLAUYDMVIVJZWWNAWWOUYCMMVMUOZVIVJZAUYCMUMUNUOZWWPVIAUYCWWRUMUQUOZWWRV + YOAWWRAWWRAVUCWWRVFVHVUEMVSVPYOZYQZWWTAUYCUYTWWSVYOAUYRUYSAUYRVUKYOZA + UYSVUQYOZXRWXAAUSUYCVMUOUYNUYCUYTXJAUSUYMUYCAUWJAUYMAUYLVVKYRZXSVYOAU + YCVYLUWIAUYMWXDUWKUWLAUYCAUYCVYLWKZUWMVWPUWNAUYTWWSUMUQUOZWXFUPUOWWSX + JAUYRUYSWXFWXFWXBWXCAWWSWXAYQZWXGAFHMUDUYHUHYSAGIMUEUYHUIYSUWOAWWSAWW + SWXAUWPUWQXPYTAWWRUWRVHWWSWWRVIVJAWWRAMUYHYRUWSWWRUWTVPUXAAMAMVUEWCZU + XBXPAUYCYPVHMYPVHZWXIVGMVIVJWWOWWQWTVYOVYPVYPWVFUYCMMUXCYGXIAUYIVUCWW + OWWNWTVYNVUEUYDMUXDWMWHYNYTWVMWWHWVPWWDWWEVCWTAWWHWVLWWIYNWVHWVNUXIVP + UXEAVYSWVLWVEYNUXFAWWBWVLTYNWVMWVHUYDUYCWWMWWGAVYKWVLVYMYNWWKAUYDUYCV + KVJWVLAUYDMUYDVMUOZUYCVKAVUCUYIUYDWXJVKVJVUEVYNMUYDUXGWMAUYCMWXEWXHAM + UYHXBXCZXPYNXKWWAWWCWVJXMWVHWVRVKVJZWVJXMQPWVHUYCWVOOWVQWVHVNWVSWXLWV + TWVJWVQWVHWVRVKUXHQULJUXJUXKWVRUYCVNWXLWWCWVJWVRUYCWVHVKUXLUXMUXNUXOU + XSUXPAWXJUYCJWXKAOJUYCOVYQJVYRJURUXQXTWVEYHUXRUXT $. + $} + + 2sqlem9.6 $e |- ( ph -> M e. NN ) $. + 2sqlem9.4 $e |- ( ph -> N e. Y ) $. + $( Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) $) + 2sqlem9 $p |- ( ph -> M e. S ) $= + ( co c1 cz vu vv cv cgcd wceq c2 cexp caddc wa wrex wcel eqeq1 2rexbidv + anbi2d oveq1 eqeq1d oveq1d eqeq2d anbi12d oveq2 oveq2d cbvrex2vw bitrdi + elab2g ibi syl wne simpr cabs cfv cgz zgz ax-mp sq1 eqcomi fveq2 eqtrdi + abs1 rspceeqv mp2an 2sqlem1 mpbir eqeltrdi cdiv cmo cmin cdvds wbr wral + 1z wi cfz ad2antrr cn cin 2sqlem7 inss2 sstri sselid cuz simprr eluz2b3 + sylanbrc simplrl simplrr simprll simprlr eqid 2sqlem8 anassrs wdc zdceq + wo nnzd sylancl dcne sylib mpjaodan ex rexlimdvva mpd ) AUAUCZUBUCZUDRZ + SUEZHYBUFUGRZYCUFUGRZUHRZUEZUIZUBTUJUATUJZGFUKZAHIUKZYKQYMYKBUCZCUCZUDR + ZSUEZDUCZYNUFUGRZYOUFUGRZUHRZUEZUIZCTUJBTUJZYKDHIIYRHUEZUUDYQHUUAUEZUIZ + CTUJBTUJYKUUEUUCUUGBCTTUUEUUBUUFYQYRHUUAULUNUMUUGYJYBYOUDRZSUEZHYFYTUHR + ZUEZUIBCUAUBTTYNYBUEZYQUUIUUFUUKUULYPUUHSYNYBYOUDUOUPUULUUAUUJHUULYSYFY + TUHYNYBUFUGUOUQURUSYOYCUEZUUIYEUUKYIUUMUUHYDSYOYCYBUDUTUPUUMUUJYHHUUMYT + YGYFUHYOYCUFUGUOVAURUSVBVCMVDVEVFAYJYLUAUBTTAYBTUKZYCTUKZUIZUIZYJYLUUQY + JUIZGSUEZYLGSVGZUURUUSUIGSFUURUUSVHSFUKSYNVIVJZUFUGRZUEBVKUJZSVKUKZSSUF + UGRZUEUVCSTUKZUVDWJSVLVMUVESVNVOBSVKUVBUVESYNSUEZUVASUFUGUVGUVASVIVJSYN + SVIVPVRVQUQVSVTBESFLWAWBWCUUQYJUUTYLUUQYJUUTUIZUIZBCDEYBYCYBGUFWDRZUHRG + WERUVJWFRZYCUVJUHRGWERUVJWFRZFUVKUVKUVLUDRZWDRZUVLUVMWDRZGHIJKLMAKUCZJU + CWGWHUVPFUKWKJIWIKSGSWFRWLRWIUUPUVHNWMAGHWGWHUUPUVHOWMAHWNUKUUPUVHAIWNH + IFWNWOWNBCDEFILMWPFWNWQWRQWSWMUVIGWNUKZUUTGUFWTVJUKAUVQUUPUVHPWMUUQYJUU + TXAGXBXCAUUNUUOUVHXDAUUNUUOUVHXEUUQYEYIUUTXFUUQYEYIUUTXGUVKXHUVLXHUVNXH + UVOXHXIXJUURUUSXKZUUSUUTXMUURGTUKZUVFUVRAUVSUUPYJAGPXNWMWJGSXLXOGSXPXQX + RXSXTYA $. + $} + + $( Lemma for 2sq . Every factor of a "proper" sum of two squares (where + the summands are coprime) is a sum of two squares. (Contributed by + Mario Carneiro, 19-Jun-2015.) $) + 2sqlem10 $p |- ( ( A e. Y /\ B e. NN /\ B || A ) -> B e. S ) $= + ( va vb wcel cdvds wral c1 cfz co wceq raleqdv vm vn cn cv wi breq1 eleq1 + wbr imbi12d ralbidv caddc oveq2 elfz1eq cabs cfv c2 cexp wrex cz 1z ax-mp + cgz zgz sq1 eqcomi fveq2 abs1 eqtrdi oveq1d rspceeqv mp2an mpbir eqeltrdi + 2sqlem1 a1d ralrimivw rgen wa cmin simplr cc nncn ad2antrr ax-1cn sylancl + csn pncan oveq2d mpbird simprr peano2nn simprl 2sqlem9 ralrimiva ex breq2 + expr imbi1d cbvralvw syl6ibr wb ralsng syl sylibrd ancld cun elnnuz fzsuc + cuz sylbi ralunb bitrdi nnind elfz1end biimpi rspcdva rspcv syl5 3imp ) E + HMZFUCMZFENUHZFGMZYAFKUDZNUHZYCUEZKHOZXTYBYCUEZYALUDZYDNUHZYIGMZUEZKHOZYG + LPFQRZFYIFSZYLYFKHYOYJYEYKYCYIFYDNUFYIFGUGUIUJYMLPUAUDZQRZOYMLPPQRZOYMLPU + BUDZQRZOZYMLPYSPUKRZQRZOZYMLYNOUAUBFYPPSYMLYQYRYPPPQULTYPYSSYMLYQYTYPYSPQ + ULTYPUUBSYMLYQUUCYPUUBPQULTYPFSYMLYQYNYPFPQULTYMLYRYIYRMZYLKHUUEYKYJUUEYI + PGYIPUMPGMPAUDZUNUOZUPUQRZSAVBURZPVBMZPPUPUQRZSUUIPUSMUUJUTPVCVAUUKPVDVEA + PVBUUHUUKPUUFPSZUUGPUPUQUULUUGPUNUOPUUFPUNVFVGVHVIVJVKADPGIVNVLVMVOVPVQYS + UCMZUUAUUAYMLUUBWFZOZVRZUUDUUMUUAUUOUUMUUAUUBYDNUHZUUBGMZUEZKHOZUUOUUMUUA + UUBYPNUHZUURUEZUAHOZUUTUUMUUAUVCUUMUUAVRZUVBUAHUVDYPHMZUVAUURUVDUVEUVAVRZ + VRZABCDGUUBYPHKLIJUVGYMLPUUBPVSRZQRZOUUAUUMUUAUVFVTUVGYMLUVIYTUVGUVHYSPQU + VGYSWAMZPWAMUVHYSSUUMUVJUUAUVFYSWBWCWDYSPWGWEWHTWIUVDUVEUVAWJUUMUUBUCMZUU + AUVFYSWKZWCUVDUVEUVAWLWMWQWNWOUUSUVBKUAHYDYPSUUQUVAUURYDYPUUBNWPWRWSWTUUM + UVKUUOUUTXAUVLYMUUTLUUBUCYIUUBSZYLUUSKHUVMYJUUQYKUURYIUUBYDNUFYIUUBGUGUIU + JXBXCXDXEUUMUUDYMLYTUUNXFZOUUPUUMYMLUUCUVNUUMYSPXIUOMUUCUVNSYSXGPYSXHXJTY + MLYTUUNXKXLXDXMYAFYNMFXNXOXPYFYHKEHYDESYEYBYCYDEFNWPWRXQXRXS $. + $} + + $( ############################################################################### GUIDES AND MISCELLANEA diff --git a/mmil.raw.html b/mmil.raw.html index 913cdae7a2..c65a311980 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12443,6 +12443,18 @@ adds ` A e. ZZ ` and ` N e. NN ` conditions + + 2sqlem11 + none + the set.mm proof uses lgsqr and m1lgs + + + + 2sq + none + the set.mm proof uses 2sqlem11 + + irrdiff ~ apdiff