Proof of Theorem dnibndlem11
| Step | Hyp | Ref
| Expression |
| 1 | | dnibndlem11.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 2 | 1 | dnicld1 36473 |
. . . . 5
⊢ (𝜑 →
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℝ) |
| 3 | | dnibndlem11.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 4 | 3 | dnicld1 36473 |
. . . . 5
⊢ (𝜑 →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) |
| 5 | 2, 4 | resubcld 11691 |
. . . 4
⊢ (𝜑 →
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∈
ℝ) |
| 6 | | halfre 12480 |
. . . . 5
⊢ (1 / 2)
∈ ℝ |
| 7 | 6 | a1i 11 |
. . . 4
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
| 8 | 2 | recnd 11289 |
. . . . . 6
⊢ (𝜑 →
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℂ) |
| 9 | 4 | recnd 11289 |
. . . . . 6
⊢ (𝜑 →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℂ) |
| 10 | 8, 9 | negsubdi2d 11636 |
. . . . 5
⊢ (𝜑 →
-((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) =
((abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)))) |
| 11 | 4, 2 | resubcld 11691 |
. . . . . 6
⊢ (𝜑 →
((abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ∈
ℝ) |
| 12 | 1, 7 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 + (1 / 2)) ∈ ℝ) |
| 13 | | reflcl 13836 |
. . . . . . . . . . 11
⊢ ((𝐵 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐵 +
(1 / 2))) ∈ ℝ) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) ∈
ℝ) |
| 15 | 14 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) ∈
ℂ) |
| 16 | 1 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 17 | 15, 16 | subcld 11620 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘(𝐵 + (1 / 2))) − 𝐵) ∈
ℂ) |
| 18 | 17 | absge0d 15483 |
. . . . . . 7
⊢ (𝜑 → 0 ≤
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) |
| 19 | 4, 2 | subge02d 11855 |
. . . . . . 7
⊢ (𝜑 → (0 ≤
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ↔ ((abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) |
| 20 | 18, 19 | mpbid 232 |
. . . . . 6
⊢ (𝜑 →
((abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) |
| 21 | | rddif 15379 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ≤ (1 / 2)) |
| 22 | 3, 21 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ≤ (1 / 2)) |
| 23 | 11, 4, 7, 20, 22 | letrd 11418 |
. . . . 5
⊢ (𝜑 →
((abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (1 /
2)) |
| 24 | 10, 23 | eqbrtrd 5165 |
. . . 4
⊢ (𝜑 →
-((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (1 /
2)) |
| 25 | 5, 7, 24 | lenegcon1d 11845 |
. . 3
⊢ (𝜑 → -(1 / 2) ≤
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) |
| 26 | 3, 7 | readdcld 11290 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + (1 / 2)) ∈ ℝ) |
| 27 | | reflcl 13836 |
. . . . . . . . 9
⊢ ((𝐴 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐴 +
(1 / 2))) ∈ ℝ) |
| 28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ∈
ℝ) |
| 29 | 28 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ∈
ℂ) |
| 30 | 3 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 31 | 29, 30 | subcld 11620 |
. . . . . 6
⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) − 𝐴) ∈
ℂ) |
| 32 | 31 | absge0d 15483 |
. . . . 5
⊢ (𝜑 → 0 ≤
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) |
| 33 | 2, 4 | subge02d 11855 |
. . . . 5
⊢ (𝜑 → (0 ≤
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ↔ ((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)))) |
| 34 | 32, 33 | mpbid 232 |
. . . 4
⊢ (𝜑 →
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) |
| 35 | | rddif 15379 |
. . . . 5
⊢ (𝐵 ∈ ℝ →
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ≤ (1 / 2)) |
| 36 | 1, 35 | syl 17 |
. . . 4
⊢ (𝜑 →
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ≤ (1 / 2)) |
| 37 | 5, 2, 7, 34, 36 | letrd 11418 |
. . 3
⊢ (𝜑 →
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (1 /
2)) |
| 38 | 25, 37 | jca 511 |
. 2
⊢ (𝜑 → (-(1 / 2) ≤
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∧
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (1 /
2))) |
| 39 | 5, 7 | absled 15469 |
. 2
⊢ (𝜑 →
((abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2) ↔ (-(1 /
2) ≤ ((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∧
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (1 /
2)))) |
| 40 | 38, 39 | mpbird 257 |
1
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 /
2)) |