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 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑀 ∈ 𝑍 ) β†’ ( ( π‘˜ ∈ 𝑍 ↦ ( 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 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑀 ∈ 𝑍 ) β†’ ( ( π‘˜ ∈ 𝑍 ↦ 𝐴 ) β€˜ 𝑀 ) ∈ β„‚ )
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 ffvelcdmda ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝑍 ) β†’ ( ( π‘˜ ∈ 𝑍 ↦ ( 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 ffvelcdmda ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝑍 ) β†’ ( ( π‘˜ ∈ 𝑍 ↦ 𝐴 ) β€˜ π‘š ) ∈ β„‚ )
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 ffvelcdmda ⊒ ( ( πœ‘ ∧ ( 𝑛 + 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 β€˜ Ξ£ π‘˜ ∈ ( 𝑀 ... 𝑁 ) 𝐴 ) )