Proof of Theorem taylfvallem1
Step | Hyp | Ref
| Expression |
1 | | taylfval.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
2 | 1 | ad2antrr 764 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑆 ∈ {ℝ, ℂ}) |
3 | | cnex 10229 |
. . . . . . . 8
⊢ ℂ
∈ V |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈
V) |
5 | | taylfval.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
6 | | taylfval.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
7 | | elpm2r 8043 |
. . . . . . 7
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
8 | 4, 1, 5, 6, 7 | syl22anc 1478 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
9 | 8 | ad2antrr 764 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
10 | | inss2 3977 |
. . . . . . 7
⊢
((0[,]𝑁) ∩
ℤ) ⊆ ℤ |
11 | | simpr 479 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) |
12 | 10, 11 | sseldi 3742 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℤ) |
13 | | inss1 3976 |
. . . . . . . . 9
⊢
((0[,]𝑁) ∩
ℤ) ⊆ (0[,]𝑁) |
14 | 13, 11 | sseldi 3742 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ (0[,]𝑁)) |
15 | | 0xr 10298 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
16 | | taylfval.n |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) |
17 | | nn0re 11513 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
18 | 17 | rexrd 10301 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ*) |
19 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑁 = +∞ → 𝑁 = +∞) |
20 | | pnfxr 10304 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
21 | 19, 20 | syl6eqel 2847 |
. . . . . . . . . . . 12
⊢ (𝑁 = +∞ → 𝑁 ∈
ℝ*) |
22 | 18, 21 | jaoi 393 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 = +∞) → 𝑁 ∈
ℝ*) |
23 | 16, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
24 | 23 | ad2antrr 764 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑁 ∈
ℝ*) |
25 | | elicc1 12432 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 𝑁 ∈ ℝ*) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁))) |
26 | 15, 24, 25 | sylancr 698 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁))) |
27 | 14, 26 | mpbid 222 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁)) |
28 | 27 | simp2d 1138 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 0 ≤ 𝑘) |
29 | | elnn0z 11602 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℤ
∧ 0 ≤ 𝑘)) |
30 | 12, 28, 29 | sylanbrc 701 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℕ0) |
31 | | dvnf 23909 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
32 | 2, 9, 30, 31 | syl3anc 1477 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
33 | | taylfval.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
34 | 33 | adantlr 753 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
35 | 32, 34 | ffvelrnd 6524 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ) |
36 | | faccl 13284 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
37 | 30, 36 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈
ℕ) |
38 | 37 | nncnd 11248 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈
ℂ) |
39 | 37 | nnne0d 11277 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ≠ 0) |
40 | 35, 38, 39 | divcld 11013 |
. 2
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
41 | | simplr 809 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑋 ∈ ℂ) |
42 | | dvnbss 23910 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → dom
((𝑆 D𝑛
𝐹)‘𝑘) ⊆ dom 𝐹) |
43 | 2, 9, 30, 42 | syl3anc 1477 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → dom ((𝑆 D𝑛 𝐹)‘𝑘) ⊆ dom 𝐹) |
44 | 5 | ad2antrr 764 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐹:𝐴⟶ℂ) |
45 | | fdm 6212 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → dom 𝐹 = 𝐴) |
47 | 43, 46 | sseqtrd 3782 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → dom ((𝑆 D𝑛 𝐹)‘𝑘) ⊆ 𝐴) |
48 | | recnprss 23887 |
. . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
49 | 1, 48 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
50 | 6, 49 | sstrd 3754 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
51 | 50 | ad2antrr 764 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐴 ⊆ ℂ) |
52 | 47, 51 | sstrd 3754 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → dom ((𝑆 D𝑛 𝐹)‘𝑘) ⊆ ℂ) |
53 | 52, 34 | sseldd 3745 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ ℂ) |
54 | 41, 53 | subcld 10604 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑋 − 𝐵) ∈ ℂ) |
55 | 54, 30 | expcld 13222 |
. 2
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((𝑋 − 𝐵)↑𝑘) ∈ ℂ) |
56 | 40, 55 | mulcld 10272 |
1
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ) |