Revise fsumadd in iset.mm

Switch to df-seq3 syntax from df-iseq syntax.  Removes several usages of
discouraged theorems.

Author: jkingdon

iset-discouraged

@@ -150,7 +150,6 @@
 "eu3h" is used by "2eu4".
 "eu3h" is used by "eu3".
 "eu3h" is used by "mo2r".
-"fisum" is used by "fsumadd".
 "fisum" is used by "fsumf1o".
 "fisumcvg" is used by "fisumcvg2".
 "fisumcvg" is used by "isummolem2a".
@@ -186,7 +185,6 @@
 "iseqeq2" is used by "seqeq2".
 "iseqeq3" is used by "cbvsum".
 "iseqeq3" is used by "fisum".
-"iseqeq3" is used by "fsumadd".
 "iseqeq3" is used by "isummo".
 "iseqeq3" is used by "seqeq3".
 "iseqeq3" is used by "sumeq1".
@@ -235,7 +233,6 @@
 "iseqvalt" is used by "iseqfclt".
 "iseqvalt" is used by "iseqp1t".
 "iser0" is used by "ser0f".
-"iseradd" is used by "fsumadd".
 "iseradd" is used by "ser3add".
 "iserf" is used by "fisumcvg".
 "iserf" is used by "ser0f".
@@ -392,7 +389,7 @@ New usage of "elirr" is discouraged (16 uses).
 New usage of "equsalh" is discouraged (5 uses).
 New usage of "eu3h" is discouraged (3 uses).
 New usage of "exmidfodomrlemrALT" is discouraged (0 uses).
-New usage of "fisum" is discouraged (2 uses).
+New usage of "fisum" is discouraged (1 uses).
 New usage of "fisumcvg" is discouraged (2 uses).
 New usage of "fisumcvg2" is discouraged (1 uses).
 New usage of "fisumser" is discouraged (2 uses).
@@ -408,7 +405,7 @@ New usage of "iseqcl" is discouraged (4 uses).
 New usage of "iseqcoll" is discouraged (1 uses).
 New usage of "iseqeq1" is discouraged (5 uses).
 New usage of "iseqeq2" is discouraged (1 uses).
-New usage of "iseqeq3" is discouraged (8 uses).
+New usage of "iseqeq3" is discouraged (7 uses).
 New usage of "iseqex" is discouraged (4 uses).
 New usage of "iseqfcl" is discouraged (4 uses).
 New usage of "iseqfclt" is discouraged (2 uses).
@@ -425,7 +422,7 @@ New usage of "iseqp1t" is discouraged (1 uses).
 New usage of "iseqval" is discouraged (4 uses).
 New usage of "iseqvalt" is discouraged (3 uses).
 New usage of "iser0" is discouraged (1 uses).
-New usage of "iseradd" is discouraged (2 uses).
+New usage of "iseradd" is discouraged (1 uses).
 New usage of "iserf" is discouraged (2 uses).
 New usage of "isummo" is discouraged (1 uses).
 New usage of "isummolem2" is discouraged (1 uses).

iset.mm

