Metamath Proof Explorer

Theorem fprodabs

Description: The absolute value of a finite product. (Contributed by Scott Fenton, 25-Dec-2017)

Ref Expression
Hypotheses fprodabs.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
fprodabs.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
fprodabs.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
Assertion fprodabs ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( abs ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fprodabs.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 fprodabs.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 fprodabs.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
4 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 oveq2 ⊢ ( 𝑎 = 𝑀 → ( 𝑀 ... 𝑎 ) = ( 𝑀 ... 𝑀 ) )
6 5 prodeq1d ⊢ ( 𝑎 = 𝑀 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 = ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 )
7 6 fveq2d ⊢ ( 𝑎 = 𝑀 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 ) )
8 5 prodeq1d ⊢ ( 𝑎 = 𝑀 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( abs ‘ 𝐴 ) )
9 7 8 eqeq12d ⊢ ( 𝑎 = 𝑀 → ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) ↔ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( abs ‘ 𝐴 ) ) )
10 9 imbi2d ⊢ ( 𝑎 = 𝑀 → ( ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) ) ↔ ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( abs ‘ 𝐴 ) ) ) )
11 oveq2 ⊢ ( 𝑎 = 𝑛 → ( 𝑀 ... 𝑎 ) = ( 𝑀 ... 𝑛 ) )
12 11 prodeq1d ⊢ ( 𝑎 = 𝑛 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 )
13 12 fveq2d ⊢ ( 𝑎 = 𝑛 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) )
14 11 prodeq1d ⊢ ( 𝑎 = 𝑛 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) )
15 13 14 eqeq12d ⊢ ( 𝑎 = 𝑛 → ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) ↔ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) ) )
16 15 imbi2d ⊢ ( 𝑎 = 𝑛 → ( ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) ) ↔ ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) ) ) )
17 oveq2 ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ( 𝑀 ... 𝑎 ) = ( 𝑀 ... ( 𝑛 + 1 ) ) )
18 17 prodeq1d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 = ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 )
19 18 fveq2d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) )
20 17 prodeq1d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( abs ‘ 𝐴 ) )
21 19 20 eqeq12d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) ↔ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( abs ‘ 𝐴 ) ) )
22 21 imbi2d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) ) ↔ ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( abs ‘ 𝐴 ) ) ) )
23 oveq2 ⊢ ( 𝑎 = 𝑁 → ( 𝑀 ... 𝑎 ) = ( 𝑀 ... 𝑁 ) )
24 23 prodeq1d ⊢ ( 𝑎 = 𝑁 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 )
25 24 fveq2d ⊢ ( 𝑎 = 𝑁 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ) )
26 23 prodeq1d ⊢ ( 𝑎 = 𝑁 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( abs ‘ 𝐴 ) )
27 25 26 eqeq12d ⊢ ( 𝑎 = 𝑁 → ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) ↔ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( abs ‘ 𝐴 ) ) )
28 27 imbi2d ⊢ ( 𝑎 = 𝑁 → ( ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑎 ) ( abs ‘ 𝐴 ) ) ↔ ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( abs ‘ 𝐴 ) ) ) )
29 csbfv2g ⊢ ( 𝑀 ∈ ℤ → ⦋ 𝑀 / 𝑘 ⦌ ( abs ‘ 𝐴 ) = ( abs ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ⦋ 𝑀 / 𝑘 ⦌ ( abs ‘ 𝐴 ) = ( abs ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) )
31 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
33 32 prodeq1d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( abs ‘ 𝐴 ) = ∏ 𝑘 ∈ { 𝑀 } ( abs ‘ 𝐴 ) )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
35 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
36 35 1 eleqtrrdi ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ 𝑍 )
37 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ )
38 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑀 / 𝑘 ⦌ 𝐴
39 38 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ
40 csbeq1a ⊢ ( 𝑘 = 𝑀 → 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
41 40 eleq1d ⊢ ( 𝑘 = 𝑀 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
42 39 41 rspc ⊢ ( 𝑀 ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
43 37 42 mpan9 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑍 ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ )
44 36 43 sylan2 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ )
45 44 abscld ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( abs ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) ∈ ℝ )
46 45 recnd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( abs ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) ∈ ℂ )
47 30 46 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ⦋ 𝑀 / 𝑘 ⦌ ( abs ‘ 𝐴 ) ∈ ℂ )
48 prodsns ⊢ ( ( 𝑀 ∈ ℤ ∧ ⦋ 𝑀 / 𝑘 ⦌ ( abs ‘ 𝐴 ) ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } ( abs ‘ 𝐴 ) = ⦋ 𝑀 / 𝑘 ⦌ ( abs ‘ 𝐴 ) )
49 34 47 48 syl2anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑘 ∈ { 𝑀 } ( abs ‘ 𝐴 ) = ⦋ 𝑀 / 𝑘 ⦌ ( abs ‘ 𝐴 ) )
50 33 49 eqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( abs ‘ 𝐴 ) = ⦋ 𝑀 / 𝑘 ⦌ ( abs ‘ 𝐴 ) )
51 31 prodeq1d ⊢ ( 𝑀 ∈ ℤ → ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = ∏ 𝑘 ∈ { 𝑀 } 𝐴 )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = ∏ 𝑘 ∈ { 𝑀 } 𝐴 )
53 prodsns ⊢ ( ( 𝑀 ∈ ℤ ∧ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
54 34 44 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
55 52 54 eqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
56 55 fveq2d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 ) = ( abs ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) )
57 30 50 56 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( abs ‘ 𝐴 ) )
58 57 expcom ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) ( abs ‘ 𝐴 ) ) )
59 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) )
60 ovex ⊢ ( 𝑛 + 1 ) ∈ V
61 csbfv2g ⊢ ( ( 𝑛 + 1 ) ∈ V → ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ ( abs ‘ 𝐴 ) = ( abs ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) )
62 60 61 ax-mp ⊢ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ ( abs ‘ 𝐴 ) = ( abs ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 )
63 62 eqcomi ⊢ ( abs ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) = ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ ( abs ‘ 𝐴 )
64 63 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) ) → ( abs ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) = ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ ( abs ‘ 𝐴 ) )
65 59 64 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) ) → ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) · ( abs ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) ) = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) · ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ ( abs ‘ 𝐴 ) ) )
66 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
67 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
68 67 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) → 𝑘 ∈ 𝑍 )
69 68 3 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ) → 𝐴 ∈ ℂ )
70 69 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ) → 𝐴 ∈ ℂ )
71 66 70 fprodp1s ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 · ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) )
72 71 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) = ( abs ‘ ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 · ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) ) )
73 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ... 𝑛 ) ∈ Fin )
74 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
75 74 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ 𝑍 )
76 75 3 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐴 ∈ ℂ )
77 76 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐴 ∈ ℂ )
78 73 77 fprodcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ∈ ℂ )
79 peano2uz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
80 79 1 eleqtrrdi ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 + 1 ) ∈ 𝑍 )
81 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴
82 81 nfel1 ⊢ Ⅎ 𝑘 ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ
83 csbeq1a ⊢ ( 𝑘 = ( 𝑛 + 1 ) → 𝐴 = ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 )
84 83 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐴 ∈ ℂ ↔ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
85 82 84 rspc ⊢ ( ( 𝑛 + 1 ) ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ → ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
86 37 85 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ )
87 80 86 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ )
88 78 87 absmuld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 · ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) ) = ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) · ( abs ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) ) )
89 72 88 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) = ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) · ( abs ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) ) )
90 89 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) = ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) · ( abs ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) ) )
91 70 abscld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
92 91 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ) → ( abs ‘ 𝐴 ) ∈ ℂ )
93 66 92 fprodp1s ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( abs ‘ 𝐴 ) = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) · ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ ( abs ‘ 𝐴 ) ) )
94 93 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) ) → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( abs ‘ 𝐴 ) = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) · ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ ( abs ‘ 𝐴 ) ) )
95 65 90 94 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( abs ‘ 𝐴 ) )
96 95 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( abs ‘ 𝐴 ) ) ) )
97 96 com12 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( abs ‘ 𝐴 ) ) ) )
98 97 a2d ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ 𝐴 ) ) → ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( abs ‘ 𝐴 ) ) ) )
99 10 16 22 28 58 98 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( abs ‘ 𝐴 ) ) )
100 4 99 mpcom ⊢ ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( abs ‘ 𝐴 ) )