Revise proof of isumss in iset.mm

Use zsumdc in place of zisum .

Author: jkingdon

iset-discouraged

@@ -277,7 +277,6 @@
 "strnfvn" is used by "strsl0".
 "zisum" is used by "fisumsers".
 "zisum" is used by "iisum".
-"zisum" is used by "isumss".
 New usage of "0cnALT" is discouraged (0 uses).
 New usage of "0reALT" is discouraged (0 uses).
 New usage of "19.21h" is discouraged (3 uses).
@@ -448,7 +447,7 @@ New usage of "strnfvn" is discouraged (3 uses).
 New usage of "tfri1dALT" is discouraged (0 uses).
 New usage of "uzind4ALT" is discouraged (0 uses).
 New usage of "xpexgALT" is discouraged (0 uses).
-New usage of "zisum" is discouraged (3 uses).
+New usage of "zisum" is discouraged (2 uses).
 Proof modification of "0cnALT" is discouraged (49 steps).
 Proof modification of "0reALT" is discouraged (15 steps).
 Proof modification of "a9evsep" is discouraged (63 steps).

iset.mm

@@ -115732,31 +115732,31 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
          (Contributed by Mario Carneiro, 21-Apr-2014.)  (Revised by Jim
          Kingdon, 21-Sep-2022.) $)
       isumss $p |- ( ph -> sum_ k e. A C = sum_ k e. B C ) $=
