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 e. RR -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ ( 1 / 2 ) )

Proof

Step Hyp Ref Expression
1 halfcn 
 |-  ( 1 / 2 ) e. CC
2 1 2timesi 
 |-  ( 2 x. ( 1 / 2 ) ) = ( ( 1 / 2 ) + ( 1 / 2 ) )
3 2thalfe1 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
4 2 3 eqtr3i 
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
5 4 oveq2i 
 |-  ( ( A - ( 1 / 2 ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( A - ( 1 / 2 ) ) + 1 )
6 recn 
 |-  ( A e. RR -> A e. CC )
7 1 a1i 
 |-  ( A e. RR -> ( 1 / 2 ) e. CC )
8 6 7 7 nppcan3d 
 |-  ( A e. RR -> ( ( A - ( 1 / 2 ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( A + ( 1 / 2 ) ) )
9 5 8 eqtr3id 
 |-  ( A e. RR -> ( ( A - ( 1 / 2 ) ) + 1 ) = ( A + ( 1 / 2 ) ) )
10 halfre 
 |-  ( 1 / 2 ) e. RR
11 readdcl 
 |-  ( ( A e. RR /\ ( 1 / 2 ) e. RR ) -> ( A + ( 1 / 2 ) ) e. RR )
12 10 11 mpan2 
 |-  ( A e. RR -> ( A + ( 1 / 2 ) ) e. RR )
13 fllep1 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( A + ( 1 / 2 ) ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
14 12 13 syl 
 |-  ( A e. RR -> ( A + ( 1 / 2 ) ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
15 9 14 eqbrtrd 
 |-  ( A e. RR -> ( ( A - ( 1 / 2 ) ) + 1 ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
16 resubcl 
 |-  ( ( A e. RR /\ ( 1 / 2 ) e. RR ) -> ( A - ( 1 / 2 ) ) e. RR )
17 10 16 mpan2 
 |-  ( A e. RR -> ( A - ( 1 / 2 ) ) e. RR )
18 reflcl 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
19 12 18 syl 
 |-  ( A e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
20 1red 
 |-  ( A e. RR -> 1 e. RR )
21 17 19 20 leadd1d 
 |-  ( A e. RR -> ( ( A - ( 1 / 2 ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) <-> ( ( A - ( 1 / 2 ) ) + 1 ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) ) )
22 15 21 mpbird 
 |-  ( A e. RR -> ( A - ( 1 / 2 ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) )
23 flle 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( A + ( 1 / 2 ) ) )
24 12 23 syl 
 |-  ( A e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( A + ( 1 / 2 ) ) )
25 id 
 |-  ( A e. RR -> A e. RR )
26 10 a1i 
 |-  ( A e. RR -> ( 1 / 2 ) e. RR )
27 absdifle 
 |-  ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR /\ A e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ ( 1 / 2 ) <-> ( ( A - ( 1 / 2 ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) /\ ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( A + ( 1 / 2 ) ) ) ) )
28 19 25 26 27 syl3anc 
 |-  ( A e. RR -> ( ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ ( 1 / 2 ) <-> ( ( A - ( 1 / 2 ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) /\ ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( A + ( 1 / 2 ) ) ) ) )
29 22 24 28 mpbir2and 
 |-  ( A e. RR -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ ( 1 / 2 ) )