Metamath Proof Explorer


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 A + 1 2 A 1 2

Proof

Step Hyp Ref Expression
1 halfcn 1 2
2 1 2timesi 2 1 2 = 1 2 + 1 2
3 2cn 2
4 2ne0 2 0
5 3 4 recidi 2 1 2 = 1
6 2 5 eqtr3i 1 2 + 1 2 = 1
7 6 oveq2i A 1 2 + 1 2 + 1 2 = A - 1 2 + 1
8 recn A A
9 1 a1i A 1 2
10 8 9 9 nppcan3d A A 1 2 + 1 2 + 1 2 = A + 1 2
11 7 10 eqtr3id A A - 1 2 + 1 = A + 1 2
12 halfre 1 2
13 readdcl A 1 2 A + 1 2
14 12 13 mpan2 A A + 1 2
15 fllep1 A + 1 2 A + 1 2 A + 1 2 + 1
16 14 15 syl A A + 1 2 A + 1 2 + 1
17 11 16 eqbrtrd A A - 1 2 + 1 A + 1 2 + 1
18 resubcl A 1 2 A 1 2
19 12 18 mpan2 A A 1 2
20 reflcl A + 1 2 A + 1 2
21 14 20 syl A A + 1 2
22 1red A 1
23 19 21 22 leadd1d A A 1 2 A + 1 2 A - 1 2 + 1 A + 1 2 + 1
24 17 23 mpbird A A 1 2 A + 1 2
25 flle A + 1 2 A + 1 2 A + 1 2
26 14 25 syl A A + 1 2 A + 1 2
27 id A A
28 12 a1i A 1 2
29 absdifle A + 1 2 A 1 2 A + 1 2 A 1 2 A 1 2 A + 1 2 A + 1 2 A + 1 2
30 21 27 28 29 syl3anc A A + 1 2 A 1 2 A 1 2 A + 1 2 A + 1 2 A + 1 2
31 24 26 30 mpbir2and A A + 1 2 A 1 2