Step | Hyp | Ref
| Expression |
1 | | taylthlem1.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | elfz1end 12371 |
. . . 4
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁)) |
3 | 1, 2 | sylib 208 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
4 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (𝑁 − 𝑚) = (𝑁 − 1)) |
5 | 4 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) |
6 | 5 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥)) |
7 | 4 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 1))) |
8 | 7 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) |
9 | 6, 8 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑚 = 1 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) |
10 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑚 = 1 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑1)) |
11 | 9, 10 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑚 = 1 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) |
12 | 11 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)))) |
13 | 12 | oveq1d 6665 |
. . . . . 6
⊢ (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵)) |
14 | 13 | eleq2d 2687 |
. . . . 5
⊢ (𝑚 = 1 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵))) |
15 | 14 | imbi2d 330 |
. . . 4
⊢ (𝑚 = 1 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵)))) |
16 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑁 − 𝑚) = (𝑁 − 𝑛)) |
17 | 16 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))) |
18 | 17 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥)) |
19 | 16 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))) |
20 | 19 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) |
21 | 18, 20 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥))) |
22 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑛)) |
23 | 21, 22 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) |
24 | 23 | mpteq2dv 4745 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)))) |
25 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦)) |
26 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) |
27 | 25, 26 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦))) |
28 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 − 𝐵) = (𝑦 − 𝐵)) |
29 | 28 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 − 𝐵)↑𝑛) = ((𝑦 − 𝐵)↑𝑛)) |
30 | 27, 29 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) |
31 | 30 | cbvmptv 4750 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) |
32 | 24, 31 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))) |
33 | 32 | oveq1d 6665 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵)) |
34 | 33 | eleq2d 2687 |
. . . . 5
⊢ (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵))) |
35 | 34 | imbi2d 330 |
. . . 4
⊢ (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵)))) |
36 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝑁 − 𝑚) = (𝑁 − (𝑛 + 1))) |
37 | 36 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))) |
38 | 37 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥)) |
39 | 36 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))) |
40 | 39 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) |
41 | 38, 40 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))) |
42 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑(𝑛 + 1))) |
43 | 41, 42 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) |
44 | 43 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1))))) |
45 | 44 | oveq1d 6665 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)) |
46 | 45 | eleq2d 2687 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵))) |
47 | 46 | imbi2d 330 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)))) |
48 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑁 → (𝑁 − 𝑚) = (𝑁 − 𝑁)) |
49 | 48 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))) |
50 | 49 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥)) |
51 | 48 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑁 → ((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑁))) |
52 | 51 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) |
53 | 50, 52 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥))) |
54 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑁)) |
55 | 53, 54 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) |
56 | 55 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))) |
57 | 56 | oveq1d 6665 |
. . . . . 6
⊢ (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵)) |
58 | 57 | eleq2d 2687 |
. . . . 5
⊢ (𝑚 = 𝑁 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵))) |
59 | 58 | imbi2d 330 |
. . . 4
⊢ (𝑚 = 𝑁 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) limℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵)))) |
60 | | taylthlem1.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
61 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) |
62 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦) = (((ℂ D𝑛 𝑇)‘𝑁)‘𝐵)) |
63 | 61, 62 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵))) |
64 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) |
65 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵)) ∈ V |
66 | 63, 64, 65 | fvmpt 6282 |
. . . . . . . . . . . 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 11351 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
72 | | nn0uz 11722 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
73 | 71, 72 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
74 | | eluzfz2b 12350 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘0) ↔ 𝑁 ∈ (0...𝑁)) |
75 | 73, 74 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
76 | | taylthlem1.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) = 𝐴) |
77 | 60, 76 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
78 | | taylthlem1.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
79 | 68, 69, 70, 75, 77, 78 | dvntaylp0 24126 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) |
80 | 79 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵))) |
81 | | cnex 10017 |
. . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℂ ∈
V) |
83 | | elpm2r 7875 |
. . . . . . . . . . . . . . 15
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
84 | 82, 68, 69, 70, 83 | syl22anc 1327 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
85 | | dvnf 23690 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑁 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ) |
86 | 68, 84, 71, 85 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ) |
87 | 86, 77 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ) |
88 | 87 | subidd 10380 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D𝑛 𝐹)‘𝑁)‘𝐵)) = 0) |
89 | 67, 80, 88 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0) |
90 | | funmpt 5926 |
. . . . . . . . . . 11
⊢ Fun
(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) |
91 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)) ∈ V |
92 | 91, 64 | dmmpti 6023 |
. . . . . . . . . . . 12
⊢ dom
(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) = 𝐴 |
93 | 60, 92 | syl6eleqr 2712 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))) |
94 | | funbrfvb 6238 |
. . . . . . . . . . 11
⊢ ((Fun
(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) ∧ 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0)) |
95 | 90, 93, 94 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0)) |
96 | 89, 95 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0) |
97 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
98 | 1, 97 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
99 | | dvnf 23690 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0)
→ ((𝑆
D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 −
1))⟶ℂ) |
100 | 68, 84, 98, 99 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 −
1))⟶ℂ) |
101 | | dvnbss 23691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0)
→ dom ((𝑆
D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹) |
102 | 68, 84, 98, 101 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹) |
103 | | fdm 6051 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
104 | 69, 103 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐹 = 𝐴) |
105 | 102, 104 | sseqtrd 3641 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴) |
106 | | fzo0end 12560 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁)) |
107 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁)) |
108 | 1, 106, 107 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 1) ∈ (0...𝑁)) |
109 | | dvn2bss 23693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ (𝑁 − 1) ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) |
110 | 68, 84, 108, 109 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) |
111 | 76, 110 | eqsstr3d 3640 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) |
112 | 105, 111 | eqssd 3620 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = 𝐴) |
113 | 112 | feq2d 6031 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)) |
114 | 100, 113 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ) |
115 | 114 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ) |
116 | 76 | feq2d 6031 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘𝑁):dom ((𝑆 D𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ)) |
117 | 86, 116 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ) |
118 | 117 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ) |
119 | 1 | nncnd 11036 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℂ) |
120 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) |
121 | 119, 120 | npcand 10396 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
122 | 121 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
123 | | recnprss 23668 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
124 | 68, 123 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
125 | | dvnp1 23688 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ0)
→ ((𝑆
D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
126 | 124, 84, 98, 125 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
127 | 122, 126 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
128 | 117 | feqmptd 6249 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦))) |
129 | 114 | feqmptd 6249 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) |
130 | 129 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))) |
131 | 127, 128,
130 | 3eqtr3rd 2665 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦))) |
132 | 70, 124 | sstrd 3613 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
133 | 132 | sselda 3603 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ) |
134 | | 1nn0 11308 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℕ0) |
136 | | elpm2r 7875 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ
↑pm 𝑆)) |
137 | 82, 68, 114, 70, 136 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ
↑pm 𝑆)) |
138 | | dvn1 23689 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ
↑pm 𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
139 | 124, 137,
138 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))) |
140 | 126, 122 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
141 | 139, 140 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
142 | 141 | dmeqd 5326 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
143 | 77, 142 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))‘1)) |
144 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵) |
145 | 68, 114, 70, 135, 143, 144 | taylpf 24120 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ) |
146 | 120, 119 | pncan3d 10395 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 + (𝑁 − 1)) = 𝑁) |
147 | 146 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵)) |
148 | 147, 78 | syl6reqr 2675 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)) |
149 | 148 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℂ
D𝑛 𝑇) =
(ℂ D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))) |
150 | 149 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ
D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1))) |
151 | 146 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
152 | 151 | dmeqd 5326 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
153 | 77, 152 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(1 + (𝑁 − 1)))) |
154 | 68, 69, 70, 98, 135, 153 | dvntaylp 24125 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵)) |
155 | 150, 154 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵)) |
156 | 155 | feq1d 6030 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔
(1(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)) |
157 | 145, 156 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 −
1)):ℂ⟶ℂ) |
158 | 157 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ) |
159 | 133, 158 | syldan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ) |
160 | | 0nn0 11307 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℕ0 |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℕ0) |
162 | | elpm2r 7875 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm
𝑆)) |
163 | 82, 68, 117, 70, 162 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm
𝑆)) |
164 | | dvn0 23687 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝐹)‘𝑁) ∈ (ℂ ↑pm
𝑆)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
165 | 124, 163,
164 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
166 | 165 | dmeqd 5326 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
167 | 77, 166 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘𝑁))‘0)) |
168 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵) |
169 | 68, 117, 70, 161, 167, 168 | taylpf 24120 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ) |
170 | 119 | addid2d 10237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0 + 𝑁) = 𝑁) |
171 | 170 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵)) |
172 | 171, 78 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇) |
173 | 172 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℂ
D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D𝑛 𝑇)) |
174 | 173 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D𝑛 𝑇)‘𝑁)) |
175 | 170 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D𝑛 𝐹)‘𝑁)) |
176 | 175 | dmeqd 5326 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
177 | 77, 176 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(0 + 𝑁))) |
178 | 68, 69, 70, 71, 161, 177 | dvntaylp 24125 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℂ
D𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵)) |
179 | 174, 178 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵)) |
180 | 179 | feq1d 6030 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)) |
181 | 169, 180 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘𝑁):ℂ⟶ℂ) |
182 | 181 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ) |
183 | 133, 182 | syldan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦) ∈ ℂ) |
184 | 124 | sselda 3603 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
185 | 184, 158 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ) |
186 | 184, 182 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦) ∈ ℂ) |
187 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
188 | 187 | cnfldtopon 22586 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
189 | | toponmax 20730 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
190 | 188, 189 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℂ ∈
(TopOpen‘ℂfld)) |
191 | | df-ss 3588 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆) |
192 | 124, 191 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∩ ℂ) = 𝑆) |
193 | | ssid 3624 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
⊆ ℂ |
194 | 193 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℂ ⊆
ℂ) |
195 | | mapsspm 7891 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
↑𝑚 ℂ) ⊆ (ℂ ↑pm
ℂ) |
196 | 68, 69, 70, 71, 77, 78 | taylpf 24120 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇:ℂ⟶ℂ) |
197 | 81, 81 | elmap 7886 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ (ℂ
↑𝑚 ℂ) ↔ 𝑇:ℂ⟶ℂ) |
198 | 196, 197 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ∈ (ℂ ↑𝑚
ℂ)) |
199 | 195, 198 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑇 ∈ (ℂ ↑pm
ℂ)) |
200 | | dvnp1 23688 |
. . . . . . . . . . . . . . . 16
⊢ ((ℂ
⊆ ℂ ∧ 𝑇
∈ (ℂ ↑pm ℂ) ∧ (𝑁 − 1) ∈ ℕ0)
→ ((ℂ D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)))) |
201 | 194, 199,
98, 200 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)))) |
202 | 121 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ
D𝑛 𝑇)‘𝑁)) |
203 | 201, 202 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ
D𝑛 𝑇)‘𝑁)) |
204 | 157 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) |
205 | 204 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦
(((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) |
206 | 181 | feqmptd 6249 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘𝑁)‘𝑦))) |
207 | 203, 205,
206 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘𝑁)‘𝑦))) |
208 | 187, 68, 190, 192, 158, 182, 207 | dvmptres3 23719 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝑆 ↦ (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) |
209 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) |
210 | | resttopon 20965 |
. . . . . . . . . . . . . . . 16
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
211 | 188, 124,
210 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
212 | | topontop 20718 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
213 | 211, 212 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
214 | | toponuni 20719 |
. . . . . . . . . . . . . . . 16
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
215 | 211, 214 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
216 | 70, 215 | sseqtrd 3641 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
217 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ ∪ ((TopOpen‘ℂfld)
↾t 𝑆) =
∪ ((TopOpen‘ℂfld)
↾t 𝑆) |
218 | 217 | ntrss2 20861 |
. . . . . . . . . . . . . 14
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ 𝐴 ⊆ ∪ ((TopOpen‘ℂfld)
↾t 𝑆))
→ ((int‘((TopOpen‘ℂfld) ↾t
𝑆))‘𝐴) ⊆ 𝐴) |
219 | 213, 216,
218 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ⊆ 𝐴) |
220 | 140 | dmeqd 5326 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
221 | 220, 76 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) = 𝐴) |
222 | 124, 114,
70, 209, 187 | dvbssntr 23664 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑆 D ((𝑆 D𝑛 𝐹)‘(𝑁 − 1))) ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴)) |
223 | 221, 222 | eqsstr3d 3640 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴)) |
224 | 219, 223 | eqssd 3620 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) = 𝐴) |
225 | 68, 185, 186, 208, 70, 209, 187, 224 | dvmptres2 23725 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦))) |
226 | 68, 115, 118, 131, 159, 183, 225 | dvmptsub 23730 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))) |
227 | 226 | breqd 4664 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D𝑛
𝑇)‘𝑁)‘𝑦)))0)) |
228 | 96, 227 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → 𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))))0) |
229 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) |
230 | 115, 159 | subcld 10392 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ) |
231 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))) |
232 | 230, 231 | fmptd 6385 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ) |
233 | 209, 187,
229, 124, 232, 70 | eldv 23662 |
. . . . . . . 8
⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ (𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵)))) |
234 | 228, 233 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵))) |
235 | 234 | simprd 479 |
. . . . . 6
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵)) |
236 | | eldifi 3732 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴) |
237 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥)) |
238 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) |
239 | 237, 238 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) |
240 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V |
241 | 239, 231,
240 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) |
242 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) |
243 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) |
244 | 242, 243 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐵 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵))) |
245 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V |
246 | 244, 231,
245 | fvmpt 6282 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵))) |
247 | 60, 246 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵))) |
248 | 68, 69, 70, 108, 77, 78 | dvntaylp0 24126 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) |
249 | 248 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵))) |
250 | 114, 60 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ) |
251 | 250 | subidd 10380 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0) |
252 | 247, 249,
251 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0) |
253 | 241, 252 | oveqan12rd 6670 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) − 0)) |
254 | 114 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ) |
255 | 132 | sselda 3603 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) |
256 | 157 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ) |
257 | 255, 256 | syldan 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ) |
258 | 254, 257 | subcld 10392 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ) |
259 | 258 | subid1d 10381 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥))) |
260 | 253, 259 | eqtr2d 2657 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵))) |
261 | 236, 260 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵))) |
262 | 132 | ssdifssd 3748 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ) |
263 | 262 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ) |
264 | 132, 60 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℂ) |
265 | 264 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) |
266 | 263, 265 | subcld 10392 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ) |
267 | 266 | exp1d 13003 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑1) = (𝑥 − 𝐵)) |
268 | 261, 267 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)) = ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) |
269 | 268 | mpteq2dva 4744 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))) |
270 | 269 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) limℂ 𝐵)) |
271 | 235, 270 | eleqtrrd 2704 |
. . . . 5
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵)) |
272 | 271 | a1i 11 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) limℂ 𝐵))) |
273 | | taylthlem1.i |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (1..^𝑁) ∧ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵))) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)) |
274 | 273 | expr 643 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1..^𝑁)) → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵))) |
275 | 274 | expcom 451 |
. . . . 5
⊢ (𝑛 ∈ (1..^𝑁) → (𝜑 → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)))) |
276 | 275 | a2d 29 |
. . . 4
⊢ (𝑛 ∈ (1..^𝑁) → ((𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵)) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵)))) |
277 | 15, 35, 47, 59, 272, 276 | fzind2 12586 |
. . 3
⊢ (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵))) |
278 | 3, 277 | mpcom 38 |
. 2
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵)) |
279 | 119 | subidd 10380 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 𝑁) = 0) |
280 | 279 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁)) = ((𝑆 D𝑛 𝐹)‘0)) |
281 | | dvn0 23687 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) |
282 | 124, 84, 281 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) |
283 | 280, 282 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁)) = 𝐹) |
284 | 283 | fveq1d 6193 |
. . . . . . 7
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) = (𝐹‘𝑥)) |
285 | 279 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑁)) = ((ℂ D𝑛 𝑇)‘0)) |
286 | | dvn0 23687 |
. . . . . . . . . 10
⊢ ((ℂ
⊆ ℂ ∧ 𝑇
∈ (ℂ ↑pm ℂ)) → ((ℂ
D𝑛 𝑇)‘0) = 𝑇) |
287 | 193, 199,
286 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘0) = 𝑇) |
288 | 285, 287 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑁)) = 𝑇) |
289 | 288 | fveq1d 6193 |
. . . . . . 7
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥) = (𝑇‘𝑥)) |
290 | 284, 289 | oveq12d 6668 |
. . . . . 6
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) = ((𝐹‘𝑥) − (𝑇‘𝑥))) |
291 | 290 | oveq1d 6665 |
. . . . 5
⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)) = (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) |
292 | 291 | mpteq2dv 4745 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))) |
293 | | taylthlem1.r |
. . . 4
⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) |
294 | 292, 293 | syl6eqr 2674 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = 𝑅) |
295 | 294 | oveq1d 6665 |
. 2
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) limℂ 𝐵) = (𝑅 limℂ 𝐵)) |
296 | 278, 295 | eleqtrd 2703 |
1
⊢ (𝜑 → 0 ∈ (𝑅 limℂ 𝐵)) |