Step | Hyp | Ref
| Expression |
1 | | fzofi 13547 |
. . . . . 6
⊢ (𝑀..^𝑁) ∈ Fin |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) |
3 | | dvfsumabs.x |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ) |
4 | | dvfsumabs.m |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
5 | | eluzel2 12443 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
7 | | eluzelz 12448 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
8 | 4, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
9 | | fzval2 13098 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) |
10 | 6, 8, 9 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) |
11 | | inss1 4143 |
. . . . . . . . . . 11
⊢ ((𝑀[,]𝑁) ∩ ℤ) ⊆ (𝑀[,]𝑁) |
12 | 10, 11 | eqsstrdi 3955 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀...𝑁) ⊆ (𝑀[,]𝑁)) |
13 | 12 | sselda 3901 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → 𝑦 ∈ (𝑀[,]𝑁)) |
14 | | dvfsumabs.a |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
15 | | cncff 23790 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℂ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℂ) |
17 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) |
18 | 17 | fmpt 6927 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℂ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℂ) |
19 | 16, 18 | sylibr 237 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℂ) |
20 | | nfcsb1v 3836 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 |
21 | 20 | nfel1 2920 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ |
22 | | csbeq1a 3825 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴) |
23 | 22 | eleq1d 2822 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐴 ∈ ℂ ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)) |
24 | 21, 23 | rspc 3525 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑀[,]𝑁) → (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℂ → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)) |
25 | 19, 24 | mpan9 510 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀[,]𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
26 | 13, 25 | syldan 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
27 | 26 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
28 | | fzofzp1 13339 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
29 | | csbeq1 3814 |
. . . . . . . . 9
⊢ (𝑦 = (𝑘 + 1) → ⦋𝑦 / 𝑥⦌𝐴 = ⦋(𝑘 + 1) / 𝑥⦌𝐴) |
30 | 29 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑦 = (𝑘 + 1) → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ↔ ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℂ)) |
31 | 30 | rspccva 3536 |
. . . . . . 7
⊢
((∀𝑦 ∈
(𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℂ) |
32 | 27, 28, 31 | syl2an 599 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℂ) |
33 | | elfzofz 13258 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (𝑀...𝑁)) |
34 | | csbeq1 3814 |
. . . . . . . . 9
⊢ (𝑦 = 𝑘 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑘 / 𝑥⦌𝐴) |
35 | 34 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑦 = 𝑘 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ↔ ⦋𝑘 / 𝑥⦌𝐴 ∈ ℂ)) |
36 | 35 | rspccva 3536 |
. . . . . . 7
⊢
((∀𝑦 ∈
(𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ∧ 𝑘 ∈ (𝑀...𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℂ) |
37 | 27, 33, 36 | syl2an 599 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℂ) |
38 | 32, 37 | subcld 11189 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℂ) |
39 | 2, 3, 38 | fsumsub 15352 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) |
40 | | vex 3412 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝑦 = 𝑀 → 𝑦 ∈ V) |
42 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑦 = 𝑀 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑀)) |
43 | 42 | biimpa 480 |
. . . . . . . 8
⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑀) |
44 | | dvfsumabs.c |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐶) |
46 | 41, 45 | csbied 3849 |
. . . . . 6
⊢ (𝑦 = 𝑀 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐶) |
47 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝑦 = 𝑁 → 𝑦 ∈ V) |
48 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑦 = 𝑁 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑁)) |
49 | 48 | biimpa 480 |
. . . . . . . 8
⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑁) |
50 | | dvfsumabs.d |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐷) |
52 | 47, 51 | csbied 3849 |
. . . . . 6
⊢ (𝑦 = 𝑁 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐷) |
53 | 34, 29, 46, 52, 4, 26 | telfsumo2 15367 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) = (𝐷 − 𝐶)) |
54 | 53 | oveq2d 7229 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) |
55 | 39, 54 | eqtrd 2777 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) |
56 | 55 | fveq2d 6721 |
. 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) = (abs‘(Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶)))) |
57 | 3, 38 | subcld 11189 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) ∈ ℂ) |
58 | 2, 57 | fsumcl 15297 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) ∈ ℂ) |
59 | 58 | abscld 15000 |
. . 3
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ∈ ℝ) |
60 | 57 | abscld 15000 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ∈ ℝ) |
61 | 2, 60 | fsumrecl 15298 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ∈ ℝ) |
62 | | dvfsumabs.y |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ) |
63 | 2, 62 | fsumrecl 15298 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑌 ∈ ℝ) |
64 | 2, 57 | fsumabs 15365 |
. . 3
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)(abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)))) |
65 | | elfzoelz 13243 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ ℤ) |
66 | 65 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℤ) |
67 | 66 | zred 12282 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ) |
68 | 67 | rexrd 10883 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ*) |
69 | | peano2re 11005 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
70 | 67, 69 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℝ) |
71 | 70 | rexrd 10883 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈
ℝ*) |
72 | 67 | lep1d 11763 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ≤ (𝑘 + 1)) |
73 | | ubicc2 13053 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ*
∧ (𝑘 + 1) ∈
ℝ* ∧ 𝑘
≤ (𝑘 + 1)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1))) |
74 | 68, 71, 72, 73 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1))) |
75 | | lbicc2 13052 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ*
∧ (𝑘 + 1) ∈
ℝ* ∧ 𝑘
≤ (𝑘 + 1)) → 𝑘 ∈ (𝑘[,](𝑘 + 1))) |
76 | 68, 71, 72, 75 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ (𝑘[,](𝑘 + 1))) |
77 | 6 | zred 12282 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℝ) |
78 | 77 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ) |
79 | 8 | zred 12282 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℝ) |
80 | 79 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ) |
81 | | elfzole1 13251 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑘) |
82 | 81 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑘) |
83 | 28 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
84 | | elfzle2 13116 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ≤ 𝑁) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ≤ 𝑁) |
86 | | iccss 13003 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ (𝑀 ≤ 𝑘 ∧ (𝑘 + 1) ≤ 𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁)) |
87 | 78, 80, 82, 85, 86 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁)) |
88 | 87 | resmptd 5908 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ↾ (𝑘[,](𝑘 + 1))) = (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) |
89 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
90 | 89 | subcn 23763 |
. . . . . . . . . . . 12
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
91 | 90 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → − ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
92 | | iccssre 13017 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀[,]𝑁) ⊆ ℝ) |
93 | 77, 79, 92 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
94 | 93 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℝ) |
95 | | ax-resscn 10786 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ |
96 | 94, 95 | sstrdi 3913 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℂ) |
97 | | ssid 3923 |
. . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ |
98 | 97 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℂ ⊆
ℂ) |
99 | | cncfmptc 23809 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℂ ∧ (𝑀[,]𝑁) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑥 ∈
(𝑀[,]𝑁) ↦ 𝑋) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
100 | 3, 96, 98, 99 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝑋) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
101 | | cncfmptid 23810 |
. . . . . . . . . . . . 13
⊢ (((𝑀[,]𝑁) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑥 ∈
(𝑀[,]𝑁) ↦ 𝑥) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
102 | 96, 97, 101 | sylancl 589 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝑥) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
103 | 100, 102 | mulcncf 24343 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝑋 · 𝑥)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
104 | 14 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
105 | 89, 91, 103, 104 | cncfmpt2f 23812 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
106 | | rescncf 23794 |
. . . . . . . . . 10
⊢ ((𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℂ))) |
107 | 87, 105, 106 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℂ)) |
108 | 88, 107 | eqeltrrd 2839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) ∈ ((𝑘[,](𝑘 + 1))–cn→ℂ)) |
109 | 95 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ⊆
ℂ) |
110 | 87, 94 | sstrd 3911 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ ℝ) |
111 | 87 | sselda 3901 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘[,](𝑘 + 1))) → 𝑥 ∈ (𝑀[,]𝑁)) |
112 | 3 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑋 ∈ ℂ) |
113 | 96 | sselda 3901 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑥 ∈ ℂ) |
114 | 112, 113 | mulcld 10853 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑋 · 𝑥) ∈ ℂ) |
115 | 19 | r19.21bi 3130 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℂ) |
116 | 115 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℂ) |
117 | 114, 116 | subcld 11189 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((𝑋 · 𝑥) − 𝐴) ∈ ℂ) |
118 | 111, 117 | syldan 594 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘[,](𝑘 + 1))) → ((𝑋 · 𝑥) − 𝐴) ∈ ℂ) |
119 | 89 | tgioo2 23700 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
120 | | iccntr 23718 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑘[,](𝑘 + 1))) = (𝑘(,)(𝑘 + 1))) |
121 | 67, 70, 120 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((int‘(topGen‘ran
(,)))‘(𝑘[,](𝑘 + 1))) = (𝑘(,)(𝑘 + 1))) |
122 | 109, 110,
118, 119, 89, 121 | dvmptntr 24868 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (ℝ D (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))) |
123 | | reelprrecn 10821 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
124 | 123 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ∈ {ℝ,
ℂ}) |
125 | | ioossicc 13021 |
. . . . . . . . . . . . . 14
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
126 | 125 | sseli 3896 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁)) |
127 | 126, 117 | sylan2 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → ((𝑋 · 𝑥) − 𝐴) ∈ ℂ) |
128 | | ovex 7246 |
. . . . . . . . . . . . 13
⊢ (𝑋 − 𝐵) ∈ V |
129 | 128 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝑋 − 𝐵) ∈ V) |
130 | 126, 114 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝑋 · 𝑥) ∈ ℂ) |
131 | 3 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝑋 ∈ ℂ) |
132 | 125, 96 | sstrid 3912 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ⊆ ℂ) |
133 | 132 | sselda 3901 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝑥 ∈ ℂ) |
134 | | 1cnd 10828 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 1 ∈ ℂ) |
135 | 109 | sselda 3901 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
136 | | 1cnd 10828 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
137 | 124 | dvmptid 24854 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
138 | 125, 94 | sstrid 3912 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ⊆ ℝ) |
139 | | iooretop 23663 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀(,)𝑁) ∈ (topGen‘ran
(,)) |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ∈ (topGen‘ran
(,))) |
141 | 124, 135,
136, 137, 138, 119, 89, 140 | dvmptres 24860 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝑥)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 1)) |
142 | 124, 133,
134, 141, 3 | dvmptcmul 24861 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 𝑥))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 1))) |
143 | 3 | mulid1d 10850 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · 1) = 𝑋) |
144 | 143 | mpteq2dv 5151 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 1)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝑋)) |
145 | 142, 144 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 𝑥))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝑋)) |
146 | 126, 116 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℂ) |
147 | | dvfsumabs.v |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) |
148 | 147 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) |
149 | | dvfsumabs.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
150 | 149 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
151 | 124, 130,
131, 145, 146, 148, 150 | dvmptsub 24864 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 − 𝐵))) |
152 | 78 | rexrd 10883 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈
ℝ*) |
153 | | iooss1 12970 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ*
∧ 𝑀 ≤ 𝑘) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) |
154 | 152, 82, 153 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) |
155 | 80 | rexrd 10883 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈
ℝ*) |
156 | | iooss2 12971 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ*
∧ (𝑘 + 1) ≤ 𝑁) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
157 | 155, 85, 156 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
158 | 154, 157 | sstrd 3911 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
159 | | iooretop 23663 |
. . . . . . . . . . . . 13
⊢ (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran
(,)) |
160 | 159 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran
(,))) |
161 | 124, 127,
129, 151, 158, 119, 89, 160 | dvmptres 24860 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) |
162 | 122, 161 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) |
163 | 162 | dmeqd 5774 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = dom (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) |
164 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵)) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵)) |
165 | 128, 164 | dmmpti 6522 |
. . . . . . . . 9
⊢ dom
(𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵)) = (𝑘(,)(𝑘 + 1)) |
166 | 163, 165 | eqtrdi 2794 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑘(,)(𝑘 + 1))) |
167 | 162 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) |
168 | 167 | fveq1d 6719 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → ((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥) = ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))‘𝑥)) |
169 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝑥 ∈ (𝑘(,)(𝑘 + 1))) |
170 | 164 | fvmpt2 6829 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ∧ (𝑋 − 𝐵) ∈ V) → ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))‘𝑥) = (𝑋 − 𝐵)) |
171 | 169, 128,
170 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))‘𝑥) = (𝑋 − 𝐵)) |
172 | 168, 171 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → ((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥) = (𝑋 − 𝐵)) |
173 | 172 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) = (abs‘(𝑋 − 𝐵))) |
174 | | dvfsumabs.l |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → (abs‘(𝑋 − 𝐵)) ≤ 𝑌) |
175 | 174 | anassrs 471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘(𝑋 − 𝐵)) ≤ 𝑌) |
176 | 173, 175 | eqbrtrd 5075 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌) |
177 | 176 | ralrimiva 3105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑘(,)(𝑘 + 1))(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌) |
178 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥abs |
179 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥ℝ |
180 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥
D |
181 | | nfmpt1 5153 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) |
182 | 179, 180,
181 | nfov 7243 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) |
183 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑦 |
184 | 182, 183 | nffv 6727 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦) |
185 | 178, 184 | nffv 6727 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) |
186 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥
≤ |
187 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑌 |
188 | 185, 186,
187 | nfbr 5100 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌 |
189 | | 2fveq3 6722 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) = (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦))) |
190 | 189 | breq1d 5063 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌)) |
191 | 188, 190 | rspc 3525 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑘(,)(𝑘 + 1)) → (∀𝑥 ∈ (𝑘(,)(𝑘 + 1))(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌 → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌)) |
192 | 177, 191 | mpan9 510 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌) |
193 | 67, 70, 108, 166, 62, 192 | dvlip 24890 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ ((𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑘 ∈ (𝑘[,](𝑘 + 1)))) → (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) ≤ (𝑌 · (abs‘((𝑘 + 1) − 𝑘)))) |
194 | 193 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑘 ∈ (𝑘[,](𝑘 + 1))) → (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) ≤ (𝑌 · (abs‘((𝑘 + 1) − 𝑘))))) |
195 | 74, 76, 194 | mp2and 699 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) ≤ (𝑌 · (abs‘((𝑘 + 1) − 𝑘)))) |
196 | | ovex 7246 |
. . . . . . . . 9
⊢ ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) ∈ V |
197 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑘 + 1) |
198 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑋 · (𝑘 + 1)) |
199 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥
− |
200 | | nfcsb1v 3836 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋(𝑘 + 1) / 𝑥⦌𝐴 |
201 | 198, 199,
200 | nfov 7243 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) |
202 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → (𝑋 · 𝑥) = (𝑋 · (𝑘 + 1))) |
203 | | csbeq1a 3825 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → 𝐴 = ⦋(𝑘 + 1) / 𝑥⦌𝐴) |
204 | 202, 203 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑘 + 1) → ((𝑋 · 𝑥) − 𝐴) = ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴)) |
205 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) = (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) |
206 | 197, 201,
204, 205 | fvmptf 6839 |
. . . . . . . . 9
⊢ (((𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)) ∧ ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) ∈ V) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) = ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴)) |
207 | 74, 196, 206 | sylancl 589 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) = ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴)) |
208 | 67 | recnd 10861 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℂ) |
209 | 3, 208 | mulcld 10853 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · 𝑘) ∈ ℂ) |
210 | 209, 37 | subcld 11189 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℂ) |
211 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑘 |
212 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑋 · 𝑘) |
213 | | nfcsb1v 3836 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑘 / 𝑥⦌𝐴 |
214 | 212, 199,
213 | nfov 7243 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴) |
215 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → (𝑋 · 𝑥) = (𝑋 · 𝑘)) |
216 | | csbeq1a 3825 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → 𝐴 = ⦋𝑘 / 𝑥⦌𝐴) |
217 | 215, 216 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → ((𝑋 · 𝑥) − 𝐴) = ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴)) |
218 | 211, 214,
217, 205 | fvmptf 6839 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (𝑘[,](𝑘 + 1)) ∧ ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℂ) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘) = ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴)) |
219 | 76, 210, 218 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘) = ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴)) |
220 | 207, 219 | oveq12d 7231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘)) = (((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) − ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴))) |
221 | | peano2cn 11004 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → (𝑘 + 1) ∈
ℂ) |
222 | 208, 221 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℂ) |
223 | 3, 222 | mulcld 10853 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · (𝑘 + 1)) ∈ ℂ) |
224 | 223, 209,
32, 37 | sub4d 11238 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) − ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴))) |
225 | | 1cnd 10828 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 1 ∈ ℂ) |
226 | 208, 225 | pncan2d 11191 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑘 + 1) − 𝑘) = 1) |
227 | 226 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = (𝑋 · 1)) |
228 | 3, 222, 208 | subdid 11288 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘))) |
229 | 227, 228,
143 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) = 𝑋) |
230 | 229 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) |
231 | 220, 224,
230 | 3eqtr2rd 2784 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) |
232 | 231 | fveq2d 6721 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) = (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘)))) |
233 | 226 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘((𝑘 + 1) − 𝑘)) = (abs‘1)) |
234 | | abs1 14861 |
. . . . . . . 8
⊢
(abs‘1) = 1 |
235 | 233, 234 | eqtrdi 2794 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘((𝑘 + 1) − 𝑘)) = 1) |
236 | 235 | oveq2d 7229 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑌 · (abs‘((𝑘 + 1) − 𝑘))) = (𝑌 · 1)) |
237 | 62 | recnd 10861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℂ) |
238 | 237 | mulid1d 10850 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑌 · 1) = 𝑌) |
239 | 236, 238 | eqtr2d 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 = (𝑌 · (abs‘((𝑘 + 1) − 𝑘)))) |
240 | 195, 232,
239 | 3brtr4d 5085 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ 𝑌) |
241 | 2, 60, 62, 240 | fsumle 15363 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌) |
242 | 59, 61, 63, 64, 241 | letrd 10989 |
. 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌) |
243 | 56, 242 | eqbrtrrd 5077 |
1
⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌) |