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 AA+12A12

Proof

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