-        ( vm cc wcel cc0 wa wceq cv cmpt cfv csu caddc cuz cif cseq4 eqid sstrd
-        cli csb simpr wral ralrimiva ad2antrr nfcsb1v nfel1 csbeq1a eleq1d rspc
-        sylc wn 0cnd wdc eleq1w dcbid adantr rspcdva ifcldadc nfcv nfv ifbieq1d
-        nfif fvmptf syl2anc fvmpts ifeq1dadc eqtr4d fmpttd ffvelrnda zisum elin
+        ( vm wcel cc0 wa cc wceq cmpt cfv csu caddc cuz cif cseq cli eqid sstrd
+        cv simpr wral ralrimiva ad2antrr nfcsb1v nfel1 csbeq1a eleq1d rspc sylc
+        csb wn 0cnd wdc eleq1w dcbid adantr rspcdva ifcldadc nfcv nfif ifbieq1d
+        nfv fvmptf syl2anc fvmpts ifeq1dadc eqtr4d fmpttd ffvelrnda zsumdc elin
         cin wss dfss1 sylib eleq2d syl5rbbr ifbid simplr adantlr iftrued eldifd
         wb cdif ad3antrrr nfeq1 eqeq1d eqeltrd iffalsed 3eqtr4d wo syl mpjaodan
-        exmiddc ifandc simpll sselda sumfct 3eqtr3d ) ABOUAZFBDUBZUCZOUDZCXLFCD
-        UBZUCZOUDZBDFUDZCDFUDZAXOUEPFGUFUCZFUAZBQZDRUGZUBZGUHUKUCXRAEBXNOYEGYAY
-        AUIZLABCYAHMUJAXLYAQZSZXLYEUCZXLBQZFXLDULZRUGZYJXNRUGYHYGYLPQYIYLTAYGUM
-        ZYHYJYKRPYHYJSZYJDPQZFBUNZYKPQZYHYJUMZAYPYGYJAYOFBIUOZUPYOYQFXLBFYKPFXL
-        DUQZURYBXLTZDYKPFXLDUSZUTVAVBZYHYJVCZSVDYHEUAZBQZVEZYJVEZEYAXLUUEXLTZUU
-        FYJEOBVFVGAUUGEYAUNZYGKVHYMVIZVJFXLYDYLYAYEPFXLVKYJFYKRYJFVLYTFRVKVNUUA
-        YCYJDYKRFOBVFUUBVMYEUIVOVPZYHYJXNYKRYNYJYQXNYKTYRUUCFXLDBXMPXMUIVQVPUUK
-        VRVSKABPXLXMAFBDPIVTWAWBAECXQOYEGYAYFLMYHYLXLCQZYJSZYKRUGZYIUUMXQRUGZYH
-        YJUUNYKRAYJUUNWOYGUUNXLCBWDZQAYJXLCBWCAUUQBXLABCWEUUQBTHBCWFWGWHWIVHWJU
-        ULYHUUPUUMYLRUGZUUOYHUUMXQYLRYHUUMSZYJXQYLTUUDUUSYJSZXQYKYLUUTUUMYQXQYK
-        TZYHUUMYJWKYHYJYQUUMUUCWLFXLDCXPPXPUIVQZVPUUTYJYKRUUSYJUMWMVSUUSUUDSZYK
-        RXQYLUVCXLCBWPZQDRTZFUVDUNZYKRTZUVCXLCBYHUUMUUDWKZUUSUUDUMZWNAUVFYGUUMU
-        UDAUVEFUVDJUOWQUVEUVGFXLUVDFYKRYTWRUUADYKRUUBWSVAVBZUVCUUMYQUVAUVHUVCYK
-        RPUVJUVCVDWTUVBVPUVCYJYKRUVIXAXBUUSUUHYJUUDXCYHUUHUUMUUKVHYJXFXDXEYHUUE
-        CQZVEZUUMVEZEYAXLUUIUVKUUMEOCVFVGAUVLEYAUNYGNVHYMVIZVRYHUVMUUOUURTUVNUU
-        MYJYKRXGXDVSXBNACPXLXPAFCDPAYBCQZSZYCYOYCVCZAYCYOUVOIWLUVPUVQSZDRPUVRAY
-        BUVDQUVEAUVOUVQXHUVRYBCBAUVOUVQWKUVPUVQUMWNJVPUVRVDWTUVPYCVEZYCUVQXCUVP
-        UUGUVSEYAYBUUEYBTUUFYCEFBVFVGAUUJUVOKVHACYAYBMXIVIYCXFXDXEZVTWAWBVSAYPX
-        OXSTYSBDOFXJXDAYOFCUNXRXTTAYOFCUVTUOCDOFXJXDXK $.
+        exmiddc ifandc simpll sselda sumfct 3eqtr3d ) ABOUKZFBDUAZUBZOUCZCXLFCD
+        UAZUBZOUCZBDFUCZCDFUCZAXOUDFGUEUBZFUKZBPZDQUFZUAZGUGUHUBXRAEBXNOYEGYAYA
+        UIZLABCYAHMUJAXLYAPZRZXLYEUBZXLBPZFXLDVBZQUFZYJXNQUFYHYGYLSPYIYLTAYGULZ
+        YHYJYKQSYHYJRZYJDSPZFBUMZYKSPZYHYJULZAYPYGYJAYOFBIUNZUOYOYQFXLBFYKSFXLD
+        UPZUQYBXLTZDYKSFXLDURZUSUTVAZYHYJVCZRVDYHEUKZBPZVEZYJVEZEYAXLUUEXLTZUUF
+        YJEOBVFVGAUUGEYAUMZYGKVHYMVIZVJFXLYDYLYAYESFXLVKYJFYKQYJFVNYTFQVKVLUUAY
+        CYJDYKQFOBVFUUBVMYEUIVOVPZYHYJXNYKQYNYJYQXNYKTYRUUCFXLDBXMSXMUIVQVPUUKV
+        RVSKABSXLXMAFBDSIVTWAWBAECXQOYEGYAYFLMYHYLXLCPZYJRZYKQUFZYIUUMXQQUFZYHY
+        JUUNYKQAYJUUNWOYGUUNXLCBWDZPAYJXLCBWCAUUQBXLABCWEUUQBTHBCWFWGWHWIVHWJUU
+        LYHUUPUUMYLQUFZUUOYHUUMXQYLQYHUUMRZYJXQYLTUUDUUSYJRZXQYKYLUUTUUMYQXQYKT
+        ZYHUUMYJWKYHYJYQUUMUUCWLFXLDCXPSXPUIVQZVPUUTYJYKQUUSYJULWMVSUUSUUDRZYKQ
+        XQYLUVCXLCBWPZPDQTZFUVDUMZYKQTZUVCXLCBYHUUMUUDWKZUUSUUDULZWNAUVFYGUUMUU
+        DAUVEFUVDJUNWQUVEUVGFXLUVDFYKQYTWRUUADYKQUUBWSUTVAZUVCUUMYQUVAUVHUVCYKQ
+        SUVJUVCVDWTUVBVPUVCYJYKQUVIXAXBUUSUUHYJUUDXCYHUUHUUMUUKVHYJXFXDXEYHUUEC
+        PZVEZUUMVEZEYAXLUUIUVKUUMEOCVFVGAUVLEYAUMYGNVHYMVIZVRYHUVMUUOUURTUVNUUM
+        YJYKQXGXDVSXBNACSXLXPAFCDSAYBCPZRZYCYOYCVCZAYCYOUVOIWLUVPUVQRZDQSUVRAYB
+        UVDPUVEAUVOUVQXHUVRYBCBAUVOUVQWKUVPUVQULWNJVPUVRVDWTUVPYCVEZYCUVQXCUVPU
+        UGUVSEYAYBUUEYBTUUFYCEFBVFVGAUUJUVOKVHACYAYBMXIVIYCXFXDXEZVTWAWBVSAYPXO
+        XSTYSBDOFXJXDAYOFCUMXRXTTAYOFCUVTUNCDOFXJXDXK $.
     $}
   $}