Proof of Theorem absrdbnd
| Step | Hyp | Ref
| Expression |
| 1 | | halfre 12480 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
| 2 | | readdcl 11238 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (1 / 2)
∈ ℝ) → (𝐴 +
(1 / 2)) ∈ ℝ) |
| 3 | 1, 2 | mpan2 691 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 + (1 / 2)) ∈
ℝ) |
| 4 | | reflcl 13836 |
. . . . . . 7
⊢ ((𝐴 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐴 +
(1 / 2))) ∈ ℝ) |
| 5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(⌊‘(𝐴 + (1 /
2))) ∈ ℝ) |
| 6 | 5 | recnd 11289 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(⌊‘(𝐴 + (1 /
2))) ∈ ℂ) |
| 7 | | abscl 15317 |
. . . . 5
⊢
((⌊‘(𝐴 +
(1 / 2))) ∈ ℂ → (abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℝ) |
| 8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℝ) |
| 9 | | recn 11245 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 10 | | abscl 15317 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
| 11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(abs‘𝐴) ∈
ℝ) |
| 12 | | 1re 11261 |
. . . . 5
⊢ 1 ∈
ℝ |
| 13 | 12 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℝ → 1 ∈
ℝ) |
| 14 | 8, 11 | resubcld 11691 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − (abs‘𝐴)) ∈
ℝ) |
| 15 | | resubcl 11573 |
. . . . . . . 8
⊢
(((⌊‘(𝐴
+ (1 / 2))) ∈ ℝ ∧ 𝐴 ∈ ℝ) →
((⌊‘(𝐴 + (1 /
2))) − 𝐴) ∈
ℝ) |
| 16 | 5, 15 | mpancom 688 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) − 𝐴) ∈
ℝ) |
| 17 | 16 | recnd 11289 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) − 𝐴) ∈
ℂ) |
| 18 | | abscl 15317 |
. . . . . 6
⊢
(((⌊‘(𝐴
+ (1 / 2))) − 𝐴)
∈ ℂ → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) |
| 19 | 17, 18 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) |
| 20 | | abs2dif 15371 |
. . . . . 6
⊢
(((⌊‘(𝐴
+ (1 / 2))) ∈ ℂ ∧ 𝐴 ∈ ℂ) →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − (abs‘𝐴)) ≤
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) |
| 21 | 6, 9, 20 | syl2anc 584 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − (abs‘𝐴)) ≤
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) |
| 22 | 1 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (1 / 2)
∈ ℝ) |
| 23 | | rddif 15379 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ≤ (1 / 2)) |
| 24 | | halflt1 12484 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
| 25 | 1, 12, 24 | ltleii 11384 |
. . . . . . 7
⊢ (1 / 2)
≤ 1 |
| 26 | 25 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (1 / 2)
≤ 1) |
| 27 | 19, 22, 13, 23, 26 | letrd 11418 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ≤ 1) |
| 28 | 14, 19, 13, 21, 27 | letrd 11418 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − (abs‘𝐴)) ≤ 1) |
| 29 | 8, 11, 13, 28 | subled 11866 |
. . 3
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(abs‘𝐴)) |
| 30 | 3 | flcld 13838 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘(𝐴 + (1 /
2))) ∈ ℤ) |
| 31 | | nn0abscl 15351 |
. . . . . . 7
⊢
((⌊‘(𝐴 +
(1 / 2))) ∈ ℤ → (abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℕ0) |
| 32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℕ0) |
| 33 | 32 | nn0zd 12639 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℤ) |
| 34 | | peano2zm 12660 |
. . . . 5
⊢
((abs‘(⌊‘(𝐴 + (1 / 2)))) ∈ ℤ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ∈
ℤ) |
| 35 | 33, 34 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ∈
ℤ) |
| 36 | | flge 13845 |
. . . 4
⊢
(((abs‘𝐴)
∈ ℝ ∧ ((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ∈ ℤ)
→ (((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(abs‘𝐴) ↔
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(⌊‘(abs‘𝐴)))) |
| 37 | 11, 35, 36 | syl2anc 584 |
. . 3
⊢ (𝐴 ∈ ℝ →
(((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(abs‘𝐴) ↔
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(⌊‘(abs‘𝐴)))) |
| 38 | 29, 37 | mpbid 232 |
. 2
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(⌊‘(abs‘𝐴))) |
| 39 | | reflcl 13836 |
. . . 4
⊢
((abs‘𝐴)
∈ ℝ → (⌊‘(abs‘𝐴)) ∈ ℝ) |
| 40 | 11, 39 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℝ →
(⌊‘(abs‘𝐴)) ∈ ℝ) |
| 41 | 8, 13, 40 | lesubaddd 11860 |
. 2
⊢ (𝐴 ∈ ℝ →
(((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(⌊‘(abs‘𝐴)) ↔ (abs‘(⌊‘(𝐴 + (1 / 2)))) ≤
((⌊‘(abs‘𝐴)) + 1))) |
| 42 | 38, 41 | mpbid 232 |
1
⊢ (𝐴 ∈ ℝ →
(abs‘(⌊‘(𝐴 + (1 / 2)))) ≤
((⌊‘(abs‘𝐴)) + 1)) |