Metamath Proof Explorer

Theorem absrdbnd

Description: Bound on the absolute value of a real number rounded to the nearest integer. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Sep-2015)

Ref Expression
Assertion absrdbnd ( 𝐴 ∈ ℝ → ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) ≤ ( ( ⌊ ‘ ( abs ‘ 𝐴 ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 halfre ⊢ ( 1 / 2 ) ∈ ℝ
2 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
4 reflcl ⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
5 3 4 syl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
6 5 recnd ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ )
7 abscl ⊢ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ → ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) ∈ ℝ )
8 6 7 syl ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) ∈ ℝ )
9 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
10 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
11 9 10 syl ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℝ )
12 1re ⊢ 1 ∈ ℝ
13 12 a1i ⊢ ( 𝐴 ∈ ℝ → 1 ∈ ℝ )
14 8 11 resubcld ⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − ( abs ‘ 𝐴 ) ) ∈ ℝ )
15 resubcl ⊢ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ∈ ℝ )
16 5 15 mpancom ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ∈ ℝ )
17 16 recnd ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ∈ ℂ )
18 abscl ⊢ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ∈ ℂ → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )
19 17 18 syl ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ∈ ℝ )
20 abs2dif ⊢ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − ( abs ‘ 𝐴 ) ) ≤ ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) )
21 6 9 20 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − ( abs ‘ 𝐴 ) ) ≤ ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) )
22 1 a1i ⊢ ( 𝐴 ∈ ℝ → ( 1 / 2 ) ∈ ℝ )
23 rddif ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ≤ ( 1 / 2 ) )
24 halflt1 ⊢ ( 1 / 2 ) < 1
25 1 12 24 ltleii ⊢ ( 1 / 2 ) ≤ 1
26 25 a1i ⊢ ( 𝐴 ∈ ℝ → ( 1 / 2 ) ≤ 1 )
27 19 22 13 23 26 letrd ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ≤ 1 )
28 14 19 13 21 27 letrd ⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − ( abs ‘ 𝐴 ) ) ≤ 1 )
29 8 11 13 28 subled ⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ≤ ( abs ‘ 𝐴 ) )
30 3 flcld ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℤ )
31 nn0abscl ⊢ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℤ → ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) ∈ ℕ0 )
32 30 31 syl ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) ∈ ℕ0 )
33 32 nn0zd ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) ∈ ℤ )
34 peano2zm ⊢ ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) ∈ ℤ → ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ∈ ℤ )
35 33 34 syl ⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ∈ ℤ )
36 flge ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ∈ ℤ ) → ( ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ≤ ( abs ‘ 𝐴 ) ↔ ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ≤ ( ⌊ ‘ ( abs ‘ 𝐴 ) ) ) )
37 11 35 36 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ≤ ( abs ‘ 𝐴 ) ↔ ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ≤ ( ⌊ ‘ ( abs ‘ 𝐴 ) ) ) )
38 29 37 mpbid ⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ≤ ( ⌊ ‘ ( abs ‘ 𝐴 ) ) )
39 reflcl ⊢ ( ( abs ‘ 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( abs ‘ 𝐴 ) ) ∈ ℝ )
40 11 39 syl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( abs ‘ 𝐴 ) ) ∈ ℝ )
41 8 13 40 lesubaddd ⊢ ( 𝐴 ∈ ℝ → ( ( ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) − 1 ) ≤ ( ⌊ ‘ ( abs ‘ 𝐴 ) ) ↔ ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) ≤ ( ( ⌊ ‘ ( abs ‘ 𝐴 ) ) + 1 ) ) )
42 38 41 mpbid ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ) ≤ ( ( ⌊ ‘ ( abs ‘ 𝐴 ) ) + 1 ) )