Proof of Theorem taylfvallem1
Step | Hyp | Ref
| Expression |
1 | | taylfval.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
2 | 1 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑆 ∈ {ℝ, ℂ}) |
3 | | cnex 10017 |
. . . . . . . 8
⊢ ℂ
∈ V |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈
V) |
5 | | taylfval.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
6 | | taylfval.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
7 | | elpm2r 7875 |
. . . . . . 7
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
8 | 4, 1, 5, 6, 7 | syl22anc 1327 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
9 | 8 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
10 | | inss2 3834 |
. . . . . . 7
⊢
((0[,]𝑁) ∩
ℤ) ⊆ ℤ |
11 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) |
12 | 10, 11 | sseldi 3601 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℤ) |
13 | | inss1 3833 |
. . . . . . . . 9
⊢
((0[,]𝑁) ∩
ℤ) ⊆ (0[,]𝑁) |
14 | 13, 11 | sseldi 3601 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ (0[,]𝑁)) |
15 | | 0xr 10086 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
16 | | taylfval.n |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) |
17 | | nn0re 11301 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
18 | 17 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ*) |
19 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑁 = +∞ → 𝑁 = +∞) |
20 | | pnfxr 10092 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
21 | 19, 20 | syl6eqel 2709 |
. . . . . . . . . . . 12
⊢ (𝑁 = +∞ → 𝑁 ∈
ℝ*) |
22 | 18, 21 | jaoi 394 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 = +∞) → 𝑁 ∈
ℝ*) |
23 | 16, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
24 | 23 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑁 ∈
ℝ*) |
25 | | elicc1 12219 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 𝑁 ∈ ℝ*) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁))) |
26 | 15, 24, 25 | sylancr 695 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁))) |
27 | 14, 26 | mpbid 222 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁)) |
28 | 27 | simp2d 1074 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 0 ≤ 𝑘) |
29 | | elnn0z 11390 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℤ
∧ 0 ≤ 𝑘)) |
30 | 12, 28, 29 | sylanbrc 698 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℕ0) |
31 | | dvnf 23690 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
32 | 2, 9, 30, 31 | syl3anc 1326 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
33 | | taylfval.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
34 | 33 | adantlr 751 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
35 | 32, 34 | ffvelrnd 6360 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ) |
36 | | faccl 13070 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
37 | 30, 36 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈
ℕ) |
38 | 37 | nncnd 11036 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈
ℂ) |
39 | 37 | nnne0d 11065 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ≠ 0) |
40 | 35, 38, 39 | divcld 10801 |
. 2
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
41 | | simplr 792 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑋 ∈ ℂ) |
42 | | dvnbss 23691 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → dom
((𝑆 D𝑛
𝐹)‘𝑘) ⊆ dom 𝐹) |
43 | 2, 9, 30, 42 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → dom ((𝑆 D𝑛 𝐹)‘𝑘) ⊆ dom 𝐹) |
44 | 5 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐹:𝐴⟶ℂ) |
45 | | fdm 6051 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → dom 𝐹 = 𝐴) |
47 | 43, 46 | sseqtrd 3641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → dom ((𝑆 D𝑛 𝐹)‘𝑘) ⊆ 𝐴) |
48 | | recnprss 23668 |
. . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
49 | 1, 48 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
50 | 6, 49 | sstrd 3613 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
51 | 50 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐴 ⊆ ℂ) |
52 | 47, 51 | sstrd 3613 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → dom ((𝑆 D𝑛 𝐹)‘𝑘) ⊆ ℂ) |
53 | 52, 34 | sseldd 3604 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ ℂ) |
54 | 41, 53 | subcld 10392 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑋 − 𝐵) ∈ ℂ) |
55 | 54, 30 | expcld 13008 |
. 2
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((𝑋 − 𝐵)↑𝑘) ∈ ℂ) |
56 | 40, 55 | mulcld 10060 |
1
⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ) |