Proof of Theorem absrdbnd
Step | Hyp | Ref
| Expression |
1 | | halfre 12187 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
2 | | readdcl 10954 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (1 / 2)
∈ ℝ) → (𝐴 +
(1 / 2)) ∈ ℝ) |
3 | 1, 2 | mpan2 688 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 + (1 / 2)) ∈
ℝ) |
4 | | reflcl 13516 |
. . . . . . 7
⊢ ((𝐴 + (1 / 2)) ∈ ℝ
→ (⌊‘(𝐴 +
(1 / 2))) ∈ ℝ) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(⌊‘(𝐴 + (1 /
2))) ∈ ℝ) |
6 | 5 | recnd 11003 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(⌊‘(𝐴 + (1 /
2))) ∈ ℂ) |
7 | | abscl 14990 |
. . . . 5
⊢
((⌊‘(𝐴 +
(1 / 2))) ∈ ℂ → (abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℝ) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℝ) |
9 | | recn 10961 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
10 | | abscl 14990 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(abs‘𝐴) ∈
ℝ) |
12 | | 1re 10975 |
. . . . 5
⊢ 1 ∈
ℝ |
13 | 12 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℝ → 1 ∈
ℝ) |
14 | 8, 11 | resubcld 11403 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − (abs‘𝐴)) ∈
ℝ) |
15 | | resubcl 11285 |
. . . . . . . 8
⊢
(((⌊‘(𝐴
+ (1 / 2))) ∈ ℝ ∧ 𝐴 ∈ ℝ) →
((⌊‘(𝐴 + (1 /
2))) − 𝐴) ∈
ℝ) |
16 | 5, 15 | mpancom 685 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) − 𝐴) ∈
ℝ) |
17 | 16 | recnd 11003 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
((⌊‘(𝐴 + (1 /
2))) − 𝐴) ∈
ℂ) |
18 | | abscl 14990 |
. . . . . 6
⊢
(((⌊‘(𝐴
+ (1 / 2))) − 𝐴)
∈ ℂ → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ) |
20 | | abs2dif 15044 |
. . . . . 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 15052 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ≤ (1 / 2)) |
24 | | halflt1 12191 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
25 | 1, 12, 24 | ltleii 11098 |
. . . . . . 7
⊢ (1 / 2)
≤ 1 |
26 | 25 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (1 / 2)
≤ 1) |
27 | 19, 22, 13, 23, 26 | letrd 11132 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ≤ 1) |
28 | 14, 19, 13, 21, 27 | letrd 11132 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − (abs‘𝐴)) ≤ 1) |
29 | 8, 11, 13, 28 | subled 11578 |
. . 3
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(abs‘𝐴)) |
30 | 3 | flcld 13518 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘(𝐴 + (1 /
2))) ∈ ℤ) |
31 | | nn0abscl 15024 |
. . . . . . 7
⊢
((⌊‘(𝐴 +
(1 / 2))) ∈ ℤ → (abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℕ0) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℕ0) |
33 | 32 | nn0zd 12424 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(abs‘(⌊‘(𝐴 + (1 / 2)))) ∈
ℤ) |
34 | | peano2zm 12363 |
. . . . 5
⊢
((abs‘(⌊‘(𝐴 + (1 / 2)))) ∈ ℤ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ∈
ℤ) |
35 | 33, 34 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ∈
ℤ) |
36 | | flge 13525 |
. . . 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 231 |
. 2
⊢ (𝐴 ∈ ℝ →
((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(⌊‘(abs‘𝐴))) |
39 | | reflcl 13516 |
. . . 4
⊢
((abs‘𝐴)
∈ ℝ → (⌊‘(abs‘𝐴)) ∈ ℝ) |
40 | 11, 39 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℝ →
(⌊‘(abs‘𝐴)) ∈ ℝ) |
41 | 8, 13, 40 | lesubaddd 11572 |
. 2
⊢ (𝐴 ∈ ℝ →
(((abs‘(⌊‘(𝐴 + (1 / 2)))) − 1) ≤
(⌊‘(abs‘𝐴)) ↔ (abs‘(⌊‘(𝐴 + (1 / 2)))) ≤
((⌊‘(abs‘𝐴)) + 1))) |
42 | 38, 41 | mpbid 231 |
1
⊢ (𝐴 ∈ ℝ →
(abs‘(⌊‘(𝐴 + (1 / 2)))) ≤
((⌊‘(abs‘𝐴)) + 1)) |