Add fsumsersdc to iset.mm

Like fisumsers but uses df-seq3 syntax.

Author: jkingdon

iset-discouraged

@@ -155,6 +155,7 @@
 "fisumcvg2" is used by "fisumsers".
 "fisumser" is used by "fsum3ser".
 "fisumser" is used by "isumclim3".
+"fisumsers" is used by "fisumser".
 "hbs1" is used by "eu1".
 "hbs1" is used by "hbab1".
 "hbs1" is used by "mopick".
@@ -382,6 +383,7 @@ New usage of "exmidfodomrlemrALT" is discouraged (0 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).
+New usage of "fisumsers" is discouraged (1 uses).
 New usage of "fnexALT" is discouraged (0 uses).
 New usage of "hbs1" is discouraged (5 uses).
 New usage of "idALT" is discouraged (0 uses).

iset.mm

@@ -115899,13 +115899,30 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
       WFWNYBSXNYCXTYDWNYBEVMWNYBWQVMWGVAVCXLTPUBOZTPVEXLYFUDWHTPAXLYFWIWJWKZAGW
       SWRYGWLWM $.
 
+    ${
+      $d A j k $.  $d B j $.  $d F j k $.  $d M j k $.  $d M k $.  $d N k $.
+      $d j k ph $.
+
+      $( Special case of series sum over a finite upper integer index set.
+         (Contributed by Mario Carneiro, 26-Jul-2013.)  (Revised by Jim
+         Kingdon, 5-May-2023.) $)
+      fsumsersdc $p |- ( ph -> sum_ k e. A B = ( seq M ( + , F ) ` N ) ) $=
+        ( vj cli cfv wcel cv wdc wral cc csu caddc cseq cuz eqid cz eluzel2 syl
+        cfz co fzssuz syl6ss ralrimiva weq eleq1w dcbid cbvralv zsumdc wfun wbr
+        sylib wceq cdm wf fclim ffun ax-mp fsum3cvg2 funbrfv mpsyl eqtrd ) ABCD
+        UAUBEFUCZNOZGVLOZAMBCDEFFUDOZVOUEAGVOPFUFPIFGUGUHABFGUIUJVOLFGUKULHADQB
+        PZRZDVOSMQBPZRZMVOSAVQDVOKUMVQVSDMVODMUNVPVRDMBUOUPUQVAJURNUSZAVLVNNUTV
+        MVNVBNVCZTNVDVTVEWATNVFVGABCDEFGHIJKLVHVLVNNVIVJVK $.
+    $}
+
     ${
       $d A j k $.  $d B j $.  $d F j k $.  $d M j k $.  $d M k $.  $d N k $.
       $d j k ph $.
 
       $( Special case of series sum over a finite upper integer index set.
          (Contributed by Mario Carneiro, 26-Jul-2013.)  (Revised by Mario
-         Carneiro, 21-Apr-2014.) $)
+         Carneiro, 21-Apr-2014.)  Use ~ fsumsersdc instead.
+         (New usage is discouraged.) $)
       fisumsers $p |- ( ph -> sum_ k e. A B = ( seq M ( + , F , CC ) ` N ) ) $=
         ( vj cc cli cfv wcel cv wdc wral csu caddc cseq4 cuz cz eluzel2 syl cfz
         eqid co fzssuz syl6ss ralrimiva weq eleq1w dcbid cbvralv sylib wfun wbr

mmil.raw.html

@@ -8323,7 +8323,7 @@
 
 <TR>
   <TD>fsumsers</TD>
-  <TD>~ fisumsers</TD>
+  <TD>~ fsumsersdc</TD>
 </TR>
 
 <TR>