Step |
Hyp |
Ref |
Expression |
1 |
|
efsep.1 |
⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) |
2 |
|
efsep.2 |
⊢ 𝑁 = ( 𝑀 + 1 ) |
3 |
|
efsep.3 |
⊢ 𝑀 ∈ ℕ0 |
4 |
|
efsep.4 |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
5 |
|
efsep.5 |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
6 |
|
efsep.6 |
⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) ) |
7 |
|
efsep.7 |
⊢ ( 𝜑 → ( 𝐵 + ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) = 𝐷 ) |
8 |
|
eqid |
⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 ) |
9 |
3
|
nn0zi |
⊢ 𝑀 ∈ ℤ |
10 |
9
|
a1i |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
11 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
12 |
|
eluznn0 |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 ) |
13 |
3 12
|
mpan |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℕ0 ) |
14 |
1
|
eftval |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) |
15 |
14
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) |
16 |
|
eftcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ ) |
17 |
4 16
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ ) |
18 |
15 17
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
19 |
13 18
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
20 |
1
|
eftlcvg |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) |
21 |
4 3 20
|
sylancl |
⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) |
22 |
8 10 11 19 21
|
isum1p |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑀 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) ) |
23 |
1
|
eftval |
⊢ ( 𝑀 ∈ ℕ0 → ( 𝐹 ‘ 𝑀 ) = ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) |
24 |
3 23
|
ax-mp |
⊢ ( 𝐹 ‘ 𝑀 ) = ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) |
25 |
2
|
eqcomi |
⊢ ( 𝑀 + 1 ) = 𝑁 |
26 |
25
|
fveq2i |
⊢ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) = ( ℤ≥ ‘ 𝑁 ) |
27 |
26
|
sumeq1i |
⊢ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) |
28 |
24 27
|
oveq12i |
⊢ ( ( 𝐹 ‘ 𝑀 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) = ( ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) |
29 |
22 28
|
eqtrdi |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) = ( ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ) |
30 |
29
|
oveq2d |
⊢ ( 𝜑 → ( 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) = ( 𝐵 + ( ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ) ) |
31 |
|
eftcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℂ ) |
32 |
4 3 31
|
sylancl |
⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℂ ) |
33 |
|
peano2nn0 |
⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 ) |
34 |
3 33
|
ax-mp |
⊢ ( 𝑀 + 1 ) ∈ ℕ0 |
35 |
2 34
|
eqeltri |
⊢ 𝑁 ∈ ℕ0 |
36 |
1
|
eftlcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
37 |
4 35 36
|
sylancl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
38 |
5 32 37
|
addassd |
⊢ ( 𝜑 → ( ( 𝐵 + ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) = ( 𝐵 + ( ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ) ) |
39 |
30 38
|
eqtr4d |
⊢ ( 𝜑 → ( 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐵 + ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ) |
40 |
7
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐵 + ( ( 𝐴 ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) = ( 𝐷 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ) |
41 |
6 39 40
|
3eqtrd |
⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐷 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) ) |