Metamath Proof Explorer

Theorem efaddlem

Description: Lemma for efadd (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses efadd.1 
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
efadd.2 
|- G = ( n e. NN0 |-> ( ( B ^ n ) / ( ! ` n ) ) )
efadd.3 
|- H = ( n e. NN0 |-> ( ( ( A + B ) ^ n ) / ( ! ` n ) ) )
efadd.4 
|- ( ph -> A e. CC )
efadd.5 
|- ( ph -> B e. CC )
Assertion efaddlem 
|- ( ph -> ( exp ` ( A + B ) ) = ( ( exp ` A ) x. ( exp ` B ) ) )

Proof

Step Hyp Ref Expression
1 efadd.1 
 |-  F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2 efadd.2 
 |-  G = ( n e. NN0 |-> ( ( B ^ n ) / ( ! ` n ) ) )
3 efadd.3 
 |-  H = ( n e. NN0 |-> ( ( ( A + B ) ^ n ) / ( ! ` n ) ) )
4 efadd.4 
 |-  ( ph -> A e. CC )
5 efadd.5 
 |-  ( ph -> B e. CC )
6 4 5 addcld 
 |-  ( ph -> ( A + B ) e. CC )
7 3 efcvg 
 |-  ( ( A + B ) e. CC -> seq 0 ( + , H ) ~~> ( exp ` ( A + B ) ) )
8 6 7 syl 
 |-  ( ph -> seq 0 ( + , H ) ~~> ( exp ` ( A + B ) ) )
9 1 eftval 
 |-  ( j e. NN0 -> ( F ` j ) = ( ( A ^ j ) / ( ! ` j ) ) )
10 9 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( F ` j ) = ( ( A ^ j ) / ( ! ` j ) ) )
11 absexp 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( abs ` ( A ^ j ) ) = ( ( abs ` A ) ^ j ) )
12 4 11 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` ( A ^ j ) ) = ( ( abs ` A ) ^ j ) )
13 faccl 
 |-  ( j e. NN0 -> ( ! ` j ) e. NN )
14 13 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ! ` j ) e. NN )
15 nnre 
 |-  ( ( ! ` j ) e. NN -> ( ! ` j ) e. RR )
16 nnnn0 
 |-  ( ( ! ` j ) e. NN -> ( ! ` j ) e. NN0 )
17 16 nn0ge0d 
 |-  ( ( ! ` j ) e. NN -> 0 <_ ( ! ` j ) )
18 15 17 absidd 
 |-  ( ( ! ` j ) e. NN -> ( abs ` ( ! ` j ) ) = ( ! ` j ) )
19 14 18 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` ( ! ` j ) ) = ( ! ` j ) )
20 12 19 oveq12d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( abs ` ( A ^ j ) ) / ( abs ` ( ! ` j ) ) ) = ( ( ( abs ` A ) ^ j ) / ( ! ` j ) ) )
21 expcl 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( A ^ j ) e. CC )
22 4 21 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( A ^ j ) e. CC )
23 14 nncnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ! ` j ) e. CC )
24 14 nnne0d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ! ` j ) =/= 0 )
25 22 23 24 absdivd 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` ( ( A ^ j ) / ( ! ` j ) ) ) = ( ( abs ` ( A ^ j ) ) / ( abs ` ( ! ` j ) ) ) )
26 eqid 
 |-  ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) )
27 26 eftval 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) ) ` j ) = ( ( ( abs ` A ) ^ j ) / ( ! ` j ) ) )
28 27 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) ) ` j ) = ( ( ( abs ` A ) ^ j ) / ( ! ` j ) ) )
29 20 25 28 3eqtr4rd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) ) ` j ) = ( abs ` ( ( A ^ j ) / ( ! ` j ) ) ) )
30 eftcl 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( ( A ^ j ) / ( ! ` j ) ) e. CC )
31 4 30 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( A ^ j ) / ( ! ` j ) ) e. CC )
32 2 eftval 
 |-  ( k e. NN0 -> ( G ` k ) = ( ( B ^ k ) / ( ! ` k ) ) )
33 32 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) = ( ( B ^ k ) / ( ! ` k ) ) )
34 eftcl 
 |-  ( ( B e. CC /\ k e. NN0 ) -> ( ( B ^ k ) / ( ! ` k ) ) e. CC )
35 5 34 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( B ^ k ) / ( ! ` k ) ) e. CC )
36 3 eftval 
 |-  ( k e. NN0 -> ( H ` k ) = ( ( ( A + B ) ^ k ) / ( ! ` k ) ) )
