Add fprodeq0 to iset.mm

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

Fix wording of comment (in both set.mm and iset.mm).

Author: jkingdon

iset.mm

@@ -124746,6 +124746,34 @@ seq n ( x. ,
       VHULZXEUVNBUVJVHVKWGWNWOWPWQWRWSWT $.
   $}
 
+  ${
+    $d K j k $.  $d M j k $.  $d N j k $.  $d Z k $.  $d ph j k $.
+    fprodeq0.1 $e |- Z = ( ZZ>= ` M ) $.
+    fprodeq0.2 $e |- ( ph -> N e. Z ) $.
+    fprodeq0.3 $e |- ( ( ph /\ k e. Z ) -> A e. CC ) $.
+    fprodeq0.4 $e |- ( ( ph /\ k = N ) -> A = 0 ) $.
+    $( Any finite product containing a zero term is itself zero.  (Contributed
+       by Scott Fenton, 27-Dec-2017.) $)
+    fprodeq0 $p |- ( ( ph /\ K e. ( ZZ>= ` N ) ) ->
+        prod_ k e. ( M ... K ) A = 0 ) $=
+      ( wcel wa cfz co cprod cmul cc0 cz syl vj cuz cfv c1 caddc clt wbr cin c0
+      wceq eluzel2 adantl ltp1d fzdisj cun w3a cle eleq2s adantr eluzelz eluzle
+      zred 3jca anim12i elfz2 sylanbrc fzsplit fzfigd cv elfzelz fzdcel syl3anc
+      wdc ralrimiva elfzuz eleqtrrdi sylan2 fprodsplitdc cmin eleqtrdi fprodm1s
+      adantlr csb csbied oveq2d peano2zm fprodcl mul01d 3eqtrd oveq1d peano2uzs
+      cc peano2zd uztrn2 syl2an adantrl syldan anassrs mul02d ) ADFUBUCLZMZEDNO
+      ZBCPEFNOZBCPZFUDUEOZDNOZBCPZQORXGQORXAXCXFBXBUACXAFXEUFUGXCXFUHUIUJXAFXAF
+      WTFSLZAFDUKULZVBUMEFXEDUNTXAFXBLZXBXCXFUOUJXAESLZDSLZXHUPEFUQUGZFDUQUGZMX
+      JXAXKXLXHAXKWTAFGLZXKIXKFEUBUCZGEFUKHURTZUSZWTXLAFDUTULZXIVCAXMWTXNAXOXMI
+      XMFXPGEFVAHURTFDVAVDFEDVEVFFEDVGTXAEDXRXSVHXAUAVIZXCLVMZUAXBXAXTXBLZMXTSL
+      ZXKXHYAYBYCXAXTEDVJULXAXKYBXRUSXAXHYBXIUSXTEFVKVLVNACVIZXBLZBWLLZWTYEAYDG
+      LZYFYEYDXPGYDEDVOHVPJVQWBVRXAXDRXGQAXDRUJWTAXDEFUDVSOZNOZBCPZCFBWCZQOYJRQ
+      ORABCEFAFGXPIHVTZYDXCLZAYGYFYMYDXPGYDEFVOHVPJVQWAAYKRYJQACFBRGIKWDWEAYJAY
+      IBCAEYHXQAXHYHSLAFXPLXHYLEFUTTFWFTVHYDYILZAYGYFYNYDXPGYDEYHVOHVPJVQWGWHWI
+      USWJXAXGXAXFBCXAXEDXAFXIWMXSVHAWTYDXFLZYFAWTYOMYGYFAYOYGWTAXEGLZYDXEUBUCL
+      YGYOAXOYPIEFGHWKTYDXEDVOEYDXEGHWNWOWPJWQWRWGWSWI $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#

set.mm

@@ -173677,8 +173677,8 @@ seq n ( x. ,
     fprodeq0.2 $e |- ( ph -> N e. Z ) $.
     fprodeq0.3 $e |- ( ( ph /\ k e. Z ) -> A e. CC ) $.
     fprodeq0.4 $e |- ( ( ph /\ k = N ) -> A = 0 ) $.
-    $( Anything finite product containing a zero term is itself zero.
-       (Contributed by Scott Fenton, 27-Dec-2017.) $)
+    $( Any finite product containing a zero term is itself zero.  (Contributed
+       by Scott Fenton, 27-Dec-2017.) $)
     fprodeq0 $p |- ( ( ph /\ K e. ( ZZ>= ` N ) ) ->
        prod_ k e. ( M ... K ) A = 0 ) $=
       ( cuz wcel cfz co cprod cmul cc0 syl elfzuz cfv wa caddc clt wbr cin wceq