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 ) )