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