37 36 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( H ` k ) = ( ( ( A + B ) ^ k ) / ( ! ` k ) ) )
38 4 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> A e. CC )
39 5 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> B e. CC )
40 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
41 binom 
 |-  ( ( A e. CC /\ B e. CC /\ k e. NN0 ) -> ( ( A + B ) ^ k ) = sum_ j e. ( 0 ... k ) ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) )
42 38 39 40 41 syl3anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A + B ) ^ k ) = sum_ j e. ( 0 ... k ) ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) )
43 42 oveq1d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( A + B ) ^ k ) / ( ! ` k ) ) = ( sum_ j e. ( 0 ... k ) ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) / ( ! ` k ) ) )
44 fzfid 
 |-  ( ( ph /\ k e. NN0 ) -> ( 0 ... k ) e. Fin )
45 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
46 45 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. NN )
47 46 nncnd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. CC )
48 bccl2 
 |-  ( j e. ( 0 ... k ) -> ( k _C j ) e. NN )
49 48 adantl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( k _C j ) e. NN )
50 49 nncnd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( k _C j ) e. CC )
51 4 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> A e. CC )
52 fznn0sub 
 |-  ( j e. ( 0 ... k ) -> ( k - j ) e. NN0 )
53 52 adantl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( k - j ) e. NN0 )
54 51 53 expcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( A ^ ( k - j ) ) e. CC )
55 5 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> B e. CC )
56 elfznn0 
 |-  ( j e. ( 0 ... k ) -> j e. NN0 )
57 56 adantl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> j e. NN0 )
58 55 57 expcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( B ^ j ) e. CC )
59 54 58 mulcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) e. CC )
60 50 59 mulcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) e. CC )
61 46 nnne0d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) =/= 0 )
62 44 47 60 61 fsumdivc 
 |-  ( ( ph /\ k e. NN0 ) -> ( sum_ j e. ( 0 ... k ) ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) / ( ! ` k ) ) = sum_ j e. ( 0 ... k ) ( ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) / ( ! ` k ) ) )
