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 
|- Z = ( ZZ>= ` M )
fprodefsum.2 
|- ( ph -> N e. Z )
fprodefsum.3 
|- ( ( ph /\ k e. Z ) -> A e. CC )
Assertion fprodefsum 
|- ( ph -> prod_ k e. ( M ... N ) ( exp ` A ) = ( exp ` sum_ k e. ( M ... N ) A ) )

Proof

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