From e0eba2325a28140d674072bbc72dcfa19a67f4d0 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 2 Nov 2024 22:04:00 -0700 Subject: [PATCH 01/13] Add 2sqlem1 to iset.mm Stated as in set.mm. The proof is similar to the set.mm proof but needs some intuitionizing. --- iset.mm | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/iset.mm b/iset.mm index 46febfd198..2ec0a280c3 100644 --- a/iset.mm +++ b/iset.mm @@ -157958,6 +157958,27 @@ 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 $. + $} + + $( ############################################################################### GUIDES AND MISCELLANEA From e03ac8a26024dae755e62d395b94f63e47823c76 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 2 Nov 2024 22:32:35 -0700 Subject: [PATCH 02/13] copy 2sqlem2 from set.mm to iset.mm --- iset.mm | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/iset.mm b/iset.mm index 2ec0a280c3..b68389d30f 100644 --- a/iset.mm +++ b/iset.mm @@ -157976,6 +157976,23 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. $} From 6917819bb7d812ce06421c2a2a70fa9daeff6810 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 2 Nov 2024 22:33:18 -0700 Subject: [PATCH 03/13] copy mul2sq from set.mm to iset.mm --- iset.mm | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/iset.mm b/iset.mm index b68389d30f..1d4ab6cf2a 100644 --- a/iset.mm +++ b/iset.mm @@ -157993,6 +157993,21 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. $} From b08697eec5f33b3eb7ee5dc1426d1d940cc06366 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 2 Nov 2024 22:44:24 -0700 Subject: [PATCH 04/13] 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. --- iset.mm | 58 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/iset.mm b/iset.mm index 1d4ab6cf2a..ff133748a7 100644 --- a/iset.mm +++ b/iset.mm @@ -158008,6 +158008,64 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. + $} + $} + $} $} From 98f634c5c39c0cc033fca419082284591bd98290 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 2 Nov 2024 22:45:58 -0700 Subject: [PATCH 05/13] copy 2sqlem4 from set.mm to iset.mm --- iset.mm | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/iset.mm b/iset.mm index ff133748a7..7419f6f0b6 100644 --- a/iset.mm +++ b/iset.mm @@ -158064,6 +158064,33 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. $} $} $} From 1f4d8bd946c350d2cabb1dbf3bf05818c30af66a Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 2 Nov 2024 22:46:37 -0700 Subject: [PATCH 06/13] copy 2sqlem5 from set.mm to iset.mm --- iset.mm | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/iset.mm b/iset.mm index 7419f6f0b6..a9f4138791 100644 --- a/iset.mm +++ b/iset.mm @@ -158092,6 +158092,22 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. $} $} From a5241bf0e755132ed3e3441113b317f25d99785b Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 2 Nov 2024 22:47:10 -0700 Subject: [PATCH 07/13] copy 2sqlem6 from set.mm to iset.mm --- iset.mm | 47 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/iset.mm b/iset.mm index a9f4138791..abfdc14ad2 100644 --- a/iset.mm +++ b/iset.mm @@ -158109,6 +158109,53 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. + $} $} From fa8345010ef39df6c839d3b2ec457b4386bdce9b Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 2 Nov 2024 22:52:54 -0700 Subject: [PATCH 08/13] 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. --- iset.mm | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/iset.mm b/iset.mm index abfdc14ad2..2a4b494efc 100644 --- a/iset.mm +++ b/iset.mm @@ -158156,6 +158156,24 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. $} From 0722cdaca809840f4c4dd8e520074cca77a88a3a Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 2 Nov 2024 23:05:50 -0700 Subject: [PATCH 09/13] 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. --- iset.mm | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/iset.mm b/iset.mm index 2a4b494efc..2f8aab5ece 100644 --- a/iset.mm +++ b/iset.mm @@ -158174,6 +158174,39 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. + $} + $} $} From 07ef7df73088d6f1c779fcf5500ce7334c5aff39 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 3 Nov 2024 07:31:52 -0800 Subject: [PATCH 10/13] Add 2sqlem8 to iset.mm Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof. --- iset.mm | 83 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/iset.mm b/iset.mm index 2f8aab5ece..548fcd9ba0 100644 --- a/iset.mm +++ b/iset.mm @@ -158205,6 +158205,89 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. $} $} $} From 0d45163c770230def576ff6f30394fda633d5a63 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 3 Nov 2024 14:41:03 -0800 Subject: [PATCH 11/13] 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. --- iset.mm | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/iset.mm b/iset.mm index 548fcd9ba0..e875429fc9 100644 --- a/iset.mm +++ b/iset.mm @@ -158289,6 +158289,33 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. $} $} From c2d85d6ad46778773a640e2b2e8977fda250e35b Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 3 Nov 2024 15:16:51 -0800 Subject: [PATCH 12/13] 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. --- iset.mm | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/iset.mm b/iset.mm index e875429fc9..c7b8dc5bdf 100644 --- a/iset.mm +++ b/iset.mm @@ -158317,6 +158317,32 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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 $. $} From 979bf87ec5d2279b13ef7cdbb8a05f95e91e554d Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 11 Nov 2024 22:06:12 -0800 Subject: [PATCH 13/13] 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 | 27 +++++++++++++-------------- mmil.raw.html | 12 ++++++++++++ 2 files changed, 25 insertions(+), 14 deletions(-) diff --git a/iset.mm b/iset.mm index c7b8dc5bdf..ae879ef0cb 100644 --- a/iset.mm +++ b/iset.mm @@ -157970,14 +157970,14 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is $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.) $) + $( 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.) $) + $( 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 @@ -158095,10 +158095,9 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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.) $) + $( 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 @@ -158115,10 +158114,10 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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.) $) + $( 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 @@ -158159,7 +158158,7 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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.) $) + $( 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 @@ -158208,7 +158207,7 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 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.) $) + $( 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 @@ -158292,7 +158291,7 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is 2sqlem9.6 $e |- ( ph -> M e. NN ) $. 2sqlem9.4 $e |- ( ph -> N e. Y ) $. - $( Lemma for ~ 2sq . (Contributed by Mario Carneiro, 19-Jun-2015.) $) + $( 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 @@ -158318,7 +158317,7 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is RXSXTYA $. $} - $( Lemma for ~ 2sq . Every factor of a "proper" sum of two squares (where + $( 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 ) $= 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