63 51 57 expcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( A ^ j ) e. CC )
64 57 13 syl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ! ` j ) e. NN )
65 64 nncnd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ! ` j ) e. CC )
66 64 nnne0d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ! ` j ) =/= 0 )
67 63 65 66 divcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( A ^ j ) / ( ! ` j ) ) e. CC )
68 2 eftval 
 |-  ( ( k - j ) e. NN0 -> ( G ` ( k - j ) ) = ( ( B ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) )
69 53 68 syl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( G ` ( k - j ) ) = ( ( B ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) )
70 55 53 expcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( B ^ ( k - j ) ) e. CC )
71 faccl 
 |-  ( ( k - j ) e. NN0 -> ( ! ` ( k - j ) ) e. NN )
72 53 71 syl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ! ` ( k - j ) ) e. NN )
73 72 nncnd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ! ` ( k - j ) ) e. CC )
74 72 nnne0d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ! ` ( k - j ) ) =/= 0 )
75 70 73 74 divcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( B ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) e. CC )
76 69 75 eqeltrd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( G ` ( k - j ) ) e. CC )
77 67 76 mulcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( A ^ j ) / ( ! ` j ) ) x. ( G ` ( k - j ) ) ) e. CC )
78 oveq2 
 |-  ( j = ( ( 0 + k ) - m ) -> ( A ^ j ) = ( A ^ ( ( 0 + k ) - m ) ) )
79 fveq2 
 |-  ( j = ( ( 0 + k ) - m ) -> ( ! ` j ) = ( ! ` ( ( 0 + k ) - m ) ) )
80 78 79 oveq12d 
 |-  ( j = ( ( 0 + k ) - m ) -> ( ( A ^ j ) / ( ! ` j ) ) = ( ( A ^ ( ( 0 + k ) - m ) ) / ( ! ` ( ( 0 + k ) - m ) ) ) )
81 oveq2 
 |-  ( j = ( ( 0 + k ) - m ) -> ( k - j ) = ( k - ( ( 0 + k ) - m ) ) )
82 81 fveq2d 
 |-  ( j = ( ( 0 + k ) - m ) -> ( G ` ( k - j ) ) = ( G ` ( k - ( ( 0 + k ) - m ) ) ) )
83 80 82 oveq12d 
 |-  ( j = ( ( 0 + k ) - m ) -> ( ( ( A ^ j ) / ( ! ` j ) ) x. ( G ` ( k - j ) ) ) = ( ( ( A ^ ( ( 0 + k ) - m ) ) / ( ! ` ( ( 0 + k ) - m ) ) ) x. ( G ` ( k - ( ( 0 + k ) - m ) ) ) ) )
84 77 83 fsumrev2 
 |-  ( ( ph /\ k e. NN0 ) -> sum_ j e. ( 0 ... k ) ( ( ( A ^ j ) / ( ! ` j ) ) x. ( G ` ( k - j ) ) ) = sum_ m e. ( 0 ... k ) ( ( ( A ^ ( ( 0 + k ) - m ) ) / ( ! ` ( ( 0 + k ) - m ) ) ) x. ( G ` ( k - ( ( 0 + k ) - m ) ) ) ) )
85 2 eftval 
 |-  ( j e. NN0 -> ( G ` j ) = ( ( B ^ j ) / ( ! ` j ) ) )
86 57 85 syl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( G ` j ) = ( ( B ^ j ) / ( ! ` j ) ) )
87 86 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( A ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) x. ( G ` j ) ) = ( ( ( A ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) x. ( ( B ^ j ) / ( ! ` j ) ) ) )
88 72 64 nnmulcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) e. NN )
89 88 nncnd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) e. CC )
90 88 nnne0d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) =/= 0 )
91 59 89 90 divrec2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) = ( ( 1 / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) )
92 54 73 58 65 74 66 divmuldivd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( A ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) x. ( ( B ^ j ) / ( ! ` j ) ) ) = ( ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) )
93 bcval2 
 |-  ( j e. ( 0 ... k ) -> ( k _C j ) = ( ( ! ` k ) / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) )
94 93 adantl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( k _C j ) = ( ( ! ` k ) / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) )
95 94 oveq1d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( k _C j ) / ( ! ` k ) ) = ( ( ( ! ` k ) / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) / ( ! ` k ) ) )
96 47 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ! ` k ) e. CC )
97 61 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ! ` k ) =/= 0 )
98 96 89 96 90 97 divdiv32d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( ! ` k ) / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) / ( ! ` k ) ) = ( ( ( ! ` k ) / ( ! ` k ) ) / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) )
99 96 97 dividd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ! ` k ) / ( ! ` k ) ) = 1 )
100 99 oveq1d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( ! ` k ) / ( ! ` k ) ) / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) = ( 1 / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) )
101 98 100 eqtrd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( ! ` k ) / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) / ( ! ` k ) ) = ( 1 / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) )
102 95 101 eqtrd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( k _C j ) / ( ! ` k ) ) = ( 1 / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) )
103 102 oveq1d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( k _C j ) / ( ! ` k ) ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) = ( ( 1 / ( ( ! ` ( k - j ) ) x. ( ! ` j ) ) ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) )
104 91 92 103 3eqtr4rd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( k _C j ) / ( ! ` k ) ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) = ( ( ( A ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) x. ( ( B ^ j ) / ( ! ` j ) ) ) )
105 87 104 eqtr4d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( A ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) x. ( G ` j ) ) = ( ( ( k _C j ) / ( ! ` k ) ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) )
106 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
107 106 ad2antlr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> k e. CC )
108 107 addlidd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( 0 + k ) = k )
109 108 oveq1d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( 0 + k ) - j ) = ( k - j ) )
110 109 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( A ^ ( ( 0 + k ) - j ) ) = ( A ^ ( k - j ) ) )
111 109 fveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ! ` ( ( 0 + k ) - j ) ) = ( ! ` ( k - j ) ) )
112 110 111 oveq12d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( A ^ ( ( 0 + k ) - j ) ) / ( ! ` ( ( 0 + k ) - j ) ) ) = ( ( A ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) )
113 109 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( k - ( ( 0 + k ) - j ) ) = ( k - ( k - j ) ) )
114 nn0cn 
 |-  ( j e. NN0 -> j e. CC )
115 57 114 syl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> j e. CC )
116 107 115 nncand 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( k - ( k - j ) ) = j )
117 113 116 eqtrd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( k - ( ( 0 + k ) - j ) ) = j )
118 117 fveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( G ` ( k - ( ( 0 + k ) - j ) ) ) = ( G ` j ) )
119 112 118 oveq12d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( A ^ ( ( 0 + k ) - j ) ) / ( ! ` ( ( 0 + k ) - j ) ) ) x. ( G ` ( k - ( ( 0 + k ) - j ) ) ) ) = ( ( ( A ^ ( k - j ) ) / ( ! ` ( k - j ) ) ) x. ( G ` j ) ) )
120 50 59 96 97 div23d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) / ( ! ` k ) ) = ( ( ( k _C j ) / ( ! ` k ) ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) )
121 105 119 120 3eqtr4rd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) / ( ! ` k ) ) = ( ( ( A ^ ( ( 0 + k ) - j ) ) / ( ! ` ( ( 0 + k ) - j ) ) ) x. ( G ` ( k - ( ( 0 + k ) - j ) ) ) ) )
122 121 sumeq2dv 
 |-  ( ( ph /\ k e. NN0 ) -> sum_ j e. ( 0 ... k ) ( ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) / ( ! ` k ) ) = sum_ j e. ( 0 ... k ) ( ( ( A ^ ( ( 0 + k ) - j ) ) / ( ! ` ( ( 0 + k ) - j ) ) ) x. ( G ` ( k - ( ( 0 + k ) - j ) ) ) ) )
