Proof of Theorem dnibndlem6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dnibndlem6.2 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 2 | 1 | dnicld1 36474 | . . . . 5
⊢ (𝜑 →
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℝ) | 
| 3 | 2 | recnd 11290 | . . . 4
⊢ (𝜑 →
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℂ) | 
| 4 |  | dnibndlem6.1 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 5 | 4 | dnicld1 36474 | . . . . 5
⊢ (𝜑 →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) | 
| 6 | 5 | recnd 11290 | . . . 4
⊢ (𝜑 →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℂ) | 
| 7 | 3, 6 | subcld 11621 | . . 3
⊢ (𝜑 →
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∈
ℂ) | 
| 8 | 7 | abscld 15476 | . 2
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ∈
ℝ) | 
| 9 |  | halfcn 12482 | . . . . . 6
⊢ (1 / 2)
∈ ℂ | 
| 10 | 9 | a1i 11 | . . . . 5
⊢ (𝜑 → (1 / 2) ∈
ℂ) | 
| 11 | 3, 10 | subcld 11621 | . . . 4
⊢ (𝜑 →
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (1 / 2)) ∈
ℂ) | 
| 12 | 11 | abscld 15476 | . . 3
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (1 / 2))) ∈
ℝ) | 
| 13 | 10, 6 | subcld 11621 | . . . 4
⊢ (𝜑 → ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∈ ℂ) | 
| 14 | 13 | abscld 15476 | . . 3
⊢ (𝜑 → (abs‘((1 / 2)
− (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ∈ ℝ) | 
| 15 | 12, 14 | readdcld 11291 | . 2
⊢ (𝜑 →
((abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (1 / 2))) + (abs‘((1 / 2)
− (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))) ∈ ℝ) | 
| 16 |  | halfre 12481 | . . . . . 6
⊢ (1 / 2)
∈ ℝ | 
| 17 | 16 | a1i 11 | . . . . 5
⊢ (𝜑 → (1 / 2) ∈
ℝ) | 
| 18 | 17, 2 | jca 511 | . . . 4
⊢ (𝜑 → ((1 / 2) ∈ ℝ
∧ (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℝ)) | 
| 19 |  | resubcl 11574 | . . . 4
⊢ (((1 / 2)
∈ ℝ ∧ (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℝ) → ((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ∈ ℝ) | 
| 20 | 18, 19 | syl 17 | . . 3
⊢ (𝜑 → ((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ∈ ℝ) | 
| 21 | 17, 5 | jca 511 | . . . 4
⊢ (𝜑 → ((1 / 2) ∈ ℝ
∧ (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ)) | 
| 22 |  | resubcl 11574 | . . . 4
⊢ (((1 / 2)
∈ ℝ ∧ (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) → ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∈ ℝ) | 
| 23 | 21, 22 | syl 17 | . . 3
⊢ (𝜑 → ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ∈ ℝ) | 
| 24 | 20, 23 | readdcld 11291 | . 2
⊢ (𝜑 → (((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ∈ ℝ) | 
| 25 | 3, 6, 10 | 3jca 1128 | . . 3
⊢ (𝜑 →
((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℂ ∧
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℂ ∧ (1 / 2) ∈
ℂ)) | 
| 26 |  | abs3dif 15371 | . . 3
⊢
(((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) ∈ ℂ ∧
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℂ ∧ (1 / 2) ∈
ℂ) → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤
((abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (1 / 2))) + (abs‘((1 / 2)
− (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))))) | 
| 27 | 25, 26 | syl 17 | . 2
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤
((abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (1 / 2))) + (abs‘((1 / 2)
− (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))))) | 
| 28 | 3, 10 | abssubd 15493 | . . . . 5
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (1 / 2))) = (abs‘((1 / 2)
− (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))))) | 
| 29 |  | rddif2 36479 | . . . . . . 7
⊢ (𝐵 ∈ ℝ → 0 ≤
((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)))) | 
| 30 | 1, 29 | syl 17 | . . . . . 6
⊢ (𝜑 → 0 ≤ ((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)))) | 
| 31 | 20, 30 | absidd 15462 | . . . . 5
⊢ (𝜑 → (abs‘((1 / 2)
− (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)))) = ((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)))) | 
| 32 | 28, 31 | eqtrd 2776 | . . . 4
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (1 / 2))) = ((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)))) | 
| 33 |  | rddif2 36479 | . . . . . 6
⊢ (𝐴 ∈ ℝ → 0 ≤
((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) | 
| 34 | 4, 33 | syl 17 | . . . . 5
⊢ (𝜑 → 0 ≤ ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) | 
| 35 | 23, 34 | absidd 15462 | . . . 4
⊢ (𝜑 → (abs‘((1 / 2)
− (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) = ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) | 
| 36 | 32, 35 | oveq12d 7450 | . . 3
⊢ (𝜑 →
((abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (1 / 2))) + (abs‘((1 / 2)
− (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))) = (((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))) | 
| 37 | 15, 36 | eqled 11365 | . 2
⊢ (𝜑 →
((abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (1 / 2))) + (abs‘((1 / 2)
− (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))) ≤ (((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))) | 
| 38 | 8, 15, 24, 27, 37 | letrd 11419 | 1
⊢ (𝜑 →
(abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (((1 / 2) −
(abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) −
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))) |