Step | Hyp | Ref
| Expression |
1 | | fzofi 12635 |
. . . . . 6
⊢ (𝑀..^𝑁) ∈ Fin |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) |
3 | | dvfsumabs.x |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ) |
4 | | dvfsumabs.m |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
5 | | eluzel2 11568 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
7 | | eluzelz 11573 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
8 | 4, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
9 | | fzval2 12200 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) |
10 | 6, 8, 9 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) |
11 | | inss1 3795 |
. . . . . . . . . . 11
⊢ ((𝑀[,]𝑁) ∩ ℤ) ⊆ (𝑀[,]𝑁) |
12 | 10, 11 | syl6eqss 3618 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀...𝑁) ⊆ (𝑀[,]𝑁)) |
13 | 12 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → 𝑦 ∈ (𝑀[,]𝑁)) |
14 | | dvfsumabs.a |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
15 | | cncff 22504 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℂ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℂ) |
17 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) |
18 | 17 | fmpt 6289 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℂ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℂ) |
19 | 16, 18 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℂ) |
20 | | nfcsb1v 3515 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 |
21 | 20 | nfel1 2765 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ |
22 | | csbeq1a 3508 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴) |
23 | 22 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐴 ∈ ℂ ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)) |
24 | 21, 23 | rspc 3276 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑀[,]𝑁) → (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℂ → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)) |
25 | 19, 24 | mpan9 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀[,]𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
26 | 13, 25 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
27 | 26 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
28 | | fzofzp1 12431 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
29 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑦 = (𝑘 + 1) → ⦋𝑦 / 𝑥⦌𝐴 = ⦋(𝑘 + 1) / 𝑥⦌𝐴) |
30 | 29 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑦 = (𝑘 + 1) → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ↔ ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℂ)) |
31 | 30 | rspccva 3281 |
. . . . . . 7
⊢
((∀𝑦 ∈
(𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℂ) |
32 | 27, 28, 31 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℂ) |
33 | | elfzofz 12354 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (𝑀...𝑁)) |
34 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑦 = 𝑘 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑘 / 𝑥⦌𝐴) |
35 | 34 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑦 = 𝑘 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ↔ ⦋𝑘 / 𝑥⦌𝐴 ∈ ℂ)) |
36 | 35 | rspccva 3281 |
. . . . . . 7
⊢
((∀𝑦 ∈
(𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ∧ 𝑘 ∈ (𝑀...𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℂ) |
37 | 27, 33, 36 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℂ) |
38 | 32, 37 | subcld 10271 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℂ) |
39 | 2, 3, 38 | fsumsub 14362 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) |
40 | | vex 3176 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝑦 = 𝑀 → 𝑦 ∈ V) |
42 | | eqeq2 2621 |
. . . . . . . . 9
⊢ (𝑦 = 𝑀 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑀)) |
43 | 42 | biimpa 500 |
. . . . . . . 8
⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑀) |
44 | | dvfsumabs.c |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐶) |
46 | 41, 45 | csbied 3526 |
. . . . . 6
⊢ (𝑦 = 𝑀 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐶) |
47 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝑦 = 𝑁 → 𝑦 ∈ V) |
48 | | eqeq2 2621 |
. . . . . . . . 9
⊢ (𝑦 = 𝑁 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑁)) |
49 | 48 | biimpa 500 |
. . . . . . . 8
⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑁) |
50 | | dvfsumabs.d |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐷) |
52 | 47, 51 | csbied 3526 |
. . . . . 6
⊢ (𝑦 = 𝑁 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐷) |
53 | 34, 29, 46, 52, 4, 26 | telfsumo2 14376 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) = (𝐷 − 𝐶)) |
54 | 53 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) |
55 | 39, 54 | eqtrd 2644 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) |
56 | 55 | fveq2d 6107 |
. 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) = (abs‘(Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶)))) |
57 | 3, 38 | subcld 10271 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) ∈ ℂ) |
58 | 2, 57 | fsumcl 14311 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) ∈ ℂ) |
59 | 58 | abscld 14023 |
. . 3
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ∈ ℝ) |
60 | 57 | abscld 14023 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ∈ ℝ) |
61 | 2, 60 | fsumrecl 14312 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ∈ ℝ) |
62 | | dvfsumabs.y |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ) |
63 | 2, 62 | fsumrecl 14312 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑌 ∈ ℝ) |
64 | 2, 57 | fsumabs 14374 |
. . 3
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)(abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)))) |
65 | | elfzoelz 12339 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ ℤ) |
66 | 65 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℤ) |
67 | 66 | zred 11358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ) |
68 | 67 | rexrd 9968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ*) |
69 | | peano2re 10088 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
70 | 67, 69 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℝ) |
71 | 70 | rexrd 9968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈
ℝ*) |
72 | 67 | lep1d 10834 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ≤ (𝑘 + 1)) |
73 | | ubicc2 12160 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ*
∧ (𝑘 + 1) ∈
ℝ* ∧ 𝑘
≤ (𝑘 + 1)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1))) |
74 | 68, 71, 72, 73 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1))) |
75 | | lbicc2 12159 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ*
∧ (𝑘 + 1) ∈
ℝ* ∧ 𝑘
≤ (𝑘 + 1)) → 𝑘 ∈ (𝑘[,](𝑘 + 1))) |
76 | 68, 71, 72, 75 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ (𝑘[,](𝑘 + 1))) |
77 | 6 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℝ) |
78 | 77 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ) |
79 | 8 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℝ) |
80 | 79 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ) |
81 | | elfzole1 12347 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑘) |
82 | 81 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑘) |
83 | 28 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
84 | | elfzle2 12216 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ≤ 𝑁) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ≤ 𝑁) |
86 | | iccss 12112 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ (𝑀 ≤ 𝑘 ∧ (𝑘 + 1) ≤ 𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁)) |
87 | 78, 80, 82, 85, 86 | syl22anc 1319 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁)) |
88 | 87 | resmptd 5371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ↾ (𝑘[,](𝑘 + 1))) = (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) |
89 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
90 | 89 | subcn 22477 |
. . . . . . . . . . . 12
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
91 | 90 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → − ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
92 | | iccssre 12126 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀[,]𝑁) ⊆ ℝ) |
93 | 77, 79, 92 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
94 | 93 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℝ) |
95 | | ax-resscn 9872 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ |
96 | 94, 95 | syl6ss 3580 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℂ) |
97 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ |
98 | 97 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℂ ⊆
ℂ) |
99 | | cncfmptc 22522 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℂ ∧ (𝑀[,]𝑁) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑥 ∈
(𝑀[,]𝑁) ↦ 𝑋) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
100 | 3, 96, 98, 99 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝑋) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
101 | | cncfmptid 22523 |
. . . . . . . . . . . . 13
⊢ (((𝑀[,]𝑁) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑥 ∈
(𝑀[,]𝑁) ↦ 𝑥) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
102 | 96, 97, 101 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝑥) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
103 | 100, 102 | mulcncf 23023 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝑋 · 𝑥)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
104 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
105 | 89, 91, 103, 104 | cncfmpt2f 22525 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
106 | | rescncf 22508 |
. . . . . . . . . 10
⊢ ((𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℂ))) |
107 | 87, 105, 106 | sylc 63 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℂ)) |
108 | 88, 107 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) ∈ ((𝑘[,](𝑘 + 1))–cn→ℂ)) |
109 | 95 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ⊆
ℂ) |
110 | 87, 94 | sstrd 3578 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ ℝ) |
111 | 87 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘[,](𝑘 + 1))) → 𝑥 ∈ (𝑀[,]𝑁)) |
112 | 3 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑋 ∈ ℂ) |
113 | 96 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑥 ∈ ℂ) |
114 | 112, 113 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑋 · 𝑥) ∈ ℂ) |
115 | 19 | r19.21bi 2916 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℂ) |
116 | 115 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℂ) |
117 | 114, 116 | subcld 10271 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((𝑋 · 𝑥) − 𝐴) ∈ ℂ) |
118 | 111, 117 | syldan 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘[,](𝑘 + 1))) → ((𝑋 · 𝑥) − 𝐴) ∈ ℂ) |
119 | 89 | tgioo2 22414 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
120 | | iccntr 22432 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑘[,](𝑘 + 1))) = (𝑘(,)(𝑘 + 1))) |
121 | 67, 70, 120 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((int‘(topGen‘ran
(,)))‘(𝑘[,](𝑘 + 1))) = (𝑘(,)(𝑘 + 1))) |
122 | 109, 110,
118, 119, 89, 121 | dvmptntr 23540 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (ℝ D (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))) |
123 | | reelprrecn 9907 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
124 | 123 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ∈ {ℝ,
ℂ}) |
125 | | ioossicc 12130 |
. . . . . . . . . . . . . 14
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
126 | 125 | sseli 3564 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁)) |
127 | 126, 117 | sylan2 490 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → ((𝑋 · 𝑥) − 𝐴) ∈ ℂ) |
128 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑋 − 𝐵) ∈ V |
129 | 128 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝑋 − 𝐵) ∈ V) |
130 | 126, 114 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝑋 · 𝑥) ∈ ℂ) |
131 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝑋 ∈ ℂ) |
132 | 125, 96 | syl5ss 3579 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ⊆ ℂ) |
133 | 132 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝑥 ∈ ℂ) |
134 | | 1cnd 9935 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 1 ∈ ℂ) |
135 | 109 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
136 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
137 | 124 | dvmptid 23526 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
138 | 125, 94 | syl5ss 3579 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ⊆ ℝ) |
139 | | iooretop 22379 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀(,)𝑁) ∈ (topGen‘ran
(,)) |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ∈ (topGen‘ran
(,))) |
141 | 124, 135,
136, 137, 138, 119, 89, 140 | dvmptres 23532 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝑥)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 1)) |
142 | 124, 133,
134, 141, 3 | dvmptcmul 23533 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 𝑥))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 1))) |
143 | 3 | mulid1d 9936 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · 1) = 𝑋) |
144 | 143 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 1)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝑋)) |
145 | 142, 144 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 𝑥))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝑋)) |
146 | 126, 116 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℂ) |
147 | | dvfsumabs.v |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) |
148 | 147 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) |
149 | | dvfsumabs.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
150 | 149 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
151 | 124, 130,
131, 145, 146, 148, 150 | dvmptsub 23536 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 − 𝐵))) |
152 | 78 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈
ℝ*) |
153 | | iooss1 12081 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ*
∧ 𝑀 ≤ 𝑘) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) |
154 | 152, 82, 153 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) |
155 | 80 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈
ℝ*) |
156 | | iooss2 12082 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ*
∧ (𝑘 + 1) ≤ 𝑁) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
157 | 155, 85, 156 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
158 | 154, 157 | sstrd 3578 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
159 | | iooretop 22379 |
. . . . . . . . . . . . 13
⊢ (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran
(,)) |
160 | 159 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran
(,))) |
161 | 124, 127,
129, 151, 158, 119, 89, 160 | dvmptres 23532 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) |
162 | 122, 161 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) |
163 | 162 | dmeqd 5248 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = dom (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) |
164 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵)) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵)) |
165 | 128, 164 | dmmpti 5936 |
. . . . . . . . 9
⊢ dom
(𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵)) = (𝑘(,)(𝑘 + 1)) |
166 | 163, 165 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑘(,)(𝑘 + 1))) |
167 | 162 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) |
168 | 167 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → ((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥) = ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))‘𝑥)) |
169 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝑥 ∈ (𝑘(,)(𝑘 + 1))) |
170 | 164 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ∧ (𝑋 − 𝐵) ∈ V) → ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))‘𝑥) = (𝑋 − 𝐵)) |
171 | 169, 128,
170 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))‘𝑥) = (𝑋 − 𝐵)) |
172 | 168, 171 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → ((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥) = (𝑋 − 𝐵)) |
173 | 172 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) = (abs‘(𝑋 − 𝐵))) |
174 | | dvfsumabs.l |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → (abs‘(𝑋 − 𝐵)) ≤ 𝑌) |
175 | 174 | anassrs 678 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘(𝑋 − 𝐵)) ≤ 𝑌) |
176 | 173, 175 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌) |
177 | 176 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑘(,)(𝑘 + 1))(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌) |
178 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥abs |
179 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥ℝ |
180 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥
D |
181 | | nfmpt1 4675 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) |
182 | 179, 180,
181 | nfov 6575 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) |
183 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑦 |
184 | 182, 183 | nffv 6110 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦) |
185 | 178, 184 | nffv 6110 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) |
186 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥
≤ |
187 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑌 |
188 | 185, 186,
187 | nfbr 4629 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌 |
189 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥) = ((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) |
190 | 189 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) = (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦))) |
191 | 190 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌)) |
192 | 188, 191 | rspc 3276 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑘(,)(𝑘 + 1)) → (∀𝑥 ∈ (𝑘(,)(𝑘 + 1))(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌 → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌)) |
193 | 177, 192 | mpan9 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌) |
194 | 67, 70, 108, 166, 62, 193 | dvlip 23560 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ ((𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑘 ∈ (𝑘[,](𝑘 + 1)))) → (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) ≤ (𝑌 · (abs‘((𝑘 + 1) − 𝑘)))) |
195 | 194 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑘 ∈ (𝑘[,](𝑘 + 1))) → (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) ≤ (𝑌 · (abs‘((𝑘 + 1) − 𝑘))))) |
196 | 74, 76, 195 | mp2and 711 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) ≤ (𝑌 · (abs‘((𝑘 + 1) − 𝑘)))) |
197 | | ovex 6577 |
. . . . . . . . 9
⊢ ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) ∈ V |
198 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑘 + 1) |
199 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑋 · (𝑘 + 1)) |
200 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥
− |
201 | | nfcsb1v 3515 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋(𝑘 + 1) / 𝑥⦌𝐴 |
202 | 199, 200,
201 | nfov 6575 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) |
203 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → (𝑋 · 𝑥) = (𝑋 · (𝑘 + 1))) |
204 | | csbeq1a 3508 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → 𝐴 = ⦋(𝑘 + 1) / 𝑥⦌𝐴) |
205 | 203, 204 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑘 + 1) → ((𝑋 · 𝑥) − 𝐴) = ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴)) |
206 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) = (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) |
207 | 198, 202,
205, 206 | fvmptf 6209 |
. . . . . . . . 9
⊢ (((𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)) ∧ ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) ∈ V) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) = ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴)) |
208 | 74, 197, 207 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) = ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴)) |
209 | 67 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℂ) |
210 | 3, 209 | mulcld 9939 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · 𝑘) ∈ ℂ) |
211 | 210, 37 | subcld 10271 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℂ) |
212 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑘 |
213 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑋 · 𝑘) |
214 | | nfcsb1v 3515 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑘 / 𝑥⦌𝐴 |
215 | 213, 200,
214 | nfov 6575 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴) |
216 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → (𝑋 · 𝑥) = (𝑋 · 𝑘)) |
217 | | csbeq1a 3508 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → 𝐴 = ⦋𝑘 / 𝑥⦌𝐴) |
218 | 216, 217 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → ((𝑋 · 𝑥) − 𝐴) = ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴)) |
219 | 212, 215,
218, 206 | fvmptf 6209 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (𝑘[,](𝑘 + 1)) ∧ ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℂ) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘) = ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴)) |
220 | 76, 211, 219 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘) = ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴)) |
221 | 208, 220 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘)) = (((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) − ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴))) |
222 | | peano2cn 10087 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → (𝑘 + 1) ∈
ℂ) |
223 | 209, 222 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℂ) |
224 | 3, 223 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · (𝑘 + 1)) ∈ ℂ) |
225 | 224, 210,
32, 37 | sub4d 10320 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) − ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴))) |
226 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 1 ∈ ℂ) |
227 | 209, 226 | pncan2d 10273 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑘 + 1) − 𝑘) = 1) |
228 | 227 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = (𝑋 · 1)) |
229 | 3, 223, 209 | subdid 10365 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘))) |
230 | 228, 229,
143 | 3eqtr3d 2652 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) = 𝑋) |
231 | 230 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) |
232 | 221, 225,
231 | 3eqtr2rd 2651 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) |
233 | 232 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) = (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘)))) |
234 | 227 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘((𝑘 + 1) − 𝑘)) = (abs‘1)) |
235 | | abs1 13885 |
. . . . . . . 8
⊢
(abs‘1) = 1 |
236 | 234, 235 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘((𝑘 + 1) − 𝑘)) = 1) |
237 | 236 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑌 · (abs‘((𝑘 + 1) − 𝑘))) = (𝑌 · 1)) |
238 | 62 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℂ) |
239 | 238 | mulid1d 9936 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑌 · 1) = 𝑌) |
240 | 237, 239 | eqtr2d 2645 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 = (𝑌 · (abs‘((𝑘 + 1) − 𝑘)))) |
241 | 196, 233,
240 | 3brtr4d 4615 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ 𝑌) |
242 | 2, 60, 62, 241 | fsumle 14372 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌) |
243 | 59, 61, 63, 64, 242 | letrd 10073 |
. 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌) |
244 | 56, 243 | eqbrtrrd 4607 |
1
⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌) |