Step | Hyp | Ref
| Expression |
1 | | taylthlem1.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | elfz1end 13155 |
. . . 4
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁)) |
3 | 1, 2 | sylib 221 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
4 | | oveq2 7230 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (𝑁 − 𝑚) = (𝑁 − 1)) |
5 | 4 | fveq2d 6730 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) |
6 | 5 | fveq1d 6728 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥)) |
7 | 4 | fveq2d 6730 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 1))) |
8 | 7 | fveq1d 6728 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) |
9 | 6, 8 | oveq12d 7240 |
. . . . . . . . 9
⊢ (𝑚 = 1 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) |
10 | | oveq2 7230 |
. . . . . . . . 9
⊢ (𝑚 = 1 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑1)) |
11 | 9, 10 | oveq12d 7240 |
. . . . . . . 8
⊢ (𝑚 = 1 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) |
12 | 11 | mpteq2dv 5160 |
. . . . . . 7
⊢ (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)))) |
13 | 12 | oveq1d 7237 |
. . . . . 6
⊢ (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵)) |
14 | 13 | eleq2d 2824 |
. . . . 5
⊢ (𝑚 = 1 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵))) |
15 | 14 | imbi2d 344 |
. . . 4
⊢ (𝑚 = 1 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵)))) |
16 | | oveq2 7230 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑁 − 𝑚) = (𝑁 − 𝑛)) |
17 | 16 | fveq2d 6730 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))) |
18 | 17 | fveq1d 6728 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥)) |
19 | 16 | fveq2d 6730 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))) |
20 | 19 | fveq1d 6728 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) |
21 | 18, 20 | oveq12d 7240 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥))) |
22 | | oveq2 7230 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑛)) |
23 | 21, 22 | oveq12d 7240 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) |
24 | 23 | mpteq2dv 5160 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)))) |
25 | | fveq2 6726 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦)) |
26 | | fveq2 6726 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) |
27 | 25, 26 | oveq12d 7240 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦))) |
28 | | oveq1 7229 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 − 𝐵) = (𝑦 − 𝐵)) |
29 | 28 | oveq1d 7237 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 − 𝐵)↑𝑛) = ((𝑦 − 𝐵)↑𝑛)) |
30 | 27, 29 | oveq12d 7240 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) |
31 | 30 | cbvmptv 5167 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) |
32 | 24, 31 | eqtrdi 2795 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))) |
33 | 32 | oveq1d 7237 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵)) |
34 | 33 | eleq2d 2824 |
. . . . 5
⊢ (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵))) |
35 | 34 | imbi2d 344 |
. . . 4
⊢ (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵)))) |
36 | | oveq2 7230 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝑁 − 𝑚) = (𝑁 − (𝑛 + 1))) |
37 | 36 | fveq2d 6730 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))) |
38 | 37 | fveq1d 6728 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥)) |
39 | 36 | fveq2d 6730 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))) |
40 | 39 | fveq1d 6728 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) |
41 | 38, 40 | oveq12d 7240 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))) |
42 | | oveq2 7230 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑(𝑛 + 1))) |
43 | 41, 42 | oveq12d 7240 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) |
44 | 43 | mpteq2dv 5160 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1))))) |
45 | 44 | oveq1d 7237 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)) |
46 | 45 | eleq2d 2824 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵))) |
47 | 46 | imbi2d 344 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)))) |
48 | | oveq2 7230 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑁 → (𝑁 − 𝑚) = (𝑁 − 𝑁)) |
49 | 48 | fveq2d 6730 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))) |
50 | 49 | fveq1d 6728 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥)) |
51 | 48 | fveq2d 6730 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → ((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑁))) |
52 | 51 | fveq1d 6728 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) |
53 | 50, 52 | oveq12d 7240 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥))) |
54 | | oveq2 7230 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑁)) |
55 | 53, 54 | oveq12d 7240 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) |
56 | 55 | mpteq2dv 5160 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))) |
57 | 56 | oveq1d 7237 |
. . . . . 6
⊢ (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵)) |
58 | 57 | eleq2d 2824 |
. . . . 5
⊢ (𝑚 = 𝑁 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵))) |
59 | 58 | imbi2d 344 |
. . . 4
⊢ (𝑚 = 𝑁 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵)))) |
60 | | taylthlem1.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
61 | | fveq2 6726 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) |
62 | | fveq2 6726 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦) = (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)) |
63 | 61, 62 | oveq12d 7240 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵))) |
64 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) |
65 | | ovex 7255 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵)) ∈ V |
66 | 63, 64, 65 | fvmpt 6827 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵))) |
67 | 60, 66 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵))) |
68 | | taylthlem1.s |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
69 | | taylthlem1.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
70 | | taylthlem1.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
71 | 1 | nnnn0d 12163 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
72 | | nn0uz 12489 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
73 | 71, 72 | eleqtrdi 2849 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
74 | | eluzfz2b 13134 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘0) ↔ 𝑁 ∈ (0...𝑁)) |
75 | 73, 74 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
76 | | taylthlem1.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) = 𝐴) |
77 | 60, 76 | eleqtrrd 2842 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
78 | | taylthlem1.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
79 | 68, 69, 70, 75, 77, 78 | dvntaylp0 25277 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) |
80 | 79 | oveq2d 7238 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵))) |
81 | | cnex 10823 |
. . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℂ ∈
V) |
83 | | elpm2r 8535 |
. . . . . . . . . . . . . . 15
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
84 | 82, 68, 69, 70, 83 | syl22anc 839 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
85 | | dvnf 24837 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑁 ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ) |
86 | 68, 84, 71, 85 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ) |
87 | 86, 77 | ffvelrnd 6914 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ) |
88 | 87 | subidd 11190 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) = 0) |
89 | 67, 80, 88 | 3eqtrd 2782 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0) |
90 | | funmpt 6427 |
. . . . . . . . . . 11
⊢ Fun
(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) |
91 | | ovex 7255 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)) ∈ V |
92 | 91, 64 | dmmpti 6531 |
. . . . . . . . . . . 12
⊢ dom
(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) = 𝐴 |
93 | 60, 92 | eleqtrrdi 2850 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))) |
94 | | funbrfvb 6776 |
. . . . . . . . . . 11
⊢ ((Fun
(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) ∧ 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0)) |
95 | 90, 93, 94 | sylancr 590 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0)) |
96 | 89, 95 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0) |
97 | | nnm1nn0 12144 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
98 | 1, 97 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
99 | | dvnf 24837 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ (𝑁 − 1) ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 −
1))⟶ℂ) |
100 | 68, 84, 98, 99 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 −
1))⟶ℂ) |
101 | | dvnbss 24838 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ (𝑁 − 1) ∈
ℕ0) → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹) |
102 | 68, 84, 98, 101 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹) |
103 | 69, 102 | fssdmd 6573 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴) |
104 | | fzo0end 13347 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁)) |
105 | | elfzofz 13271 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁)) |
106 | 1, 104, 105 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 1) ∈ (0...𝑁)) |
107 | | dvn2bss 24840 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ (𝑁 − 1) ∈
(0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) |
108 | 68, 84, 106, 107 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) |
109 | 76, 108 | eqsstrrd 3949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) |
110 | 103, 109 | eqssd 3927 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = 𝐴) |
111 | 110 | feq2d 6540 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)) |
112 | 100, 111 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ) |
113 | 112 | ffvelrnda 6913 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ) |
114 | 76 | feq2d 6540 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ)) |
115 | 86, 114 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ) |
116 | 115 | ffvelrnda 6913 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ) |
117 | 1 | nncnd 11859 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℂ) |
118 | | 1cnd 10841 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) |
119 | 117, 118 | npcand 11206 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
120 | 119 | fveq2d 6730 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
121 | | recnprss 24814 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
122 | 68, 121 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
123 | | dvnp1 24835 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)
∧ (𝑁 − 1) ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
124 | 122, 84, 98, 123 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
125 | 120, 124 | eqtr3d 2780 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
126 | 115 | feqmptd 6789 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦))) |
127 | 112 | feqmptd 6789 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) |
128 | 127 | oveq2d 7238 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))) |
129 | 125, 126,
128 | 3eqtr3rd 2787 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦))) |
130 | 70, 122 | sstrd 3920 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
131 | 130 | sselda 3910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ) |
132 | | 1nn0 12119 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℕ0) |
134 | | elpm2r 8535 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ
↑pm 𝑆)) |
135 | 82, 68, 112, 70, 134 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ
↑pm 𝑆)) |
136 | | dvn1 24836 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ
↑pm 𝑆))
→ ((𝑆
D𝑛 ((𝑆
D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
137 | 122, 135,
136 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
138 | 124, 120 | eqtr3d 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
139 | 137, 138 | eqtrd 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
140 | 139 | dmeqd 5783 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
141 | 77, 140 | eleqtrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1)) |
142 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵) |
143 | 68, 112, 70, 133, 141, 142 | taylpf 25271 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ) |
144 | 118, 117 | pncan3d 11205 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 + (𝑁 − 1)) = 𝑁) |
145 | 144 | oveq1d 7237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵)) |
146 | 78, 145 | eqtr4id 2798 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)) |
147 | 146 | oveq2d 7238 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℂ
D𝑛 𝑇) =
(ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))) |
148 | 147 | fveq1d 6728 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ
D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1))) |
149 | 144 | fveq2d 6730 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
150 | 149 | dmeqd 5783 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
151 | 77, 150 | eleqtrrd 2842 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1)))) |
152 | 68, 69, 70, 98, 133, 151 | dvntaylp 25276 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵)) |
153 | 148, 152 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵)) |
154 | 153 | feq1d 6539 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔
(1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)) |
155 | 143, 154 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 −
1)):ℂ⟶ℂ) |
156 | 155 | ffvelrnda 6913 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ) |
157 | 131, 156 | syldan 594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ) |
158 | | 0nn0 12118 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℕ0 |
159 | 158 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℕ0) |
160 | | elpm2r 8535 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆)) |
161 | 82, 68, 115, 70, 160 | syl22anc 839 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆)) |
162 | | dvn0 24834 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
163 | 122, 161,
162 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
164 | 163 | dmeqd 5783 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
165 | 77, 164 | eleqtrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0)) |
166 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵) |
167 | 68, 115, 70, 159, 165, 166 | taylpf 25271 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ) |
168 | 117 | addid2d 11046 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0 + 𝑁) = 𝑁) |
169 | 168 | oveq1d 7237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵)) |
170 | 169, 78 | eqtr4di 2797 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇) |
171 | 170 | oveq2d 7238 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℂ
D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D𝑛 𝑇)) |
172 | 171 | fveq1d 6728 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D𝑛 𝑇)‘𝑁)) |
173 | 168 | fveq2d 6730 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
174 | 173 | dmeqd 5783 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
175 | 77, 174 | eleqtrrd 2842 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁))) |
176 | 68, 69, 70, 71, 159, 175 | dvntaylp 25276 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵)) |
177 | 172, 176 | eqtr3d 2780 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵)) |
178 | 177 | feq1d 6539 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)) |
179 | 167, 178 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘𝑁):ℂ⟶ℂ) |
180 | 179 | ffvelrnda 6913 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ) |
181 | 131, 180 | syldan 594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦) ∈ ℂ) |
182 | 122 | sselda 3910 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
183 | 182, 156 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ) |
184 | 182, 180 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦) ∈ ℂ) |
185 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
186 | 185 | cnfldtopon 23693 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
187 | | toponmax 21836 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
188 | 186, 187 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℂ ∈
(TopOpen‘ℂfld)) |
189 | | df-ss 3892 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆) |
190 | 122, 189 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∩ ℂ) = 𝑆) |
191 | | ssid 3932 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
⊆ ℂ |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℂ ⊆
ℂ) |
193 | | mapsspm 8566 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
↑m ℂ) ⊆ (ℂ ↑pm
ℂ) |
194 | 68, 69, 70, 71, 77, 78 | taylpf 25271 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇:ℂ⟶ℂ) |
195 | 81, 81 | elmap 8561 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ (ℂ
↑m ℂ) ↔ 𝑇:ℂ⟶ℂ) |
196 | 194, 195 | sylibr 237 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ∈ (ℂ ↑m
ℂ)) |
197 | 193, 196 | sselid 3907 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑇 ∈ (ℂ ↑pm
ℂ)) |
198 | | dvnp1 24835 |
. . . . . . . . . . . . . . . 16
⊢ ((ℂ
⊆ ℂ ∧ 𝑇
∈ (ℂ ↑pm ℂ) ∧ (𝑁 − 1) ∈ ℕ0)
→ ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)))) |
199 | 192, 197,
98, 198 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)))) |
200 | 119 | fveq2d 6730 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ
D𝑛 𝑇)‘𝑁)) |
201 | 199, 200 | eqtr3d 2780 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ
D𝑛 𝑇)‘𝑁)) |
202 | 155 | feqmptd 6789 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) |
203 | 202 | oveq2d 7238 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦
(((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) |
204 | 179 | feqmptd 6789 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘𝑁)‘𝑦))) |
205 | 201, 203,
204 | 3eqtr3d 2786 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘𝑁)‘𝑦))) |
206 | 185, 68, 188, 190, 156, 180, 205 | dvmptres3 24866 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝑆 ↦ (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) |
207 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) |
208 | | resttopon 22071 |
. . . . . . . . . . . . . . . 16
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
209 | 186, 122,
208 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
210 | | topontop 21823 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
211 | 209, 210 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
212 | | toponuni 21824 |
. . . . . . . . . . . . . . . 16
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
213 | 209, 212 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
214 | 70, 213 | sseqtrd 3950 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
215 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ ∪ ((TopOpen‘ℂfld)
↾t 𝑆) =
∪ ((TopOpen‘ℂfld)
↾t 𝑆) |
216 | 215 | ntrss2 21967 |
. . . . . . . . . . . . . 14
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝐴 ⊆ ∪ ((TopOpen‘ℂfld)
↾t 𝑆))
→ ((int‘((TopOpen‘ℂfld) ↾t
𝑆))‘𝐴) ⊆ 𝐴) |
217 | 211, 214,
216 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴) |
218 | 138 | dmeqd 5783 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
219 | 218, 76 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = 𝐴) |
220 | 122, 112,
70, 207, 185 | dvbssntr 24810 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴)) |
221 | 219, 220 | eqsstrrd 3949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴)) |
222 | 217, 221 | eqssd 3927 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) = 𝐴) |
223 | 68, 183, 184, 206, 70, 207, 185, 222 | dvmptres2 24872 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) |
224 | 68, 113, 116, 129, 157, 181, 223 | dvmptsub 24877 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))) |
225 | 224 | breqd 5073 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0)) |
226 | 96, 225 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → 𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))))0) |
227 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) |
228 | 113, 157 | subcld 11202 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ) |
229 | 228 | fmpttd 6941 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ) |
230 | 207, 185,
227, 122, 229, 70 | eldv 24808 |
. . . . . . . 8
⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ (𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵)))) |
231 | 226, 230 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵))) |
232 | 231 | simprd 499 |
. . . . . 6
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵)) |
233 | | eldifi 4050 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴) |
234 | | fveq2 6726 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥)) |
235 | | fveq2 6726 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) |
236 | 234, 235 | oveq12d 7240 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) |
237 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) |
238 | | ovex 7255 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V |
239 | 236, 237,
238 | fvmpt 6827 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) |
240 | | fveq2 6726 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) |
241 | | fveq2 6726 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) |
242 | 240, 241 | oveq12d 7240 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵))) |
243 | | ovex 7255 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V |
244 | 242, 237,
243 | fvmpt 6827 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵))) |
245 | 60, 244 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵))) |
246 | 68, 69, 70, 106, 77, 78 | dvntaylp0 25277 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) |
247 | 246 | oveq2d 7238 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵))) |
248 | 112, 60 | ffvelrnd 6914 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ) |
249 | 248 | subidd 11190 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0) |
250 | 245, 247,
249 | 3eqtrd 2782 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0) |
251 | 239, 250 | oveqan12rd 7242 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) − 0)) |
252 | 112 | ffvelrnda 6913 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ) |
253 | 130 | sselda 3910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) |
254 | 155 | ffvelrnda 6913 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ) |
255 | 253, 254 | syldan 594 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ) |
256 | 252, 255 | subcld 11202 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ) |
257 | 256 | subid1d 11191 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) |
258 | 251, 257 | eqtr2d 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵))) |
259 | 233, 258 | sylan2 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵))) |
260 | 130 | ssdifssd 4066 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ) |
261 | 260 | sselda 3910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ) |
262 | 130, 60 | sseldd 3911 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℂ) |
263 | 262 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) |
264 | 261, 263 | subcld 11202 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ) |
265 | 264 | exp1d 13724 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑1) = (𝑥 − 𝐵)) |
266 | 259, 265 | oveq12d 7240 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)) = ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) |
267 | 266 | mpteq2dva 5159 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))) |
268 | 267 | oveq1d 7237 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵)) |
269 | 232, 268 | eleqtrrd 2842 |
. . . . 5
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵)) |
270 | 269 | a1i 11 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵))) |
271 | | taylthlem1.i |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (1..^𝑁) ∧ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵))) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)) |
272 | 271 | expr 460 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1..^𝑁)) → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵))) |
273 | 272 | expcom 417 |
. . . . 5
⊢ (𝑛 ∈ (1..^𝑁) → (𝜑 → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)))) |
274 | 273 | a2d 29 |
. . . 4
⊢ (𝑛 ∈ (1..^𝑁) → ((𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵)) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)))) |
275 | 15, 35, 47, 59, 270, 274 | fzind2 13373 |
. . 3
⊢ (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵))) |
276 | 3, 275 | mpcom 38 |
. 2
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵)) |
277 | 117 | subidd 11190 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 𝑁) = 0) |
278 | 277 | fveq2d 6730 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁)) = ((𝑆 D𝑛 𝐹)‘0)) |
279 | | dvn0 24834 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ ((𝑆
D𝑛 𝐹)‘0) = 𝐹) |
280 | 122, 84, 279 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) |
281 | 278, 280 | eqtrd 2778 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁)) = 𝐹) |
282 | 281 | fveq1d 6728 |
. . . . . . 7
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) = (𝐹‘𝑥)) |
283 | 277 | fveq2d 6730 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑁)) = ((ℂ D𝑛 𝑇)‘0)) |
284 | | dvn0 24834 |
. . . . . . . . . 10
⊢ ((ℂ
⊆ ℂ ∧ 𝑇
∈ (ℂ ↑pm ℂ)) → ((ℂ
D𝑛 𝑇)‘0) = 𝑇) |
285 | 191, 197,
284 | sylancr 590 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘0) = 𝑇) |
286 | 283, 285 | eqtrd 2778 |
. . . . . . . 8
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑁)) = 𝑇) |
287 | 286 | fveq1d 6728 |
. . . . . . 7
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥) = (𝑇‘𝑥)) |
288 | 282, 287 | oveq12d 7240 |
. . . . . 6
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) = ((𝐹‘𝑥) − (𝑇‘𝑥))) |
289 | 288 | oveq1d 7237 |
. . . . 5
⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)) = (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) |
290 | 289 | mpteq2dv 5160 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))) |
291 | | taylthlem1.r |
. . . 4
⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) |
292 | 290, 291 | eqtr4di 2797 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = 𝑅) |
293 | 292 | oveq1d 7237 |
. 2
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵) = (𝑅 limℂ 𝐵)) |
294 | 276, 293 | eleqtrd 2841 |
1
⊢ (𝜑 → 0 ∈ (𝑅 limℂ 𝐵)) |