| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzofi 14016 | . . . . . 6
⊢ (𝑀..^𝑁) ∈ Fin | 
| 2 | 1 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) | 
| 3 |  | dvfsumabs.x | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ) | 
| 4 |  | dvfsumabs.m | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 5 |  | eluzel2 12884 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | 
| 6 | 4, 5 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 7 |  | eluzelz 12889 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | 
| 8 | 4, 7 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 9 |  | fzval2 13551 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) | 
| 10 | 6, 8, 9 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) | 
| 11 |  | inss1 4236 | . . . . . . . . . . 11
⊢ ((𝑀[,]𝑁) ∩ ℤ) ⊆ (𝑀[,]𝑁) | 
| 12 | 10, 11 | eqsstrdi 4027 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀...𝑁) ⊆ (𝑀[,]𝑁)) | 
| 13 | 12 | sselda 3982 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → 𝑦 ∈ (𝑀[,]𝑁)) | 
| 14 |  | dvfsumabs.a | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ)) | 
| 15 |  | cncff 24920 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℂ) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℂ) | 
| 17 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) | 
| 18 | 17 | fmpt 7129 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℂ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℂ) | 
| 19 | 16, 18 | sylibr 234 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℂ) | 
| 20 |  | nfcsb1v 3922 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 | 
| 21 | 20 | nfel1 2921 | . . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ | 
| 22 |  | csbeq1a 3912 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴) | 
| 23 | 22 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐴 ∈ ℂ ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)) | 
| 24 | 21, 23 | rspc 3609 | . . . . . . . . . 10
⊢ (𝑦 ∈ (𝑀[,]𝑁) → (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℂ → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)) | 
| 25 | 19, 24 | mpan9 506 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀[,]𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) | 
| 26 | 13, 25 | syldan 591 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) | 
| 27 | 26 | ralrimiva 3145 | . . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) | 
| 28 |  | fzofzp1 13804 | . . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) | 
| 29 |  | csbeq1 3901 | . . . . . . . . 9
⊢ (𝑦 = (𝑘 + 1) → ⦋𝑦 / 𝑥⦌𝐴 = ⦋(𝑘 + 1) / 𝑥⦌𝐴) | 
| 30 | 29 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑦 = (𝑘 + 1) → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ↔ ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℂ)) | 
| 31 | 30 | rspccva 3620 | . . . . . . 7
⊢
((∀𝑦 ∈
(𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℂ) | 
| 32 | 27, 28, 31 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℂ) | 
| 33 |  | elfzofz 13716 | . . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (𝑀...𝑁)) | 
| 34 |  | csbeq1 3901 | . . . . . . . . 9
⊢ (𝑦 = 𝑘 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑘 / 𝑥⦌𝐴) | 
| 35 | 34 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑦 = 𝑘 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ↔ ⦋𝑘 / 𝑥⦌𝐴 ∈ ℂ)) | 
| 36 | 35 | rspccva 3620 | . . . . . . 7
⊢
((∀𝑦 ∈
(𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ ∧ 𝑘 ∈ (𝑀...𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℂ) | 
| 37 | 27, 33, 36 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℂ) | 
| 38 | 32, 37 | subcld 11621 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℂ) | 
| 39 | 2, 3, 38 | fsumsub 15825 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) | 
| 40 |  | vex 3483 | . . . . . . . 8
⊢ 𝑦 ∈ V | 
| 41 | 40 | a1i 11 | . . . . . . 7
⊢ (𝑦 = 𝑀 → 𝑦 ∈ V) | 
| 42 |  | eqeq2 2748 | . . . . . . . . 9
⊢ (𝑦 = 𝑀 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑀)) | 
| 43 | 42 | biimpa 476 | . . . . . . . 8
⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑀) | 
| 44 |  | dvfsumabs.c | . . . . . . . 8
⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) | 
| 45 | 43, 44 | syl 17 | . . . . . . 7
⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐶) | 
| 46 | 41, 45 | csbied 3934 | . . . . . 6
⊢ (𝑦 = 𝑀 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐶) | 
| 47 | 40 | a1i 11 | . . . . . . 7
⊢ (𝑦 = 𝑁 → 𝑦 ∈ V) | 
| 48 |  | eqeq2 2748 | . . . . . . . . 9
⊢ (𝑦 = 𝑁 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑁)) | 
| 49 | 48 | biimpa 476 | . . . . . . . 8
⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑁) | 
| 50 |  | dvfsumabs.d | . . . . . . . 8
⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) | 
| 51 | 49, 50 | syl 17 | . . . . . . 7
⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐷) | 
| 52 | 47, 51 | csbied 3934 | . . . . . 6
⊢ (𝑦 = 𝑁 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐷) | 
| 53 | 34, 29, 46, 52, 4, 26 | telfsumo2 15840 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) = (𝐷 − 𝐶)) | 
| 54 | 53 | oveq2d 7448 | . . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) | 
| 55 | 39, 54 | eqtrd 2776 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) | 
| 56 | 55 | fveq2d 6909 | . 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) = (abs‘(Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶)))) | 
| 57 | 3, 38 | subcld 11621 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) ∈ ℂ) | 
| 58 | 2, 57 | fsumcl 15770 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) ∈ ℂ) | 
| 59 | 58 | abscld 15476 | . . 3
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ∈ ℝ) | 
| 60 | 57 | abscld 15476 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ∈ ℝ) | 
| 61 | 2, 60 | fsumrecl 15771 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ∈ ℝ) | 
| 62 |  | dvfsumabs.y | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℝ) | 
| 63 | 2, 62 | fsumrecl 15771 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑌 ∈ ℝ) | 
| 64 | 2, 57 | fsumabs 15838 | . . 3
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)(abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)))) | 
| 65 |  | elfzoelz 13700 | . . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ ℤ) | 
| 66 | 65 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℤ) | 
| 67 | 66 | zred 12724 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ) | 
| 68 | 67 | rexrd 11312 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ*) | 
| 69 |  | peano2re 11435 | . . . . . . . . 9
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) | 
| 70 | 67, 69 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℝ) | 
| 71 | 70 | rexrd 11312 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈
ℝ*) | 
| 72 | 67 | lep1d 12200 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ≤ (𝑘 + 1)) | 
| 73 |  | ubicc2 13506 | . . . . . . 7
⊢ ((𝑘 ∈ ℝ*
∧ (𝑘 + 1) ∈
ℝ* ∧ 𝑘
≤ (𝑘 + 1)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1))) | 
| 74 | 68, 71, 72, 73 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1))) | 
| 75 |  | lbicc2 13505 | . . . . . . 7
⊢ ((𝑘 ∈ ℝ*
∧ (𝑘 + 1) ∈
ℝ* ∧ 𝑘
≤ (𝑘 + 1)) → 𝑘 ∈ (𝑘[,](𝑘 + 1))) | 
| 76 | 68, 71, 72, 75 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ (𝑘[,](𝑘 + 1))) | 
| 77 | 6 | zred 12724 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 78 | 77 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ) | 
| 79 | 8 | zred 12724 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 80 | 79 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ) | 
| 81 |  | elfzole1 13708 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑘) | 
| 82 | 81 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑘) | 
| 83 | 28 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) | 
| 84 |  | elfzle2 13569 | . . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ≤ 𝑁) | 
| 85 | 83, 84 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ≤ 𝑁) | 
| 86 |  | iccss 13456 | . . . . . . . . . . 11
⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ (𝑀 ≤ 𝑘 ∧ (𝑘 + 1) ≤ 𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁)) | 
| 87 | 78, 80, 82, 85, 86 | syl22anc 838 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁)) | 
| 88 | 87 | resmptd 6057 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ↾ (𝑘[,](𝑘 + 1))) = (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) | 
| 89 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 90 | 89 | subcn 24889 | . . . . . . . . . . . 12
⊢  −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) | 
| 91 | 90 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → − ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) | 
| 92 |  | iccssre 13470 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀[,]𝑁) ⊆ ℝ) | 
| 93 | 77, 79, 92 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℝ) | 
| 95 |  | ax-resscn 11213 | . . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ | 
| 96 | 94, 95 | sstrdi 3995 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℂ) | 
| 97 |  | ssid 4005 | . . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ | 
| 98 | 97 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℂ ⊆
ℂ) | 
| 99 |  | cncfmptc 24939 | . . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℂ ∧ (𝑀[,]𝑁) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑥 ∈
(𝑀[,]𝑁) ↦ 𝑋) ∈ ((𝑀[,]𝑁)–cn→ℂ)) | 
| 100 | 3, 96, 98, 99 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝑋) ∈ ((𝑀[,]𝑁)–cn→ℂ)) | 
| 101 |  | cncfmptid 24940 | . . . . . . . . . . . . 13
⊢ (((𝑀[,]𝑁) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑥 ∈
(𝑀[,]𝑁) ↦ 𝑥) ∈ ((𝑀[,]𝑁)–cn→ℂ)) | 
| 102 | 96, 97, 101 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝑥) ∈ ((𝑀[,]𝑁)–cn→ℂ)) | 
| 103 | 100, 102 | mulcncf 25481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝑋 · 𝑥)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) | 
| 104 | 14 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℂ)) | 
| 105 | 89, 91, 103, 104 | cncfmpt2f 24942 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) | 
| 106 |  | rescncf 24924 | . . . . . . . . . 10
⊢ ((𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℂ))) | 
| 107 | 87, 105, 106 | sylc 65 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ ((𝑋 · 𝑥) − 𝐴)) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℂ)) | 
| 108 | 88, 107 | eqeltrrd 2841 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) ∈ ((𝑘[,](𝑘 + 1))–cn→ℂ)) | 
| 109 | 95 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ⊆
ℂ) | 
| 110 | 87, 94 | sstrd 3993 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ ℝ) | 
| 111 | 87 | sselda 3982 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘[,](𝑘 + 1))) → 𝑥 ∈ (𝑀[,]𝑁)) | 
| 112 | 3 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑋 ∈ ℂ) | 
| 113 | 96 | sselda 3982 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑥 ∈ ℂ) | 
| 114 | 112, 113 | mulcld 11282 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑋 · 𝑥) ∈ ℂ) | 
| 115 | 19 | r19.21bi 3250 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℂ) | 
| 116 | 115 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℂ) | 
| 117 | 114, 116 | subcld 11621 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((𝑋 · 𝑥) − 𝐴) ∈ ℂ) | 
| 118 | 111, 117 | syldan 591 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘[,](𝑘 + 1))) → ((𝑋 · 𝑥) − 𝐴) ∈ ℂ) | 
| 119 |  | tgioo4 24827 | . . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 120 |  | iccntr 24844 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑘[,](𝑘 + 1))) = (𝑘(,)(𝑘 + 1))) | 
| 121 | 67, 70, 120 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((int‘(topGen‘ran
(,)))‘(𝑘[,](𝑘 + 1))) = (𝑘(,)(𝑘 + 1))) | 
| 122 | 109, 110,
118, 119, 89, 121 | dvmptntr 26010 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (ℝ D (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))) | 
| 123 |  | reelprrecn 11248 | . . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} | 
| 124 | 123 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ∈ {ℝ,
ℂ}) | 
| 125 |  | ioossicc 13474 | . . . . . . . . . . . . . 14
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) | 
| 126 | 125 | sseli 3978 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁)) | 
| 127 | 126, 117 | sylan2 593 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → ((𝑋 · 𝑥) − 𝐴) ∈ ℂ) | 
| 128 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ (𝑋 − 𝐵) ∈ V | 
| 129 | 128 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝑋 − 𝐵) ∈ V) | 
| 130 | 126, 114 | sylan2 593 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝑋 · 𝑥) ∈ ℂ) | 
| 131 | 3 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝑋 ∈ ℂ) | 
| 132 | 125, 96 | sstrid 3994 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ⊆ ℂ) | 
| 133 | 132 | sselda 3982 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝑥 ∈ ℂ) | 
| 134 |  | 1cnd 11257 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 1 ∈ ℂ) | 
| 135 | 109 | sselda 3982 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) | 
| 136 |  | 1cnd 11257 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) | 
| 137 | 124 | dvmptid 25996 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) | 
| 138 | 125, 94 | sstrid 3994 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ⊆ ℝ) | 
| 139 |  | iooretop 24787 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀(,)𝑁) ∈ (topGen‘ran
(,)) | 
| 140 | 139 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ∈ (topGen‘ran
(,))) | 
| 141 | 124, 135,
136, 137, 138, 119, 89, 140 | dvmptres 26002 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝑥)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 1)) | 
| 142 | 124, 133,
134, 141, 3 | dvmptcmul 26003 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 𝑥))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 1))) | 
| 143 | 3 | mulridd 11279 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · 1) = 𝑋) | 
| 144 | 143 | mpteq2dv 5243 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 1)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝑋)) | 
| 145 | 142, 144 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 · 𝑥))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝑋)) | 
| 146 | 126, 116 | sylan2 593 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℂ) | 
| 147 |  | dvfsumabs.v | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) | 
| 148 | 147 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) | 
| 149 |  | dvfsumabs.b | . . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) | 
| 150 | 149 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) | 
| 151 | 124, 130,
131, 145, 146, 148, 150 | dvmptsub 26006 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝑋 − 𝐵))) | 
| 152 | 78 | rexrd 11312 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈
ℝ*) | 
| 153 |  | iooss1 13423 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ*
∧ 𝑀 ≤ 𝑘) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) | 
| 154 | 152, 82, 153 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) | 
| 155 | 80 | rexrd 11312 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈
ℝ*) | 
| 156 |  | iooss2 13424 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ*
∧ (𝑘 + 1) ≤ 𝑁) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) | 
| 157 | 155, 85, 156 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) | 
| 158 | 154, 157 | sstrd 3993 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) | 
| 159 |  | iooretop 24787 | . . . . . . . . . . . . 13
⊢ (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran
(,)) | 
| 160 | 159 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran
(,))) | 
| 161 | 124, 127,
129, 151, 158, 119, 89, 160 | dvmptres 26002 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) | 
| 162 | 122, 161 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) | 
| 163 | 162 | dmeqd 5915 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = dom (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) | 
| 164 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵)) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵)) | 
| 165 | 128, 164 | dmmpti 6711 | . . . . . . . . 9
⊢ dom
(𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵)) = (𝑘(,)(𝑘 + 1)) | 
| 166 | 163, 165 | eqtrdi 2792 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑘(,)(𝑘 + 1))) | 
| 167 | 162 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) = (𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))) | 
| 168 | 167 | fveq1d 6907 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → ((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥) = ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))‘𝑥)) | 
| 169 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝑥 ∈ (𝑘(,)(𝑘 + 1))) | 
| 170 | 164 | fvmpt2 7026 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ∧ (𝑋 − 𝐵) ∈ V) → ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))‘𝑥) = (𝑋 − 𝐵)) | 
| 171 | 169, 128,
170 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → ((𝑥 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 − 𝐵))‘𝑥) = (𝑋 − 𝐵)) | 
| 172 | 168, 171 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → ((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥) = (𝑋 − 𝐵)) | 
| 173 | 172 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) = (abs‘(𝑋 − 𝐵))) | 
| 174 |  | dvfsumabs.l | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → (abs‘(𝑋 − 𝐵)) ≤ 𝑌) | 
| 175 | 174 | anassrs 467 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘(𝑋 − 𝐵)) ≤ 𝑌) | 
| 176 | 173, 175 | eqbrtrd 5164 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌) | 
| 177 | 176 | ralrimiva 3145 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑘(,)(𝑘 + 1))(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌) | 
| 178 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥abs | 
| 179 |  | nfcv 2904 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥ℝ | 
| 180 |  | nfcv 2904 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥
D | 
| 181 |  | nfmpt1 5249 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) | 
| 182 | 179, 180,
181 | nfov 7462 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))) | 
| 183 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑦 | 
| 184 | 182, 183 | nffv 6915 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦) | 
| 185 | 178, 184 | nffv 6915 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) | 
| 186 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑥
≤ | 
| 187 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑥𝑌 | 
| 188 | 185, 186,
187 | nfbr 5189 | . . . . . . . . . 10
⊢
Ⅎ𝑥(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌 | 
| 189 |  | 2fveq3 6910 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) = (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦))) | 
| 190 | 189 | breq1d 5152 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌)) | 
| 191 | 188, 190 | rspc 3609 | . . . . . . . . 9
⊢ (𝑦 ∈ (𝑘(,)(𝑘 + 1)) → (∀𝑥 ∈ (𝑘(,)(𝑘 + 1))(abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑥)) ≤ 𝑌 → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌)) | 
| 192 | 177, 191 | mpan9 506 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → (abs‘((ℝ D (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)))‘𝑦)) ≤ 𝑌) | 
| 193 | 67, 70, 108, 166, 62, 192 | dvlip 26033 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ ((𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑘 ∈ (𝑘[,](𝑘 + 1)))) → (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) ≤ (𝑌 · (abs‘((𝑘 + 1) − 𝑘)))) | 
| 194 | 193 | ex 412 | . . . . . 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 7465 | . . . . . . . . 9
⊢ ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) ∈ V | 
| 197 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑥(𝑘 + 1) | 
| 198 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑋 · (𝑘 + 1)) | 
| 199 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑥
− | 
| 200 |  | nfcsb1v 3922 | . . . . . . . . . . 11
⊢
Ⅎ𝑥⦋(𝑘 + 1) / 𝑥⦌𝐴 | 
| 201 | 198, 199,
200 | nfov 7462 | . . . . . . . . . 10
⊢
Ⅎ𝑥((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) | 
| 202 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → (𝑋 · 𝑥) = (𝑋 · (𝑘 + 1))) | 
| 203 |  | csbeq1a 3912 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → 𝐴 = ⦋(𝑘 + 1) / 𝑥⦌𝐴) | 
| 204 | 202, 203 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑥 = (𝑘 + 1) → ((𝑋 · 𝑥) − 𝐴) = ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴)) | 
| 205 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) = (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴)) | 
| 206 | 197, 201,
204, 205 | fvmptf 7036 | . . . . . . . . 9
⊢ (((𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)) ∧ ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) ∈ V) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) = ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴)) | 
| 207 | 74, 196, 206 | sylancl 586 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) = ((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴)) | 
| 208 | 67 | recnd 11290 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℂ) | 
| 209 | 3, 208 | mulcld 11282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · 𝑘) ∈ ℂ) | 
| 210 | 209, 37 | subcld 11621 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℂ) | 
| 211 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑥𝑘 | 
| 212 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑋 · 𝑘) | 
| 213 |  | nfcsb1v 3922 | . . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑘 / 𝑥⦌𝐴 | 
| 214 | 212, 199,
213 | nfov 7462 | . . . . . . . . . 10
⊢
Ⅎ𝑥((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴) | 
| 215 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → (𝑋 · 𝑥) = (𝑋 · 𝑘)) | 
| 216 |  | csbeq1a 3912 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → 𝐴 = ⦋𝑘 / 𝑥⦌𝐴) | 
| 217 | 215, 216 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑥 = 𝑘 → ((𝑋 · 𝑥) − 𝐴) = ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴)) | 
| 218 | 211, 214,
217, 205 | fvmptf 7036 | . . . . . . . . 9
⊢ ((𝑘 ∈ (𝑘[,](𝑘 + 1)) ∧ ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℂ) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘) = ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴)) | 
| 219 | 76, 210, 218 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘) = ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴)) | 
| 220 | 207, 219 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘)) = (((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) − ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴))) | 
| 221 |  | peano2cn 11434 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → (𝑘 + 1) ∈
ℂ) | 
| 222 | 208, 221 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℂ) | 
| 223 | 3, 222 | mulcld 11282 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · (𝑘 + 1)) ∈ ℂ) | 
| 224 | 223, 209,
32, 37 | sub4d 11670 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (((𝑋 · (𝑘 + 1)) − ⦋(𝑘 + 1) / 𝑥⦌𝐴) − ((𝑋 · 𝑘) − ⦋𝑘 / 𝑥⦌𝐴))) | 
| 225 |  | 1cnd 11257 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 1 ∈ ℂ) | 
| 226 | 208, 225 | pncan2d 11623 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑘 + 1) − 𝑘) = 1) | 
| 227 | 226 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = (𝑋 · 1)) | 
| 228 | 3, 222, 208 | subdid 11720 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘))) | 
| 229 | 227, 228,
143 | 3eqtr3d 2784 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) = 𝑋) | 
| 230 | 229 | oveq1d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) | 
| 231 | 220, 224,
230 | 3eqtr2rd 2783 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) = (((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘))) | 
| 232 | 231 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) = (abs‘(((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘(𝑘 + 1)) − ((𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ ((𝑋 · 𝑥) − 𝐴))‘𝑘)))) | 
| 233 | 226 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘((𝑘 + 1) − 𝑘)) = (abs‘1)) | 
| 234 |  | abs1 15337 | . . . . . . . 8
⊢
(abs‘1) = 1 | 
| 235 | 233, 234 | eqtrdi 2792 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘((𝑘 + 1) − 𝑘)) = 1) | 
| 236 | 235 | oveq2d 7448 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑌 · (abs‘((𝑘 + 1) − 𝑘))) = (𝑌 · 1)) | 
| 237 | 62 | recnd 11290 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 ∈ ℂ) | 
| 238 | 237 | mulridd 11279 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑌 · 1) = 𝑌) | 
| 239 | 236, 238 | eqtr2d 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑌 = (𝑌 · (abs‘((𝑘 + 1) − 𝑘)))) | 
| 240 | 195, 232,
239 | 3brtr4d 5174 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ 𝑌) | 
| 241 | 2, 60, 62, 240 | fsumle 15836 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(abs‘(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌) | 
| 242 | 59, 61, 63, 64, 241 | letrd 11419 | . 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈ (𝑀..^𝑁)(𝑋 − (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌) | 
| 243 | 56, 242 | eqbrtrrd 5166 | 1
⊢ (𝜑 → (abs‘(Σ𝑘 ∈ (𝑀..^𝑁)𝑋 − (𝐷 − 𝐶))) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑌) |