# Metamath Proof Explorer

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

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

### Proof

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