Proof of Theorem dnibndlem9
| Step | Hyp | Ref
| Expression |
| 1 | | dnibndlem9.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 2 | 1 | dnicld1 36473 |
. . . . . . 7
⊢ (𝜑 →
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℝ) |
| 3 | 2 | recnd 11289 |
. . . . . 6
⊢ (𝜑 →
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℂ) |
| 4 | | dnibndlem9.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 5 | 4 | dnicld1 36473 |
. . . . . . 7
⊢ (𝜑 →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) |
| 6 | 5 | recnd 11289 |
. . . . . 6
⊢ (𝜑 →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℂ) |
| 7 | 3, 6 | subcld 11620 |
. . . . 5
⊢ (𝜑 →
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∈
ℂ) |
| 8 | 7 | abscld 15475 |
. . . 4
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ∈
ℝ) |
| 9 | | halfre 12480 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
| 10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
| 11 | 10, 2 | jca 511 |
. . . . . 6
⊢ (𝜑 → ((1 / 2) ∈ ℝ
∧ (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℝ)) |
| 12 | | resubcl 11573 |
. . . . . 6
⊢ (((1 / 2)
∈ ℝ ∧ (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℝ) → ((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ∈ ℝ) |
| 13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → ((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ∈ ℝ) |
| 14 | 10, 5 | jca 511 |
. . . . . 6
⊢ (𝜑 → ((1 / 2) ∈ ℝ
∧ (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ)) |
| 15 | | resubcl 11573 |
. . . . . 6
⊢ (((1 / 2)
∈ ℝ ∧ (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) → ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∈ ℝ) |
| 16 | 14, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∈ ℝ) |
| 17 | 13, 16 | readdcld 11290 |
. . . 4
⊢ (𝜑 → (((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ∈ ℝ) |
| 18 | 1 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 19 | 1, 10 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 + (1 / 2)) ∈ ℝ) |
| 20 | | reflcl 13836 |
. . . . . . . . . 10
⊢ ((𝐵 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐵 +
(1 / 2))) ∈ ℝ) |
| 21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) ∈
ℝ) |
| 22 | 21 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) ∈
ℂ) |
| 23 | 10 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
| 24 | 22, 23 | subcld 11620 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
∈ ℂ) |
| 25 | 18, 24 | subcld 11620 |
. . . . . 6
⊢ (𝜑 → (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) ∈
ℂ) |
| 26 | 4, 10 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (1 / 2)) ∈ ℝ) |
| 27 | | reflcl 13836 |
. . . . . . . . . 10
⊢ ((𝐴 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐴 +
(1 / 2))) ∈ ℝ) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ∈
ℝ) |
| 29 | 28 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ∈
ℂ) |
| 30 | 29, 23 | addcld 11280 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) ∈
ℂ) |
| 31 | 4 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 32 | 30, 31 | subcld 11620 |
. . . . . 6
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) −
𝐴) ∈
ℂ) |
| 33 | 25, 32 | addcld 11280 |
. . . . 5
⊢ (𝜑 → ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))
∈ ℂ) |
| 34 | 33 | abscld 15475 |
. . . 4
⊢ (𝜑 → (abs‘((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))) ∈ ℝ) |
| 35 | 4, 1 | dnibndlem6 36484 |
. . . 4
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))) |
| 36 | 21, 10 | jca 511 |
. . . . . . . . 9
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) ∈ ℝ
∧ (1 / 2) ∈ ℝ)) |
| 37 | | resubcl 11573 |
. . . . . . . . 9
⊢
(((⌊‘(𝐵
+ (1 / 2))) ∈ ℝ ∧ (1 / 2) ∈ ℝ) →
((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) ∈ ℝ) |
| 38 | 36, 37 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
∈ ℝ) |
| 39 | 1, 38 | jca 511 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))
∈ ℝ)) |
| 40 | | resubcl 11573 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧
((⌊‘(𝐵 + (1 /
2))) − (1 / 2)) ∈ ℝ) → (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) ∈
ℝ) |
| 41 | 39, 40 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) ∈
ℝ) |
| 42 | 28, 10 | readdcld 11290 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) ∈
ℝ) |
| 43 | 42, 4 | jca 511 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) ∈
ℝ ∧ 𝐴 ∈
ℝ)) |
| 44 | | resubcl 11573 |
. . . . . . 7
⊢
((((⌊‘(𝐴
+ (1 / 2))) + (1 / 2)) ∈ ℝ ∧ 𝐴 ∈ ℝ) →
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)
∈ ℝ) |
| 45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) −
𝐴) ∈
ℝ) |
| 46 | 1 | dnibndlem7 36485 |
. . . . . 6
⊢ (𝜑 → ((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 /
2)))) |
| 47 | 4 | dnibndlem8 36486 |
. . . . . 6
⊢ (𝜑 → ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)) |
| 48 | 13, 16, 41, 45, 46, 47 | le2addd 11882 |
. . . . 5
⊢ (𝜑 → (((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))) |
| 49 | 41, 45 | readdcld 11290 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))
∈ ℝ) |
| 50 | | dnibndlem4 36482 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → 0 ≤
(𝐵 −
((⌊‘(𝐵 + (1 /
2))) − (1 / 2)))) |
| 51 | 1, 50 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 /
2)))) |
| 52 | | 0red 11264 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
| 53 | | dnibndlem5 36483 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 0 <
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)) |
| 54 | 4, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 <
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)) |
| 55 | 52, 45, 54 | ltled 11409 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)) |
| 56 | 41, 45, 51, 55 | addge0d 11839 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))) |
| 57 | 49, 56 | absidd 15461 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))) = ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))) |
| 58 | 57 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → ((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))
= (abs‘((𝐵 −
((⌊‘(𝐵 + (1 /
2))) − (1 / 2))) + (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴)))) |
| 59 | 48, 58 | breqtrd 5169 |
. . . 4
⊢ (𝜑 → (((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (abs‘((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)))) |
| 60 | 8, 17, 34, 35, 59 | letrd 11418 |
. . 3
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (abs‘((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)))) |
| 61 | | dnibndlem9.1 |
. . . . 5
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
| 62 | | dnibndlem9.4 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) =
((⌊‘(𝐴 + (1 /
2))) + 1)) |
| 63 | 61, 4, 1, 62 | dnibndlem3 36481 |
. . . 4
⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (abs‘((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴)))) |
| 64 | 63 | eqcomd 2743 |
. . 3
⊢ (𝜑 → (abs‘((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) +
(((⌊‘(𝐴 + (1 /
2))) + (1 / 2)) − 𝐴))) = (abs‘(𝐵 − 𝐴))) |
| 65 | 60, 64 | breqtrd 5169 |
. 2
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (abs‘(𝐵 − 𝐴))) |
| 66 | 61, 4, 1 | dnibndlem1 36479 |
. 2
⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)) ↔
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (abs‘(𝐵 − 𝐴)))) |
| 67 | 65, 66 | mpbird 257 |
1
⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴))) |