efaddlem

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

	Ref	Expression
Hypotheses	efadd.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
	efadd.2	$⊢ G = (n \in ℕ_{0} ⟼ \frac{B^{n}}{n!})$
	efadd.3	$⊢ H = (n \in ℕ_{0} ⟼ \frac{{(A + B)}^{n}}{n!})$
	efadd.4	$⊢ φ \to A \in ℂ$
	efadd.5	$⊢ φ \to B \in ℂ$
Assertion	efaddlem	$⊢ φ \to e^{A + B} = e^{A} e^{B}$

Proof

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

Metamath Proof Explorer

Theorem efaddlem

Proof