Step | Hyp | Ref
| Expression |
1 | | efadd.4 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) |
2 | | efadd.5 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℂ) |
3 | 1, 2 | addcld 10738 |
. . 3
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) |
4 | | efadd.3 |
. . . 4
⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛))) |
5 | 4 | efcvg 15530 |
. . 3
⊢ ((𝐴 + 𝐵) ∈ ℂ → seq0( + , 𝐻) ⇝ (exp‘(𝐴 + 𝐵))) |
6 | 3, 5 | syl 17 |
. 2
⊢ (𝜑 → seq0( + , 𝐻) ⇝ (exp‘(𝐴 + 𝐵))) |
7 | | efadd.1 |
. . . . . 6
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) |
8 | 7 | eftval 15522 |
. . . . 5
⊢ (𝑗 ∈ ℕ0
→ (𝐹‘𝑗) = ((𝐴↑𝑗) / (!‘𝑗))) |
9 | 8 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = ((𝐴↑𝑗) / (!‘𝑗))) |
10 | | absexp 14754 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (abs‘(𝐴↑𝑗)) = ((abs‘𝐴)↑𝑗)) |
11 | 1, 10 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘(𝐴↑𝑗)) = ((abs‘𝐴)↑𝑗)) |
12 | | faccl 13735 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ (!‘𝑗) ∈
ℕ) |
13 | 12 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘𝑗) ∈
ℕ) |
14 | | nnre 11723 |
. . . . . . . 8
⊢
((!‘𝑗) ∈
ℕ → (!‘𝑗)
∈ ℝ) |
15 | | nnnn0 11983 |
. . . . . . . . 9
⊢
((!‘𝑗) ∈
ℕ → (!‘𝑗)
∈ ℕ0) |
16 | 15 | nn0ge0d 12039 |
. . . . . . . 8
⊢
((!‘𝑗) ∈
ℕ → 0 ≤ (!‘𝑗)) |
17 | 14, 16 | absidd 14872 |
. . . . . . 7
⊢
((!‘𝑗) ∈
ℕ → (abs‘(!‘𝑗)) = (!‘𝑗)) |
18 | 13, 17 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘(!‘𝑗)) =
(!‘𝑗)) |
19 | 11, 18 | oveq12d 7188 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘(𝐴↑𝑗)) / (abs‘(!‘𝑗))) = (((abs‘𝐴)↑𝑗) / (!‘𝑗))) |
20 | | expcl 13539 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (𝐴↑𝑗) ∈
ℂ) |
21 | 1, 20 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑𝑗) ∈ ℂ) |
22 | 13 | nncnd 11732 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘𝑗) ∈
ℂ) |
23 | 13 | nnne0d 11766 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘𝑗) ≠
0) |
24 | 21, 22, 23 | absdivd 14905 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘((𝐴↑𝑗) / (!‘𝑗))) = ((abs‘(𝐴↑𝑗)) / (abs‘(!‘𝑗)))) |
25 | | eqid 2738 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦
(((abs‘𝐴)↑𝑛) / (!‘𝑛))) |
26 | 25 | eftval 15522 |
. . . . . 6
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))‘𝑗) = (((abs‘𝐴)↑𝑗) / (!‘𝑗))) |
27 | 26 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))‘𝑗) = (((abs‘𝐴)↑𝑗) / (!‘𝑗))) |
28 | 19, 24, 27 | 3eqtr4rd 2784 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))‘𝑗) = (abs‘((𝐴↑𝑗) / (!‘𝑗)))) |
29 | | eftcl 15519 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ ((𝐴↑𝑗) / (!‘𝑗)) ∈ ℂ) |
30 | 1, 29 | sylan 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴↑𝑗) / (!‘𝑗)) ∈ ℂ) |
31 | | efadd.2 |
. . . . . 6
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛))) |
32 | 31 | eftval 15522 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) = ((𝐵↑𝑘) / (!‘𝑘))) |
33 | 32 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = ((𝐵↑𝑘) / (!‘𝑘))) |
34 | | eftcl 15519 |
. . . . 5
⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐵↑𝑘) / (!‘𝑘)) ∈ ℂ) |
35 | 2, 34 | sylan 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐵↑𝑘) / (!‘𝑘)) ∈ ℂ) |
36 | 4 | eftval 15522 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝐻‘𝑘) = (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘))) |
37 | 36 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘))) |
38 | 1 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈
ℂ) |
39 | 2 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) |
40 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
41 | | binom 15278 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐴 + 𝐵)↑𝑘) = Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗)))) |
42 | 38, 39, 40, 41 | syl3anc 1372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑘) = Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗)))) |
43 | 42 | oveq1d 7185 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)) = (Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) / (!‘𝑘))) |
44 | | fzfid 13432 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
45 | | faccl 13735 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
46 | 45 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(!‘𝑘) ∈
ℕ) |
47 | 46 | nncnd 11732 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(!‘𝑘) ∈
ℂ) |
48 | | bccl2 13775 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0...𝑘) → (𝑘C𝑗) ∈ ℕ) |
49 | 48 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘C𝑗) ∈ ℕ) |
50 | 49 | nncnd 11732 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘C𝑗) ∈ ℂ) |
51 | 1 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐴 ∈ ℂ) |
52 | | fznn0sub 13030 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑘) → (𝑘 − 𝑗) ∈
ℕ0) |
53 | 52 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − 𝑗) ∈
ℕ0) |
54 | 51, 53 | expcld 13602 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴↑(𝑘 − 𝑗)) ∈ ℂ) |
55 | 2 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐵 ∈ ℂ) |
56 | | elfznn0 13091 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑘) → 𝑗 ∈ ℕ0) |
57 | 56 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝑗 ∈ ℕ0) |
58 | 55, 57 | expcld 13602 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐵↑𝑗) ∈ ℂ) |
59 | 54, 58 | mulcld 10739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗)) ∈ ℂ) |
60 | 50, 59 | mulcld 10739 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) ∈ ℂ) |
61 | 46 | nnne0d 11766 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(!‘𝑘) ≠
0) |
62 | 44, 47, 60, 61 | fsumdivc 15234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) / (!‘𝑘))) |
63 | 51, 57 | expcld 13602 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴↑𝑗) ∈ ℂ) |
64 | 57, 12 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑗) ∈ ℕ) |
65 | 64 | nncnd 11732 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑗) ∈ ℂ) |
66 | 64 | nnne0d 11766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑗) ≠ 0) |
67 | 63, 65, 66 | divcld 11494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐴↑𝑗) / (!‘𝑗)) ∈ ℂ) |
68 | 31 | eftval 15522 |
. . . . . . . . . . . 12
⊢ ((𝑘 − 𝑗) ∈ ℕ0 → (𝐺‘(𝑘 − 𝑗)) = ((𝐵↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗)))) |
69 | 53, 68 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘 − 𝑗)) = ((𝐵↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗)))) |
70 | 55, 53 | expcld 13602 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐵↑(𝑘 − 𝑗)) ∈ ℂ) |
71 | | faccl 13735 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 − 𝑗) ∈ ℕ0 →
(!‘(𝑘 − 𝑗)) ∈
ℕ) |
72 | 53, 71 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘(𝑘 − 𝑗)) ∈ ℕ) |
73 | 72 | nncnd 11732 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘(𝑘 − 𝑗)) ∈ ℂ) |
74 | 72 | nnne0d 11766 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘(𝑘 − 𝑗)) ≠ 0) |
75 | 70, 73, 74 | divcld 11494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐵↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗))) ∈ ℂ) |
76 | 69, 75 | eqeltrd 2833 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘 − 𝑗)) ∈ ℂ) |
77 | 67, 76 | mulcld 10739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑𝑗) / (!‘𝑗)) · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ) |
78 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝑗 = ((0 + 𝑘) − 𝑚) → (𝐴↑𝑗) = (𝐴↑((0 + 𝑘) − 𝑚))) |
79 | | fveq2 6674 |
. . . . . . . . . . 11
⊢ (𝑗 = ((0 + 𝑘) − 𝑚) → (!‘𝑗) = (!‘((0 + 𝑘) − 𝑚))) |
80 | 78, 79 | oveq12d 7188 |
. . . . . . . . . 10
⊢ (𝑗 = ((0 + 𝑘) − 𝑚) → ((𝐴↑𝑗) / (!‘𝑗)) = ((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚)))) |
81 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝑗 = ((0 + 𝑘) − 𝑚) → (𝑘 − 𝑗) = (𝑘 − ((0 + 𝑘) − 𝑚))) |
82 | 81 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑗 = ((0 + 𝑘) − 𝑚) → (𝐺‘(𝑘 − 𝑗)) = (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))) |
83 | 80, 82 | oveq12d 7188 |
. . . . . . . . 9
⊢ (𝑗 = ((0 + 𝑘) − 𝑚) → (((𝐴↑𝑗) / (!‘𝑗)) · (𝐺‘(𝑘 − 𝑗))) = (((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))) |
84 | 77, 83 | fsumrev2 15230 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
Σ𝑗 ∈ (0...𝑘)(((𝐴↑𝑗) / (!‘𝑗)) · (𝐺‘(𝑘 − 𝑗))) = Σ𝑚 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))) |
85 | 31 | eftval 15522 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
→ (𝐺‘𝑗) = ((𝐵↑𝑗) / (!‘𝑗))) |
86 | 57, 85 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘𝑗) = ((𝐵↑𝑗) / (!‘𝑗))) |
87 | 86 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗))) · (𝐺‘𝑗)) = (((𝐴↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗))) · ((𝐵↑𝑗) / (!‘𝑗)))) |
88 | 72, 64 | nnmulcld 11769 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘(𝑘 − 𝑗)) · (!‘𝑗)) ∈ ℕ) |
89 | 88 | nncnd 11732 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘(𝑘 − 𝑗)) · (!‘𝑗)) ∈ ℂ) |
90 | 88 | nnne0d 11766 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘(𝑘 − 𝑗)) · (!‘𝑗)) ≠ 0) |
91 | 59, 89, 90 | divrec2d 11498 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗)) / ((!‘(𝑘 − 𝑗)) · (!‘𝑗))) = ((1 / ((!‘(𝑘 − 𝑗)) · (!‘𝑗))) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗)))) |
92 | 54, 73, 58, 65, 74, 66 | divmuldivd 11535 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗))) · ((𝐵↑𝑗) / (!‘𝑗))) = (((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗)) / ((!‘(𝑘 − 𝑗)) · (!‘𝑗)))) |
93 | | bcval2 13757 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑘) → (𝑘C𝑗) = ((!‘𝑘) / ((!‘(𝑘 − 𝑗)) · (!‘𝑗)))) |
94 | 93 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘C𝑗) = ((!‘𝑘) / ((!‘(𝑘 − 𝑗)) · (!‘𝑗)))) |
95 | 94 | oveq1d 7185 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝑘C𝑗) / (!‘𝑘)) = (((!‘𝑘) / ((!‘(𝑘 − 𝑗)) · (!‘𝑗))) / (!‘𝑘))) |
96 | 47 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑘) ∈ ℂ) |
97 | 61 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘𝑘) ≠ 0) |
98 | 96, 89, 96, 90, 97 | divdiv32d 11519 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((!‘𝑘) / ((!‘(𝑘 − 𝑗)) · (!‘𝑗))) / (!‘𝑘)) = (((!‘𝑘) / (!‘𝑘)) / ((!‘(𝑘 − 𝑗)) · (!‘𝑗)))) |
99 | 96, 97 | dividd 11492 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((!‘𝑘) / (!‘𝑘)) = 1) |
100 | 99 | oveq1d 7185 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((!‘𝑘) / (!‘𝑘)) / ((!‘(𝑘 − 𝑗)) · (!‘𝑗))) = (1 / ((!‘(𝑘 − 𝑗)) · (!‘𝑗)))) |
101 | 98, 100 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((!‘𝑘) / ((!‘(𝑘 − 𝑗)) · (!‘𝑗))) / (!‘𝑘)) = (1 / ((!‘(𝑘 − 𝑗)) · (!‘𝑗)))) |
102 | 95, 101 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝑘C𝑗) / (!‘𝑘)) = (1 / ((!‘(𝑘 − 𝑗)) · (!‘𝑗)))) |
103 | 102 | oveq1d 7185 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) = ((1 / ((!‘(𝑘 − 𝑗)) · (!‘𝑗))) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗)))) |
104 | 91, 92, 103 | 3eqtr4rd 2784 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) = (((𝐴↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗))) · ((𝐵↑𝑗) / (!‘𝑗)))) |
105 | 87, 104 | eqtr4d 2776 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗))) · (𝐺‘𝑗)) = (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗)))) |
106 | | nn0cn 11986 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
107 | 106 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝑘 ∈ ℂ) |
108 | 107 | addid2d 10919 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (0 + 𝑘) = 𝑘) |
109 | 108 | oveq1d 7185 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((0 + 𝑘) − 𝑗) = (𝑘 − 𝑗)) |
110 | 109 | oveq2d 7186 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴↑((0 + 𝑘) − 𝑗)) = (𝐴↑(𝑘 − 𝑗))) |
111 | 109 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (!‘((0 + 𝑘) − 𝑗)) = (!‘(𝑘 − 𝑗))) |
112 | 110, 111 | oveq12d 7188 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) = ((𝐴↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗)))) |
113 | 109 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − ((0 + 𝑘) − 𝑗)) = (𝑘 − (𝑘 − 𝑗))) |
114 | | nn0cn 11986 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℂ) |
115 | 57, 114 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝑗 ∈ ℂ) |
116 | 107, 115 | nncand 11080 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − (𝑘 − 𝑗)) = 𝑗) |
117 | 113, 116 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − ((0 + 𝑘) − 𝑗)) = 𝑗) |
118 | 117 | fveq2d 6678 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗))) = (𝐺‘𝑗)) |
119 | 112, 118 | oveq12d 7188 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))) = (((𝐴↑(𝑘 − 𝑗)) / (!‘(𝑘 − 𝑗))) · (𝐺‘𝑗))) |
120 | 50, 59, 96, 97 | div23d 11531 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) / (!‘𝑘)) = (((𝑘C𝑗) / (!‘𝑘)) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗)))) |
121 | 105, 119,
120 | 3eqtr4rd 2784 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) / (!‘𝑘)) = (((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗))))) |
122 | 121 | sumeq2dv 15153 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗))))) |
123 | | oveq2 7178 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑚 → ((0 + 𝑘) − 𝑗) = ((0 + 𝑘) − 𝑚)) |
124 | 123 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑚 → (𝐴↑((0 + 𝑘) − 𝑗)) = (𝐴↑((0 + 𝑘) − 𝑚))) |
125 | 123 | fveq2d 6678 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑚 → (!‘((0 + 𝑘) − 𝑗)) = (!‘((0 + 𝑘) − 𝑚))) |
126 | 124, 125 | oveq12d 7188 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑚 → ((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) = ((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚)))) |
127 | 123 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑚 → (𝑘 − ((0 + 𝑘) − 𝑗)) = (𝑘 − ((0 + 𝑘) − 𝑚))) |
128 | 127 | fveq2d 6678 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑚 → (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗))) = (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))) |
129 | 126, 128 | oveq12d 7188 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑚 → (((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))) = (((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))) |
130 | 129 | cbvsumv 15146 |
. . . . . . . . 9
⊢
Σ𝑗 ∈
(0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑗)) / (!‘((0 + 𝑘) − 𝑗))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑗)))) = Σ𝑚 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚)))) |
131 | 122, 130 | eqtrdi 2789 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) / (!‘𝑘)) = Σ𝑚 ∈ (0...𝑘)(((𝐴↑((0 + 𝑘) − 𝑚)) / (!‘((0 + 𝑘) − 𝑚))) · (𝐺‘(𝑘 − ((0 + 𝑘) − 𝑚))))) |
132 | 84, 131 | eqtr4d 2776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
Σ𝑗 ∈ (0...𝑘)(((𝐴↑𝑗) / (!‘𝑗)) · (𝐺‘(𝑘 − 𝑗))) = Σ𝑗 ∈ (0...𝑘)(((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) / (!‘𝑘))) |
133 | 62, 132 | eqtr4d 2776 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(Σ𝑗 ∈ (0...𝑘)((𝑘C𝑗) · ((𝐴↑(𝑘 − 𝑗)) · (𝐵↑𝑗))) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝐴↑𝑗) / (!‘𝑗)) · (𝐺‘(𝑘 − 𝑗)))) |
134 | 43, 133 | eqtrd 2773 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐴 + 𝐵)↑𝑘) / (!‘𝑘)) = Σ𝑗 ∈ (0...𝑘)(((𝐴↑𝑗) / (!‘𝑗)) · (𝐺‘(𝑘 − 𝑗)))) |
135 | 37, 134 | eqtrd 2773 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(((𝐴↑𝑗) / (!‘𝑗)) · (𝐺‘(𝑘 − 𝑗)))) |
136 | 1 | abscld 14886 |
. . . . . 6
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) |
137 | 136 | recnd 10747 |
. . . . 5
⊢ (𝜑 → (abs‘𝐴) ∈
ℂ) |
138 | 25 | efcllem 15523 |
. . . . 5
⊢
((abs‘𝐴)
∈ ℂ → seq0( + , (𝑛 ∈ ℕ0 ↦
(((abs‘𝐴)↑𝑛) / (!‘𝑛)))) ∈ dom ⇝ ) |
139 | 137, 138 | syl 17 |
. . . 4
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))) ∈ dom ⇝ ) |
140 | 31 | efcllem 15523 |
. . . . 5
⊢ (𝐵 ∈ ℂ → seq0( + ,
𝐺) ∈ dom ⇝
) |
141 | 2, 140 | syl 17 |
. . . 4
⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝
) |
142 | 9, 28, 30, 33, 35, 135, 139, 141 | mertens 15334 |
. . 3
⊢ (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0
((𝐴↑𝑗) / (!‘𝑗)) · Σ𝑘 ∈ ℕ0 ((𝐵↑𝑘) / (!‘𝑘)))) |
143 | | efval 15525 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) =
Σ𝑗 ∈
ℕ0 ((𝐴↑𝑗) / (!‘𝑗))) |
144 | 1, 143 | syl 17 |
. . . 4
⊢ (𝜑 → (exp‘𝐴) = Σ𝑗 ∈ ℕ0 ((𝐴↑𝑗) / (!‘𝑗))) |
145 | | efval 15525 |
. . . . 5
⊢ (𝐵 ∈ ℂ →
(exp‘𝐵) =
Σ𝑘 ∈
ℕ0 ((𝐵↑𝑘) / (!‘𝑘))) |
146 | 2, 145 | syl 17 |
. . . 4
⊢ (𝜑 → (exp‘𝐵) = Σ𝑘 ∈ ℕ0 ((𝐵↑𝑘) / (!‘𝑘))) |
147 | 144, 146 | oveq12d 7188 |
. . 3
⊢ (𝜑 → ((exp‘𝐴) · (exp‘𝐵)) = (Σ𝑗 ∈ ℕ0 ((𝐴↑𝑗) / (!‘𝑗)) · Σ𝑘 ∈ ℕ0 ((𝐵↑𝑘) / (!‘𝑘)))) |
148 | 142, 147 | breqtrrd 5058 |
. 2
⊢ (𝜑 → seq0( + , 𝐻) ⇝ ((exp‘𝐴) · (exp‘𝐵))) |
149 | | climuni 14999 |
. 2
⊢ ((seq0( +
, 𝐻) ⇝
(exp‘(𝐴 + 𝐵)) ∧ seq0( + , 𝐻) ⇝ ((exp‘𝐴) · (exp‘𝐵))) → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵))) |
150 | 6, 148, 149 | syl2anc 587 |
1
⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵))) |