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 addid2d
 |-  ( ( ( 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 ) ) )