# 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 ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|\le ⌊\left|{A}\right|⌋+1$

### Proof

Step Hyp Ref Expression
1 halfre ${⊢}\frac{1}{2}\in ℝ$
2 readdcl ${⊢}\left({A}\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to {A}+\left(\frac{1}{2}\right)\in ℝ$
3 1 2 mpan2 ${⊢}{A}\in ℝ\to {A}+\left(\frac{1}{2}\right)\in ℝ$
4 reflcl ${⊢}{A}+\left(\frac{1}{2}\right)\in ℝ\to ⌊{A}+\left(\frac{1}{2}\right)⌋\in ℝ$
5 3 4 syl ${⊢}{A}\in ℝ\to ⌊{A}+\left(\frac{1}{2}\right)⌋\in ℝ$
6 5 recnd ${⊢}{A}\in ℝ\to ⌊{A}+\left(\frac{1}{2}\right)⌋\in ℂ$
7 abscl ${⊢}⌊{A}+\left(\frac{1}{2}\right)⌋\in ℂ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|\in ℝ$
8 6 7 syl ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|\in ℝ$
9 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
10 abscl ${⊢}{A}\in ℂ\to \left|{A}\right|\in ℝ$
11 9 10 syl ${⊢}{A}\in ℝ\to \left|{A}\right|\in ℝ$
12 1re ${⊢}1\in ℝ$
13 12 a1i ${⊢}{A}\in ℝ\to 1\in ℝ$
14 8 11 resubcld ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-\left|{A}\right|\in ℝ$
15 resubcl ${⊢}\left(⌊{A}+\left(\frac{1}{2}\right)⌋\in ℝ\wedge {A}\in ℝ\right)\to ⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\in ℝ$
16 5 15 mpancom ${⊢}{A}\in ℝ\to ⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\in ℝ$
17 16 recnd ${⊢}{A}\in ℝ\to ⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\in ℂ$
18 abscl ${⊢}⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\in ℂ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\right|\in ℝ$
19 17 18 syl ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\right|\in ℝ$
20 abs2dif ${⊢}\left(⌊{A}+\left(\frac{1}{2}\right)⌋\in ℂ\wedge {A}\in ℂ\right)\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-\left|{A}\right|\le \left|⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\right|$
21 6 9 20 syl2anc ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-\left|{A}\right|\le \left|⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\right|$
22 1 a1i ${⊢}{A}\in ℝ\to \frac{1}{2}\in ℝ$
23 rddif ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\right|\le \frac{1}{2}$
24 halflt1 ${⊢}\frac{1}{2}<1$
25 1 12 24 ltleii ${⊢}\frac{1}{2}\le 1$
26 25 a1i ${⊢}{A}\in ℝ\to \frac{1}{2}\le 1$
27 19 22 13 23 26 letrd ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋-{A}\right|\le 1$
28 14 19 13 21 27 letrd ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-\left|{A}\right|\le 1$
29 8 11 13 28 subled ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\le \left|{A}\right|$
30 3 flcld ${⊢}{A}\in ℝ\to ⌊{A}+\left(\frac{1}{2}\right)⌋\in ℤ$
31 nn0abscl ${⊢}⌊{A}+\left(\frac{1}{2}\right)⌋\in ℤ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|\in {ℕ}_{0}$
32 30 31 syl ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|\in {ℕ}_{0}$
33 32 nn0zd ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|\in ℤ$
34 peano2zm ${⊢}\left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|\in ℤ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\in ℤ$
35 33 34 syl ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\in ℤ$
36 flge ${⊢}\left(\left|{A}\right|\in ℝ\wedge \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\in ℤ\right)\to \left(\left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\le \left|{A}\right|↔\left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\le ⌊\left|{A}\right|⌋\right)$
37 11 35 36 syl2anc ${⊢}{A}\in ℝ\to \left(\left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\le \left|{A}\right|↔\left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\le ⌊\left|{A}\right|⌋\right)$
38 29 37 mpbid ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\le ⌊\left|{A}\right|⌋$
39 reflcl ${⊢}\left|{A}\right|\in ℝ\to ⌊\left|{A}\right|⌋\in ℝ$
40 11 39 syl ${⊢}{A}\in ℝ\to ⌊\left|{A}\right|⌋\in ℝ$
41 8 13 40 lesubaddd ${⊢}{A}\in ℝ\to \left(\left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|-1\le ⌊\left|{A}\right|⌋↔\left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|\le ⌊\left|{A}\right|⌋+1\right)$
42 38 41 mpbid ${⊢}{A}\in ℝ\to \left|⌊{A}+\left(\frac{1}{2}\right)⌋\right|\le ⌊\left|{A}\right|⌋+1$