Add fprodabs to iset.mm

Stated as in set.mm.  The proof needs a little bit of intutionizing but
most steps are unchanged from the set.mm proof.

Author: jkingdon

iset.mm

@@ -124711,6 +124711,41 @@ seq n ( x. ,
       XNWTHHIXNWTLHMJHWOLHMVPVQVRVSPXNXAHFGHFWOVTWAVRWBWCWDWEWF $.
   $}
 
+  ${
+    $d A a n $.  $d M a k n $.  $d N a k $.  $d Z a k n $.  $d ph a k n $.
+    fprodabs.1 $e |- Z = ( ZZ>= ` M ) $.
+    fprodabs.2 $e |- ( ph -> N e. Z ) $.
+    fprodabs.3 $e |- ( ( ph /\ k e. Z ) -> A e. CC ) $.
+    $( The absolute value of a finite product.  (Contributed by Scott Fenton,
+       25-Dec-2017.) $)
+    fprodabs $p |- ( ph -> ( abs ` prod_ k e. ( M ... N ) A ) =
+      prod_ k e. ( M ... N ) ( abs ` A ) ) $=
+      ( cfv wcel cfz co cprod cabs wceq wi prodeq1d fveq2d cc va vn eleqtrdi cv
+      cuz c1 caddc oveq2 eqeq12d imbi2d cz wa csb csbfv2g adantl csn fzsn simpr
+      uzid eleqtrrdi ralrimiva nfcsb1v nfel1 csbeq1a eleq1d mpan9 sylan2 abscld
+      wral rspc recnd eqeltrd prodsns syl2anc 3eqtr4rd expcom w3a cmul peano2uz
+      eqtrd syl eqcomd 3ad2ant2 oveq12d elfzuz adantlr fprodp1s eluzel2 eluzelz
+      simp3 fzfigd fprodcl absmuld 3adant3 3eqtr4d 3exp com12 a2d uzind4 mpcom
+      ) EDUEJZKADELMZBCNZOJZXBBOJZCNZPZAEFXAHGUCADUAUDZLMZBCNZOJZXIXECNZPZQADDL
+      MZBCNZOJZXNXECNZPZQADUBUDZLMZBCNZOJZXTXECNZPZQADXSUFUGMZLMZBCNZOJZYFXECNZ
+      PZQAXGQUAUBDEXHDPZXMXRAYKXKXPXLXQYKXJXOOYKXIXNBCXHDDLUHZRSYKXIXNXECYLRUIU
+      JXHXSPZXMYDAYMXKYBXLYCYMXJYAOYMXIXTBCXHXSDLUHZRSYMXIXTXECYNRUIUJXHYEPZXMY
+      JAYOXKYHXLYIYOXJYGOYOXIYFBCXHYEDLUHZRSYOXIYFXECYPRUIUJXHEPZXMXGAYQXKXDXLX
+      FYQXJXCOYQXIXBBCXHEDLUHZRSYQXIXBXECYRRUIUJADUKKZXRAYSULZCDXEUMZCDBUMZOJZX
+      QXPYSUUAUUCPACDBUKOUNUOZYTXQDUPZXECNZUUAYTXNUUEXECYSXNUUEPADUQZUORYTYSUUA
+      TKUUFUUAPAYSURZYTUUAUUCTUUDYTUUCYTUUBYSADFKZUUBTKZYSDXAFDUSGUTABTKZCFVIZU
+      UIUUJAUUKCFIVAZUUKUUJCDFCUUBTCDBVBVCCUDZDPBUUBTCDBVDVEVJVFVGZVHVKVLXECDUK
+      VMVNVTYTXOUUBOYTXOUUEBCNZUUBYSXOUUPPAYSXNUUEBCUUGRUOYTYSUUJUUPUUBPUUHUUOB
+      CDUKVMVNVTSVOVPXSXAKZAYDYJAUUQYDYJQAUUQYDYJAUUQYDVQZYBCYEBUMZOJZVRMZYCCYE
+      XEUMZVRMZYHYIUURYBYCUUTUVBVRAUUQYDWJUUQAUUTUVBPYDUUQUVBUUTUUQYEXAKUVBUUTP
+      DXSVSZCYEBXAOUNWAWBWCWDAUUQYHUVAPYDAUUQULZYHYAUUSVRMZOJUVAUVEYGUVFOUVEBCD
+      XSAUUQURZAUUNYFKZUUKUUQUVHAUUNFKZUUKUVHUUNXAFUUNDYEWEGUTIVGWFZWGSUVEYAUUS
+      UVEXTBCUVEDXSUUQYSADXSWHUOUUQXSUKKADXSWIUOWKAUUNXTKZUUKUUQUVKAUVIUUKUVKUU
+      NXAFUUNDXSWEGUTIVGWFWLUUQAYEFKZUUSTKZUUQYEXAFUVDGUTAUULUVLUVMUUMUUKUVMCYE
+      FCUUSTCYEBVBVCUUNYEPBUUSTCYEBVDVEVJVFVGWMVTWNAUUQYIUVCPYDUVEXECDXSUVGUVEU
+      VHULZXEUVNBUVJVHVKWGWNWOWPWQWRWSWT $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#