Metamath Proof Explorer

Theorem rebtwnz

Description: There is a unique greatest integer less than or equal to a real number. Exercise 4 of Apostol p. 28. (Contributed by NM, 15-Nov-2004)

Ref Expression
Assertion rebtwnz 
|- ( A e. RR -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( A e. RR -> -u A e. RR )
2 zbtwnre 
 |-  ( -u A e. RR -> E! y e. ZZ ( -u A <_ y /\ y < ( -u A + 1 ) ) )
3 1 2 syl 
 |-  ( A e. RR -> E! y e. ZZ ( -u A <_ y /\ y < ( -u A + 1 ) ) )
4 znegcl 
 |-  ( x e. ZZ -> -u x e. ZZ )
5 znegcl 
 |-  ( y e. ZZ -> -u y e. ZZ )
6 zcn 
 |-  ( y e. ZZ -> y e. CC )
7 zcn 
 |-  ( x e. ZZ -> x e. CC )
8 negcon2 
 |-  ( ( y e. CC /\ x e. CC ) -> ( y = -u x <-> x = -u y ) )
9 6 7 8 syl2an 
 |-  ( ( y e. ZZ /\ x e. ZZ ) -> ( y = -u x <-> x = -u y ) )
10 5 9 reuhyp 
 |-  ( y e. ZZ -> E! x e. ZZ y = -u x )
11 breq2 
 |-  ( y = -u x -> ( -u A <_ y <-> -u A <_ -u x ) )
12 breq1 
 |-  ( y = -u x -> ( y < ( -u A + 1 ) <-> -u x < ( -u A + 1 ) ) )
13 11 12 anbi12d 
 |-  ( y = -u x -> ( ( -u A <_ y /\ y < ( -u A + 1 ) ) <-> ( -u A <_ -u x /\ -u x < ( -u A + 1 ) ) ) )
14 4 10 13 reuxfr1 
 |-  ( E! y e. ZZ ( -u A <_ y /\ y < ( -u A + 1 ) ) <-> E! x e. ZZ ( -u A <_ -u x /\ -u x < ( -u A + 1 ) ) )
15 zre 
 |-  ( x e. ZZ -> x e. RR )
16 leneg 
 |-  ( ( x e. RR /\ A e. RR ) -> ( x <_ A <-> -u A <_ -u x ) )
17 16 ancoms 
 |-  ( ( A e. RR /\ x e. RR ) -> ( x <_ A <-> -u A <_ -u x ) )
18 peano2rem 
 |-  ( A e. RR -> ( A - 1 ) e. RR )
19 ltneg 
 |-  ( ( ( A - 1 ) e. RR /\ x e. RR ) -> ( ( A - 1 ) < x <-> -u x < -u ( A - 1 ) ) )
20 18 19 sylan 
 |-  ( ( A e. RR /\ x e. RR ) -> ( ( A - 1 ) < x <-> -u x < -u ( A - 1 ) ) )
21 1re 
 |-  1 e. RR
22 ltsubadd 
 |-  ( ( A e. RR /\ 1 e. RR /\ x e. RR ) -> ( ( A - 1 ) < x <-> A < ( x + 1 ) ) )
23 21 22 mp3an2 
 |-  ( ( A e. RR /\ x e. RR ) -> ( ( A - 1 ) < x <-> A < ( x + 1 ) ) )
24 recn 
 |-  ( A e. RR -> A e. CC )
25 ax-1cn 
 |-  1 e. CC
26 negsubdi 
 |-  ( ( A e. CC /\ 1 e. CC ) -> -u ( A - 1 ) = ( -u A + 1 ) )
27 24 25 26 sylancl 
 |-  ( A e. RR -> -u ( A - 1 ) = ( -u A + 1 ) )
28 27 adantr 
 |-  ( ( A e. RR /\ x e. RR ) -> -u ( A - 1 ) = ( -u A + 1 ) )
29 28 breq2d 
 |-  ( ( A e. RR /\ x e. RR ) -> ( -u x < -u ( A - 1 ) <-> -u x < ( -u A + 1 ) ) )
30 20 23 29 3bitr3d 
 |-  ( ( A e. RR /\ x e. RR ) -> ( A < ( x + 1 ) <-> -u x < ( -u A + 1 ) ) )
31 17 30 anbi12d 
 |-  ( ( A e. RR /\ x e. RR ) -> ( ( x <_ A /\ A < ( x + 1 ) ) <-> ( -u A <_ -u x /\ -u x < ( -u A + 1 ) ) ) )
32 15 31 sylan2 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( ( x <_ A /\ A < ( x + 1 ) ) <-> ( -u A <_ -u x /\ -u x < ( -u A + 1 ) ) ) )
33 32 bicomd 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( ( -u A <_ -u x /\ -u x < ( -u A + 1 ) ) <-> ( x <_ A /\ A < ( x + 1 ) ) ) )
34 33 reubidva 
 |-  ( A e. RR -> ( E! x e. ZZ ( -u A <_ -u x /\ -u x < ( -u A + 1 ) ) <-> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )
35 14 34 syl5bb 
 |-  ( A e. RR -> ( E! y e. ZZ ( -u A <_ y /\ y < ( -u A + 1 ) ) <-> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )
36 3 35 mpbid 
 |-  ( A e. RR -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )