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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ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 syl6eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ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 ‘ 𝐵 ) ) )