Metamath Proof Explorer

Theorem absrdbnd

Description: Bound on the absolute value of a real number rounded to the nearest integer. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Sep-2015)

Ref Expression
Assertion absrdbnd 
|- ( A e. RR -> ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) <_ ( ( |_ ` ( abs ` A ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 halfre 
 |-  ( 1 / 2 ) e. RR
2 readdcl 
 |-  ( ( A e. RR /\ ( 1 / 2 ) e. RR ) -> ( A + ( 1 / 2 ) ) e. RR )
3 1 2 mpan2 
 |-  ( A e. RR -> ( A + ( 1 / 2 ) ) e. RR )
4 reflcl 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
5 3 4 syl 
 |-  ( A e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
6 5 recnd 
 |-  ( A e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC )
7 abscl 
 |-  ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC -> ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) e. RR )
8 6 7 syl 
 |-  ( A e. RR -> ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) e. RR )
9 recn 
 |-  ( A e. RR -> A e. CC )
10 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
11 9 10 syl 
 |-  ( A e. RR -> ( abs ` A ) e. RR )
12 1re 
 |-  1 e. RR
13 12 a1i 
 |-  ( A e. RR -> 1 e. RR )
14 8 11 resubcld 
 |-  ( A e. RR -> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - ( abs ` A ) ) e. RR )
15 resubcl 
 |-  ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR /\ A e. RR ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) e. RR )
16 5 15 mpancom 
 |-  ( A e. RR -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) e. RR )
17 16 recnd 
 |-  ( A e. RR -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) e. CC )
18 abscl 
 |-  ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) e. CC -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )
19 17 18 syl 
 |-  ( A e. RR -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )
20 abs2dif 
 |-  ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC /\ A e. CC ) -> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - ( abs ` A ) ) <_ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
21 6 9 20 syl2anc 
 |-  ( A e. RR -> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - ( abs ` A ) ) <_ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
22 1 a1i 
 |-  ( A e. RR -> ( 1 / 2 ) e. RR )
23 rddif 
 |-  ( A e. RR -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ ( 1 / 2 ) )
24 halflt1 
 |-  ( 1 / 2 ) < 1
25 1 12 24 ltleii 
 |-  ( 1 / 2 ) <_ 1
26 25 a1i 
 |-  ( A e. RR -> ( 1 / 2 ) <_ 1 )
27 19 22 13 23 26 letrd 
 |-  ( A e. RR -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ 1 )
28 14 19 13 21 27 letrd 
 |-  ( A e. RR -> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - ( abs ` A ) ) <_ 1 )
29 8 11 13 28 subled 
 |-  ( A e. RR -> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) <_ ( abs ` A ) )
30 3 flcld 
 |-  ( A e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. ZZ )
31 nn0abscl 
 |-  ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. ZZ -> ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) e. NN0 )
32 30 31 syl 
 |-  ( A e. RR -> ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) e. NN0 )
33 32 nn0zd 
 |-  ( A e. RR -> ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) e. ZZ )
34 peano2zm 
 |-  ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) e. ZZ -> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) e. ZZ )
35 33 34 syl 
 |-  ( A e. RR -> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) e. ZZ )
36 flge 
 |-  ( ( ( abs ` A ) e. RR /\ ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) e. ZZ ) -> ( ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) <_ ( abs ` A ) <-> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) <_ ( |_ ` ( abs ` A ) ) ) )
37 11 35 36 syl2anc 
 |-  ( A e. RR -> ( ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) <_ ( abs ` A ) <-> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) <_ ( |_ ` ( abs ` A ) ) ) )
38 29 37 mpbid 
 |-  ( A e. RR -> ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) <_ ( |_ ` ( abs ` A ) ) )
39 reflcl 
 |-  ( ( abs ` A ) e. RR -> ( |_ ` ( abs ` A ) ) e. RR )
40 11 39 syl 
 |-  ( A e. RR -> ( |_ ` ( abs ` A ) ) e. RR )
41 8 13 40 lesubaddd 
 |-  ( A e. RR -> ( ( ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) - 1 ) <_ ( |_ ` ( abs ` A ) ) <-> ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) <_ ( ( |_ ` ( abs ` A ) ) + 1 ) ) )
42 38 41 mpbid 
 |-  ( A e. RR -> ( abs ` ( |_ ` ( A + ( 1 / 2 ) ) ) ) <_ ( ( |_ ` ( abs ` A ) ) + 1 ) )