Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈ V |
2 | | eqid 2610 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
3 | 2 | cnfldtopon 22396 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
4 | 3 | toponunii 20547 |
. . . . . . 7
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
5 | 4 | restid 15917 |
. . . . . 6
⊢
((TopOpen‘ℂfld) ∈ V →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
6 | 1, 5 | ax-mp 5 |
. . . . 5
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
7 | 6 | eqcomi 2619 |
. . . 4
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
8 | | cnelprrecn 9908 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
10 | | toponmax 20543 |
. . . . 5
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
11 | 3, 10 | mp1i 13 |
. . . 4
⊢ (𝜑 → ℂ ∈
(TopOpen‘ℂfld)) |
12 | | fzfid 12634 |
. . . 4
⊢ (𝜑 → (0...(𝑁 + 1)) ∈ Fin) |
13 | | dvtaylp.s |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑆 ∈ {ℝ, ℂ}) |
15 | | cnex 9896 |
. . . . . . . . . . . 12
⊢ ℂ
∈ V |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ℂ ∈
V) |
17 | | dvtaylp.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
18 | | dvtaylp.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
19 | | elpm2r 7761 |
. . . . . . . . . . 11
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
20 | 16, 13, 17, 18, 19 | syl22anc 1319 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
21 | 20 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
22 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0) |
23 | 22 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
24 | | dvnf 23496 |
. . . . . . . . 9
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
25 | 14, 21, 23, 24 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
26 | | 0z 11265 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
27 | | dvtaylp.n |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
28 | | peano2nn0 11210 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
30 | 29 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
31 | | fzval2 12200 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℤ ∧ (𝑁 +
1) ∈ ℤ) → (0...(𝑁 + 1)) = ((0[,](𝑁 + 1)) ∩ ℤ)) |
32 | 26, 30, 31 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (0...(𝑁 + 1)) = ((0[,](𝑁 + 1)) ∩ ℤ)) |
33 | 32 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ (0...(𝑁 + 1)) ↔ 𝑘 ∈ ((0[,](𝑁 + 1)) ∩ ℤ))) |
34 | 33 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ((0[,](𝑁 + 1)) ∩ ℤ)) |
35 | | dvtaylp.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1))) |
36 | 13, 17, 18, 29, 35 | taylplem1 23921 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,](𝑁 + 1)) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
37 | 34, 36 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
38 | 25, 37 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ) |
39 | | faccl 12932 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
40 | 23, 39 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (!‘𝑘) ∈ ℕ) |
41 | 40 | nncnd 10913 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (!‘𝑘) ∈ ℂ) |
42 | 40 | nnne0d 10942 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (!‘𝑘) ≠ 0) |
43 | 38, 41, 42 | divcld 10680 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
44 | 43 | 3adant3 1074 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
45 | | simp3 1056 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
46 | | recnprss 23474 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
47 | 13, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
48 | 18, 47 | sstrd 3578 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
49 | | dvnbss 23497 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ (𝑁 + 1) ∈ ℕ0) → dom
((𝑆 D𝑛
𝐹)‘(𝑁 + 1)) ⊆ dom 𝐹) |
50 | 13, 20, 29, 49 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)) ⊆ dom 𝐹) |
51 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
52 | 17, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝐴) |
53 | 50, 52 | sseqtrd 3604 |
. . . . . . . . . 10
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)) ⊆ 𝐴) |
54 | 53, 35 | sseldd 3569 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
55 | 48, 54 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
56 | 55 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) |
57 | 45, 56 | subcld 10271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → (𝑥 − 𝐵) ∈ ℂ) |
58 | 22 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → 𝑘 ∈ ℕ0) |
59 | 57, 58 | expcld 12870 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → ((𝑥 − 𝐵)↑𝑘) ∈ ℂ) |
60 | 44, 59 | mulcld 9939 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)) ∈ ℂ) |
61 | | 0cnd 9912 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ 𝑘 = 0) → 0 ∈
ℂ) |
62 | 58 | nn0cnd 11230 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → 𝑘 ∈ ℂ) |
63 | 62 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℂ) |
64 | 57 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑥 − 𝐵) ∈ ℂ) |
65 | 58 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ0) |
66 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → ¬ 𝑘 = 0) |
67 | 66 | neqned 2789 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ≠ 0) |
68 | | elnnne0 11183 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0
∧ 𝑘 ≠
0)) |
69 | 65, 67, 68 | sylanbrc 695 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ) |
70 | | nnm1nn0 11211 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) |
71 | 69, 70 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 − 1) ∈
ℕ0) |
72 | 64, 71 | expcld 12870 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → ((𝑥 − 𝐵)↑(𝑘 − 1)) ∈ ℂ) |
73 | 63, 72 | mulcld 9939 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))) ∈
ℂ) |
74 | 61, 73 | ifclda 4070 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) ∈
ℂ) |
75 | 44, 74 | mulcld 9939 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) ∈
ℂ) |
76 | 8 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ℂ ∈ {ℝ,
ℂ}) |
77 | 59 | 3expa 1257 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → ((𝑥 − 𝐵)↑𝑘) ∈ ℂ) |
78 | 74 | 3expa 1257 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) ∈
ℂ) |
79 | 57 | 3expa 1257 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → (𝑥 − 𝐵) ∈ ℂ) |
80 | | 1cnd 9935 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → 1 ∈
ℂ) |
81 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) |
82 | 23 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑦 ∈ ℂ) → 𝑘 ∈ ℕ0) |
83 | 81, 82 | expcld 12870 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑦 ∈ ℂ) → (𝑦↑𝑘) ∈ ℂ) |
84 | | c0ex 9913 |
. . . . . . . . 9
⊢ 0 ∈
V |
85 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑘 · (𝑦↑(𝑘 − 1))) ∈ V |
86 | 84, 85 | ifex 4106 |
. . . . . . . 8
⊢ if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1)))) ∈ V |
87 | 86 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑦 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1)))) ∈ V) |
88 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
89 | 76 | dvmptid 23526 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1)) |
90 | 55 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) |
91 | | 0cnd 9912 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → 0 ∈
ℂ) |
92 | 55 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝐵 ∈ ℂ) |
93 | 76, 92 | dvmptc 23527 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ 𝐵)) = (𝑥 ∈ ℂ ↦ 0)) |
94 | 76, 88, 80, 89, 90, 91, 93 | dvmptsub 23536 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥 − 𝐵))) = (𝑥 ∈ ℂ ↦ (1 −
0))) |
95 | | 1m0e1 11008 |
. . . . . . . . 9
⊢ (1
− 0) = 1 |
96 | 95 | mpteq2i 4669 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ ↦ (1
− 0)) = (𝑥 ∈
ℂ ↦ 1) |
97 | 94, 96 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥 − 𝐵))) = (𝑥 ∈ ℂ ↦ 1)) |
98 | | dvexp2 23523 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1)))))) |
99 | 23, 98 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1)))))) |
100 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = (𝑥 − 𝐵) → (𝑦↑𝑘) = ((𝑥 − 𝐵)↑𝑘)) |
101 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥 − 𝐵) → (𝑦↑(𝑘 − 1)) = ((𝑥 − 𝐵)↑(𝑘 − 1))) |
102 | 101 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 − 𝐵) → (𝑘 · (𝑦↑(𝑘 − 1))) = (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) |
103 | 102 | ifeq2d 4055 |
. . . . . . 7
⊢ (𝑦 = (𝑥 − 𝐵) → if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1)))) = if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) |
104 | 76, 76, 79, 80, 83, 87, 97, 99, 100, 103 | dvmptco 23541 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ ((𝑥 − 𝐵)↑𝑘))) = (𝑥 ∈ ℂ ↦ (if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) · 1))) |
105 | 78 | mulid1d 9936 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → (if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) · 1) = if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) |
106 | 105 | mpteq2dva 4672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑥 ∈ ℂ ↦ (if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) · 1)) = (𝑥 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))))) |
107 | 104, 106 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ ((𝑥 − 𝐵)↑𝑘))) = (𝑥 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))))) |
108 | 76, 77, 78, 107, 43 | dvmptcmul 23533 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) = (𝑥 ∈ ℂ ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))))) |
109 | 7, 2, 9, 11, 12, 60, 75, 108 | dvmptfsum 23542 |
. . 3
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦
Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))))) |
110 | | 1zzd 11285 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 1 ∈
ℤ) |
111 | | 0zd 11266 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 0 ∈
ℤ) |
112 | 27 | nn0zd 11356 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℤ) |
113 | 112 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑁 ∈ ℤ) |
114 | | dvfg 23476 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
115 | 13, 114 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ) |
116 | 47, 17, 18 | dvbss 23471 |
. . . . . . . 8
⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝐴) |
117 | 116, 18 | sstrd 3578 |
. . . . . . 7
⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑆) |
118 | | 1nn0 11185 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
119 | 118 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℕ0) |
120 | | dvnadd 23498 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (1 ∈ ℕ0 ∧
𝑁 ∈
ℕ0)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(1 + 𝑁))) |
121 | 13, 20, 119, 27, 120 | syl22anc 1319 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(1 + 𝑁))) |
122 | | dvn1 23495 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹)) |
123 | 47, 20, 122 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹)) |
124 | 123 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1)) = (𝑆 D𝑛 (𝑆 D 𝐹))) |
125 | 124 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘𝑁) = ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑁)) |
126 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
127 | 27 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
128 | 126, 127 | addcomd 10117 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 + 𝑁) = (𝑁 + 1)) |
129 | 128 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(1 + 𝑁)) = ((𝑆 D𝑛 𝐹)‘(𝑁 + 1))) |
130 | 121, 125,
129 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑁 + 1))) |
131 | 130 | dmeqd 5248 |
. . . . . . . 8
⊢ (𝜑 → dom ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑁) = dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1))) |
132 | 35, 131 | eleqtrrd 2691 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑁)) |
133 | 13, 115, 117, 27, 132 | taylplem2 23922 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑗 ∈ (0...𝑁)) → (((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥 − 𝐵)↑𝑗)) ∈ ℂ) |
134 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑗 = (𝑘 − 1) → ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗) = ((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))) |
135 | 134 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 − 1) → (((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) = (((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵)) |
136 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 − 1) → (!‘𝑗) = (!‘(𝑘 − 1))) |
137 | 135, 136 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑗 = (𝑘 − 1) → ((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) = ((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1)))) |
138 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑗 = (𝑘 − 1) → ((𝑥 − 𝐵)↑𝑗) = ((𝑥 − 𝐵)↑(𝑘 − 1))) |
139 | 137, 138 | oveq12d 6567 |
. . . . . 6
⊢ (𝑗 = (𝑘 − 1) → (((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥 − 𝐵)↑𝑗)) = (((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥 − 𝐵)↑(𝑘 − 1)))) |
140 | 110, 111,
113, 133, 139 | fsumshft 14354 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥 − 𝐵)↑𝑗)) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥 − 𝐵)↑(𝑘 − 1)))) |
141 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ) |
142 | 141 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ ℕ) |
143 | 142 | nnne0d 10942 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ≠ 0) |
144 | | ifnefalse 4048 |
. . . . . . . . . 10
⊢ (𝑘 ≠ 0 → if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) = (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) |
145 | 143, 144 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) = (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) |
146 | 145 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) |
147 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝜑) |
148 | | 1eluzge0 11608 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(ℤ≥‘0) |
149 | | fzss1 12251 |
. . . . . . . . . . . . 13
⊢ (1 ∈
(ℤ≥‘0) → (1...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))) |
150 | 148, 149 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1...(𝑁 + 1))
⊆ (0...(𝑁 +
1)) |
151 | 150 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ (0...(𝑁 + 1))) |
152 | 151 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ (0...(𝑁 + 1))) |
153 | 147, 152,
43 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
154 | 142 | nncnd 10913 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ ℂ) |
155 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑥 ∈ ℂ) |
156 | 55 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐵 ∈ ℂ) |
157 | 155, 156 | subcld 10271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑥 − 𝐵) ∈ ℂ) |
158 | 142, 70 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑘 − 1) ∈
ℕ0) |
159 | 157, 158 | expcld 12870 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑥 − 𝐵)↑(𝑘 − 1)) ∈ ℂ) |
160 | 153, 154,
159 | mulassd 9942 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘) · ((𝑥 − 𝐵)↑(𝑘 − 1))) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) |
161 | | facp1 12927 |
. . . . . . . . . . . . 13
⊢ ((𝑘 − 1) ∈
ℕ0 → (!‘((𝑘 − 1) + 1)) = ((!‘(𝑘 − 1)) · ((𝑘 − 1) +
1))) |
162 | 158, 161 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘((𝑘 − 1) + 1)) = ((!‘(𝑘 − 1)) · ((𝑘 − 1) +
1))) |
163 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 1 ∈
ℂ) |
164 | 154, 163 | npcand 10275 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑘 − 1) + 1) = 𝑘) |
165 | 164 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘((𝑘 − 1) + 1)) = (!‘𝑘)) |
166 | 164 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((!‘(𝑘 − 1)) · ((𝑘 − 1) + 1)) = ((!‘(𝑘 − 1)) · 𝑘)) |
167 | 162, 165,
166 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘𝑘) = ((!‘(𝑘 − 1)) · 𝑘)) |
168 | 167 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / (!‘𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / ((!‘(𝑘 − 1)) · 𝑘))) |
169 | 23 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℂ) |
170 | 38, 169, 41, 42 | div23d 10717 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / (!‘𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘)) |
171 | 147, 152,
170 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / (!‘𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘)) |
172 | 147, 152,
38 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ) |
173 | | faccl 12932 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 − 1) ∈
ℕ0 → (!‘(𝑘 − 1)) ∈ ℕ) |
174 | 158, 173 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘(𝑘 − 1)) ∈ ℕ) |
175 | 174 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘(𝑘 − 1)) ∈ ℂ) |
176 | 174 | nnne0d 10942 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘(𝑘 − 1)) ≠ 0) |
177 | 172, 175,
154, 176, 143 | divcan5rd 10707 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / ((!‘(𝑘 − 1)) · 𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘(𝑘 − 1)))) |
178 | 13 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑆 ∈ {ℝ, ℂ}) |
179 | 20 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
180 | 118 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 1 ∈
ℕ0) |
181 | | dvnadd 23498 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)) ∧ (1 ∈ ℕ0 ∧
(𝑘 − 1) ∈
ℕ0)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘(𝑘 − 1)) = ((𝑆 D𝑛 𝐹)‘(1 + (𝑘 − 1)))) |
182 | 178, 179,
180, 158, 181 | syl22anc 1319 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘(𝑘 − 1)) = ((𝑆 D𝑛 𝐹)‘(1 + (𝑘 − 1)))) |
183 | 123 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹)) |
184 | 183 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1)) = (𝑆 D𝑛 (𝑆 D 𝐹))) |
185 | 184 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘(𝑘 − 1)) = ((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))) |
186 | 163, 154 | pncan3d 10274 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (1 + (𝑘 − 1)) = 𝑘) |
187 | 186 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 𝐹)‘(1 + (𝑘 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑘)) |
188 | 182, 185,
187 | 3eqtr3rd 2653 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))) |
189 | 188 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) = (((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵)) |
190 | 189 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘(𝑘 − 1))) = ((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1)))) |
191 | 177, 190 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / ((!‘(𝑘 − 1)) · 𝑘)) = ((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1)))) |
192 | 168, 171,
191 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘) = ((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1)))) |
193 | 192 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘) · ((𝑥 − 𝐵)↑(𝑘 − 1))) = (((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥 − 𝐵)↑(𝑘 − 1)))) |
194 | 146, 160,
193 | 3eqtr2d 2650 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) = (((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥 − 𝐵)↑(𝑘 − 1)))) |
195 | 194 | sumeq2dv 14281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) = Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥 − 𝐵)↑(𝑘 − 1)))) |
196 | | 0p1e1 11009 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
197 | 196 | oveq1i 6559 |
. . . . . . 7
⊢ ((0 +
1)...(𝑁 + 1)) = (1...(𝑁 + 1)) |
198 | 197 | sumeq1i 14276 |
. . . . . 6
⊢
Σ𝑘 ∈ ((0
+ 1)...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥 − 𝐵)↑(𝑘 − 1))) = Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥 − 𝐵)↑(𝑘 − 1))) |
199 | 195, 198 | syl6eqr 2662 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥 − 𝐵)↑(𝑘 − 1)))) |
200 | 150 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (1...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))) |
201 | 78 | an32s 842 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 + 1))) → if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) ∈
ℂ) |
202 | 151, 201 | sylan2 490 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) ∈
ℂ) |
203 | 153, 202 | mulcld 9939 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) ∈
ℂ) |
204 | | eldif 3550 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1))) ↔ (𝑘 ∈ (0...(𝑁 + 1)) ∧ ¬ 𝑘 ∈ (1...(𝑁 + 1)))) |
205 | 68 | biimpri 217 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑘 ≠ 0) →
𝑘 ∈
ℕ) |
206 | 22, 205 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑘 ≠ 0) → 𝑘 ∈ ℕ) |
207 | | nnuz 11599 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
208 | 206, 207 | syl6eleq 2698 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑘 ≠ 0) → 𝑘 ∈
(ℤ≥‘1)) |
209 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑁 + 1) ∈
(ℤ≥‘𝑘)) |
210 | 209 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑘 ≠ 0) → (𝑁 + 1) ∈
(ℤ≥‘𝑘)) |
211 | | elfzuzb 12207 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...(𝑁 + 1)) ↔ (𝑘 ∈ (ℤ≥‘1)
∧ (𝑁 + 1) ∈
(ℤ≥‘𝑘))) |
212 | 208, 210,
211 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑘 ≠ 0) → 𝑘 ∈ (1...(𝑁 + 1))) |
213 | 212 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 ≠ 0 → 𝑘 ∈ (1...(𝑁 + 1)))) |
214 | 213 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑘 ≠ 0 → 𝑘 ∈ (1...(𝑁 + 1)))) |
215 | 214 | necon1bd 2800 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (¬ 𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 = 0)) |
216 | 215 | impr 647 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑘 ∈ (0...(𝑁 + 1)) ∧ ¬ 𝑘 ∈ (1...(𝑁 + 1)))) → 𝑘 = 0) |
217 | 204, 216 | sylan2b 491 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → 𝑘 = 0) |
218 | 217 | iftrued 4044 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))) = 0) |
219 | 218 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0)) |
220 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1))) → 𝑘 ∈ (0...(𝑁 + 1))) |
221 | 43 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
222 | 220, 221 | sylan2 490 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
223 | 222 | mul01d 10114 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0) = 0) |
224 | 219, 223 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) = 0) |
225 | | fzfid 12634 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (0...(𝑁 + 1)) ∈
Fin) |
226 | 200, 203,
224, 225 | fsumss 14303 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))))) |
227 | 140, 199,
226 | 3eqtr2rd 2651 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1))))) = Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥 − 𝐵)↑𝑗))) |
228 | 227 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥 − 𝐵)↑(𝑘 − 1)))))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥 − 𝐵)↑𝑗)))) |
229 | 109, 228 | eqtrd 2644 |
. 2
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦
Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥 − 𝐵)↑𝑗)))) |
230 | | eqid 2610 |
. . . 4
⊢ ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵) = ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵) |
231 | 13, 17, 18, 29, 35, 230 | taylpfval 23923 |
. . 3
⊢ (𝜑 → ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵) = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
232 | 231 | oveq2d 6565 |
. 2
⊢ (𝜑 → (ℂ D ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) |
233 | | eqid 2610 |
. . 3
⊢ (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵) = (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵) |
234 | 13, 115, 117, 27, 132, 233 | taylpfval 23923 |
. 2
⊢ (𝜑 → (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥 − 𝐵)↑𝑗)))) |
235 | 229, 232,
234 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (ℂ D ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵)) = (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵)) |