Metamath Proof Explorer

Theorem fprodefsum

Description: Move the exponential function from inside a finite product to outside a finite sum. (Contributed by Scott Fenton, 26-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 fprodefsum.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 fprodefsum.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 fprodefsum.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
4 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 oveq2 ⊢ ( 𝑎 = 𝑀 → ( 𝑀 ... 𝑎 ) = ( 𝑀 ... 𝑀 ) )
6 5 prodeq1d ⊢ ( 𝑎 = 𝑀 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ∏ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) )
7 5 sumeq1d ⊢ ( 𝑎 = 𝑀 → Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
8 7 fveq2d ⊢ ( 𝑎 = 𝑀 → ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) )
9 6 8 eqeq12d ⊢ ( 𝑎 = 𝑀 → ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ↔ ∏ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) )
10 9 imbi2d ⊢ ( 𝑎 = 𝑀 → ( ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ↔ ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ) )
11 oveq2 ⊢ ( 𝑎 = 𝑛 → ( 𝑀 ... 𝑎 ) = ( 𝑀 ... 𝑛 ) )
12 11 prodeq1d ⊢ ( 𝑎 = 𝑛 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) )
13 11 sumeq1d ⊢ ( 𝑎 = 𝑛 → Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
14 13 fveq2d ⊢ ( 𝑎 = 𝑛 → ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) )
15 12 14 eqeq12d ⊢ ( 𝑎 = 𝑛 → ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ↔ ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) )
16 15 imbi2d ⊢ ( 𝑎 = 𝑛 → ( ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ↔ ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ) )
17 oveq2 ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ( 𝑀 ... 𝑎 ) = ( 𝑀 ... ( 𝑛 + 1 ) ) )
18 17 prodeq1d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) )
19 17 sumeq1d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
20 19 fveq2d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) )
21 18 20 eqeq12d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ↔ ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) )
22 21 imbi2d ⊢ ( 𝑎 = ( 𝑛 + 1 ) → ( ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ↔ ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ) )
23 oveq2 ⊢ ( 𝑎 = 𝑁 → ( 𝑀 ... 𝑎 ) = ( 𝑀 ... 𝑁 ) )
24 23 prodeq1d ⊢ ( 𝑎 = 𝑁 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) )
25 23 sumeq1d ⊢ ( 𝑎 = 𝑁 → Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
26 25 fveq2d ⊢ ( 𝑎 = 𝑁 → ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) )
27 24 26 eqeq12d ⊢ ( 𝑎 = 𝑁 → ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ↔ ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) )
28 27 imbi2d ⊢ ( 𝑎 = 𝑁 → ( ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑎 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ↔ ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ) )
29 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
31 30 prodeq1d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ∏ 𝑚 ∈ { 𝑀 } ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
33 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
34 33 1 eleqtrrdi ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ 𝑍 )
35 efcl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ )
36 3 35 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( exp ‘ 𝐴 ) ∈ ℂ )
37 36 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) : 𝑍 ⟶ ℂ )
38 37 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑀 ) ∈ ℂ )
39 34 38 sylan2 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑀 ) ∈ ℂ )
40 fveq2 ⊢ ( 𝑚 = 𝑀 → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑀 ) )
41 40 prodsn ⊢ ( ( 𝑀 ∈ ℤ ∧ ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑀 ) ∈ ℂ ) → ∏ 𝑚 ∈ { 𝑀 } ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑀 ) )
42 32 39 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑚 ∈ { 𝑀 } ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑀 ) )
43 34 adantl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ 𝑍 )
44 fvex ⊢ ( exp ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) ∈ V
45 nfcv ⊢ Ⅎ 𝑘 𝑀
46 nfcv ⊢ Ⅎ 𝑘 exp
47 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑀 / 𝑘 ⦌ 𝐴
48 46 47 nffv ⊢ Ⅎ 𝑘 ( exp ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
49 csbeq1a ⊢ ( 𝑘 = 𝑀 → 𝐴 = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
50 49 fveq2d ⊢ ( 𝑘 = 𝑀 → ( exp ‘ 𝐴 ) = ( exp ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) )
51 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) )
52 45 48 50 51 fvmptf ⊢ ( ( 𝑀 ∈ 𝑍 ∧ ( exp ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) ∈ V ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑀 ) = ( exp ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) )
53 43 44 52 sylancl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑀 ) = ( exp ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) )
54 31 42 53 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) )
55 30 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → Σ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑚 ∈ { 𝑀 } ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
56 3 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) : 𝑍 ⟶ ℂ )
57 56 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑀 ) ∈ ℂ )
58 34 57 sylan2 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑀 ) ∈ ℂ )
59 fveq2 ⊢ ( 𝑚 = 𝑀 → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑀 ) )
60 59 sumsn ⊢ ( ( 𝑀 ∈ ℤ ∧ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑀 ) ∈ ℂ ) → Σ 𝑚 ∈ { 𝑀 } ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑀 ) )
61 32 58 60 syl2anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → Σ 𝑚 ∈ { 𝑀 } ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑀 ) )
62 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ )
63 47 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ
64 49 eleq1d ⊢ ( 𝑘 = 𝑀 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
65 63 64 rspc ⊢ ( 𝑀 ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
66 65 impcom ⊢ ( ( ∀ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ ∧ 𝑀 ∈ 𝑍 ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ )
67 62 34 66 syl2an ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ )
68 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) = ( 𝑘 ∈ 𝑍 ↦ 𝐴 )
69 68 fvmpts ⊢ ( ( 𝑀 ∈ 𝑍 ∧ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ∈ ℂ ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑀 ) = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
70 43 67 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑀 ) = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
71 55 61 70 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → Σ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ⦋ 𝑀 / 𝑘 ⦌ 𝐴 )
72 71 fveq2d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) = ( exp ‘ ⦋ 𝑀 / 𝑘 ⦌ 𝐴 ) )
73 54 72 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∏ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) )
74 73 expcom ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑀 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) )
75 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) → ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) )
76 1 peano2uzs ⊢ ( 𝑛 ∈ 𝑍 → ( 𝑛 + 1 ) ∈ 𝑍 )
77 simpr ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( 𝑛 + 1 ) ∈ 𝑍 )
78 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴
79 78 nfel1 ⊢ Ⅎ 𝑘 ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ
80 csbeq1a ⊢ ( 𝑘 = ( 𝑛 + 1 ) → 𝐴 = ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 )
81 80 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐴 ∈ ℂ ↔ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
82 79 81 rspc ⊢ ( ( 𝑛 + 1 ) ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ → ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
83 62 82 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ )
84 efcl ⊢ ( ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ → ( exp ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) ∈ ℂ )
85 83 84 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( exp ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) ∈ ℂ )
86 nfcv ⊢ Ⅎ 𝑘 ( 𝑛 + 1 )
87 46 78 nffv ⊢ Ⅎ 𝑘 ( exp ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 )
88 80 fveq2d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( exp ‘ 𝐴 ) = ( exp ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) )
89 86 87 88 51 fvmptf ⊢ ( ( ( 𝑛 + 1 ) ∈ 𝑍 ∧ ( exp ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) ∈ ℂ ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) )
90 77 85 89 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) )
91 68 fvmpts ⊢ ( ( ( 𝑛 + 1 ) ∈ 𝑍 ∧ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ∈ ℂ ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) = ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 )
92 77 83 91 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) = ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 )
93 92 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( exp ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) = ( exp ‘ ⦋ ( 𝑛 + 1 ) / 𝑘 ⦌ 𝐴 ) )
94 90 93 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) )
95 76 94 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) )
96 95 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) )
97 75 96 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) → ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) · ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ ( 𝑛 + 1 ) ) ) = ( ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) · ( exp ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) ) )
98 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
99 98 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
100 elfzuz ⊢ ( 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
101 100 1 eleqtrrdi ⊢ ( 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) → 𝑚 ∈ 𝑍 )
102 37 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) ∈ ℂ )
103 101 102 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) ∈ ℂ )
104 103 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) ∈ ℂ )
105 fveq2 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ ( 𝑛 + 1 ) ) )
106 99 104 105 fprodp1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) · ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ ( 𝑛 + 1 ) ) ) )
107 106 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) → ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) · ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ ( 𝑛 + 1 ) ) ) )
108 56 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
109 101 108 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
110 109 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
111 fveq2 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) )
112 99 110 111 fsump1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) + ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) )
113 112 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) = ( exp ‘ ( Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) + ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) ) )
114 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ... 𝑛 ) ∈ Fin )
115 elfzuz ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
116 115 1 eleqtrrdi ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑛 ) → 𝑚 ∈ 𝑍 )
117 116 108 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
118 117 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
119 114 118 fsumcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
120 56 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
121 76 120 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
122 efadd ⊢ ( ( Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ ∧ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) → ( exp ‘ ( Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) + ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) ) = ( ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) · ( exp ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) ) )
123 119 121 122 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( exp ‘ ( Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) + ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) ) = ( ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) · ( exp ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) ) )
124 113 123 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) = ( ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) · ( exp ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) ) )
125 124 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) → ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) = ( ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) · ( exp ‘ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ ( 𝑛 + 1 ) ) ) ) )
126 97 107 125 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) → ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) )
127 126 3exp ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) → ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ) )
128 127 com12 ⊢ ( 𝑛 ∈ 𝑍 → ( 𝜑 → ( ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) → ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ) )
129 128 a2d ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) → ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ) )
130 1 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
131 129 130 eleq2s ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑛 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) → ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... ( 𝑛 + 1 ) ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) ) )
132 10 16 22 28 74 131 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) ) )
133 4 132 mpcom ⊢ ( 𝜑 → ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) )
134 fvres ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) )
135 fzssuz ⊢ ( 𝑀 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 )
136 135 1 sseqtrri ⊢ ( 𝑀 ... 𝑁 ) ⊆ 𝑍
137 resmpt ⊢ ( ( 𝑀 ... 𝑁 ) ⊆ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ↾ ( 𝑀 ... 𝑁 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( exp ‘ 𝐴 ) ) )
138 136 137 ax-mp ⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ↾ ( 𝑀 ... 𝑁 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( exp ‘ 𝐴 ) )
139 138 fveq1i ⊢ ( ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 )
140 134 139 eqtr3di ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) )
141 140 prodeq2i ⊢ ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 )
142 prodfc ⊢ ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( exp ‘ 𝐴 )
143 141 142 eqtri ⊢ ∏ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ ( exp ‘ 𝐴 ) ) ‘ 𝑚 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( exp ‘ 𝐴 )
144 fvres ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
145 resmpt ⊢ ( ( 𝑀 ... 𝑁 ) ⊆ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑁 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) )
146 136 145 ax-mp ⊢ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑁 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 )
147 146 fveq1i ⊢ ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑚 )
148 144 147 eqtr3di ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑚 ) )
149 148 sumeq2i ⊢ Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑚 )
150 sumfc ⊢ Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴
151 149 150 eqtri ⊢ Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴
152 151 fveq2i ⊢ ( exp ‘ Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ) = ( exp ‘ Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 )
153 133 143 152 3eqtr3g ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( exp ‘ 𝐴 ) = ( exp ‘ Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ) )