Metamath Proof Explorer

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

Ref Expression
Hypotheses efadd.1 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) )
efadd.2 𝐺 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐵𝑛 ) / ( ! ‘ 𝑛 ) ) )
efadd.3 𝐻 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
efadd.4 ( 𝜑𝐴 ∈ ℂ )
efadd.5 ( 𝜑𝐵 ∈ ℂ )
Assertion efaddlem ( 𝜑 → ( exp ‘ ( 𝐴 + 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ 𝐵 ) ) )

Proof

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