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 0 A n n !
efadd.2 G = n 0 B n n !
efadd.3 H = n 0 A + B n n !
efadd.4 φ A
efadd.5 φ B
Assertion efaddlem φ e A + B = e A e B

Proof

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