Step | Hyp | Ref
| Expression |
1 | | taylth.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
2 | | taylth.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
3 | | 1eluzge0 11608 |
. . . . . . . . . . . 12
⊢ 1 ∈
(ℤ≥‘0) |
4 | | fzss1 12251 |
. . . . . . . . . . . 12
⊢ (1 ∈
(ℤ≥‘0) → (1...𝑁) ⊆ (0...𝑁)) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
(0...𝑁) |
6 | | taylthlem2.m |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ (1..^𝑁)) |
7 | | fzofzp1 12431 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ (1..^𝑁) → (𝑀 + 1) ∈ (1...𝑁)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁)) |
9 | 5, 8 | sseldi 3566 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 1) ∈ (0...𝑁)) |
10 | | fznn0sub2 12315 |
. . . . . . . . . 10
⊢ ((𝑀 + 1) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁)) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁)) |
12 | | elfznn0 12302 |
. . . . . . . . 9
⊢ ((𝑁 − (𝑀 + 1)) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈
ℕ0) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − (𝑀 + 1)) ∈
ℕ0) |
14 | | dvnfre 23521 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) →
((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ) |
15 | 2, 1, 13, 14 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ) |
16 | | reelprrecn 9907 |
. . . . . . . . . . . 12
⊢ ℝ
∈ {ℝ, ℂ} |
17 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
18 | | cnex 9896 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ V |
19 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ∈
V) |
20 | | reex 9906 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
21 | 20 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈
V) |
22 | | ax-resscn 9872 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
23 | | fss 5969 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝐴⟶ℂ) |
24 | 2, 22, 23 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
25 | | elpm2r 7761 |
. . . . . . . . . . . 12
⊢
(((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
26 | 19, 21, 24, 1, 25 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
27 | | dvnbss 23497 |
. . . . . . . . . . 11
⊢ ((ℝ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℝ) ∧ (𝑁 −
(𝑀 + 1)) ∈
ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹) |
28 | 17, 26, 13, 27 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹) |
29 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴) |
30 | 2, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝐴) |
31 | 28, 30 | sseqtrd 3604 |
. . . . . . . . 9
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ 𝐴) |
32 | | taylth.d |
. . . . . . . . . 10
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘𝑁) = 𝐴) |
33 | | dvn2bss 23499 |
. . . . . . . . . . 11
⊢ ((ℝ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℝ) ∧ (𝑁 −
(𝑀 + 1)) ∈ (0...𝑁)) → dom ((ℝ
D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) |
34 | 17, 26, 11, 33 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) |
35 | 32, 34 | eqsstr3d 3603 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ dom ((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))) |
36 | 31, 35 | eqssd 3585 |
. . . . . . . 8
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = 𝐴) |
37 | 36 | feq2d 5944 |
. . . . . . 7
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ ↔ ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ)) |
38 | 15, 37 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ) |
39 | 38 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ) |
40 | 1 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
41 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ →
((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) |
42 | 41 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) |
43 | | resubdrg 19773 |
. . . . . . . . . . . 12
⊢ (ℝ
∈ (SubRing‘ℂfld) ∧ ℝfld ∈
DivRing) |
44 | 43 | simpli 473 |
. . . . . . . . . . 11
⊢ ℝ
∈ (SubRing‘ℂfld) |
45 | 44 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈
(SubRing‘ℂfld)) |
46 | | taylth.n |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) |
47 | 46 | nnnn0d 11228 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
48 | | taylth.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
49 | 48, 32 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ dom ((ℝ D𝑛
𝐹)‘𝑁)) |
50 | | taylth.t |
. . . . . . . . . . . 12
⊢ 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵) |
51 | 1, 48 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) |
52 | 2 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐹:𝐴⟶ℝ) |
53 | 1 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ⊆ ℝ) |
54 | | elfznn0 12302 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
55 | 54 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
56 | | dvnfre 23521 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑘 ∈ ℕ0) → ((ℝ
D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ) |
57 | 52, 53, 55, 56 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((ℝ D𝑛
𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ) |
58 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ℝ ∈ {ℝ,
ℂ}) |
59 | 26 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
60 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁)) |
61 | | dvn2bss 23499 |
. . . . . . . . . . . . . . . 16
⊢ ((ℝ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℝ) ∧ 𝑘 ∈
(0...𝑁)) → dom
((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ
D𝑛 𝐹)‘𝑘)) |
62 | 58, 59, 60, 61 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ
D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ
D𝑛 𝐹)‘𝑘)) |
63 | 49 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛
𝐹)‘𝑁)) |
64 | 62, 63 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛
𝐹)‘𝑘)) |
65 | 57, 64 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((ℝ D𝑛
𝐹)‘𝑘)‘𝐵) ∈ ℝ) |
66 | | faccl 12932 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
67 | 55, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
68 | 65, 67 | nndivred 10946 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((ℝ D𝑛
𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℝ) |
69 | 17, 24, 1, 47, 49, 50, 45, 51, 68 | taylply2 23926 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ∈ (Poly‘ℝ) ∧
(deg‘𝑇) ≤ 𝑁)) |
70 | 69 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈
(Poly‘ℝ)) |
71 | | dvnply2 23846 |
. . . . . . . . . 10
⊢ ((ℝ
∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) →
((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈
(Poly‘ℝ)) |
72 | 45, 70, 13, 71 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈
(Poly‘ℝ)) |
73 | | plyreres 23842 |
. . . . . . . . 9
⊢
(((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) →
(((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾
ℝ):ℝ⟶ℝ) |
74 | 72, 73 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾
ℝ):ℝ⟶ℝ) |
75 | 74 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) ∈
ℝ) |
76 | 42, 75 | eqeltrrd 2689 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ) |
77 | 40, 76 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ) |
78 | 39, 77 | resubcld 10337 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ ℝ) |
79 | | eqid 2610 |
. . . 4
⊢ (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) |
80 | 78, 79 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))):𝐴⟶ℝ) |
81 | 51 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ) |
82 | 40, 81 | resubcld 10337 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 − 𝐵) ∈ ℝ) |
83 | | elfzouz 12343 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (1..^𝑁) → 𝑀 ∈
(ℤ≥‘1)) |
84 | 6, 83 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
85 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
86 | 84, 85 | syl6eleqr 2699 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
87 | 86 | nnnn0d 11228 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
88 | 87 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑀 ∈
ℕ0) |
89 | | 1nn0 11185 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
90 | 89 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 1 ∈
ℕ0) |
91 | 88, 90 | nn0addcld 11232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑀 + 1) ∈
ℕ0) |
92 | 82, 91 | reexpcld 12887 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℝ) |
93 | | eqid 2610 |
. . . 4
⊢ (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) = (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) |
94 | 92, 93 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℝ) |
95 | | retop 22375 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ Top |
96 | | uniretop 22376 |
. . . . . . 7
⊢ ℝ =
∪ (topGen‘ran (,)) |
97 | 96 | ntrss2 20671 |
. . . . . 6
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) →
((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴) |
98 | 95, 1, 97 | sylancr 694 |
. . . . 5
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴) |
99 | 46 | nncnd 10913 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
100 | 86 | nncnd 10913 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℂ) |
101 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) |
102 | 99, 100, 101 | nppcan2d 10297 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − (𝑀 + 1)) + 1) = (𝑁 − 𝑀)) |
103 | 102 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))) |
104 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
105 | | dvnp1 23494 |
. . . . . . . . . 10
⊢ ((ℝ
⊆ ℂ ∧ 𝐹
∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) →
((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))) |
106 | 104, 26, 13, 105 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))) |
107 | 103, 106 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)) = (ℝ D ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))) |
108 | 107 | dmeqd 5248 |
. . . . . . 7
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)) = dom (ℝ D ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))) |
109 | | fzonnsub 12362 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ (1..^𝑁) → (𝑁 − 𝑀) ∈ ℕ) |
110 | 6, 109 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ) |
111 | 110 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 𝑀) ∈
ℕ0) |
112 | | dvnbss 23497 |
. . . . . . . . . 10
⊢ ((ℝ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℝ) ∧ (𝑁 −
𝑀) ∈
ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ dom 𝐹) |
113 | 17, 26, 111, 112 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ dom 𝐹) |
114 | 113, 30 | sseqtrd 3604 |
. . . . . . . 8
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ 𝐴) |
115 | | elfzofz 12354 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (1...𝑁)) |
116 | 6, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ (1...𝑁)) |
117 | 5, 116 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (0...𝑁)) |
118 | | fznn0sub2 12315 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (0...𝑁) → (𝑁 − 𝑀) ∈ (0...𝑁)) |
119 | 117, 118 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 𝑀) ∈ (0...𝑁)) |
120 | | dvn2bss 23499 |
. . . . . . . . . 10
⊢ ((ℝ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℝ) ∧ (𝑁 −
𝑀) ∈ (0...𝑁)) → dom ((ℝ
D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))) |
121 | 17, 26, 119, 120 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))) |
122 | 32, 121 | eqsstr3d 3603 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ dom ((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))) |
123 | 114, 122 | eqssd 3585 |
. . . . . . 7
⊢ (𝜑 → dom ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)) = 𝐴) |
124 | 108, 123 | eqtr3d 2646 |
. . . . . 6
⊢ (𝜑 → dom (ℝ D ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴) |
125 | | fss 5969 |
. . . . . . . 8
⊢
((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ) |
126 | 38, 22, 125 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ) |
127 | | eqid 2610 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
128 | 127 | tgioo2 22414 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
129 | 104, 126,
1, 128, 127 | dvbssntr 23470 |
. . . . . 6
⊢ (𝜑 → dom (ℝ D ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) ⊆
((int‘(topGen‘ran (,)))‘𝐴)) |
130 | 124, 129 | eqsstr3d 3603 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ((int‘(topGen‘ran
(,)))‘𝐴)) |
131 | 98, 130 | eqssd 3585 |
. . . 4
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘𝐴) = 𝐴) |
132 | 96 | isopn3 20680 |
. . . . 5
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)) |
133 | 95, 1, 132 | sylancr 694 |
. . . 4
⊢ (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)) |
134 | 131, 133 | mpbird 246 |
. . 3
⊢ (𝜑 → 𝐴 ∈ (topGen‘ran
(,))) |
135 | | eqid 2610 |
. . 3
⊢ (𝐴 ∖ {𝐵}) = (𝐴 ∖ {𝐵}) |
136 | | difss 3699 |
. . . 4
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 |
137 | 39 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ) |
138 | | dvnf 23496 |
. . . . . . . . . 10
⊢ ((ℝ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℝ) ∧ (𝑁 −
𝑀) ∈
ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ) |
139 | 17, 26, 111, 138 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ) |
140 | 123 | feq2d 5944 |
. . . . . . . . 9
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ ↔ ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℂ)) |
141 | 139, 140 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℂ) |
142 | 141 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ) |
143 | | dvnfre 23521 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − 𝑀) ∈ ℕ0) →
((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ) |
144 | 2, 1, 111, 143 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ) |
145 | 123 | feq2d 5944 |
. . . . . . . . . 10
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ ↔ ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℝ)) |
146 | 144, 145 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℝ) |
147 | 146 | feqmptd 6159 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀)) = (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦))) |
148 | 38 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))) |
149 | 148 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) |
150 | 107, 147,
149 | 3eqtr3rd 2653 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦))) |
151 | 77 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ) |
152 | | fvex 6113 |
. . . . . . . 8
⊢
(((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ V |
153 | 152 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ V) |
154 | 76 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ) |
155 | | recn 9905 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
156 | | dvnply2 23846 |
. . . . . . . . . . . 12
⊢ ((ℝ
∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ0) →
((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) ∈
(Poly‘ℝ)) |
157 | 45, 70, 111, 156 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀)) ∈
(Poly‘ℝ)) |
158 | | plyf 23758 |
. . . . . . . . . . 11
⊢
(((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ) →
((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)):ℂ⟶ℂ) |
159 | 157, 158 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀)):ℂ⟶ℂ) |
160 | 159 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ) |
161 | 155, 160 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ) |
162 | 127 | cnfldtopon 22396 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
163 | | toponmax 20543 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
164 | 162, 163 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ℂ ∈
(TopOpen‘ℂfld)) |
165 | | df-ss 3554 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
166 | 104, 165 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ ∩ ℂ) =
ℝ) |
167 | | plyf 23758 |
. . . . . . . . . . 11
⊢
(((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) →
((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 +
1))):ℂ⟶ℂ) |
168 | 72, 167 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 +
1))):ℂ⟶ℂ) |
169 | 168 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ) |
170 | 102 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀))) |
171 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
172 | 171 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ⊆
ℂ) |
173 | | mapsspm 7777 |
. . . . . . . . . . . . 13
⊢ (ℂ
↑𝑚 ℂ) ⊆ (ℂ ↑pm
ℂ) |
174 | | plyf 23758 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ (Poly‘ℝ)
→ 𝑇:ℂ⟶ℂ) |
175 | 70, 174 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇:ℂ⟶ℂ) |
176 | 18, 18 | elmap 7772 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ (ℂ
↑𝑚 ℂ) ↔ 𝑇:ℂ⟶ℂ) |
177 | 175, 176 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ (ℂ ↑𝑚
ℂ)) |
178 | 173, 177 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ (ℂ ↑pm
ℂ)) |
179 | | dvnp1 23494 |
. . . . . . . . . . . 12
⊢ ((ℂ
⊆ ℂ ∧ 𝑇
∈ (ℂ ↑pm ℂ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) →
((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))))) |
180 | 172, 178,
13, 179 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))))) |
181 | 170, 180 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀)) = (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))))) |
182 | 159 | feqmptd 6159 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀)) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))) |
183 | 168 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) |
184 | 183 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ D ((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) |
185 | 181, 182,
184 | 3eqtr3rd 2653 |
. . . . . . . . 9
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))) |
186 | 127, 17, 164, 166, 169, 160, 185 | dvmptres3 23525 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
(((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℝ ↦ (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))) |
187 | 17, 154, 161, 186, 1, 128, 127, 134 | dvmptres 23532 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦))) |
188 | 17, 137, 142, 150, 151, 153, 187 | dvmptsub 23536 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦)))) |
189 | 188 | dmeqd 5248 |
. . . . 5
⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = dom (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦)))) |
190 | | ovex 6577 |
. . . . . 6
⊢
((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦)) ∈ V |
191 | | eqid 2610 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦))) |
192 | 190, 191 | dmmpti 5936 |
. . . . 5
⊢ dom
(𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦))) = 𝐴 |
193 | 189, 192 | syl6eq 2660 |
. . . 4
⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = 𝐴) |
194 | 136, 193 | syl5sseqr 3617 |
. . 3
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))) |
195 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) |
196 | 51 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐵 ∈ ℝ) |
197 | 196 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐵 ∈ ℂ) |
198 | 195, 197 | subcld 10271 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 − 𝐵) ∈ ℂ) |
199 | 87 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑀 ∈
ℕ0) |
200 | 89 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 1 ∈
ℕ0) |
201 | 199, 200 | nn0addcld 11232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑀 + 1) ∈
ℕ0) |
202 | 198, 201 | expcld 12870 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ) |
203 | 155, 202 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ) |
204 | 100 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑀 ∈ ℂ) |
205 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 1 ∈
ℂ) |
206 | 204, 205 | addcld 9938 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℂ) |
207 | 198, 199 | expcld 12870 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑦 − 𝐵)↑𝑀) ∈ ℂ) |
208 | 206, 207 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ ℂ) |
209 | 155, 208 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ ℂ) |
210 | 18 | prid2 4242 |
. . . . . . . . . . 11
⊢ ℂ
∈ {ℝ, ℂ} |
211 | 210 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
212 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
213 | | elfznn 12241 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 + 1) ∈ (1...𝑁) → (𝑀 + 1) ∈ ℕ) |
214 | 8, 213 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
215 | 214 | nnnn0d 11228 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 + 1) ∈
ℕ0) |
216 | 215 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑀 + 1) ∈
ℕ0) |
217 | 212, 216 | expcld 12870 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑀 + 1)) ∈ ℂ) |
218 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝑀 + 1) · (𝑥↑𝑀)) ∈ V |
219 | 218 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑀 + 1) · (𝑥↑𝑀)) ∈ V) |
220 | 211 | dvmptid 23526 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1)) |
221 | | 0cnd 9912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 0 ∈
ℂ) |
222 | 51 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℂ) |
223 | 211, 222 | dvmptc 23527 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝐵)) = (𝑦 ∈ ℂ ↦ 0)) |
224 | 211, 195,
205, 220, 197, 221, 223 | dvmptsub 23536 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦 − 𝐵))) = (𝑦 ∈ ℂ ↦ (1 −
0))) |
225 | | 1m0e1 11008 |
. . . . . . . . . . . 12
⊢ (1
− 0) = 1 |
226 | 225 | mpteq2i 4669 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ ↦ (1
− 0)) = (𝑦 ∈
ℂ ↦ 1) |
227 | 224, 226 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦 − 𝐵))) = (𝑦 ∈ ℂ ↦ 1)) |
228 | | dvexp 23522 |
. . . . . . . . . . . 12
⊢ ((𝑀 + 1) ∈ ℕ →
(ℂ D (𝑥 ∈
ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))))) |
229 | 214, 228 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))))) |
230 | 100, 101 | pncand 10272 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
231 | 230 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥↑((𝑀 + 1) − 1)) = (𝑥↑𝑀)) |
232 | 231 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))) = ((𝑀 + 1) · (𝑥↑𝑀))) |
233 | 232 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑𝑀)))) |
234 | 229, 233 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑𝑀)))) |
235 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 − 𝐵) → (𝑥↑(𝑀 + 1)) = ((𝑦 − 𝐵)↑(𝑀 + 1))) |
236 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 − 𝐵) → (𝑥↑𝑀) = ((𝑦 − 𝐵)↑𝑀)) |
237 | 236 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 − 𝐵) → ((𝑀 + 1) · (𝑥↑𝑀)) = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) |
238 | 211, 211,
198, 205, 217, 219, 227, 234, 235, 237 | dvmptco 23541 |
. . . . . . . . 9
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1))) |
239 | 208 | mulid1d 9936 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1) = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) |
240 | 239 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1)) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))) |
241 | 238, 240 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))) |
242 | 127, 17, 164, 166, 202, 208, 241 | dvmptres3 23525 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℝ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))) |
243 | 17, 203, 209, 242, 1, 128, 127, 134 | dvmptres 23532 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))) |
244 | 243 | dmeqd 5248 |
. . . . 5
⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = dom (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))) |
245 | | ovex 6577 |
. . . . . 6
⊢ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ V |
246 | | eqid 2610 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) = (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) |
247 | 245, 246 | dmmpti 5936 |
. . . . 5
⊢ dom
(𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) = 𝐴 |
248 | 244, 247 | syl6eq 2660 |
. . . 4
⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = 𝐴) |
249 | 136, 248 | syl5sseqr 3617 |
. . 3
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))) |
250 | 17, 24, 1, 11, 49, 50 | dvntaylp0 23930 |
. . . . . 6
⊢ (𝜑 → (((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) |
251 | 250 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))) |
252 | 126, 48 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) ∈ ℂ) |
253 | 252 | subidd 10259 |
. . . . 5
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0) |
254 | 251, 253 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0) |
255 | 127 | subcn 22477 |
. . . . . . 7
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
256 | 255 | a1i 11 |
. . . . . 6
⊢ (𝜑 → − ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
257 | | dvcn 23490 |
. . . . . . . 8
⊢
(((ℝ ⊆ ℂ ∧ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D
((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴) → ((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴–cn→ℂ)) |
258 | 104, 126,
1, 124, 257 | syl31anc 1321 |
. . . . . . 7
⊢ (𝜑 → ((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴–cn→ℂ)) |
259 | 148, 258 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴–cn→ℂ)) |
260 | | plycn 23821 |
. . . . . . . 8
⊢
(((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) →
((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ)) |
261 | 72, 260 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((ℂ
D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ)) |
262 | 1, 22 | syl6ss 3580 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
263 | | cncfmptid 22523 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝑦
∈ 𝐴 ↦ 𝑦) ∈ (𝐴–cn→ℂ)) |
264 | 262, 171,
263 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ 𝑦) ∈ (𝐴–cn→ℂ)) |
265 | 261, 264 | cncfmpt1f 22524 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴–cn→ℂ)) |
266 | 127, 256,
259, 265 | cncfmpt2f 22525 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) ∈ (𝐴–cn→ℂ)) |
267 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) |
268 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) |
269 | 267, 268 | oveq12d 6567 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵))) |
270 | 266, 48, 269 | cnmptlimc 23460 |
. . . 4
⊢ (𝜑 → ((((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) ∈ ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) limℂ 𝐵)) |
271 | 254, 270 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) limℂ 𝐵)) |
272 | 222 | subidd 10259 |
. . . . . 6
⊢ (𝜑 → (𝐵 − 𝐵) = 0) |
273 | 272 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) = (0↑(𝑀 + 1))) |
274 | 214 | 0expd 12886 |
. . . . 5
⊢ (𝜑 → (0↑(𝑀 + 1)) = 0) |
275 | 273, 274 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) = 0) |
276 | 262 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ) |
277 | 276, 202 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ) |
278 | 277, 93 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℂ) |
279 | | dvcn 23490 |
. . . . . 6
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D
(𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = 𝐴) → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ∈ (𝐴–cn→ℂ)) |
280 | 104, 278,
1, 248, 279 | syl31anc 1321 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ∈ (𝐴–cn→ℂ)) |
281 | | oveq1 6556 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑦 − 𝐵) = (𝐵 − 𝐵)) |
282 | 281 | oveq1d 6564 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((𝑦 − 𝐵)↑(𝑀 + 1)) = ((𝐵 − 𝐵)↑(𝑀 + 1))) |
283 | 280, 48, 282 | cnmptlimc 23460 |
. . . 4
⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) limℂ 𝐵)) |
284 | 275, 283 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) limℂ 𝐵)) |
285 | 262 | ssdifssd 3710 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ) |
286 | 285 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℂ) |
287 | 222 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) |
288 | 286, 287 | subcld 10271 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦 − 𝐵) ∈ ℂ) |
289 | | eldifsni 4261 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐴 ∖ {𝐵}) → 𝑦 ≠ 𝐵) |
290 | 289 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ≠ 𝐵) |
291 | 286, 287,
290 | subne0d 10280 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦 − 𝐵) ≠ 0) |
292 | 214 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ) |
293 | 292 | nnzd 11357 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℤ) |
294 | 288, 291,
293 | expne0d 12876 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ≠ 0) |
295 | 294 | necomd 2837 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑦 − 𝐵)↑(𝑀 + 1))) |
296 | 295 | neneqd 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑦 − 𝐵)↑(𝑀 + 1))) |
297 | 296 | nrexdv 2984 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1))) |
298 | | df-ima 5051 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) |
299 | 298 | eleq2i 2680 |
. . . . 5
⊢ (0 ∈
((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵}))) |
300 | | resmpt 5369 |
. . . . . . 7
⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) |
301 | 136, 300 | ax-mp 5 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) |
302 | | ovex 6577 |
. . . . . 6
⊢ ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ V |
303 | 301, 302 | elrnmpti 5297 |
. . . . 5
⊢ (0 ∈
ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1))) |
304 | 299, 303 | bitri 263 |
. . . 4
⊢ (0 ∈
((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1))) |
305 | 297, 304 | sylnibr 318 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵}))) |
306 | 100 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℂ) |
307 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 1 ∈
ℂ) |
308 | 306, 307 | addcld 9938 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ) |
309 | 286, 207 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑𝑀) ∈ ℂ) |
310 | 292 | nnne0d 10942 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0) |
311 | 86 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ) |
312 | 311 | nnzd 11357 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ) |
313 | 288, 291,
312 | expne0d 12876 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑𝑀) ≠ 0) |
314 | 308, 309,
310, 313 | mulne0d 10558 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ≠ 0) |
315 | 314 | necomd 2837 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) |
316 | 315 | neneqd 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) |
317 | 316 | nrexdv 2984 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) |
318 | 243 | imaeq1d 5384 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵}))) |
319 | | df-ima 5051 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) |
320 | 318, 319 | syl6eq 2660 |
. . . . . 6
⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))) |
321 | 320 | eleq2d 2673 |
. . . . 5
⊢ (𝜑 → (0 ∈ ((ℝ D
(𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})))) |
322 | | resmpt 5369 |
. . . . . . 7
⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))) |
323 | 136, 322 | ax-mp 5 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) |
324 | 323, 245 | elrnmpti 5297 |
. . . . 5
⊢ (0 ∈
ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) |
325 | 321, 324 | syl6bb 275 |
. . . 4
⊢ (𝜑 → (0 ∈ ((ℝ D
(𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))) |
326 | 317, 325 | mtbird 314 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ((ℝ D
(𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵}))) |
327 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴) |
328 | 141 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ) |
329 | 327, 328 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ) |
330 | 1 | ssdifssd 3710 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℝ) |
331 | 330 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ) |
332 | 331 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ) |
333 | 159 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ
D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ) |
334 | 332, 333 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ) |
335 | 329, 334 | subcld 10271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) ∈ ℂ) |
336 | 51 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℝ) |
337 | 331, 336 | resubcld 10337 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℝ) |
338 | 87 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈
ℕ0) |
339 | 337, 338 | reexpcld 12887 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ∈ ℝ) |
340 | 339 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ∈ ℂ) |
341 | 336 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) |
342 | 332, 341 | subcld 10271 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ) |
343 | | eldifsni 4261 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ≠ 𝐵) |
344 | 343 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ≠ 𝐵) |
345 | 332, 341,
344 | subne0d 10280 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ≠ 0) |
346 | 338 | nn0zd 11356 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ) |
347 | 342, 345,
346 | expne0d 12876 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ≠ 0) |
348 | 335, 340,
347 | divcld 10680 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) ∈ ℂ) |
349 | 214 | nnrecred 10943 |
. . . . . . 7
⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ) |
350 | 349 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℂ) |
351 | 350 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (1 / (𝑀 + 1)) ∈ ℂ) |
352 | | txtopon 21204 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
→ ((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ ×
ℂ))) |
353 | 162, 162,
352 | mp2an 704 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ ×
ℂ)) |
354 | 353 | toponunii 20547 |
. . . . . . . 8
⊢ (ℂ
× ℂ) = ∪
((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) |
355 | 354 | restid 15917 |
. . . . . . 7
⊢
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ ×
ℂ)) → (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
ℂ)) = ((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld))) |
356 | 353, 355 | ax-mp 5 |
. . . . . 6
⊢
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
ℂ)) = ((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) |
357 | 356 | eqcomi 2619 |
. . . . 5
⊢
((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) ↾t (ℂ ×
ℂ)) |
358 | | taylthlem2.i |
. . . . 5
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))) limℂ 𝐵)) |
359 | | limcresi 23455 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) limℂ 𝐵) ⊆ (((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵) |
360 | | resmpt 5369 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1)))) |
361 | 136, 360 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) |
362 | 361 | oveq1i 6559 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) limℂ 𝐵) |
363 | 359, 362 | sseqtri 3600 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) limℂ 𝐵) ⊆ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) limℂ 𝐵) |
364 | | cncfmptc 22522 |
. . . . . . . 8
⊢ (((1 /
(𝑀 + 1)) ∈ ℝ
∧ 𝐴 ⊆ ℂ
∧ ℝ ⊆ ℂ) → (𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴–cn→ℝ)) |
365 | 349, 262,
104, 364 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴–cn→ℝ)) |
366 | | eqidd 2611 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (1 / (𝑀 + 1)) = (1 / (𝑀 + 1))) |
367 | 365, 48, 366 | cnmptlimc 23460 |
. . . . . 6
⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) limℂ 𝐵)) |
368 | 363, 367 | sseldi 3566 |
. . . . 5
⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) limℂ 𝐵)) |
369 | 127 | mulcn 22478 |
. . . . . 6
⊢ ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
370 | | 0cn 9911 |
. . . . . . 7
⊢ 0 ∈
ℂ |
371 | | opelxpi 5072 |
. . . . . . 7
⊢ ((0
∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → 〈0, (1 /
(𝑀 + 1))〉 ∈
(ℂ × ℂ)) |
372 | 370, 350,
371 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → 〈0, (1 / (𝑀 + 1))〉 ∈ (ℂ
× ℂ)) |
373 | 354 | cncnpi 20892 |
. . . . . 6
⊢ ((
· ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) ∧ 〈0, (1 / (𝑀 + 1))〉 ∈ (ℂ ×
ℂ)) → · ∈ ((((TopOpen‘ℂfld)
×t (TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈0, (1 / (𝑀 + 1))〉)) |
374 | 369, 372,
373 | sylancr 694 |
. . . . 5
⊢ (𝜑 → · ∈
((((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) CnP
(TopOpen‘ℂfld))‘〈0, (1 / (𝑀 + 1))〉)) |
375 | 348, 351,
172, 172, 127, 357, 358, 368, 374 | limccnp2 23462 |
. . . 4
⊢ (𝜑 → (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) limℂ 𝐵)) |
376 | 350 | mul02d 10113 |
. . . 4
⊢ (𝜑 → (0 · (1 / (𝑀 + 1))) = 0) |
377 | 188 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥)) |
378 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥)) |
379 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) |
380 | 378, 379 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥))) |
381 | | ovex 6577 |
. . . . . . . . . . 11
⊢
((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) ∈ V |
382 | 380, 191,
381 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥))) |
383 | 327, 382 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥))) |
384 | 377, 383 | sylan9eq 2664 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥))) |
385 | 243 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥)) |
386 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝑦 − 𝐵) = (𝑥 − 𝐵)) |
387 | 386 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((𝑦 − 𝐵)↑𝑀) = ((𝑥 − 𝐵)↑𝑀)) |
388 | 387 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀))) |
389 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)) ∈ V |
390 | 388, 246,
389 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀))) |
391 | 327, 390 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀))) |
392 | 385, 391 | sylan9eq 2664 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀))) |
393 | 214 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ) |
394 | 393 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ) |
395 | 394, 340 | mulcomd 9940 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)) = (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1))) |
396 | 392, 395 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1))) |
397 | 384, 396 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1)))) |
398 | 393 | nnne0d 10942 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0) |
399 | 335, 340,
394, 347, 398 | divdiv1d 10711 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) / (𝑀 + 1)) = (((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1)))) |
400 | 348, 394,
398 | divrecd 10683 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) / (𝑀 + 1)) = ((((((ℝ D𝑛
𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) |
401 | 397, 399,
400 | 3eqtr2rd 2651 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))) |
402 | 401 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥)))) |
403 | 402 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ
D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))) limℂ 𝐵)) |
404 | 375, 376,
403 | 3eltr3d 2702 |
. . 3
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))) limℂ 𝐵)) |
405 | 1, 80, 94, 134, 48, 135, 194, 249, 271, 284, 305, 326, 404 | lhop 23583 |
. 2
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) limℂ 𝐵)) |
406 | 327 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ 𝐴) |
407 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥)) |
408 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) |
409 | 407, 408 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))) |
410 | | ovex 6577 |
. . . . . . 7
⊢
((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) ∈ V |
411 | 409, 79, 410 | fvmpt 6191 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))) |
412 | 406, 411 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))) |
413 | 386 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((𝑦 − 𝐵)↑(𝑀 + 1)) = ((𝑥 − 𝐵)↑(𝑀 + 1))) |
414 | | ovex 6577 |
. . . . . . 7
⊢ ((𝑥 − 𝐵)↑(𝑀 + 1)) ∈ V |
415 | 413, 93, 414 | fvmpt 6191 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥 − 𝐵)↑(𝑀 + 1))) |
416 | 406, 415 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥 − 𝐵)↑(𝑀 + 1))) |
417 | 412, 416 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) |
418 | 417 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1))))) |
419 | 418 | oveq1d 6564 |
. 2
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛
𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵)) |
420 | 405, 419 | eleqtrd 2690 |
1
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ
D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛
𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵)) |