123 oveq2 
 |-  ( j = m -> ( ( 0 + k ) - j ) = ( ( 0 + k ) - m ) )
124 123 oveq2d 
 |-  ( j = m -> ( A ^ ( ( 0 + k ) - j ) ) = ( A ^ ( ( 0 + k ) - m ) ) )
125 123 fveq2d 
 |-  ( j = m -> ( ! ` ( ( 0 + k ) - j ) ) = ( ! ` ( ( 0 + k ) - m ) ) )
126 124 125 oveq12d 
 |-  ( j = m -> ( ( A ^ ( ( 0 + k ) - j ) ) / ( ! ` ( ( 0 + k ) - j ) ) ) = ( ( A ^ ( ( 0 + k ) - m ) ) / ( ! ` ( ( 0 + k ) - m ) ) ) )
127 123 oveq2d 
 |-  ( j = m -> ( k - ( ( 0 + k ) - j ) ) = ( k - ( ( 0 + k ) - m ) ) )
128 127 fveq2d 
 |-  ( j = m -> ( G ` ( k - ( ( 0 + k ) - j ) ) ) = ( G ` ( k - ( ( 0 + k ) - m ) ) ) )
129 126 128 oveq12d 
 |-  ( j = m -> ( ( ( A ^ ( ( 0 + k ) - j ) ) / ( ! ` ( ( 0 + k ) - j ) ) ) x. ( G ` ( k - ( ( 0 + k ) - j ) ) ) ) = ( ( ( A ^ ( ( 0 + k ) - m ) ) / ( ! ` ( ( 0 + k ) - m ) ) ) x. ( G ` ( k - ( ( 0 + k ) - m ) ) ) ) )
130 129 cbvsumv 
 |-  sum_ j e. ( 0 ... k ) ( ( ( A ^ ( ( 0 + k ) - j ) ) / ( ! ` ( ( 0 + k ) - j ) ) ) x. ( G ` ( k - ( ( 0 + k ) - j ) ) ) ) = sum_ m e. ( 0 ... k ) ( ( ( A ^ ( ( 0 + k ) - m ) ) / ( ! ` ( ( 0 + k ) - m ) ) ) x. ( G ` ( k - ( ( 0 + k ) - m ) ) ) )
131 122 130 eqtrdi 
 |-  ( ( ph /\ k e. NN0 ) -> sum_ j e. ( 0 ... k ) ( ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) / ( ! ` k ) ) = sum_ m e. ( 0 ... k ) ( ( ( A ^ ( ( 0 + k ) - m ) ) / ( ! ` ( ( 0 + k ) - m ) ) ) x. ( G ` ( k - ( ( 0 + k ) - m ) ) ) ) )
132 84 131 eqtr4d 
 |-  ( ( ph /\ k e. NN0 ) -> sum_ j e. ( 0 ... k ) ( ( ( A ^ j ) / ( ! ` j ) ) x. ( G ` ( k - j ) ) ) = sum_ j e. ( 0 ... k ) ( ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) / ( ! ` k ) ) )
133 62 132 eqtr4d 
 |-  ( ( ph /\ k e. NN0 ) -> ( sum_ j e. ( 0 ... k ) ( ( k _C j ) x. ( ( A ^ ( k - j ) ) x. ( B ^ j ) ) ) / ( ! ` k ) ) = sum_ j e. ( 0 ... k ) ( ( ( A ^ j ) / ( ! ` j ) ) x. ( G ` ( k - j ) ) ) )
134 43 133 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( A + B ) ^ k ) / ( ! ` k ) ) = sum_ j e. ( 0 ... k ) ( ( ( A ^ j ) / ( ! ` j ) ) x. ( G ` ( k - j ) ) ) )
135 37 134 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( ( ( A ^ j ) / ( ! ` j ) ) x. ( G ` ( k - j ) ) ) )
136 4 abscld 
 |-  ( ph -> ( abs ` A ) e. RR )
137 136 recnd 
 |-  ( ph -> ( abs ` A ) e. CC )
138 26 efcllem 
 |-  ( ( abs ` A ) e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
139 137 138 syl 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
140 2 efcllem 
 |-  ( B e. CC -> seq 0 ( + , G ) e. dom ~~> )
141 5 140 syl 
 |-  ( ph -> seq 0 ( + , G ) e. dom ~~> )
142 10 29 31 33 35 135 139 141 mertens 
 |-  ( ph -> seq 0 ( + , H ) ~~> ( sum_ j e. NN0 ( ( A ^ j ) / ( ! ` j ) ) x. sum_ k e. NN0 ( ( B ^ k ) / ( ! ` k ) ) ) )
143 efval 
 |-  ( A e. CC -> ( exp ` A ) = sum_ j e. NN0 ( ( A ^ j ) / ( ! ` j ) ) )
144 4 143 syl 
 |-  ( ph -> ( exp ` A ) = sum_ j e. NN0 ( ( A ^ j ) / ( ! ` j ) ) )
145 efval 
 |-  ( B e. CC -> ( exp ` B ) = sum_ k e. NN0 ( ( B ^ k ) / ( ! ` k ) ) )
146 5 145 syl 
 |-  ( ph -> ( exp ` B ) = sum_ k e. NN0 ( ( B ^ k ) / ( ! ` k ) ) )
147 144 146 oveq12d 
 |-  ( ph -> ( ( exp ` A ) x. ( exp ` B ) ) = ( sum_ j e. NN0 ( ( A ^ j ) / ( ! ` j ) ) x. sum_ k e. NN0 ( ( B ^ k ) / ( ! ` k ) ) ) )
148 142 147 breqtrrd 
 |-  ( ph -> seq 0 ( + , H ) ~~> ( ( exp ` A ) x. ( exp ` B ) ) )
149 climuni 
 |-  ( ( seq 0 ( + , H ) ~~> ( exp ` ( A + B ) ) /\ seq 0 ( + , H ) ~~> ( ( exp ` A ) x. ( exp ` B ) ) ) -> ( exp ` ( A + B ) ) = ( ( exp ` A ) x. ( exp ` B ) ) )
150 8 148 149 syl2anc 
 |-  ( ph -> ( exp ` ( A + B ) ) = ( ( exp ` A ) x. ( exp ` B ) ) )