@@ -116296,56 +116296,55 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
                         ( sum_ k e. A B + sum_ k e. A C ) ) $=
       ( vj vn wceq caddc co cfv cn wcel c1 cc0 cc fveq2 vf vm c0 csu chash wf1o
       cfz cv wex 00id sum0 oveq12i 3eqtr4ri sumeq1 oveq12d 3eqtr4a a1i cmpt cle
-      wa wi wbr ccom cif cuz simprl nnuz syl6eleq elnnuz biimpri adantl adantlr
-      cseq4 wf fmpttd simprr f1of syl fco syl2anc ad2antrr cz 1zzd nnzd eluzelz
-      w3a ad2antlr 3jca eluzle simpr jca elfz2 sylanbrc ffvelrnd wn 0cnd adantr
-      wdc zdcle ifcldadc weq ifbieq1d eqid fvmptg eqeltrd simpll wral ffvelrnda
-      breq1 addcld fvmpt2 eqtr4d ralrimiva nffvmpt1 nfcv nfov nfeq eqeq12d rspc
+      wa wi wbr ccom cif cseq cuz simprl nnuz syl6eleq eqid weq ifbieq1d elnnuz
+      breq1 biimpri adantl wf adantlr fmpttd simprr syl fco syl2anc ad2antrr cz
+      f1of 1zzd nnzd eluzelz ad2antlr 3jca eluzle simpr elfz2 sylanbrc ffvelrnd
+      w3a jca wn 0cnd wdc adantr ifcldadc fvmptd3 eqeltrd simpll wral ffvelrnda
+      zdcle addcld fvmpt2 eqtr4d ralrimiva nffvmpt1 nfcv nfov nfeq eqeq12d rspc
       fvco3 sylan 3eqtr4d iftrued eqcomi iffalsed wo exmiddc mpjaodan ad3antrrr
-      sylc iseradd fisum cbvmptv iseqeq3 ax-mp fveq1i syl6eq sumfct 3eqtr3d
-      expr exlimdv expimpd cfn fz1f1o mpjaod ) ABUCKZBCDLMZEUDZBCEUDZBDEUDZLMZK
-      ZBUENZOPZQUUMUGMZBUAUHZUFZUAUIZUTZUUFUULVAAUUFUCUUGEUDZUCCEUDZUCDEUDZLMZU
-      UHUUKRRLMZRUVCUUTUJUVARUVBRLCEUKDEUKULUUGEUKUMBUCUUGEUNUUFUUIUVAUUJUVBLBU
-      CCEUNBUCDEUNUOUPUQAUUNUURUULAUUNUTUUQUULUAAUUNUUQUULAUUNUUQUTZUTZBUBUHZEB
-      UUGURZNZUBUDZBUVGEBCURZNZUBUDZBUVGEBDURZNZUBUDZLMZUUHUUKUVFUUMLSIOIUHZUUM
-      USVBZUVRUVHUUPVCZNZRVDZURZQVMZNZUUMLSIOUVSUVRUVKUUPVCZNZRVDZURZQVMZNZUUML
-      SIOUVSUVRUVNUUPVCZNZRVDZURZQVMZNZLMUVJUVQUVFJUWIUWOUWCQUUMUVFUUMOQVENZAUU
-      NUUQVFZVGVHUVFJUHZUWRPZUTZUWTUWINZUWTUUMUSVBZUWTUWFNZRVDZSUXBUWTOPZUXFSPU
-      XCUXFKUXAUXGUVFUXGUXAUWTVIVJVKZUXBUXDUXERSUXBUXDUTZUUOSUWTUWFUVFUUOSUWFVN
-      ZUXAUXDUVFBSUVKVNUUOBUUPVNZUXJUVFEBCSAEUHZBPZCSPZUVEGVLZVOZUVFUUQUXKAUUNU
-      UQVPZUUOBUUPVQVRZUUOBSUVKUUPVSVTWAUXIQWBPZUUMWBPZUWTWBPZWFQUWTUSVBZUXDUTU
-      WTUUOPZUXIUXSUXTUYAUXIWCUXIUUMUVFUUNUXAUXDUWSWAWDUXAUYAUVFUXDQUWTWEWGWHUX
-      IUYBUXDUXAUYBUVFUXDQUWTWIWGUXBUXDWJZWKUWTQUUMWLWMZWNUXBUXDWOZUTZWPZUXBUYA
-      UXTUXDWRZUXBUWTUXHWDUXBUUMUVFUUNUXAUWSWQWDUWTUUMWSVTZWTZIUWTUWHUXFOSUWIIJ
-      XAZUVSUXDUWGUXERUVRUWTUUMUSXIZUVRUWTUWFTXBUWIXCXDVTZUYKXEUXBUWTUWONZUXDUW
-      TUWLNZRVDZSUXBUXGUYQSPUYOUYQKUXHUXBUXDUYPRSUXIUUOSUWTUWLUXIBSUVNVNZUXKUUO
-      SUWLVNUVFUYRUXAUXDUVFEBDSAUXMDSPZUVEHVLZVOZWAUVFUXKUXAUXDUXRWAZUUOBSUVNUU
-      PVSVTUYEWNUYHUYJWTZIUWTUWNUYQOSUWOUYLUVSUXDUWMUYPRUYMUVRUWTUWLTXBUWOXCXDV
-      TZVUCXEUXBUXDUWTUVTNZRVDZUXFUYQLMZUWTUWCNZUXCUYOLMUXBUXDVUFVUGKUYFUXIVUEU
-      XEUYPLMZVUFVUGUXIUVFUYCVUEVUIKUVFUXAUXDXFUYEUVFUYCUTZUWTUUPNZUVHNZVUKUVKN
-      ZVUKUVNNZLMZVUEVUIVUJVUKBPUXLUVHNZUXLUVKNZUXLUVNNZLMZKZEBXGZVULVUOKZUVFUU
-      OBUWTUUPUXRXHAVVAUVEUYCAVUTEBAUXMUTZVUPUUGVUSVVCUXMUUGSPZVUPUUGKAUXMWJZVV
-      CCDGHXJZEBUUGSUVHUVHXCXKVTVVCVUQCVURDLVVCUXMUXNVUQCKVVEGEBCSUVKUVKXCXKVTV
-      VCUXMUYSVURDKVVEHEBDSUVNUVNXCXKVTUOXLXMWAVUTVVBEVUKBEVULVUOEBUUGVUKXNEVUM
-      VUNLEBCVUKXNELXOEBDVUKXNXPXQUXLVUKKZVUPVULVUSVUOUXLVUKUVHTVVGVUQVUMVURVUN
-      LUXLVUKUVKTUXLVUKUVNTUOXRXSYJUVFUXKUYCVUEVULKUXRUUOBUWTUVHUUPXTYAZVUJUXEV
-      UMUYPVUNLUVFUXKUYCUXEVUMKUXRUUOBUWTUVKUUPXTYAZUVFUXKUYCUYPVUNKUXRUUOBUWTU
-      VNUUPXTYAZUOYBVTUXIUXDVUERUYDYCUXIUXFUXEUYQUYPLUXIUXDUXERUYDYCUXIUXDUYPRU
-      YDYCUOYBUYGRUVDVUFVUGUVDRUJYDUYGUXDVUERUXBUYFWJZYEUYGUXFRUYQRLUYGUXDUXERV
-      VKYEUYGUXDUYPRVVKYEUOUPUXBUYIUXDUYFYFUYJUXDYGVRYHUXBUXGVUFSPVUHVUFKUXHUXB
-      UXDVUERSUXIUUOSUWTUVTUXIBSUVHVNZUXKUUOSUVTVNAVVLUVEUXAUXDAEBUUGSVVFVOYIVU
-      BUUOBSUVHUUPVSVTUYEWNUYHUYJWTIUWTUWBVUFOSUWCUYLUVSUXDUWAVUERUYMUVRUWTUVTT
-      XBUWCXCXDVTUXBUXCUXFUYOUYQLUYNVUDUOYBYKUVFUVJUUMLSJOVUFURZQVMZNUWEUVFBUVI
-      VULUBJUUPUVTUUMUVGVUKUVHTUWSUXQUVFBSUVGUVHUVFEBUUGSUVFUXMUTCDUXOUYTXJVOXH
-      VVHYLUUMVVNUWDVVMUWCKVVNUWDKJIOVUFUWBJIXAZUXDUVSVUEUWARUWTUVRUUMUSXIZUWTU
-      VRUVTTXBYMLSVVMUWCQYNYOYPYQUVFUVMUWKUVPUWQLUVFUVMUUMLSJOUXFURZQVMZNUWKUVF
-      BUVLVUMUBJUUPUWFUUMUVGVUKUVKTUWSUXQUVFBSUVGUVKUXPXHVVIYLUUMVVRUWJVVQUWIKV
-      VRUWJKJIOUXFUWHVVOUXDUVSUXEUWGRVVPUWTUVRUWFTXBYMLSVVQUWIQYNYOYPYQUVFUVPUU
-      MLSJOUYQURZQVMZNUWQUVFBUVOVUNUBJUUPUWLUUMUVGVUKUVNTUWSUXQUVFBSUVGUVNVUAXH
-      VVJYLUUMVVTUWPVVSUWOKVVTUWPKJIOUYQUWNVVOUXDUVSUYPUWMRVVPUWTUVRUWLTXBYMLSV
-      VSUWOQYNYOYPYQUOYBAUVJUUHKZUVEAVVDEBXGVWAAVVDEBVVFXMBUUGUBEYRVRWQAUVQUUKK
-      UVEAUVMUUIUVPUUJLAUXNEBXGUVMUUIKAUXNEBGXMBCUBEYRVRAUYSEBXGUVPUUJKAUYSEBHX
-      MBDUBEYRVRUOWQYSYTUUAUUBABUUCPUUFUUSYFFBUAUUDVRUUE $.
+      sylc ser3add fsum3 cbvmptv seqeq3 ax-mp fveq1i syl6eq sumfct 3eqtr3d expr
+      exlimdv expimpd cfn fz1f1o mpjaod ) ABUCKZBCDLMZEUDZBCEUDZBDEUDZLMZKZBUEN
+      ZOPZQUUMUGMZBUAUHZUFZUAUIZUTZUUFUULVAAUUFUCUUGEUDZUCCEUDZUCDEUDZLMZUUHUUK
+      RRLMZRUVCUUTUJUVARUVBRLCEUKDEUKULUUGEUKUMBUCUUGEUNUUFUUIUVAUUJUVBLBUCCEUN
+      BUCDEUNUOUPUQAUUNUURUULAUUNUTUUQUULUAAUUNUUQUULAUUNUUQUTZUTZBUBUHZEBUUGUR
+      ZNZUBUDZBUVGEBCURZNZUBUDZBUVGEBDURZNZUBUDZLMZUUHUUKUVFUUMLIOIUHZUUMUSVBZU
+      VRUVHUUPVCZNZRVDZURZQVEZNZUUMLIOUVSUVRUVKUUPVCZNZRVDZURZQVEZNZUUMLIOUVSUV
+      RUVNUUPVCZNZRVDZURZQVEZNZLMUVJUVQUVFJUWIUWOUWCQUUMUVFUUMOQVFNZAUUNUUQVGZV
+      HVIUVFJUHZUWRPZUTZUWTUWINZUWTUUMUSVBZUWTUWFNZRVDZSUXBIUWTUWHUXFOUWISUWIVJ
+      IJVKZUVSUXDUWGUXERUVRUWTUUMUSVNZUVRUWTUWFTVLUXAUWTOPZUVFUXIUXAUWTVMVOVPZU
+      XBUXDUXERSUXBUXDUTZUUOSUWTUWFUVFUUOSUWFVQZUXAUXDUVFBSUVKVQUUOBUUPVQZUXLUV
+      FEBCSAEUHZBPZCSPZUVEGVRZVSZUVFUUQUXMAUUNUUQVTZUUOBUUPWFWAZUUOBSUVKUUPWBWC
+      WDUXKQWEPZUUMWEPZUWTWEPZWQQUWTUSVBZUXDUTUWTUUOPZUXKUYAUYBUYCUXKWGUXKUUMUV
+      FUUNUXAUXDUWSWDWHUXAUYCUVFUXDQUWTWIWJWKUXKUYDUXDUXAUYDUVFUXDQUWTWLWJUXBUX
+      DWMZWRUWTQUUMWNWOZWPUXBUXDWSZUTZWTZUXBUYCUYBUXDXAZUXBUWTUXJWHUXBUUMUVFUUN
+      UXAUWSXBWHUWTUUMXIWCZXCZXDZUYMXEUXBUWTUWONZUXDUWTUWLNZRVDZSUXBIUWTUWNUYQO
+      UWOSUWOVJUXGUVSUXDUWMUYPRUXHUVRUWTUWLTVLUXJUXBUXDUYPRSUXKUUOSUWTUWLUXKBSU
+      VNVQZUXMUUOSUWLVQUVFUYRUXAUXDUVFEBDSAUXODSPZUVEHVRZVSZWDUVFUXMUXAUXDUXTWD
+      ZUUOBSUVNUUPWBWCUYGWPUYJUYLXCZXDZVUCXEUXBUXDUWTUVTNZRVDZUXFUYQLMZUWTUWCNU
+      XCUYOLMUXBUXDVUFVUGKUYHUXKVUEUXEUYPLMZVUFVUGUXKUVFUYEVUEVUHKUVFUXAUXDXFUY
+      GUVFUYEUTZUWTUUPNZUVHNZVUJUVKNZVUJUVNNZLMZVUEVUHVUIVUJBPUXNUVHNZUXNUVKNZU
+      XNUVNNZLMZKZEBXGZVUKVUNKZUVFUUOBUWTUUPUXTXHAVUTUVEUYEAVUSEBAUXOUTZVUOUUGV
+      URVVBUXOUUGSPZVUOUUGKAUXOWMZVVBCDGHXJZEBUUGSUVHUVHVJXKWCVVBVUPCVUQDLVVBUX
+      OUXPVUPCKVVDGEBCSUVKUVKVJXKWCVVBUXOUYSVUQDKVVDHEBDSUVNUVNVJXKWCUOXLXMWDVU
+      SVVAEVUJBEVUKVUNEBUUGVUJXNEVULVUMLEBCVUJXNELXOEBDVUJXNXPXQUXNVUJKZVUOVUKV
+      URVUNUXNVUJUVHTVVFVUPVULVUQVUMLUXNVUJUVKTUXNVUJUVNTUOXRXSYJUVFUXMUYEVUEVU
+      KKUXTUUOBUWTUVHUUPXTYAZVUIUXEVULUYPVUMLUVFUXMUYEUXEVULKUXTUUOBUWTUVKUUPXT
+      YAZUVFUXMUYEUYPVUMKUXTUUOBUWTUVNUUPXTYAZUOYBWCUXKUXDVUERUYFYCUXKUXFUXEUYQ
+      UYPLUXKUXDUXERUYFYCUXKUXDUYPRUYFYCUOYBUYIRUVDVUFVUGUVDRUJYDUYIUXDVUERUXBU
+      YHWMZYEUYIUXFRUYQRLUYIUXDUXERVVJYEUYIUXDUYPRVVJYEUOUPUXBUYKUXDUYHYFUYLUXD
+      YGWAYHUXBIUWTUWBVUFOUWCSUWCVJUXGUVSUXDUWAVUERUXHUVRUWTUVTTVLUXJUXBUXDVUER
+      SUXKUUOSUWTUVTUXKBSUVHVQZUXMUUOSUVTVQAVVKUVEUXAUXDAEBUUGSVVEVSYIVUBUUOBSU
+      VHUUPWBWCUYGWPUYJUYLXCXDUXBUXCUXFUYOUYQLUYNVUDUOYBYKUVFUVJUUMLJOVUFURZQVE
+      ZNUWEUVFBUVIVUKUBJUUPUVTUUMUVGVUJUVHTUWSUXSUVFBSUVGUVHUVFEBUUGSUVFUXOUTCD
+      UXQUYTXJVSXHVVGYLUUMVVMUWDVVLUWCKVVMUWDKJIOVUFUWBJIVKZUXDUVSVUEUWARUWTUVR
+      UUMUSVNZUWTUVRUVTTVLYMLVVLUWCQYNYOYPYQUVFUVMUWKUVPUWQLUVFUVMUUMLJOUXFURZQ
+      VEZNUWKUVFBUVLVULUBJUUPUWFUUMUVGVUJUVKTUWSUXSUVFBSUVGUVKUXRXHVVHYLUUMVVQU
+      WJVVPUWIKVVQUWJKJIOUXFUWHVVNUXDUVSUXEUWGRVVOUWTUVRUWFTVLYMLVVPUWIQYNYOYPY
+      QUVFUVPUUMLJOUYQURZQVEZNUWQUVFBUVOVUMUBJUUPUWLUUMUVGVUJUVNTUWSUXSUVFBSUVG
+      UVNVUAXHVVIYLUUMVVSUWPVVRUWOKVVSUWPKJIOUYQUWNVVNUXDUVSUYPUWMRVVOUWTUVRUWL
+      TVLYMLVVRUWOQYNYOYPYQUOYBAUVJUUHKZUVEAVVCEBXGVVTAVVCEBVVEXMBUUGUBEYRWAXBA
+      UVQUUKKUVEAUVMUUIUVPUUJLAUXPEBXGUVMUUIKAUXPEBGXMBCUBEYRWAAUYSEBXGUVPUUJKA
+      UYSEBHXMBDUBEYRWAUOXBYSYTUUAUUBABUUCPUUFUUSYFFBUAUUDWAUUE $.
   $}
 
   ${