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 \mathbb{Z}$$
31		nn0abscl	$$⊢⌊A+\left(\frac{1}{2}\right)⌋\in \mathbb{Z}\to \left|⌊A+\left(\frac{1}{2}\right)⌋\right|\in {\mathbb{N}}_0$$
32	30 31	syl	$$⊢A\in ℝ\to \left|⌊A+\left(\frac{1}{2}\right)⌋\right|\in {\mathbb{N}}_0$$
33	32	nn0zd	$$⊢A\in ℝ\to \left|⌊A+\left(\frac{1}{2}\right)⌋\right|\in \mathbb{Z}$$
34		peano2zm	$$⊢\left|⌊A+\left(\frac{1}{2}\right)⌋\right|\in \mathbb{Z}\to \left|⌊A+\left(\frac{1}{2}\right)⌋\right|-1\in \mathbb{Z}$$
35	33 34	syl	$$⊢A\in ℝ\to \left|⌊A+\left(\frac{1}{2}\right)⌋\right|-1\in \mathbb{Z}$$
36		flge	$$⊢\left(\left|A\right|\in ℝ\wedge \left|⌊A+\left(\frac{1}{2}\right)⌋\right|-1\in \mathbb{Z}\right)\to \left(\left|⌊A+\left(\frac{1}{2}\right)⌋\right|-1\le \left|A\right|\leftrightarrow \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|\leftrightarrow \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|⌋\leftrightarrow \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$$