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 2cn
 |-  2 e. CC
4 2ne0
 |-  2 =/= 0
5 3 4 recidi
 |-  ( 2 x. ( 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 e. RR -> A e. CC )
9 1 a1i
 |-  ( A e. RR -> ( 1 / 2 ) e. CC )
10 8 9 9 nppcan3d
 |-  ( A e. RR -> ( ( A - ( 1 / 2 ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( A + ( 1 / 2 ) ) )
11 7 10 eqtr3id
 |-  ( A e. RR -> ( ( A - ( 1 / 2 ) ) + 1 ) = ( A + ( 1 / 2 ) ) )
12 halfre
 |-  ( 1 / 2 ) e. RR
13 readdcl
 |-  ( ( A e. RR /\ ( 1 / 2 ) e. RR ) -> ( A + ( 1 / 2 ) ) e. RR )
14 12 13 mpan2
 |-  ( A e. RR -> ( A + ( 1 / 2 ) ) e. RR )
15 fllep1
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( A + ( 1 / 2 ) ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
16 14 15 syl
 |-  ( A e. RR -> ( A + ( 1 / 2 ) ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
17 11 16 eqbrtrd
 |-  ( A e. RR -> ( ( A - ( 1 / 2 ) ) + 1 ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
18 resubcl
 |-  ( ( A e. RR /\ ( 1 / 2 ) e. RR ) -> ( A - ( 1 / 2 ) ) e. RR )
19 12 18 mpan2
 |-  ( A e. RR -> ( A - ( 1 / 2 ) ) e. RR )
20 reflcl
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
21 14 20 syl
 |-  ( A e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
22 1red
 |-  ( A e. RR -> 1 e. RR )
23 19 21 22 leadd1d
 |-  ( A e. RR -> ( ( A - ( 1 / 2 ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) <-> ( ( A - ( 1 / 2 ) ) + 1 ) <_ ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) ) )
24 17 23 mpbird
 |-  ( A e. RR -> ( A - ( 1 / 2 ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) )
25 flle
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( A + ( 1 / 2 ) ) )
26 14 25 syl
 |-  ( A e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( A + ( 1 / 2 ) ) )
27 id
 |-  ( A e. RR -> A e. RR )
28 12 a1i
 |-  ( A e. RR -> ( 1 / 2 ) e. RR )
29 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 ) ) ) ) )
30 21 27 28 29 syl3anc
 |-  ( A e. RR -> ( ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ ( 1 / 2 ) <-> ( ( A - ( 1 / 2 ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) /\ ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( A + ( 1 / 2 ) ) ) ) )
31 24 26 30 mpbir2and
 |-  ( A e. RR -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ ( 1 / 2 ) )