Add fprodshft to iset.mm

Stated as in set.mm.  The proof needs intuitionizing in a few places but
is mostly unchanged from the set.mm proof.

Author: jkingdon

iset.mm

@@ -124774,6 +124774,26 @@ seq n ( x. ,
       YGYOAXOYPIEFGHWKTYDXEDVOEYDXEGHWNWOWPJWQWRWGWSWI $.
   $}
 
+  ${
+    $d A k $.  $d B j $.  $d j k $.  $d j ph $.  $d K j $.  $d K k $.
+    $d k ph $.  $d M j $.  $d M k $.  $d N j $.  $d N k $.
+    fprodshft.1 $e |- ( ph -> K e. ZZ ) $.
+    fprodshft.2 $e |- ( ph -> M e. ZZ ) $.
+    fprodshft.3 $e |- ( ph -> N e. ZZ ) $.
+    fprodshft.4 $e |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC ) $.
+    ${
+      fprodshft.5 $e |- ( j = ( k - K ) -> A = B ) $.
+      $( Shift the index of a finite product.  (Contributed by Scott Fenton,
+         5-Jan-2018.) $)
+      fprodshft $p |- ( ph -> prod_ j e. ( M ... N ) A
+          = prod_ k e. ( ( M + K ) ... ( N + K ) ) B ) $=
+        ( cfz co caddc cv cmin wcel cz cmpt zaddcld fzfigd mptfzshft eqid oveq1
+        wa simpr elfzelz adantl adantr zsubcld fvmptd3 fprodf1o ) AGHNOBGFPOZHF
+        POZNOZCDEDUQDQZFROZUAZEQZFROZMAUOUPAGFJIUBAHFKIUBUCADFGHIJKUDAVAUQSZUGZ
+        DVAUSVBUQUTTUTUEURVAFRUFAVCUHVDVAFVCVATSAVAUOUPUIUJAFTSVCIUKULUMLUN $.
+    $}
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#