From 5940ce19c1970f7a3f82a90ddab47e8140b61377 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 6 Sep 2025 11:14:11 -0700 Subject: [PATCH 01/21] add gsumzsubmcl to mmil.html --- mmil.raw.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mmil.raw.html b/mmil.raw.html index ad394de6f..e94ee93b0 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11373,7 +11373,7 @@ - gsumsubmcl + gsumzsubmcl , gsumsubmcl ~ gsumfzsubmcl The group sum needs to be indexed by consecutive integers. Also, we don't need From 6f3381c3f7acf979d6aa4923873e88e0f8639e51 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 6 Sep 2025 15:07:38 -0700 Subject: [PATCH 02/21] add gsumsubgcl to mmil.html --- mmil.raw.html | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index e94ee93b0..5662d63c0 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11380,6 +11380,13 @@ commutativity since the order is specified. + + gsumsubgcl + none + at least at present, just use ~ gsumfzsubmcl although it + wouldn't be hard to add a version for groups rather than monoids + + gsummptfidmadd ~ gsumfzmptfidmadd From b2e83a0344d88f284c01e0c0f4da58c818fc5948 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 6 Sep 2025 17:03:29 -0700 Subject: [PATCH 03/21] add gsumzaddlem , gsumzadd , gsumadd to mmil.html --- mmil.raw.html | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 5662d63c0..3813e6248 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11387,6 +11387,13 @@ wouldn't be hard to add a version for groups rather than monoids + + gsumzaddlem , gsumzadd , gsumadd + none + should be possible to prove versions indexed by + consecutive integers. + + gsummptfidmadd ~ gsumfzmptfidmadd From 0eb720e6653c3516b4b54a8e8a20cd0ee0b75853 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 6 Sep 2025 17:05:47 -0700 Subject: [PATCH 04/21] add gsummptfsadd to mmil.html --- mmil.raw.html | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 3813e6248..439dbcdfb 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11394,6 +11394,13 @@ consecutive integers. + + gsummptfsadd + none + should be possible (for sums indexed by consecutive integers) + given a theorem similar to gsumadd + + gsummptfidmadd ~ gsumfzmptfidmadd From bb31fcdbce95ba884915c738521ccbd46e1b1c15 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 6 Sep 2025 17:39:52 -0700 Subject: [PATCH 05/21] add gsum split theorems to mmil.html This is gsumzsplit , gsumsplit , gsumsplit2 , gsummptfidmsplit , gsummptfidmsplitres , gsummptfzsplit , and gsummptfzsplitl --- mmil.raw.html | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 439dbcdfb..0a0ff1102 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11415,6 +11415,21 @@ consecutive integers. + + gsumzsplit , gsumsplit , gsumsplit2 , gsummptfidmsplit , + gsummptfidmsplitres + none + should be possible to prove versions indexed by + consecutive integers (compare with gsummptfzsplit and gsummptfzsplitl + ). + + + + gsummptfzsplit , gsummptfzsplitl + none + apparently these would be provable as stated + + mgpval ~ mgpvalg From b6763e6eab8f86775bfddd5bb22e9168cecd8a8e Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 8 Sep 2025 12:48:32 -0700 Subject: [PATCH 06/21] Add gsumfzconst to iset.mm This is gsumconst from set.mm where the sum is indexed by consecutive integers. The proof is a new one by induction. --- iset.mm | 43 +++++++++++++++++++++++++++++++++++++++++++ mmil.raw.html | 8 ++++++++ 2 files changed, 51 insertions(+) diff --git a/iset.mm b/iset.mm index 0da793396..80eda4296 100644 --- a/iset.mm +++ b/iset.mm @@ -155954,6 +155954,49 @@ by a normal subgroup (resp. two-sided ideal). (Contributed by Mario FGIUFCCAJKOPUGQRGBUODUEUHASUIIBUOEUEUHATUIUJUMABCDEFGHIJKLMNOPQRSTUKUL $. $} + ${ + $d .x. f $. $d .x. j w $. $d A f k x $. $d B f k x $. $d B j k w $. + $d G f k x $. $d G j k w $. $d M j k w $. $d N k w $. $d X f k x $. + $d X j k w $. + gsumconst.b $e |- B = ( Base ` G ) $. + gsumconst.m $e |- .x. = ( .g ` G ) $. + $( Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) + (Revised by Jim Kingdon, 6-Sep-2025.) $) + gsumfzconst $p |- ( ( G e. Mnd /\ N e. ( ZZ>= ` M ) /\ X e. B ) -> + ( G gsum ( k e. ( M ... N ) |-> X ) ) = ( ( ( N - M ) + 1 ) .x. X ) ) $= + ( wcel cfv cfz co cgsu cmin c1 caddc wceq wi oveq1d vw vj cmnd cuz w3a wa + simp2 3simpb cv oveq2 mpteq1d oveq2d oveq1 eqeq12d imbi2d cz simplr mulg1 + cmpt syl cc0 zcn subidd 0p1e1 eqtrdi adantl cplusg cseq eqid uzid simpllr + simpll fmpttd gsumval2 cvv simpr cfn fzfigd mptexd plusgslid slotex seq1g + syl3anc eqidd elfz3 fvmptd3 3eqtrd 3eqtr4rd expcom wss fzssp1 a1i resmptd + cres eqtrd peano2uz eluzfz2 oveq12d simplll eluzel2 wf adantr gsumsplit1r + 3syl cn uznn0sub nn0p1nn mulgnnp1 syl2anc 3eqtr4d cneg eluzelcn zcnd 1cnd + cn0 negcld add32d negsubd addcld 3eqtr3d ex a2d uzind4 sylc ) DUCJZFEUDKZ + JZGAJZUEYGYEYHUFZDCEFLMZGUSZNMZFEOMZPQMZGBMZRZYEYGYHUGYEYGYHUHYIDCEUAUIZL + MZGUSZNMZYQEOMZPQMZGBMZRZSYIDCEELMZGUSZNMZEEOMZPQMZGBMZRZSYIDCEUBUIZLMZGU + SZNMZUULEOMZPQMZGBMZRZSYIDCEUULPQMZLMZGUSZNMZUUTEOMZPQMZGBMZRZSYIYPSUAUBE + FYQERZUUDUUKYIUVHYTUUGUUCUUJUVHYSUUFDNUVHCYRUUEGYQEELUJUKULUVHUUBUUIGBUVH + UUAUUHPQYQEEOUMTTUNUOYQUULRZUUDUUSYIUVIYTUUOUUCUURUVIYSUUNDNUVICYRUUMGYQU + ULELUJUKULUVIUUBUUQGBUVIUUAUUPPQYQUULEOUMTTUNUOYQUUTRZUUDUVGYIUVJYTUVCUUC + UVFUVJYSUVBDNUVJCYRUVAGYQUUTELUJUKULUVJUUBUVEGBUVJUUAUVDPQYQUUTEOUMTTUNUO + YQFRZUUDYPYIUVKYTYLUUCYOUVKYSYKDNUVKCYRYJGYQFELUJUKULUVKUUBYNGBUVKUUAYMPQ + YQFEOUMTTUNUOYIEUPJZUUKYIUVLUFZPGBMZGUUJUUGUVMYHUVNGRYEYHUVLUQZABDGHIURUT + UVLUUJUVNRYIUVLUUIPGBUVLUUIVAPQMPUVLUUHVAPQUVLEEVBVCTVDVETVFUVMUUGEDVGKZU + UFEVHKZEUUFKZGUVMAUVPUUFDEEUCHUVPVIZYEYHUVLVLZUVLEYFJYIEVJVFUVMCUUEGAYEYH + UVLCUIZUUEJVKVMVNUVMUVLUUFVOJUVPVOJZUVQUVRRYIUVLVPZUVMCUUEGVQUVMEEUWCUWCV + RVSUVMYEUWBUVTDVGUCVTWAUTUVPUUFEVOVOWBWCUVMCEGGUUEUUFAUUFVIUWAERGWDUVLEUU + EJYIEWEVFUVOWFWGWHWIUULYFJZYIUUSUVGYIUWDUUSUVGSYIUWDUFZUUSUVGUWEUUSUFZUVC + UUQPQMZGBMZUVFUWFDUVBUUMWNZNMZUUTUVBKZUVPMUURGUVPMZUVCUWHUWFUWJUURUWKGUVP + UWFUWJUUOUURUWFUWIUUNDNUWFCUVAUUMGUUMUVAWJUWFEUULWKWLWMULUWEUUSVPWOUWFCUU + TGGUVAUVBAUVBVIUWAUUTRGWDUWFUWDUUTYFJUUTUVAJYIUWDUUSUQZEUULWPEUUTWQXDYEYH + UWDUUSVKZWFWRUWFAUVPUVBDEUULUCHUVSYEYHUWDUUSWSUWFUWDUVLUWMEUULWTZUTUWMUWE + UVAAUVBXAUUSUWECUVAGAYEYHUWDUWAUVAJVKVMXBXCUWFUUQXEJZYHUWHUWLRUWFUWDUUPXO + JUWPUWMEUULXFUUPXGXDUWNAUVPBDUUQGHIUVSXHXIXJUWFUWDUWHUVFRUWMUWDUWGUVEGBUW + DUUQUVDPQUWDUULEXKZQMZPQMUUTUWQQMUUQUVDUWDUULUWQPEUULXLZUWDEUWDEUWOXMZXPU + WDXNZXQUWDUWRUUPPQUWDUULEUWSUWTXRTUWDUUTEUWDUULPUWSUXAXSUWTXRXTTTUTWOYAWI + YBYCYD $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# diff --git a/mmil.raw.html b/mmil.raw.html index 0a0ff1102..279219c4b 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11430,6 +11430,14 @@ apparently these would be provable as stated + + gsumconst + ~ gsumfzconst + requires that the series is indexed by consecutive integers + and has an element (if the latter condition is an issue, detect it + with something like ~ fzn and handle it with ~ gsum0g ) + + mgpval ~ mgpvalg From 0aecacb16b60443338eb6c1c35ce66fb9a7bec7c Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 8 Sep 2025 18:34:26 -0700 Subject: [PATCH 07/21] add gsumconstf to mmil.html --- mmil.raw.html | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 279219c4b..4ec4c3c60 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11438,6 +11438,13 @@ with something like ~ fzn and handle it with ~ gsum0g ) + + gsumconstf + none + it should be possible to adapt ~ gsumfzconst to a version with + a not-free-in hypothesis + + mgpval ~ mgpvalg From 8fb1ad3244a2ff8c129931c0fc54b189efc2d4e8 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 8 Sep 2025 18:36:40 -0700 Subject: [PATCH 08/21] add gsummptshft to mmil.html --- mmil.raw.html | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 4ec4c3c60..12836382d 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11445,6 +11445,13 @@ a not-free-in hypothesis + + gsummptshft + none + presumably provable (the sums are already indexed by consecutive + integers) + + mgpval ~ mgpvalg From 8cee88f76a79acc8996158e5f840e21f10313996 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 8 Sep 2025 21:27:30 -0700 Subject: [PATCH 09/21] Add gsumfzmhm to iset.mm This is gsummhm from set.mm but where the sum is indexed by consecutive integers. The proof is from gsumfzval , seqhomog , and some monoid theorems. --- iset.mm | 36 ++++++++++++++++++++++++++++++++++++ mmil.raw.html | 7 +++++++ 2 files changed, 43 insertions(+) diff --git a/iset.mm b/iset.mm index 80eda4296..c832a7681 100644 --- a/iset.mm +++ b/iset.mm @@ -155997,6 +155997,42 @@ by a normal subgroup (resp. two-sided ideal). (Contributed by Mario YBYCYD $. $} + ${ + $d B x y $. $d F x y $. $d G x y $. $d H x y $. $d K x y $. + $d M x y $. $d N x y $. $d ph x y $. + gsummhm.b $e |- B = ( Base ` G ) $. + gsummhm.z $e |- .0. = ( 0g ` G ) $. + gsummhm.g $e |- ( ph -> G e. CMnd ) $. + gsummhm.h $e |- ( ph -> H e. Mnd ) $. + gsummhm.m $e |- ( ph -> M e. ZZ ) $. + gsummhm.n $e |- ( ph -> N e. ZZ ) $. + gsummhm.k $e |- ( ph -> K e. ( G MndHom H ) ) $. + gsummhm.f $e |- ( ph -> F : ( M ... N ) --> B ) $. + $( Apply a monoid homomorphism to a group sum. (Contributed by Mario + Carneiro, 15-Dec-2014.) (Revised by AV, 6-Jun-2019.) (Revised by Jim + Kingdon, 8-Sep-2025.) $) + gsumfzmhm $p |- ( ph -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) $= + ( cfv wcel adantr vx vy clt wbr ccom cgsu co wceq wn wa c0g cmhm eqid syl + mhm0 cplusg cseq cif ccmn gsumfzval simpr iftrued eqtrd fveq2d cbs wf cfz + cmnd mhmf fco syl2anc 3eqtr4rd cvv cv cmnmndd simprl simprr mndcl syl3anc + adantlr ffvelcdmda cz cle cuz zred nltled eluz2 syl3anbrc ad2antrr mhmlin + fvco3 eqcomd cfn fzfigd fexd coexg plusgslid slotex seqhomog iffalsed wdc + wo zdclt exmiddc mpjaodan ) AHGUCUDZEFCUEZUFUGZDCUFUGZFRZUHXFUIZAXFUJZIFR + ZEUKRZXJXHAXMXNUHZXFAFDEULUGZSZXOPDEFXNIKXNUMZUOUNTXLXIIFXLXIXFIHDUPRZCGU + QRZURZIAXIYAUHZXFABXSCDGHUSIJKXSUMZLNOQUTZTXLXFIXTAXFVAZVBVCVDXLXHXFXNHEU + PRZXGGUQRZURZXNAXHYHUHZXFAEVERZYFXGEGHVHXNYJUMZXRYFUMZMNOABYJFVFZGHVGUGZB + CVFZYNYJXGVFAXQYMPBYJDEFJYKVIUNQYNBYJFCVJVKUTZTXLXFXNYGYEVBVCVLAXKUJZXTFR + YGXJXHYQUAUBXSYFBCXGFGHVMVMVMVMAUAVNZBSZUBVNZBSZUJZYRYTXSUGZBSZXKAUUBUJDV + HSZYSUUAUUDAUUEUUBADLVOTAYSUUAVPAYSUUAVQBXSDYRYTJYCVRVSVTAYRYNSZYRCRZBSXK + AYNBYRCQWAVTYQGWBSZHWBSZGHWCUDHGWDRSAUUHXKNTZAUUIXKOTZYQGHYQGUUJWEYQHUUKW + EAXKVAZWFGHWGWHYQUUBUJXQYSUUAUUCFRYRFRYTFRYFUGUHAXQXKUUBPWIYQYSUUAVPYQYSU + UAVQBXSYFDEFYRYTJYCYLWJVSYQUUFUJZYRXGRZUUGFRZUUMYOUUFUUNUUOUHAYOXKUUFQWIY + QUUFVAYNBYRFCWKVKWLACVMSZXKAYNBWMCQAGHNOWNWOZTAXGVMSZXKAXQUUPUURPUUQFCXPV + MWPVKTAXSVMSZXKADUSSUUSLDUPUSWQWRUNTAYFVMSZXKAEVHSUUTMEUPVHWQWRUNTWSYQXIX + TFYQXIYAXTAYBXKYDTYQXFIXTUULWTVCVDYQXHYHYGAYIXKYPTYQXFXNYGUULWTVCVLAXFXAZ + XFXKXBAUUIUUHUVAONHGXCVKXFXDUNXE $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# diff --git a/mmil.raw.html b/mmil.raw.html index 12836382d..662b6e3f5 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11452,6 +11452,13 @@ integers) + + gsummhm + ~ gsumfzmhm + The group sum needs to be indexed by + consecutive integers. + + mgpval ~ mgpvalg From 828791d0fd10c2aaa49a721e2bba470afa1d45d5 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Tue, 9 Sep 2025 16:41:55 -0700 Subject: [PATCH 10/21] Add gsumfzmhm2 to iset.mm This is gsummhm2 from set.mm where the sum is indexed by consecutive integers. The proof is similar to the set.mm proof. --- iset.mm | 26 ++++++++++++++++++++++++++ mmil.raw.html | 7 +++++++ 2 files changed, 33 insertions(+) diff --git a/iset.mm b/iset.mm index c832a7681..1a7225123 100644 --- a/iset.mm +++ b/iset.mm @@ -156033,6 +156033,32 @@ by a normal subgroup (resp. two-sided ideal). (Contributed by Mario XFXKXBAUUIUUHUVAONHGXCVKXFXDUNXE $. $} + ${ + $d k x N $. $d k x M $. $d k x B $. $d k C $. $d x D $. $d x E $. + $d k ph $. $d x G $. $d x H $. $d x X $. + gsummhm2.b $e |- B = ( Base ` G ) $. + gsummhm2.z $e |- .0. = ( 0g ` G ) $. + gsummhm2.g $e |- ( ph -> G e. CMnd ) $. + gsummhm2.h $e |- ( ph -> H e. Mnd ) $. + gsumfzmhm2.m $e |- ( ph -> M e. ZZ ) $. + gsumfzmhm2.n $e |- ( ph -> N e. ZZ ) $. + gsummhm2.k $e |- ( ph -> ( x e. B |-> C ) e. ( G MndHom H ) ) $. + gsumfzmhm2.f $e |- ( ( ph /\ k e. ( M ... N ) ) -> X e. B ) $. + gsummhm2.1 $e |- ( x = X -> C = D ) $. + gsumfzmhm2.2 $e |- ( x = ( G gsum ( k e. ( M ... N ) |-> X ) ) + -> C = E ) $. + $( Apply a group homomorphism to a group sum, mapping version with implicit + substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by + AV, 6-Jun-2019.) (Revised by Jim Kingdon, 9-Sep-2025.) $) + gsumfzmhm2 $p |- ( ph -> ( H gsum ( k e. ( M ... N ) |-> D ) ) = E ) $= + ( cmpt cfz co ccom cgsu cfv fmpttd gsumfzmhm eqidd fmptco oveq2d cbs eqid + cmnmndd gsumfzcl wcel cv wceq eleq1d wf wral cmhm mhmf syl sylibr rspcdva + fmpt fvmptd3 3eqtr3d ) AIBCDUDZFJKUEUFZLUDZUGZUHUFHVOUHUFZVMUIIFVNEUDZUHU + FGACVOHIVMJKMNOPQRSTAFVNLCUAUJZUKAVPVRIUHAFBVNCLDEVOVMUAAVOULAVMULUBUMUNA + BVQDGCVMIUOUIZVMUPZUCACVOHJKMNOAHPUQRSVSURZADVTUSZGVTUSBCVQBUTVQVADGVTUCV + BACVTVMVCZWCBCVDAVMHIVEUFUSWDTCVTHIVMNVTUPVFVGBCVTDVMWAVJVHWBVIVKVL $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# diff --git a/mmil.raw.html b/mmil.raw.html index 662b6e3f5..7ac99d280 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11459,6 +11459,13 @@ consecutive integers. + + gsummhm2 + ~ gsumfzmhm2 + The group sum needs to be indexed by + consecutive integers. + + mgpval ~ mgpvalg From 17fab448f64a0882a02970f48b1e7f870f680ca2 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 10 Sep 2025 12:17:04 -0700 Subject: [PATCH 11/21] Add gsumfzconstf to iset.mm This is gsumconstf from set.mm but indexed by consecutive integers. It is also gsumfzconst from iset.mm but with a freeness hypothesis in place of distinct variables. The proof is similar to the set.mm proof of gsumconstf . --- iset.mm | 14 ++++++++++++++ mmil.raw.html | 8 ++++++++ 2 files changed, 22 insertions(+) diff --git a/iset.mm b/iset.mm index 1a7225123..79c518ac9 100644 --- a/iset.mm +++ b/iset.mm @@ -155997,6 +155997,20 @@ by a normal subgroup (resp. two-sided ideal). (Contributed by Mario YBYCYD $. $} + ${ + $d k l N $. $d k l M $. $d l B $. $d l G $. $d l X $. + gsumconstf.k $e |- F/_ k X $. + gsumconstf.b $e |- B = ( Base ` G ) $. + gsumconstf.m $e |- .x. = ( .g ` G ) $. + $( Sum of a constant series. (Contributed by Thierry Arnoux, + 5-Jul-2017.) $) + gsumfzconstf $p |- ( ( G e. Mnd /\ N e. ( ZZ>= ` M ) /\ X e. B ) -> + ( G gsum ( k e. ( M ... N ) |-> X ) ) = ( ( ( N - M ) + 1 ) .x. X ) ) $= + ( vl cmnd wcel cuz cfv w3a cfz co cmpt cgsu cmin c1 caddc nfcv weq cbvmpt + eqidd oveq2i gsumfzconst eqtrid ) DLMFENOMGAMPDCEFQRZGSZTRDKUKGSZTRFEUARU + BUCRGBRULUMDTCKUKGGKGUDHCKUEGUGUFUHABKDEFGIJUIUJ $. + $} + ${ $d B x y $. $d F x y $. $d G x y $. $d H x y $. $d K x y $. $d M x y $. $d N x y $. $d ph x y $. diff --git a/mmil.raw.html b/mmil.raw.html index 7ac99d280..966a5bfe7 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11438,6 +11438,14 @@ with something like ~ fzn and handle it with ~ gsum0g ) + + gsumconstf + ~ gsumfzconstf + requires that the series is indexed by consecutive integers + and has an element (if the latter condition is an issue, detect it + with something like ~ fzn and handle it with ~ gsum0g ) + + gsumconstf none From f091fcbdfd150eaea3165e0808be22d20487fcc7 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 10 Sep 2025 16:41:27 -0700 Subject: [PATCH 12/21] Add gsumfzsnfd to iset.mm This is gsumsnfd from set.mm except that M has to be an integer. Naming this similarly to the other gsumfz* theorems seems more appealing than trying to use a different convention. The proof is similar to the set.mm proof. --- iset.mm | 25 +++++++++++++++++++++++++ mmil.raw.html | 6 ++++++ 2 files changed, 31 insertions(+) diff --git a/iset.mm b/iset.mm index 79c518ac9..009ece26b 100644 --- a/iset.mm +++ b/iset.mm @@ -156073,6 +156073,31 @@ by a normal subgroup (resp. two-sided ideal). (Contributed by Mario BACVTVMVCZWCBCVDAVMHIVEUFUSWDTCVTHIVMNVTUPVFVGBCVTDVMWAVJVHWBVIVKVL $. $} + ${ + $d k M $. + gsumsnd.b $e |- B = ( Base ` G ) $. + gsumsnd.g $e |- ( ph -> G e. Mnd ) $. + gsumfzsnd.m $e |- ( ph -> M e. ZZ ) $. + gsumsnd.c $e |- ( ph -> C e. B ) $. + gsumsnd.s $e |- ( ( ph /\ k = M ) -> A = C ) $. + ${ + gsumsnfd.p $e |- F/ k ph $. + gsumsnfd.c $e |- F/_ k C $. + $( Group sum of a singleton, deduction form, using bound-variable + hypotheses instead of distinct variable conditions. (Contributed by + Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, + 28-Mar-2018.) (Revised by AV, 11-Dec-2019.) $) + gsumfzsnfd $p |- ( ph -> ( G gsum ( k e. { M } |-> A ) ) = C ) $= + ( cmpt cgsu co c1 wcel wceq csn caddc cmg cfv cfz elsni sylan2 mpteq2da + cmin cv oveq2d cz fzsn syl mpteq1d cmnd uzidd eqid gsumfzconstf syl3anc + cuz 3eqtr2d cc0 zcnd subidd oveq1d 0p1e1 eqtrdi mulg1 3eqtrd ) AFEGUAZB + OZPQZGGUIQZRUBQZDFUCUDZQZRDVPQZDAVMFEVKDOZPQFEGGUEQZDOZPQZVQAVLVSFPAEVK + BDMEUJZVKSAWCGTBDTWCGUFLUGUHUKAWAVSFPAEVTVKDAGULSVTVKTJGUMUNUOUKAFUPSGG + VAUDSDCSZWBVQTIAGJUQKCVPEFGGDNHVPURZUSUTVBAVORDVPAVOVCRUBQRAVNVCRUBAGAG + JVDVEVFVGVHVFAWDVRDTKCVPFDHWEVIUNVJ $. + $} + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# diff --git a/mmil.raw.html b/mmil.raw.html index 966a5bfe7..1a2b9a0e8 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11474,6 +11474,12 @@ consecutive integers. + + gsumsnfd + ~ gsumfzsnfd + The group sum needs to be indexed by an integer + + mgpval ~ mgpvalg From 06b6d2d83cb81a929874b7789e340b49cf45a786 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 10 Sep 2025 16:50:37 -0700 Subject: [PATCH 13/21] Add gsumsnd , gsumsnf , gsumsn to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 1a2b9a0e8..b61d41393 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11480,6 +11480,12 @@ The group sum needs to be indexed by an integer + + gsumsnd , gsumsnf , gsumsn + none + should be possible with small changes (see ~ gsumfzsnfd ) + + mgpval ~ mgpvalg From 215d997b5d2ba99f4c5bf595d70b67e33fa5ec07 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 10 Sep 2025 16:58:43 -0700 Subject: [PATCH 14/21] add gsumpr to mmil.html --- mmil.raw.html | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index b61d41393..51d835a83 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11486,6 +11486,14 @@ should be possible with small changes (see ~ gsumfzsnfd ) + + gsumpr + none + Should be possible with some changes. Because ` M ` and ` N ` + would need to be consecutive integers, perhaps it would be easier + to just state them as ` M ` and ` M + 1 ` . + + mgpval ~ mgpvalg From 6794ab6a881928640da2a7dcfd0530e80d51a5ef Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 10 Sep 2025 17:22:35 -0700 Subject: [PATCH 15/21] Add mpocnfldadd to iset.mm Stated as in set.mm. This is provided for compatibility with set.mm but at least so far makes no effort to reduce axiom usage. The proof is based on the set.mm proof of cnfldadd . --- iset-discouraged | 3 ++- iset.mm | 9 +++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/iset-discouraged b/iset-discouraged index 728601ef7..2a28b8878 100644 --- a/iset-discouraged +++ b/iset-discouraged @@ -70,6 +70,7 @@ "ax-addf" is used by "addcncntop". "ax-addf" is used by "addex". "ax-addf" is used by "cnfldplusf". +"ax-addf" is used by "mpocnfldadd". "ax-addrcl" is used by "readdcl". "ax-arch" is used by "arch". "ax-caucvg" is used by "caucvgre". @@ -354,7 +355,7 @@ New usage of "ax-1re" is discouraged (1 uses). New usage of "ax-addass" is discouraged (1 uses). New usage of "ax-addcl" is discouraged (1 uses). New usage of "ax-addcom" is discouraged (1 uses). -New usage of "ax-addf" is discouraged (3 uses). +New usage of "ax-addf" is discouraged (4 uses). New usage of "ax-addrcl" is discouraged (1 uses). New usage of "ax-arch" is discouraged (1 uses). New usage of "ax-caucvg" is discouraged (1 uses). diff --git a/iset.mm b/iset.mm index 009ece26b..f62755139 100644 --- a/iset.mm +++ b/iset.mm @@ -165338,6 +165338,15 @@ left ideal which is also a right ideal (or a left ideal over the opposite sseqtrri strslfv ax-mp ) ABCADEFGHADEBIINJKLMOEFAKZPOQFRKZULOSFTKZUAZDUMULU NUBUOUOOUCFUDKPZUEDUOUPUFUGUIUHUJUK $. + ${ + $d x y $. + $( The addition operation of the field of complex numbers. Version of + ~ cnfldadd using maps-to notation. (Contributed by GG, 31-Mar-2025.) $) + mpocnfldadd $p |- ( x e. CC , y e. CC |-> ( x + y ) ) = ( +g ` CCfld ) $= + ( caddc cc cv cmpo ccnfld cplusg cfv cxp wfn wceq ax-addf ffn fnovim mp2b + co wf cnfldadd eqtr3i ) CABDDAEBECQFZGHIDDJZDCRCUBKCUALMUBDCNABDDCOPST $. + $} + $( The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) $) From 18e8340c514b1e31364798fe9ab625424a14ab58 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Tue, 9 Sep 2025 17:46:23 -0700 Subject: [PATCH 16/21] Add gsumfzfsum to iset.mm This is gsumfsum from set.mm but where the sums are indexed by consecutive integers. As with the set.mm proof the proof separates the empty case (lemma gsumfzfsumlem0 ) from the inhabited case (lemma gsumfzfsumlemm , here proved by induction which is perhaps simpler than trying to adapt theorems like fsum3 ). --- iset.mm | 80 +++++++++++++++++++++++++++++++++++++++++++++++++++ mmil.raw.html | 6 ++++ 2 files changed, 86 insertions(+) diff --git a/iset.mm b/iset.mm index f62755139..f632c395c 100644 --- a/iset.mm +++ b/iset.mm @@ -165538,6 +165538,86 @@ left ideal which is also a right ideal (or a left ideal over the opposite UDURACUEEFZUQJAFZUTAFUOVCUQACUFTVBUOVDUQACJUHUGTAUSCUPJUSUIUJUKULUMUN $. $} + ${ + $d M k $. $d N k $. + gsumfzfsumlem0.m $e |- ( ph -> M e. ZZ ) $. + gsumfzfsumlem0.n $e |- ( ph -> N e. ZZ ) $. + gsumfzfsumlem0.lt $e |- ( ph -> N < M ) $. + $( Lemma for ~ gsumfzfsum . The case where the sum is empty. (Contributed + by Jim Kingdon, 9-Sep-2025.) $) + gsumfzfsumlem0 $p |- ( ph -> ( CCfld gsum ( k e. ( M ... N ) |-> B ) ) + = sum_ k e. ( M ... N ) B ) $= + ( ccnfld c0 cgsu co cc0 cmpt csu crg wcel wceq cz eqtrdi cfz cnring ax-mp + cnfld0 gsum0g clt wbr wb fzn syl2anc mpbid mpteq1d oveq2d sumeq1d 3eqtr4a + mpt0 sum0 ) AIJKLZMICDEUALZBNZKLUSBCOZIPQURMRUBIPMUDUEUCAUTJIKAUTCJBNJACU + SJBAEDUFUGZUSJRZHADSQESQVBVCUHFGDEUIUJUKZULCBUPTUMAVAJBCOMAUSJBCVDUNBCUQT + UO $. + $} + + ${ + $d B j w $. $d B j x y $. $d M j k w $. $d M j k x y $. $d N j k w $. + $d j k ph w $. + gsumfzfsumlemm.n $e |- ( ph -> N e. ( ZZ>= ` M ) ) $. + gsumfzfsumlemm.b $e |- ( ( ph /\ k e. ( M ... N ) ) -> B e. CC ) $. + $( Lemma for ~ gsumfzfsum . The case where the sum is inhabited. + (Contributed by Jim Kingdon, 9-Sep-2025.) $) + gsumfzfsumlemm $p |- ( ph -> ( CCfld gsum ( k e. ( M ... N ) |-> B ) ) + = sum_ k e. ( M ... N ) B ) $= + ( cfz co wcel ccnfld cmpt cgsu csu wceq syl wi caddc cc adantl vw cuz cfv + vj vx vy eluzfz2 cv c1 mpteq1d oveq2d sumeq1d eqeq12d imbi2d csn cnfldbas + oveq2 csb cmnd cnring ringmnd mp1i eluzel2 wral eluzfz1 ralrimiva nfcsb1v + crg cz nfel1 csbeq1a eleq1d rspc sylc nfv gsumfzsnfd sumsns syl2anc eqtrd + fzsn 3eqtr4d a1i cfzo wa simpr oveq1d cres cmpo mpocnfldadd adantr simpll + elfzouz elfzoel2 ad2antlr elfzelz cle wbr elfzle1 elfzoelz peano2zd letrd + zred elfzle2 fzofzp1 elfzd fmpttd gsumsplit1r wss fzssp1 resmpt rspcsbela + peano2uz syl2anr eqid fvmpts oveq12d cnfld0 fzelp1 sylan2 gsumfzcl addcld + cc0 oveq1 ovmpog syl3anc 3eqtrd cun fzsuc fzfigd wn fsumsplitsn ex expcom + fzp1nel a2d fzind2 mpcom ) EDEHIZJZAKCYRBLZMIZYRBCNZOZAEDUBUCZJZYSFDEUGPA + KCDUAUHZHIZBLZMIZUUGBCNZOZQAKCDDHIZBLZMIZUULBCNZOZQZAKCDUDUHZHIZBLZMIZUUS + BCNZOZQAKCDUURUIRIZHIZBLZMIZUVEBCNZOZQAUUCQUAUDEDEUUFDOZUUKUUPAUVJUUIUUNU + UJUUOUVJUUHUUMKMUVJCUUGUULBUUFDDHUQZUJUKUVJUUGUULBCUVKULUMUNUUFUUROZUUKUV + CAUVLUUIUVAUUJUVBUVLUUHUUTKMUVLCUUGUUSBUUFUURDHUQZUJUKUVLUUGUUSBCUVMULUMU + NUUFUVDOZUUKUVIAUVNUUIUVGUUJUVHUVNUUHUVFKMUVNCUUGUVEBUUFUVDDHUQZUJUKUVNUU + GUVEBCUVOULUMUNUUFEOZUUKUUCAUVPUUIUUAUUJUUBUVPUUHYTKMUVPCUUGYRBUUFEDHUQZU + JUKUVPUUGYRBCUVQULUMUNUUQUUEAKCDUOZBLZMICDBURZUUNUUOABSUVTCKDUPKVHJZKUSJZ + AUTKVAZVBAUUEDVIJZFDEVCPZADYRJZBSJZCYRVDZUVTSJZAUUEUWFFDEVEPAUWGCYRGVFZUW + GUWICDYRCUVTSCDBVGZVJCUHZDOZBUVTSCDBVKZVLVMVNZUWMBUVTOAUWNTACVOUWKVPAUUMU + VSKMACUULUVRBAUWDUULUVROUWEDVTZPUJUKAUUOUVRBCNZUVTAUWDUUOUWQOUWEUWDUULUVR + BCUWPULPAUWDUWIUWQUVTOUWEUWOBCDVIVQVRVSWAWBUURDEWCIJZAUVCUVIAUWRUVCUVIQAU + WRWDZUVCUVIUWSUVCWDZUVACUVDBURZRIZUVBUXARIZUVGUVHUWTUVAUVBUXARUWSUVCWEWFU + WSUVGUXBOUVCUWSUVGKUVFUUSWGZMIZUVDUVFUCZUEUFSSUEUHZUFUHZRIZWHZIUVAUXAUXJI + ZUXBUWSSUXJUVFKDUURVHUPUEUFWIUWAUWSUTWBAUWDUWRUWEWJZUWRUURUUDJZAUURDEWLZT + ZUWSCUVEBSUWSUWLUVEJZWDZAUWLYRJUWGAUWRUXPWKZUXQUWLDEUXQAUWDUXRUWEPUWREVIJ + AUXPUURDEWMWNZUXPUWLVIJUWSUWLDUVDWOTZUXPDUWLWPWQUWSUWLDUVDWRTUXQUWLUVDEUX + QUWLUXTXBUXQUVDUXQUURUWRUURVIJZAUXPUURDEWSZWNWTXBUXQEUXSXBUXPUWLUVDWPWQUW + SUWLDUVDXCTUXQUVDYRJZUVDEWPWQUWRUYCAUXPDEUURXDZWNUVDDEXCPXAXEGVRZXFXGUWSU + XEUVAUXFUXAUXJUWSUXDUUTKMUUSUVEXHUXDUUTOUWSDUURXICUVEUUSBXJVBUKUWSUVDUVEJ + ZUXASJZUXFUXAOUWSUVDUUDJZUYFUWRUYHAUWRUXMUYHUXNDUURXLPTDUVDUGPUWRUYCUWHUY + GAUYDUWJCUVDYRBSXKXMZCUVDBUVEUVFSUVFXNXOVRXPUWSUVASJUYGUXBSJUXKUXBOUWSSUU + TKDUURYBUPXQUWAUWBUWSUTUWCVBUXLUWRUYAAUYBTZUWSCUUSBSUWLUUSJUWSUXPUWGUWLDU + URXRUYEXSZXFXTZUYIUWSUVAUXAUYLUYIYAUEUFUVAUXASSUXIUXBUXJUVAUXHRISUXGUVAUX + HRYCUXHUXAUVARUQUXJXNYDYEYFWJUWSUVHUXCOUVCUWSUVHUUSUVDUOYGZBCNUXCUWSUVEUY + MBCUWSUXMUVEUYMOUXODUURYHPULUWSUUSUVDBUXACVIUWSCVOCUVDBVGUWSDUURUXLUYJYIU + WSUURUYJWTUVDUUSJYJUWSDUURYNWBUYKCUVDBVKUYIYKVSWJWAYLYMYOYPYQ $. + $} + + ${ + $d M k $. $d N k $. $d ph k $. + gsumfzfsum.m $e |- ( ph -> M e. ZZ ) $. + gsumfzfsum.n $e |- ( ph -> N e. ZZ ) $. + gsumfzfsum.2 $e |- ( ( ph /\ k e. ( M ... N ) ) -> B e. CC ) $. + $( Relate a group sum on ` CCfld ` to a finite sum on the complex numbers. + (Contributed by Mario Carneiro, 28-Dec-2014.) $) + gsumfzfsum $p |- ( ph -> ( CCfld gsum ( k e. ( M ... N ) |-> B ) ) + = sum_ k e. ( M ... N ) B ) $= + ( clt wbr ccnfld cfz co cmpt wa cz wcel adantr simpr zred cgsu csu wn cle + wceq gsumfzfsumlem0 cuz cfv nltled eluz2 syl3anbrc adantlr gsumfzfsumlemm + cv cc wdc wo zdclt syl2anc exmiddc syl mpjaodan ) AEDIJZKCDELMZBNUAMVDBCU + BUEVCUCZAVCOBCDEADPQZVCFRAEPQZVCGRAVCSUFAVEOZBCDEVHVFVGDEUDJEDUGUHQAVFVEF + RZAVGVEGRZVHDEVHDVITVHEVJTAVESUIDEUJUKACUNVDQBUOQVEHULUMAVCUPZVCVEUQAVGVF + VKGFEDURUSVCUTVAVB $. + $} + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= diff --git a/mmil.raw.html b/mmil.raw.html index 51d835a83..1cb9e739c 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12561,6 +12561,12 @@ presumably not provable + + gsumfsum + ~ gsumfzfsum + requires the sums to be indexed by consecutive integers + + zringlpirlem1 , zringlpirlem2 , zringlpirlem3 , zringlpir , zringndrg , zringcyg From 5f716ce4fea1928357f9427be1d484e8eaf36566 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 11 Sep 2025 11:10:52 -0700 Subject: [PATCH 17/21] Add submmulg to iset.mm Stated as in set.mm. The proof is the set.mm proof with one small change in extensible structure theorems. --- iset.mm | 19 +++++++++++++++++++ mmil.raw.html | 6 ------ 2 files changed, 19 insertions(+), 6 deletions(-) diff --git a/iset.mm b/iset.mm index f632c395c..007495b2a 100644 --- a/iset.mm +++ b/iset.mm @@ -153313,6 +153313,25 @@ since the target of the homomorphism (operator ` O ` in our model) need ( vx vy csubmnd cfv wcel cbs cplusg cmnd c0g eqid submrcl submss submcl cv subm0cl mulgnn0subcl ) ACIJKGHCLJZCMJZABCDNECOJZUCPZFUDPZACQUCACUFRUDA CGTHTUGSUEPZACUEUHUAUB $. + + submmulg.h $e |- H = ( G |`s S ) $. + submmulg.t $e |- .x. = ( .g ` H ) $. + $( A group multiple is the same if evaluated in a submonoid. (Contributed + by Mario Carneiro, 15-Jun-2015.) $) + submmulg $p |- ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> + ( N .xb X ) = ( N .x. X ) ) $= + ( cfv wcel co wceq cc0 c1 syl eqid adantr 3eqtr4d csubmnd cn0 w3a csn cxp + cn wa cplusg cseq simpl1 cmnd cress a1i submrcl ressplusgd seqeq2d fveq1d + eqidd cbs simpr wss submss 3ad2ant1 sseldd mulgnn syl2anc submbas eleqtrd + id simp3 c0g subm0 mulg0 oveq1d wo simp2 elnn0 sylib mpjaodan ) ADUAKZLZF + UBLZGALZUCZFUFLZFGBMZFGCMZNFONZWDWEUGZFDUHKZUFGUDUEZPUIZKZFEUHKZWKPUIZKZW + FWGWIFWLWOWIWJWNWKPWIWAWJWNNWAWBWCWEUJWAAWJDEVTUKEDAULMNWAIUMWAWJURWAVIAD + UNUOQUPUQWIWEGDUSKZLZWFWMNWDWEUTZWDWRWEWDAWQGWAWBAWQVAWCWQADWQRZVBVCWAWBW + CVJZVDZSWQWJWLBDFGWTWJRHWLRVEVFWIWEGEUSKZLZWGWPNWSWDXDWEWDGAXCXAWAWBAXCNW + CAEDIVGVCVHZSXCWNWOCEFGXCRZWNRJWORVEVFTWDWHUGZOGBMZOGCMZWFWGXGDVKKZEVKKZX + HXIXGWAXJXKNWAWBWCWHUJAEDXJIXJRZVLQXGWRXHXJNWDWRWHXBSWQBDGXJWTXLHVMQXGXDX + IXKNWDXDWHXESXCCEGXKXFXKRJVMQTXGFOGBWDWHUTZVNXGFOGCXMVNTWDWBWEWHVOWAWBWCV + PFVQVRVS $. $} diff --git a/mmil.raw.html b/mmil.raw.html index 1cb9e739c..ae740e93c 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -11227,12 +11227,6 @@ hypotheses in deduction form - - submmulg - none - the set.mm proof uses ressplusg - - pwsmulg none From 45579098a9053f87e71d8c11f0b30ac650c57152 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 11 Sep 2025 19:31:16 -0700 Subject: [PATCH 18/21] Add mpocnfldmul to iset.mm Stated as in set.mm. At least for now, this uses the same complex number axioms as cnfldmul . The proof is from ax-mulf and cnfldmul . --- iset-discouraged | 3 ++- iset.mm | 10 ++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/iset-discouraged b/iset-discouraged index 2a28b8878..0459c3db5 100644 --- a/iset-discouraged +++ b/iset-discouraged @@ -87,6 +87,7 @@ "ax-mulass" is used by "mulass". "ax-mulcl" is used by "mulcl". "ax-mulcom" is used by "mulcom". +"ax-mulf" is used by "mpocnfldmul". "ax-mulf" is used by "mulcncntop". "ax-mulf" is used by "mulex". "ax-mulrcl" is used by "remulcl". @@ -371,7 +372,7 @@ New usage of "ax-io" is discouraged (1 uses). New usage of "ax-mulass" is discouraged (1 uses). New usage of "ax-mulcl" is discouraged (1 uses). New usage of "ax-mulcom" is discouraged (1 uses). -New usage of "ax-mulf" is discouraged (2 uses). +New usage of "ax-mulf" is discouraged (3 uses). New usage of "ax-mulrcl" is discouraged (1 uses). New usage of "ax0id" is discouraged (0 uses). New usage of "ax0lt1" is discouraged (0 uses). diff --git a/iset.mm b/iset.mm index 007495b2a..3a0456289 100644 --- a/iset.mm +++ b/iset.mm @@ -165375,6 +165375,16 @@ left ideal which is also a right ideal (or a left ideal over the opposite ccj cun strslfv ax-mp ) ABCADEFGHADEBIIJKLMNOEFALZPOQFRLZOSFTLZULUAZDUMUNUL UBUOUOOUCFUHLPZUIDUOUPUDUEUFUGUJUK $. + ${ + $d x y $. + $( The multiplication operation of the field of complex numbers. Version + of ~ cnfldmul using maps-to notation. (Contributed by GG, + 31-Mar-2025.) $) + mpocnfldmul $p |- ( x e. CC , y e. CC |-> ( x x. y ) ) = ( .r ` CCfld ) $= + ( cmul cc cv co cmpo ccnfld cmulr cfv cxp wf wfn wceq ax-mulf fnovim mp2b + ffn cnfldmul eqtr3i ) CABDDAEBECFGZHIJDDKZDCLCUBMCUANOUBDCRABDDCPQST $. + $} + $( The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.) $) From 09b3242f7fc00a2b898fe5c1f5e1450402e82c2d Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 11 Sep 2025 17:17:42 -0700 Subject: [PATCH 19/21] Add cnfldui to iset.mm This is similar to drngui from set.mm but for CCfld in particular, not division rings in general. The proof is a new one from crngunit , dvdsrd , and recapb . --- iset.mm | 19 +++++++++++++++++++ mmil.raw.html | 13 +++++++++++++ 2 files changed, 32 insertions(+) diff --git a/iset.mm b/iset.mm index 3a0456289..bb9ebc5b5 100644 --- a/iset.mm +++ b/iset.mm @@ -165647,6 +165647,25 @@ left ideal which is also a right ideal (or a left ideal over the opposite VKGFEDURUSVCUTVAVB $. $} + ${ + $d u v x y z $. + $( The invertible complex numbers are exactly those apart from zero. This + is ~ recapb but expressed in terms of ` CCfld ` . (Contributed by Jim + Kingdon, 11-Sep-2025.) $) + cnfldui $p |- { z e. CC | z =//= 0 } = ( Unit ` CCfld ) $= + ( vy vu vv ccnfld cfv cv cc0 cap wbr cc wcel wa cmul co c1 wceq eqid wtru + a1i cui crab wrex recapb pm5.32i breq1 elrab cdsr cmpo ccrg cncrng cnfld1 + vx wb crngunit ax-mp cbs cnfldbas eqidd csrg crg cnring cmulr mpocnfldmul + ringsrg dvdsrd mptru simpr simpl mulcld oveq1 oveq2 ovmpog syl3anc mulcom + eqtr4d eqeq1d rexbidva 3bitri 3bitr4ri eqriv eqcomi ) EUAFZAGZHIJZAKUBZUM + WCWFUMGZKLZWGHIJZMWHWGBGZNOZPQZBKUCZMZWGWFLWGWCLZWHWIWMBWGUDUEWEWIAWGKWDW + GHIUFUGWOWGPEUHFZJZWHWJWGCDKKCGZDGZNOZUIZOZPQZBKUCZMZWNEUJLWOWQUNUKWPEWCP + WGWCRULWPRUOUPWQXEUNSBKWPEXAWGPKEUQFQSURTSWPUSEUTLZSEVALXFVBEVEUPTXAEVCFQ + SCDVDTVFVGWHXDWMWHXCWLBKWHWJKLZMZXBWKPXHXBWJWGNOZWKXHXGWHXIKLXBXIQWHXGVHZ + WHXGVIZXHWJWGXJXKVJCDWJWGKKWTXIXAWJWSNOKWRWJWSNVKWSWGWJNVLXARVMVNWGWJVOVP + VQVRUEVSVTWAWB $. + $} + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= diff --git a/mmil.raw.html b/mmil.raw.html index ae740e93c..a778cc33b 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12020,6 +12020,19 @@ once we define division rings this should follow + + drngui + ~ cnfldui + for complex numbers + + + + none + for general division rings. To provide theorems like + this we'd need more development of apartness rings and/or + ~ df-apr . + + issubdrg none From c4bffafca5325a82a5994b47dd76e752b295dd9a Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 11 Sep 2025 16:24:19 -0700 Subject: [PATCH 20/21] Add expghmap to iset.mm This is expghm from set.mm with not equal changed to apart. The proof is basically the set.mm proof but needs changes of not equal to apart and other intuitionizations on most steps. --- iset.mm | 33 +++++++++++++++++++++++++++++++++ mmil.raw.html | 5 ++--- 2 files changed, 35 insertions(+), 3 deletions(-) diff --git a/iset.mm b/iset.mm index bb9ebc5b5..9c251925a 100644 --- a/iset.mm +++ b/iset.mm @@ -165814,6 +165814,39 @@ According to Wikipedia ("Integer", 25-May-2019, ( ccnfld crg wcel cz cvv cmgp cfv cress co czring wceq cnring df-zring eqid zex mgpress mp2an ) ABCDECAFGZDHIJFGKLODAJRBEMRNPQ $. + ${ + $d A r s u v x z $. $d U u v $. + expghm.m $e |- M = ( mulGrp ` CCfld ) $. + expghmap.u $e |- U = ( M |`s { z e. CC | z =//= 0 } ) $. + $( Exponentiation is a group homomorphism from addition to multiplication. + (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, + 10-Jun-2019.) (Revised by Jim Kingdon, 11-Sep-2025.) $) + expghmap $p |- ( ( A e. CC /\ A =//= 0 ) -> + ( x e. ZZ |-> ( A ^ x ) ) e. ( ZZring GrpHom U ) ) $= + ( vu vv cc wcel wa cz cv cexp co cfv cmul wceq wtru cc0 cap wbr crab cmpt + vr vs caddc cmpo wral czring cghm expclzaplem 3expa fmpttd expaddzap eqid + oveq2 zaddcl adantl simpll simplr expclzapd fvmptd3 simprl simprr oveq12d + wf 3eqtr4d ralrimivva anassrs eqeltrd simpr mulcld oveq1 syl3anc ralbidva + ovmpog eqeq2d mpbird cgrp zringgrp ccnfld crg cnring cnfldui cress oveq1i + cmgp eqtri unitgrp ax-mp zringbas cbs cvv a1i cnfldbas mgpbasg mp1i mgpex + pm3.2i wss apsscn ressbas2d mptru zringplusg cplusg mpocnfldmul mgpplusgg + cnex rabex ressplusgd isghm mpbiran sylanbrc ) CJKZCUAUBUCZLZMBNUAUBUCZBJ + UDZAMCANZOPZUEZVHZHNZINZUHPZYCQZYEYCQZYFYCQZUFUGJJUFNZUGNZRPZUIZPZSZIMUJZ + HMUJZYCUKDULPKZXRAMYBXTXPXQYAMKYBXTKBCYAUMUNUOXRYRYHYIYJRPZSZIMUJZHMUJXRU + UAHIMMXRYEMKZYFMKZLZLZCYGOPZCYEOPZCYFOPZRPYHYTCYEYFUPUUFAYGYBUUGMYCJYCUQZ + YAYGCOURUUEYGMKXRYEYFUSUTZUUFCYGXPXQUUEVAZXPXQUUEVBZUUKVCVDUUFYIUUHYJUUIR + UUFAYEYBUUHMYCJUUJYAYECOURZXRUUCUUDVEZUUFCYEUULUUMUUOVCZVDUUFAYFYBUUIMYCJ + UUJYAYFCOURZXRUUCUUDVFZUUFCYFUULUUMUURVCZVDVGVIVJXRYQUUBHMXRUUCLZYPUUAIMU + UTUUDLZYOYTYHUVAYIJKYJJKYTJKYOYTSUVAYIUUHJUVAAYEYBUUHMYCJUUJUUNXRUUCUUDVB + XRUUCUUDUUHJKUUPVKZVDUVBVLZUVAYJUUIJUVAAYFYBUUIMYCJUUJUUQUUTUUDVMXRUUCUUD + UUIJKUUSVKZVDUVDVLZUVAYIYJUVCUVEVNUFUGYIYJJJYMYTYNYIYLRPJYKYIYLRVOYLYJYIR + URYNUQVRVPVSVQVQVTYSUKWAKZDWAKZLYDYRLUVFUVGWBWCWDKZUVGWEWCXTDBWFDEXTWGPZW + CWIQZXTWGPGEUVJXTWGFWHWJWKWLXAIHUHYNUKDYCMXTWMXTDWNQSTXTJDEWODUVISTGWPZUV + HJEWNQSTWEJWCEWDFWQWRWSUVHEWOKTWEWCEWDFWTWSZXTJXBTBJUAXCWPXDXEXFYNDXGQSTX + TYNEDWOWOUVKUVHYNEXGQSTWEWCYNEWDFUFUGXHXIWSXTWOKTXSBJXJXKWPUVLXLXEXMXNXO + $. + $} + ${ $d n x y B $. $d f x y F $. $d f n x y R $. $d n .x. $. $d n x y .1. $. mulgghm2.m $e |- .x. = ( .g ` R ) $. diff --git a/mmil.raw.html b/mmil.raw.html index a778cc33b..78a59b312 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12611,9 +12611,8 @@ expghm - none - the set.mm proof uses drngui - there would appear to be issues - around not equal to zero versus invertible + ~ expghmap + changes not equal to apart From 50f2229f0b281d5efa4cd921793ba2b590aa2b8b Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 11 Sep 2025 08:16:10 -0700 Subject: [PATCH 21/21] Add lgseisenlem4 to iset.mm Stated as in set.mm. The proof is basically the set.mm proof but requires intuitionizing in many places for a variety of reasons. Remove one sentence from the comment in set.mm (which seemed to be an incorrect copy-paste from lgseisenlem2 ). --- iset.mm | 90 +++++++++++++++++++++++++++++++++++++++++++++++++++ mmil.raw.html | 2 +- set.mm | 5 ++- 3 files changed, 93 insertions(+), 4 deletions(-) diff --git a/iset.mm b/iset.mm index 9c251925a..2b91e954b 100644 --- a/iset.mm +++ b/iset.mm @@ -183636,6 +183636,96 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is UBUYAWLABUXJUXTVUSVXQXFAVUSVUBUYAUXJVVIXHWKUXAVVIUXBWUBVUSUXPKUYCVYGU YBUXOVVGVYJWUCVXOUXFYEUXG $. $} + + ${ + $( Lemma for Eisenstein's lemma. (Contributed by Mario Carneiro, + 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.) $) + lgseisenlem4 $p |- ( ph -> ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = + ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) + ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) ) $= + ( vk vz c1 cmin co c2 cdiv cexp cmo cneg cfz cv cmul cfl cfv csu wceq + cdvds wbr cmpt cgsu czring cz zringbas zring0 cabl wcel ccmn zringabl + cc0 ablcmn mp1i ccrg cn0 cprime csn eldifad prmnn nnnn0d cn nnzd cmhm + syl cbs wf crg eqid m1expcl adantl ccnfld zringmpg cap csubmnd neg1cn + cress cc neg1ap0 mp2an ax-mp zsubrg sylancr syl2anc gausslemma2dlem0a + wb fmpttd cq adantr nnmulcl fveq2d cof ffvelcdmd mgpbasg eleqtrd prmz + oveq2 zmulcld zexpcl oveqd oveq2d cfn eqidd syl3anc caddc eqtrid zcnd + nnq nncnd eqtrd 3eqtrd a1i syl22anc wn 1cnd cuz oveq1d 3eqtr3d eqtr3d + 1exp mpbid cmg zncrng crngmgp cmnmndd 1zzd cdif oddprm ccom crngringd + crh zrhrhm rhmf cofmpt cmgp rhmmhm crab cghm expghmap ghmmhm unitsubm + cnring cnfldui resmhm2 crn csubrg subrgsubm frnd resmhm2b mpbii mhmco + wss eqeltrrd wa znq 2nn elfznn zq qmulcl flqcld gsumfzmhm2 cur cplusg + cmulr neg1z zmodcld eqeltrid gsumfzmptfidmadd2 mgpplusgg ofeqd fzfigd + 3eqtr4d offval2 zringmulr rhmmul clt nnmulcld nngt0d modqval div23apd + nnap0d pncan3d 2cnd mul12d expaddzap expmulzap eldifsni necomd neneqd + nn0zd wne 2z uzid dvdsprm mtbird oexpneg negeqd 2nn0 expmuld neg1sqe1 + syl2an mulassd mullidd mpteq2dva lgseisenlem3 3eqtr3rd feq3d gsumfzcl + oveq1i c0g eleqtrrd ringridm cmnd nnuz eleqtrdi gsumfzconst zringring + npcand mhmmulg submmulg cnfldexp subrgsubg subgsubm df-zring gsumsubm + csubg gsumfzfsum fsumzcl zndvds moddvds mpbird ) AEDUCUDUEUFUGUEZUHUE + ZDUIUEUCUJZUCVUJUKUEZEDUGUEZUFBULZUMUEZUMUEZUNUOZBUPZUHUEZDUIUEUQZDVU + KVUTUDUEURUSZAVUKIUOZVUTIUOZUQZVVBAHBVUMVULVURUHUEZIUOZUTZVAUEZVULVBB + VUMVURUTZVAUEZUHUEZIUOZVVCVVDAUAVCVULUAULZUHUEZIUOZVVGBVVMVBHUCVUJVUR + VJVDVEVBVFVGVBVHVGAVIVBVKVLAHAKVMVGZHVHVGADVNVGZVVQADVOVGZVVRADVOUFVP + ZLVQZVVSDDVRZVSWCDKRUUAWCZKHSUUBWCZUUCZAUUDZAVUJADVOVVTUUEVGZVUJVTVGL + DUUFWCZWAZAIUAVCVVOUTZUUGZUAVCVVPUTVBHWBUEZAUAVCVVOVCKWDUOZIAIVBKUUIU + EVGZVCVWMIWEZAKWFVGZVWNAKVWCUUHZKITUUJWCZVCVWMVBKIVDVWMWGZUUKWCZVVNVC + VGVVOVCVGAVVNWHWIZUULAIWJUUMUOZVCWOUEZHWBUEVGZVWJVBVXCWBUEVGZVWKVWLVG + AVWNVXDVWRVBKIVXCHWKSUUNWCZAVWJVBVXBWBUEVGZVXEVWJVBVXBUBULVJWLUSUBWPU + UOZWOUEZWBUEVGZVXHVXBWMUOZVGZVXGVWJVBVXIUUPUEVGZVXJVULWPVGZVULVJWLUSZ + VXMWNWQUAUBVULVXIVXBVXBWGZVXIWGZUUQWRVBVXIVWJUURWSWJWFVGVXLUUTWJVXHVX + BUBUVAVXPUUSWSVBVXBVXIVWJVXHVXQUVBWRAVCVXKVGZVWJUVCVCUVJVXGVXEXDVCWJU + VDUOVGZVXRWTVCWJVXBVXPUVEWSZAVCVCVWJAUAVCVVOVCVXAXEUVFVBVXBVXCVWJVCVX + CWGZUVGXAUVHVBVXCHIVWJUVIXBUVKAVUOVUMVGZUVLZVUQVYCVUNXFVGZVUPXFVGZVUQ + XFVGVYCEVCVGZDVTVGZVYDAVYFVYBAEAEMXCZWAXGAVYGVYBADLXCZXGZEDUVMXBVYCVU + PVCVGVYEVYCVUPVYCUFVTVGVUOVTVGZVUPVTVGUVNVYBVYKAVUOVUJUVOZWIZUFVUOXHX + AZWAZVUPUVPWCVUNVUPUVQXBUVRZVVNVURUQVVOVVFIVVNVURVULUHXOXIVVNVVKUQVVO + VVLIVVNVVKVULUHXOXIUVSAVVIKUVTUOZKUWBUOZUEZHBVUMEIUOZUTZVAUEZVVIVVCAH + VVHBVUMVULFUHUEZEUMUEZIUOZUTZVYRXJZUEZVAUEZVVIHWUFVAUEZVYRUEZWUBVYSAH + VVHWUFHUWAUOZXJZUEZVAUEVVIWUJWULUEWUIWUKABHWDUOZVVGWUEWULVVHHWUFUCVUJ + WUOWGZWULWGVWDVWFVWIVYCVVGVWMWUOVYCVCVWMVVFIAVWOVYBVWTXGZVYCVURVCVGZV + VFVCVGZVYPVURWHWCZXKZAVWMWUOUQZVYBAVVQWVBVWCVWMKHVMSVWSXLWCZXGZXMVYCW + UEVWMWUOVYCVCVWMWUDIWUQVYCWUCEVYCVULVCVGFVNVGWUCVCVGUWCVYCFEVUPUMUEZD + UIUEZVNOVYCWVEDVYCEVUPVYCEVOVGZVYFAWVGVYBAEVOVVTMVQZXGEXNZWCZVYOXPZVY + CVVSVYGAVVSVYBVWAXGZVWBWCZUWDUWEZVULFXQXAZWVJXPZXKZWVDXMVVHWGWUFWGUWF + AWUHWUNHVAAWUGWUMVVHWUFAVYRWULAVVQVYRWULUQVWCKVYRHVMSVYRWGZUWGWCZUWHX + RXSAVYRWULVVIWUJWVSXRUWJAWUHWUAHVAAWUHBVUMVVGWUEVYRUEZUTWUAABVUMVVGWU + EVYRVVHWUFXTVWMVWMAUCVUJVWFVWIUWIZWVAWVQAVVHYAAWUFYAUWKABVUMWVTVYTVYC + VVFWUDUMUEZIUOZWVTVYTVYCVWNWUSWUDVCVGWWCWVTUQAVWNVYBVWRXGWUTWVPVVFWUD + VBKUMVYRIVCVDUWLWVRUWMYBVYCWWBEIVYCVVFWUCUMUEZEUMUEUCEUMUEWWBEVYCWWDU + CEUMVYCVULDVURUMUEZFYCUEZUHUEZVULUFEVUOUMUEZUMUEZUHUEZWWDUCVYCWWFWWIV + ULUHVYCWWFWWEWVEWWEUDUEZYCUEWVEWWIVYCFWWKWWEYCVYCFWVEDWVEDUGUEZUNUOZU + MUEZUDUEZWWKVYCFWVFWWOOVYCWVEXFVGZDXFVGZVJDUWNUSWVFWWOUQVYCWVEVTVGWWP + VYCEVUPAEVTVGZVYBVYHXGVYNUWOWVEYFWCAWWQVYBAVYGWWQVYIDYFWCXGVYCDVYJUWP + WVEDUWQYBYDVYCWWNWWEWVEUDVYCWWMVURDUMVYCWWLVUQUNVYCEVUPDVYCEWVJYEZVYC + VUPVYNYGVYCDWVMYGVYCDWVMUWSUWRXIXSXSYHXSVYCWWEWVEVYCWWEVYCDVURVYCVVSD + VCVGZWVLDXNWCZVYPXPZYEVYCWVEWVKYEUWTVYCEUFVUOWWSVYCUXAVYCVUOVYMYGUXBY + IXSVYCWWGVULWWEUHUEZWUCUMUEZWWDVYCVXNVXOWWEVCVGFVCVGWWGWXDUQVXNVYCWNY + JZVXOVYCWQYJZWXBVYCFWVNUXHVULWWEFUXCYKVYCWXCVVFWUCUMVYCWXCVULDUHUEZVU + RUHUEZVVFVYCVXNVXOWWTWURWXCWXHUQWXEWXFWXAVYPVULDVURUXDYKVYCWXGVULVURU + HVYCWXGUCDUHUEZUJZVULVYCUCWPVGVYGUFDURUSZYLWXGWXJUQVYCYMWVMVYCWXKUFDU + QZAWXLYLVYBAUFDADUFAVWGDUFUXILDVOUFUXEWCUXFUXGXGVYCUFUFYNUOVGZVVSWXKW + XLXDUFVCVGWXMUXJUFUXKWSWVLDUFUXLXAUXMUCDUXNYBVYCWXIUCVYCWWTWXIUCUQWXA + DYRWCUXOYHYOYHYOYHVYCWWJVULUFUHUEZWWHUHUEZUCVYCVULUFWWHWXEVYCWWHAWWRV + YKWWHVTVGVYBVYHVYLEVUOXHUXSZVSUFVNVGVYCUXPYJUXQVYCWXOUCWWHUHUEZUCWXNU + CWWHUHUXRUYGVYCWWHVCVGWXQUCUQVYCWWHWXPWAWWHYRWCYDYHYPYOVYCVVFWUCEVYCV + VFWUTYEVYCWUCWVOYEWWSUXTVYCEWWSUYAYPXIYQUYBYHXSAWUJVYQVVIVYRABCDEFGHI + JKLMNOPQRSTUYCXSUYDAVWPVVIVWMVGVYSVVIUQVWQAVVIWUOVWMAWUOVVHHUCVUJHUYH + UOZWUPWXRWGVWEVWFVWIAVUMVWMVVHWEVUMWUOVVHWEABVUMVVGVWMWVAXEAVWMWUOVVH + VUMWVCUYEYSUYFWVCUYIVWMKVYRVYQVVIVWSWVRVYQWGUYJXBAWUBVUJUCUDUEUCYCUEZ + VYTHYTUOZUEZVUJVYTWXTUEZVVCAHUYKVGVUJUCYNUOZVGVYTWUOVGWUBWYAUQVWEAVUJ + VTWYCVWHUYLUYMAVYTVWMWUOAVCVWMEIVWTAWVGVYFWVHWVIWCZXKWVCXMWUOWXTBHUCV + UJVYTWUPWXTWGZUYNYBAWXSVUJVYTWXTAVUJUCAVUJVWHYGAYMUYPYOAVUJEVXCYTUOZU + EZIUOZWYBVVCAVXDVUJVNVGZVYFWYHWYBUQVXFAVUJVWHVSZWYDVCWYFWXTIVXCHVUJEV + BWFVGVCVXCWDUOUQUYOVCVBVXCWFWKVDXLWSWYFWGZWYEUYQYBAWYGVUKIAVUJEVXBYTU + OZUEZWYGVUKAVXRWYIVYFWYMWYGUQVXRAVXTYJWYJWYDVCWYLWYFVXBVXCVUJEWYLWGVY + AWYKUYRYBAEWPVGWYIWYMVUKUQAEWYDYEWYJEVUJUYSXBYQXIYQYIYPAVVLVUTIAVVKVU + SVULUHAWJVVJVAUEVVKVUSAVUMVCVVJWJVBXTWWAVCWJVUDUOVGZVCWJWMUOVGAVXSWYN + WTVCWJUYTWSVCWJVUAVLABVUMVURVCVYPXEVUBVUCAVURBUCVUJVWFVWIVYCVURVYPYEV + UEYQXSXIYPAVVRVUKVCVGZVUTVCVGZVVEVVBXDADVYIVSAVYFWYIWYOWYDWYJEVUJXQXB + ZAVUSVCVGWYPAVUMVURBWWAVYPVUFVUSWHWCZVUKVUTIDKRTVUGYBYSAVYGWYOWYPVVAV + VBXDVYIWYQWYRVUKVUTDVUHYBVUI $. + $} $} $} diff --git a/mmil.raw.html b/mmil.raw.html index 78a59b312..71837d915 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -15275,7 +15275,7 @@ - lgseisenlem3 , lgseisenlem4 , lgseisen + lgseisen none presumably the set.mm proofs can be adapted once we have added more theorems concerning ` gsum ` . diff --git a/set.mm b/set.mm index 21b4d0f96..1e8ae3f43 100644 --- a/set.mm +++ b/set.mm @@ -402803,9 +402803,8 @@ multiple of the prime (in which case it is ` 0 ` , see ~ lgsne0 ) and NUYOVUEVUFABUWTUXJUYKVWSWTABUWTUXKXAXAUXJUYLVXAVUFVURUXIIXCVUOXDUWOVXTU YKUXFKUXMVXCUXLUXEUYMVXEVYAVWQUWPYMUWQ $. - $( Lemma for ~ lgseisen . The function ` M ` is an injection (and hence - a bijection by the pigeonhole principle). (Contributed by Mario - Carneiro, 18-Jun-2015.) (Proof shortened by AV, 15-Jun-2019.) $) + $( Lemma for ~ lgseisen . (Contributed by Mario Carneiro, 18-Jun-2015.) + (Proof shortened by AV, 15-Jun-2019.) $) lgseisenlem4 $p |- ( ph -> ( ( Q ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( -u 1 ^ sum_ x e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( |_ ` ( ( Q / P ) x. ( 2 x. x ) ) ) ) mod P ) ) $=