| Step | Hyp | Ref
| Expression |
| 1 | | dvfsum.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑇(,)+∞) |
| 2 | | ioossre 13448 |
. . . . . . . . 9
⊢ (𝑇(,)+∞) ⊆
ℝ |
| 3 | 1, 2 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℝ |
| 4 | | dvfsumlem1.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝑆) |
| 5 | 3, 4 | sselid 3981 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 6 | | dvfsumlem1.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
| 7 | 6, 1 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝑇(,)+∞)) |
| 8 | | dvfsum.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 9 | 8 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈
ℝ*) |
| 10 | | elioopnf 13483 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ ℝ*
→ (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
| 12 | 7, 11 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)) |
| 13 | 12 | simpld 494 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 14 | | reflcl 13836 |
. . . . . . . 8
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ∈
ℝ) |
| 15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (⌊‘𝑋) ∈
ℝ) |
| 16 | 5, 15 | resubcld 11691 |
. . . . . 6
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℝ) |
| 17 | | csbeq1 3902 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
| 18 | 17 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ)) |
| 19 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
| 20 | | dvfsum.a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
| 21 | | dvfsum.b1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
| 22 | | dvfsum.b3 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
| 23 | 19, 20, 21, 22 | dvmptrecl 26064 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) |
| 24 | 23 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
| 25 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝐵 |
| 26 | | nfcsb1v 3923 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
| 27 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
| 28 | 25, 26, 27 | cbvmpt 5253 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐵) |
| 29 | 28 | fmpt 7130 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑆 ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
| 30 | 24, 29 | sylibr 234 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
| 31 | 18, 30, 4 | rspcdva 3623 |
. . . . . 6
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ) |
| 32 | 16, 31 | remulcld 11291 |
. . . . 5
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
| 33 | | csbeq1 3902 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑌 / 𝑥⦌𝐴) |
| 34 | 33 | eleq1d 2826 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)) |
| 35 | 20 | fmpttd 7135 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ) |
| 36 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐴 |
| 37 | | nfcsb1v 3923 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 |
| 38 | | csbeq1a 3913 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴) |
| 39 | 36, 37, 38 | cbvmpt 5253 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑆 ↦ 𝐴) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) |
| 40 | 39 | fmpt 7130 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑆 ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ) |
| 41 | 35, 40 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
| 42 | 34, 41, 4 | rspcdva 3623 |
. . . . 5
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ) |
| 43 | 32, 42 | resubcld 11691 |
. . . 4
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
| 44 | 13, 15 | resubcld 11691 |
. . . . . 6
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ) |
| 45 | | csbeq1 3902 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
| 46 | 45 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) |
| 47 | 46, 30, 6 | rspcdva 3623 |
. . . . . 6
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ) |
| 48 | 44, 47 | remulcld 11291 |
. . . . 5
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
| 49 | | csbeq1 3902 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑋 / 𝑥⦌𝐴) |
| 50 | 49 | eleq1d 2826 |
. . . . . 6
⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)) |
| 51 | 50, 41, 6 | rspcdva 3623 |
. . . . 5
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ) |
| 52 | 48, 51 | resubcld 11691 |
. . . 4
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
| 53 | | fzfid 14014 |
. . . . 5
⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin) |
| 54 | | dvfsum.b2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
| 55 | 54 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ) |
| 56 | | elfzuz 13560 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 57 | | dvfsum.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 58 | 56, 57 | eleqtrrdi 2852 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍) |
| 59 | | dvfsum.c |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) |
| 60 | 59 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
| 61 | 60 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ) |
| 62 | 55, 58, 61 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ) |
| 63 | 53, 62 | fsumrecl 15770 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ) |
| 64 | 44, 31 | remulcld 11291 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
| 65 | 64, 51 | resubcld 11691 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
| 66 | 5, 13 | resubcld 11691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℝ) |
| 67 | 31, 66 | remulcld 11291 |
. . . . . . . 8
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℝ) |
| 68 | 31 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
| 69 | 5 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℂ) |
| 70 | 13 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
| 71 | 68, 69, 70 | subdid 11719 |
. . . . . . . . 9
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) = ((⦋𝑌 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑌 / 𝑥⦌𝐵 · 𝑋))) |
| 72 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 73 | 72 | mulcn 24889 |
. . . . . . . . . . 11
⊢ ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
| 74 | | pnfxr 11315 |
. . . . . . . . . . . . . . . 16
⊢ +∞
∈ ℝ* |
| 75 | 74 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 76 | 12 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 < 𝑋) |
| 77 | 5 | ltpnfd 13163 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 < +∞) |
| 78 | | iccssioo 13456 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (𝑇 < 𝑋 ∧ 𝑌 < +∞)) → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞)) |
| 79 | 9, 75, 76, 77, 78 | syl22anc 839 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞)) |
| 80 | 79, 2 | sstrdi 3996 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
| 81 | | ax-resscn 11212 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
| 82 | 80, 81 | sstrdi 3996 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℂ) |
| 83 | 81 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 84 | | cncfmptc 24938 |
. . . . . . . . . . . 12
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 85 | 31, 82, 83, 84 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 86 | | cncfmptid 24939 |
. . . . . . . . . . . 12
⊢ (((𝑋[,]𝑌) ⊆ ℝ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 87 | 80, 81, 86 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 88 | | remulcl 11240 |
. . . . . . . . . . 11
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑌 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ) |
| 89 | 72, 73, 85, 87, 81, 88 | cncfmpt2ss 24942 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 90 | | reelprrecn 11247 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
| 91 | 90 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 92 | | ioossicc 13473 |
. . . . . . . . . . . . . . 15
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
| 93 | 92, 80 | sstrid 3995 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ ℝ) |
| 94 | 93 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ) |
| 95 | 94 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ) |
| 96 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 1 ∈ ℂ) |
| 97 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
| 98 | 97 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
| 99 | | 1cnd 11256 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
| 100 | 91 | dvmptid 25995 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
| 101 | 72 | tgioo2 24824 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 102 | | iooretop 24786 |
. . . . . . . . . . . . . 14
⊢ (𝑋(,)𝑌) ∈ (topGen‘ran
(,)) |
| 103 | 102 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋(,)𝑌) ∈ (topGen‘ran
(,))) |
| 104 | 91, 98, 99, 100, 93, 101, 72, 103 | dvmptres 26001 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 1)) |
| 105 | 91, 95, 96, 104, 68 | dvmptcmul 26002 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 1))) |
| 106 | 68 | mulridd 11278 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · 1) = ⦋𝑌 / 𝑥⦌𝐵) |
| 107 | 106 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵)) |
| 108 | 105, 107 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵)) |
| 109 | 79, 1 | sseqtrrdi 4025 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ 𝑆) |
| 110 | 109 | resmptd 6058 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) = (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴)) |
| 111 | 20 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
| 112 | 111 | fmpttd 7135 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
| 113 | 22 | dmeqd 5916 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = dom (𝑥 ∈ 𝑆 ↦ 𝐵)) |
| 114 | 21 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ 𝑉) |
| 115 | | dmmptg 6262 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
𝑆 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑆 ↦ 𝐵) = 𝑆) |
| 116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑥 ∈ 𝑆 ↦ 𝐵) = 𝑆) |
| 117 | 113, 116 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = 𝑆) |
| 118 | | dvcn 25957 |
. . . . . . . . . . . . . . . 16
⊢
(((ℝ ⊆ ℂ ∧ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ ∧ 𝑆 ⊆ ℝ) ∧ dom (ℝ D
(𝑥 ∈ 𝑆 ↦ 𝐴)) = 𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) |
| 119 | 83, 112, 19, 117, 118 | syl31anc 1375 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) |
| 120 | | cncfcdm 24924 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) → ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ)) |
| 121 | 81, 119, 120 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ)) |
| 122 | 35, 121 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ)) |
| 123 | 39, 122 | eqeltrrid 2846 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ (𝑆–cn→ℝ)) |
| 124 | | rescncf 24923 |
. . . . . . . . . . . 12
⊢ ((𝑋[,]𝑌) ⊆ 𝑆 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ (𝑆–cn→ℝ) → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ))) |
| 125 | 109, 123,
124 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 126 | 110, 125 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 127 | 41 | r19.21bi 3251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
| 128 | 127 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
| 129 | 30 | r19.21bi 3251 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
| 130 | 39 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (ℝ
D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴)) |
| 131 | 22, 130, 28 | 3eqtr3g 2800 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐵)) |
| 132 | 92, 109 | sstrid 3995 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ 𝑆) |
| 133 | 91, 128, 129, 131, 132, 101, 72, 103 | dvmptres 26001 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐵)) |
| 134 | 92 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑋(,)𝑌) → 𝑦 ∈ (𝑋[,]𝑌)) |
| 135 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝜑) |
| 136 | 109 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ 𝑆) |
| 137 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈ 𝑆) |
| 138 | | dvfsum.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 139 | 138 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ∈ ℝ) |
| 140 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ ℝ) |
| 141 | | elicc2 13452 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌))) |
| 142 | 13, 5, 141 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌))) |
| 143 | 142 | biimpa 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌)) |
| 144 | 143 | simp1d 1143 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ) |
| 145 | | dvfsumlem1.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ≤ 𝑋) |
| 146 | 145 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ≤ 𝑋) |
| 147 | 143 | simp2d 1144 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ≤ 𝑦) |
| 148 | 139, 140,
144, 146, 147 | letrd 11418 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ≤ 𝑦) |
| 149 | 143 | simp3d 1145 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ≤ 𝑌) |
| 150 | | dvfsumlem1.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ≤ 𝑈) |
| 151 | 150 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ≤ 𝑈) |
| 152 | | simp2r 1201 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → 𝑌 ∈ 𝑆) |
| 153 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑘 ∈ 𝑆 ↔ 𝑌 ∈ 𝑆)) |
| 154 | 153 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → ((𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆))) |
| 155 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑦 ≤ 𝑘 ↔ 𝑦 ≤ 𝑌)) |
| 156 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑘 ≤ 𝑈 ↔ 𝑌 ≤ 𝑈)) |
| 157 | 155, 156 | 3anbi23d 1441 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → ((𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈))) |
| 158 | 154, 157 | 3anbi23d 1441 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑌 → ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)))) |
| 159 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑘 ∈ V |
| 160 | 159, 59 | csbie 3934 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝑘 /
𝑥⦌𝐵 = 𝐶 |
| 161 | | csbeq1 3902 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → ⦋𝑘 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
| 162 | 160, 161 | eqtr3id 2791 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → 𝐶 = ⦋𝑌 / 𝑥⦌𝐵) |
| 163 | 162 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑌 → (𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵 ↔ ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
| 164 | 158, 163 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑌 → (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) ↔ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵))) |
| 165 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) |
| 166 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐶 |
| 167 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥
≤ |
| 168 | 166, 167,
26 | nfbr 5190 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵 |
| 169 | 165, 168 | nfim 1896 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
| 170 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆)) |
| 171 | 170 | anbi1d 631 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆))) |
| 172 | | breq2 5147 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑦)) |
| 173 | | breq1 5146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑘 ↔ 𝑦 ≤ 𝑘)) |
| 174 | 172, 173 | 3anbi12d 1439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈))) |
| 175 | 171, 174 | 3anbi23d 1441 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)))) |
| 176 | 27 | breq2d 5155 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
| 177 | 175, 176 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵))) |
| 178 | | dvfsum.l |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) |
| 179 | 169, 177,
178 | chvarfv 2240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
| 180 | 164, 179 | vtoclg 3554 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝑆 → ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
| 181 | 152, 180 | mpcom 38 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
| 182 | 135, 136,
137, 148, 149, 151, 181 | syl123anc 1389 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
| 183 | 134, 182 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
| 184 | 13 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
| 185 | 5 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
| 186 | | dvfsumlem1.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
| 187 | | lbicc2 13504 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌)) |
| 188 | 184, 185,
186, 187 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌)) |
| 189 | | ubicc2 13505 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌)) |
| 190 | 184, 185,
186, 189 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌)) |
| 191 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑋)) |
| 192 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑌)) |
| 193 | 13, 5, 89, 108, 126, 133, 183, 188, 190, 186, 191, 49, 192, 33 | dvle 26046 |
. . . . . . . . 9
⊢ (𝜑 → ((⦋𝑌 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑌 / 𝑥⦌𝐵 · 𝑋)) ≤ (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴)) |
| 194 | 71, 193 | eqbrtrd 5165 |
. . . . . . . 8
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ≤ (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴)) |
| 195 | 67, 42, 51, 194 | lesubd 11867 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ≤ (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
| 196 | 64 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
| 197 | 32 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
| 198 | 42 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ) |
| 199 | 196, 197,
198 | subsubd 11648 |
. . . . . . . 8
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴)) |
| 200 | 197, 196 | negsubdi2d 11636 |
. . . . . . . . . . 11
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵))) |
| 201 | 15 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘𝑋) ∈
ℂ) |
| 202 | 69, 70, 201 | nnncan2d 11655 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) = (𝑌 − 𝑋)) |
| 203 | 202 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · ⦋𝑌 / 𝑥⦌𝐵) = ((𝑌 − 𝑋) · ⦋𝑌 / 𝑥⦌𝐵)) |
| 204 | 16 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℂ) |
| 205 | 44 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ) |
| 206 | 204, 205,
68 | subdird 11720 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵))) |
| 207 | 66 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℂ) |
| 208 | 207, 68 | mulcomd 11282 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − 𝑋) · ⦋𝑌 / 𝑥⦌𝐵) = (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
| 209 | 203, 206,
208 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
| 210 | 209 | negeqd 11502 |
. . . . . . . . . . 11
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = -(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
| 211 | 200, 210 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = -(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
| 212 | 211 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = (-(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) + ⦋𝑌 / 𝑥⦌𝐴)) |
| 213 | 67 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℂ) |
| 214 | 213, 198 | negsubdid 11635 |
. . . . . . . . 9
⊢ (𝜑 → -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴) = (-(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) + ⦋𝑌 / 𝑥⦌𝐴)) |
| 215 | 212, 214 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴)) |
| 216 | 213, 198 | negsubdi2d 11636 |
. . . . . . . 8
⊢ (𝜑 → -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
| 217 | 199, 215,
216 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
| 218 | 195, 217 | breqtrrd 5171 |
. . . . . 6
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴))) |
| 219 | 51, 64, 43, 218 | lesubd 11867 |
. . . . 5
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
| 220 | | flle 13839 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ≤
𝑋) |
| 221 | 13, 220 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘𝑋) ≤ 𝑋) |
| 222 | 13, 15 | subge0d 11853 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝑋 − (⌊‘𝑋)) ↔ (⌊‘𝑋) ≤ 𝑋)) |
| 223 | 221, 222 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋))) |
| 224 | 45 | breq2d 5155 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → (⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵 ↔ ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
| 225 | 182 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
| 226 | 224, 225,
188 | rspcdva 3623 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
| 227 | 31, 47, 44, 223, 226 | lemul2ad 12208 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵)) |
| 228 | 64, 48, 51, 227 | lesub1dd 11879 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
| 229 | 43, 65, 52, 219, 228 | letrd 11418 |
. . . 4
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
| 230 | 43, 52, 63, 229 | leadd1dd 11877 |
. . 3
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
| 231 | | dvfsum.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 232 | | dvfsum.md |
. . . 4
⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) |
| 233 | | dvfsum.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈
ℝ*) |
| 234 | | dvfsum.h |
. . . 4
⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) |
| 235 | | dvfsumlem1.6 |
. . . 4
⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) |
| 236 | 1, 57, 231, 138, 232, 8, 20, 21, 54, 22, 59, 233, 178, 234, 6, 4, 145, 186, 150, 235 | dvfsumlem1 26066 |
. . 3
⊢ (𝜑 → (𝐻‘𝑌) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
| 237 | 13 | leidd 11829 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ 𝑋) |
| 238 | 184, 185,
233, 186, 150 | xrletrd 13204 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ 𝑈) |
| 239 | | fllep1 13841 |
. . . . 5
⊢ (𝑋 ∈ ℝ → 𝑋 ≤ ((⌊‘𝑋) + 1)) |
| 240 | 13, 239 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ ((⌊‘𝑋) + 1)) |
| 241 | 1, 57, 231, 138, 232, 8, 20, 21, 54, 22, 59, 233, 178, 234, 6, 6, 145, 237, 238, 240 | dvfsumlem1 26066 |
. . 3
⊢ (𝜑 → (𝐻‘𝑋) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
| 242 | 230, 236,
241 | 3brtr4d 5175 |
. 2
⊢ (𝜑 → (𝐻‘𝑌) ≤ (𝐻‘𝑋)) |
| 243 | 52, 47 | resubcld 11691 |
. . . . 5
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
| 244 | 43, 31 | resubcld 11691 |
. . . . 5
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
| 245 | | peano2rem 11576 |
. . . . . . . . . . 11
⊢ ((𝑋 − (⌊‘𝑋)) ∈ ℝ → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℝ) |
| 246 | 44, 245 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℝ) |
| 247 | 246, 47 | remulcld 11291 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
| 248 | 247, 51 | resubcld 11691 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
| 249 | | peano2rem 11576 |
. . . . . . . . . . 11
⊢ ((𝑌 − (⌊‘𝑋)) ∈ ℝ → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
| 250 | 16, 249 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
| 251 | 250, 47 | remulcld 11291 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
| 252 | 251, 42 | resubcld 11691 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
| 253 | 250, 31 | remulcld 11291 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
| 254 | 253, 42 | resubcld 11691 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
| 255 | 247 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
| 256 | 251 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
| 257 | 255, 256 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) ∈ ℂ) |
| 258 | 257, 198 | addcomd 11463 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
| 259 | 255, 256,
198 | subsubd 11648 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴)) |
| 260 | 198, 256,
255 | subsub2d 11649 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) = (⦋𝑌 / 𝑥⦌𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
| 261 | 258, 259,
260 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
| 262 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℂ) |
| 263 | 204, 205,
262 | nnncan2d 11655 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋)))) |
| 264 | 263, 202 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = (𝑌 − 𝑋)) |
| 265 | 264 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · ⦋𝑋 / 𝑥⦌𝐵) = ((𝑌 − 𝑋) · ⦋𝑋 / 𝑥⦌𝐵)) |
| 266 | 250 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℂ) |
| 267 | 246 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℂ) |
| 268 | 47 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ) |
| 269 | 266, 267,
268 | subdird 11720 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · ⦋𝑋 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) |
| 270 | 207, 268 | mulcomd 11282 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − 𝑋) · ⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
| 271 | 265, 269,
270 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) = (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
| 272 | 271 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
| 273 | 261, 272 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
| 274 | 47, 66 | remulcld 11291 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℝ) |
| 275 | | cncfmptc 24938 |
. . . . . . . . . . . . . . 15
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 276 | 47, 82, 83, 275 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 277 | | remulcl 11240 |
. . . . . . . . . . . . . 14
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑋 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ) |
| 278 | 72, 73, 276, 87, 81, 277 | cncfmpt2ss 24942 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
| 279 | 91, 95, 96, 104, 268 | dvmptcmul 26002 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 1))) |
| 280 | 268 | mulridd 11278 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · 1) = ⦋𝑋 / 𝑥⦌𝐵) |
| 281 | 280 | mpteq2dv 5244 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵)) |
| 282 | 279, 281 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵)) |
| 283 | 6 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ 𝑆) |
| 284 | 144 | rexrd 11311 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ*) |
| 285 | 185 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈
ℝ*) |
| 286 | 233 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑈 ∈
ℝ*) |
| 287 | 284, 285,
286, 149, 151 | xrletrd 13204 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ≤ 𝑈) |
| 288 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
| 289 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆)) |
| 290 | 289 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → ((𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆))) |
| 291 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑋 ≤ 𝑘 ↔ 𝑋 ≤ 𝑦)) |
| 292 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑘 ≤ 𝑈 ↔ 𝑦 ≤ 𝑈)) |
| 293 | 291, 292 | 3anbi23d 1441 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → ((𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈))) |
| 294 | 290, 293 | 3anbi23d 1441 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)))) |
| 295 | | csbeq1 3902 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → ⦋𝑘 / 𝑥⦌𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
| 296 | 160, 295 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐵) |
| 297 | 296 | breq1d 5153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → (𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
| 298 | 294, 297 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑦 → (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) ↔ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
| 299 | | simp2l 1200 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝑋 ∈ 𝑆) |
| 300 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) |
| 301 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵 |
| 302 | 166, 167,
301 | nfbr 5190 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵 |
| 303 | 300, 302 | nfim 1896 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
| 304 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆)) |
| 305 | 304 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → ((𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆))) |
| 306 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋)) |
| 307 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑘 ↔ 𝑋 ≤ 𝑘)) |
| 308 | 306, 307 | 3anbi12d 1439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈))) |
| 309 | 305, 308 | 3anbi23d 1441 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)))) |
| 310 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
| 311 | 310 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → (𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
| 312 | 309, 311 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
| 313 | 303, 312,
178 | vtoclg1f 3570 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ 𝑆 → ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
| 314 | 299, 313 | mpcom 38 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
| 315 | 288, 298,
314 | vtocl 3558 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
| 316 | 135, 283,
136, 146, 147, 287, 315 | syl123anc 1389 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
| 317 | 134, 316 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
| 318 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑋)) |
| 319 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑌)) |
| 320 | 13, 5, 126, 133, 278, 282, 317, 188, 190, 186, 49, 318, 33, 319 | dvle 26046 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((⦋𝑋 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑋 / 𝑥⦌𝐵 · 𝑋))) |
| 321 | 268, 69, 70 | subdid 11719 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) = ((⦋𝑋 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑋 / 𝑥⦌𝐵 · 𝑋))) |
| 322 | 320, 321 | breqtrrd 5171 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
| 323 | 42, 51, 274, 322 | subled 11866 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐴) |
| 324 | 273, 323 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) ≤ ⦋𝑋 / 𝑥⦌𝐴) |
| 325 | 247, 252,
51, 324 | subled 11866 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
| 326 | 250 | renegcld 11690 |
. . . . . . . . . . . 12
⊢ (𝜑 → -((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
| 327 | | 1red 11262 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) |
| 328 | 5, 15, 327 | lesubadd2d 11862 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) ≤ 1 ↔ 𝑌 ≤ ((⌊‘𝑋) + 1))) |
| 329 | 235, 328 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ≤ 1) |
| 330 | 16, 327 | suble0d 11854 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ (𝑌 − (⌊‘𝑋)) ≤ 1)) |
| 331 | 329, 330 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ≤ 0) |
| 332 | 250 | le0neg1d 11834 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1))) |
| 333 | 331, 332 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1)) |
| 334 | 31, 47, 326, 333, 226 | lemul2ad 12208 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
| 335 | 266, 68 | mulneg1d 11716 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵)) |
| 336 | 266, 268 | mulneg1d 11716 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
| 337 | 334, 335,
336 | 3brtr3d 5174 |
. . . . . . . . . 10
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
| 338 | 251, 253 | lenegd 11842 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ↔ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) |
| 339 | 337, 338 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵)) |
| 340 | 251, 253,
42, 339 | lesub1dd 11879 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
| 341 | 248, 252,
254, 325, 340 | letrd 11418 |
. . . . . . 7
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
| 342 | 205, 262,
268 | subdird 11720 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − (1 · ⦋𝑋 / 𝑥⦌𝐵))) |
| 343 | 268 | mullidd 11279 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵) |
| 344 | 343 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − (1 · ⦋𝑋 / 𝑥⦌𝐵)) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵)) |
| 345 | 342, 344 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵)) |
| 346 | 345 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
| 347 | 204, 262,
68 | subdird 11720 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵))) |
| 348 | 68 | mullidd 11279 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
⦋𝑌 / 𝑥⦌𝐵) = ⦋𝑌 / 𝑥⦌𝐵) |
| 349 | 348 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 350 | 347, 349 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 351 | 350 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
| 352 | 341, 346,
351 | 3brtr3d 5174 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
| 353 | 48 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
| 354 | 51 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℂ) |
| 355 | 353, 354,
268 | sub32d 11652 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
| 356 | 197, 198,
68 | sub32d 11652 |
. . . . . 6
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
| 357 | 352, 355,
356 | 3brtr4d 5175 |
. . . . 5
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 358 | 243, 244,
63, 357 | leadd1dd 11877 |
. . . 4
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
| 359 | 52 | recnd 11289 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ) |
| 360 | 63 | recnd 11289 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ) |
| 361 | 359, 360,
268 | addsubd 11641 |
. . . 4
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵) = (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
| 362 | 43 | recnd 11289 |
. . . . 5
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ) |
| 363 | 362, 360,
68 | addsubd 11641 |
. . . 4
⊢ (𝜑 → (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵) = (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
| 364 | 358, 361,
363 | 3brtr4d 5175 |
. . 3
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 365 | 241 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) = (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵)) |
| 366 | 236 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵) = (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 367 | 364, 365,
366 | 3brtr4d 5175 |
. 2
⊢ (𝜑 → ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 368 | 242, 367 | jca 511 |
1
⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) |