Add finite product closure theorems to iset.mm

These are fprodcl , fprodrecl , fprodzcl , fprodnncl , fprodrpcl ,
fprodnn0cl , fprodcllemf , and fprodreclf

They are copied from set.mm without change.

Author: jkingdon

iset.mm

@@ -124599,6 +124599,98 @@ seq n ( x. ,
       PEFPVEKULAVEUNUOAVHVCMTDPMUPZUQVCVEUQJMDURVIVEVCMDUSVAUTVB $.
   $}
 
+  ${
+    $d A k x y $.  $d B x y $.  $d ph k x y $.
+    fprodcl.1 $e |- ( ph -> A e. Fin ) $.
+
+    ${
+      fprodcl.2 $e |- ( ( ph /\ k e. A ) -> B e. CC ) $.
+      $( Closure of a finite product of complex numbers.  (Contributed by Scott
+         Fenton, 14-Dec-2017.) $)
+      fprodcl $p |- ( ph -> prod_ k e. A B e. CC ) $=
+        ( vx vy cc ssidd cv wcel wa cmul co mulcl adantl 1cnd fprodcllem ) AGHB
+        CIDAIJGKZILHKZILMTUANOILATUAPQEFARS $.
+    $}
+
+    ${
+      fprodrecl.2 $e |- ( ( ph /\ k e. A ) -> B e. RR ) $.
+      $( Closure of a finite product of real numbers.  (Contributed by Scott
+         Fenton, 14-Dec-2017.) $)
+      fprodrecl $p |- ( ph -> prod_ k e. A B e. RR ) $=
+        ( vx vy cr cc wss ax-resscn a1i cv wcel wa cmul co remulcl adantl 1red
+        fprodcllem ) AGHBCIDIJKALMGNZIOHNZIOPUCUDQRIOAUCUDSTEFAUAUB $.
+    $}
+
+    ${
+      fprodzcl.2 $e |- ( ( ph /\ k e. A ) -> B e. ZZ ) $.
+      $( Closure of a finite product of integers.  (Contributed by Scott
+         Fenton, 14-Dec-2017.) $)
+      fprodzcl $p |- ( ph -> prod_ k e. A B e. ZZ ) $=
+        ( vx vy cz cc wss zsscn a1i cv wcel wa cmul co zmulcl adantl fprodcllem
+        1zzd ) AGHBCIDIJKALMGNZIOHNZIOPUCUDQRIOAUCUDSTEFAUBUA $.
+    $}
+
+    ${
+      fprodnncl.2 $e |- ( ( ph /\ k e. A ) -> B e. NN ) $.
+      $( Closure of a finite product of positive integers.  (Contributed by
+         Scott Fenton, 14-Dec-2017.) $)
+      fprodnncl $p |- ( ph -> prod_ k e. A B e. NN ) $=
+        ( vx vy cn cc wss nnsscn a1i cv wcel wa cmul co nnmulcl adantl c1 1nn
+        fprodcllem ) AGHBCIDIJKALMGNZIOHNZIOPUDUEQRIOAUDUESTEFUAIOAUBMUC $.
+    $}
+
+    ${
+      fprodrpcl.2 $e |- ( ( ph /\ k e. A ) -> B e. RR+ ) $.
+      $( Closure of a finite product of positive reals.  (Contributed by Scott
+         Fenton, 14-Dec-2017.) $)
+      fprodrpcl $p |- ( ph -> prod_ k e. A B e. RR+ ) $=
+        ( vx vy crp cc wss cr rpssre ax-resscn sstri a1i cv wcel wa cmul adantl
+        co rpmulcl c1 1rp fprodcllem ) AGHBCIDIJKAILJMNOPGQZIRHQZIRSUGUHTUBIRAU
+        GUHUCUAEFUDIRAUEPUF $.
+    $}
+
+    ${
+      fprodnn0cl.2 $e |- ( ( ph /\ k e. A ) -> B e. NN0 ) $.
+      $( Closure of a finite product of nonnegative integers.  (Contributed by
+         Scott Fenton, 14-Dec-2017.) $)
+      fprodnn0cl $p |- ( ph -> prod_ k e. A B e. NN0 ) $=
+        ( vx vy cn0 cc wss nn0sscn a1i cv wcel wa cmul co nn0mulcl adantl 1nn0
+        c1 fprodcllem ) AGHBCIDIJKALMGNZIOHNZIOPUDUEQRIOAUDUESTEFUBIOAUAMUC $.
+    $}
+  $}
+
+  ${
+    $d A j k x y $.  $d B j x y $.  $d S j k x y $.  $d j ph x y $.
+    fprodcllemf.ph $e |- F/ k ph $.
+    fprodcllemf.s $e |- ( ph -> S C_ CC ) $.
+    fprodcllemf.xy $e |- ( ( ph /\ ( x e. S /\ y e. S ) )
+                           -> ( x x. y ) e. S ) $.
+    fprodcllemf.a $e |- ( ph -> A e. Fin ) $.
+    fprodcllemf.b $e |- ( ( ph /\ k e. A ) -> B e. S ) $.
+    fprodcllemf.1 $e |- ( ph -> 1 e. S ) $.
+    $( Finite product closure lemma.  A version of ~ fprodcllem using
+       bound-variable hypotheses instead of distinct variable conditions.
+       (Contributed by Glauco Siliprandi, 5-Apr-2020.) $)
+    fprodcllemf $p |- ( ph -> prod_ k e. A B e. S ) $=
+      ( vj cprod cv csb nfcv nfcsb1v wcel csbeq1a cbvprodi wa wsbc wral ralrimi
+      ex rspsbc mpan9 wb cvv sbcel1g elv sylib fprodcllem eqeltrid ) ADEGODGNPZ
+      EQZNOFDEURGNNERGUQESGUQEUAUBABCDURFNIJKAUQDTZUCEFTZGUQUDZURFTZAUTGDUEUSVA
+      AUTGDHAGPDTUTLUGUFUTGUQDUHUIVAVBUJNGUQEFUKULUMUNMUOUP $.
+  $}
+
+  ${
+    $d A k x y $.  $d B x y $.  $d ph x y $.
+    fprodreclf.kph $e |- F/ k ph $.
+    fprodcl.a $e |- ( ph -> A e. Fin ) $.
+    fprodrecl.b $e |- ( ( ph /\ k e. A ) -> B e. RR ) $.
+    $( Closure of a finite product of real numbers.  A version of ~ fprodrecl
+       using bound-variable hypotheses instead of distinct variable conditions.
+       (Contributed by Glauco Siliprandi, 5-Apr-2020.) $)
+    fprodreclf $p |- ( ph -> prod_ k e. A B e. RR ) $=
+      ( vx vy cr cc wss ax-resscn a1i cv wcel wa cmul co remulcl adantl 1red
+      fprodcllemf ) AHIBCJDEJKLAMNHOZJPIOZJPQUDUERSJPAUDUETUAFGAUBUC $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#