Theorem rddif

Description: The difference between a real number and its nearest integer is less than or equal to one half. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Sep-2015)

	Ref	Expression
Assertion	rddif	$$⊢A\in ℝ\to \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\le \frac{1}{2}$$

Proof

Step	Hyp	Ref	Expression
1		halfcn	$$⊢\frac{1}{2}\in ℂ$$
2	1	2timesi	$$⊢2\left(\frac{1}{2}\right)=\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
3		2cn	$$⊢2\in ℂ$$
4		2ne0	$$⊢2\ne 0$$
5	3 4	recidi	$$⊢2\left(\frac{1}{2}\right)=1$$
6	2 5	eqtr3i	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
7	6	oveq2i	$$⊢\left(A-\left(\frac{1}{2}\right)\right)+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=A-\left(\frac{1}{2}\right)+1$$
8		recn	$$⊢A\in ℝ\to A\in ℂ$$
9	1	a1i	$$⊢A\in ℝ\to \frac{1}{2}\in ℂ$$
10	8 9 9	nppcan3d	$$⊢A\in ℝ\to \left(A-\left(\frac{1}{2}\right)\right)+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=A+\left(\frac{1}{2}\right)$$
11	7 10	eqtr3id	$$⊢A\in ℝ\to A-\left(\frac{1}{2}\right)+1=A+\left(\frac{1}{2}\right)$$
12		halfre	$$⊢\frac{1}{2}\in ℝ$$
13		readdcl	$$⊢\left(A\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to A+\left(\frac{1}{2}\right)\in ℝ$$
14	12 13	mpan2	$$⊢A\in ℝ\to A+\left(\frac{1}{2}\right)\in ℝ$$
15		fllep1	$$⊢A+\left(\frac{1}{2}\right)\in ℝ\to A+\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋+1$$
16	14 15	syl	$$⊢A\in ℝ\to A+\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋+1$$
17	11 16	eqbrtrd	$$⊢A\in ℝ\to A-\left(\frac{1}{2}\right)+1\le ⌊A+\left(\frac{1}{2}\right)⌋+1$$
18		resubcl	$$⊢\left(A\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to A-\left(\frac{1}{2}\right)\in ℝ$$
19	12 18	mpan2	$$⊢A\in ℝ\to A-\left(\frac{1}{2}\right)\in ℝ$$
20		reflcl	$$⊢A+\left(\frac{1}{2}\right)\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋\in ℝ$$
21	14 20	syl	$$⊢A\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋\in ℝ$$
22		1red	$$⊢A\in ℝ\to 1\in ℝ$$
23	19 21 22	leadd1d	$$⊢A\in ℝ\to \left(A-\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋\leftrightarrow A-\left(\frac{1}{2}\right)+1\le ⌊A+\left(\frac{1}{2}\right)⌋+1\right)$$
24	17 23	mpbird	$$⊢A\in ℝ\to A-\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋$$
25		flle	$$⊢A+\left(\frac{1}{2}\right)\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋\le A+\left(\frac{1}{2}\right)$$
26	14 25	syl	$$⊢A\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋\le A+\left(\frac{1}{2}\right)$$
27		id	$$⊢A\in ℝ\to A\in ℝ$$
28	12	a1i	$$⊢A\in ℝ\to \frac{1}{2}\in ℝ$$
29		absdifle	$$⊢\left(⌊A+\left(\frac{1}{2}\right)⌋\in ℝ\wedge A\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to \left(\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\le \frac{1}{2}\leftrightarrow \left(A-\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋\wedge ⌊A+\left(\frac{1}{2}\right)⌋\le A+\left(\frac{1}{2}\right)\right)\right)$$
30	21 27 28 29	syl3anc	$$⊢A\in ℝ\to \left(\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\le \frac{1}{2}\leftrightarrow \left(A-\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋\wedge ⌊A+\left(\frac{1}{2}\right)⌋\le A+\left(\frac{1}{2}\right)\right)\right)$$
31	24 26 30	mpbir2and	$$⊢A\in ℝ\to \left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\le \frac{1}{2}$$