Metamath Proof Explorer

Theorem zbtwnre

Description: There is a unique integer between a real number and the number plus one. Exercise 5 of Apostol p. 28. (Contributed by NM, 13-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 zmin 
 |-  ( A e. RR -> E! x e. ZZ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) )
2 zre 
 |-  ( y e. ZZ -> y e. RR )
3 zre 
 |-  ( x e. ZZ -> x e. RR )
4 peano2rem 
 |-  ( x e. RR -> ( x - 1 ) e. RR )
5 3 4 syl 
 |-  ( x e. ZZ -> ( x - 1 ) e. RR )
6 ltletr 
 |-  ( ( ( x - 1 ) e. RR /\ A e. RR /\ y e. RR ) -> ( ( ( x - 1 ) < A /\ A <_ y ) -> ( x - 1 ) < y ) )
7 5 6 syl3an1 
 |-  ( ( x e. ZZ /\ A e. RR /\ y e. RR ) -> ( ( ( x - 1 ) < A /\ A <_ y ) -> ( x - 1 ) < y ) )
8 7 3expa 
 |-  ( ( ( x e. ZZ /\ A e. RR ) /\ y e. RR ) -> ( ( ( x - 1 ) < A /\ A <_ y ) -> ( x - 1 ) < y ) )
9 2 8 sylan2 
 |-  ( ( ( x e. ZZ /\ A e. RR ) /\ y e. ZZ ) -> ( ( ( x - 1 ) < A /\ A <_ y ) -> ( x - 1 ) < y ) )
10 zlem1lt 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x <_ y <-> ( x - 1 ) < y ) )
11 10 adantlr 
 |-  ( ( ( x e. ZZ /\ A e. RR ) /\ y e. ZZ ) -> ( x <_ y <-> ( x - 1 ) < y ) )
12 9 11 sylibrd 
 |-  ( ( ( x e. ZZ /\ A e. RR ) /\ y e. ZZ ) -> ( ( ( x - 1 ) < A /\ A <_ y ) -> x <_ y ) )
13 12 exp4b 
 |-  ( ( x e. ZZ /\ A e. RR ) -> ( y e. ZZ -> ( ( x - 1 ) < A -> ( A <_ y -> x <_ y ) ) ) )
14 13 com23 
 |-  ( ( x e. ZZ /\ A e. RR ) -> ( ( x - 1 ) < A -> ( y e. ZZ -> ( A <_ y -> x <_ y ) ) ) )
15 14 ralrimdv 
 |-  ( ( x e. ZZ /\ A e. RR ) -> ( ( x - 1 ) < A -> A. y e. ZZ ( A <_ y -> x <_ y ) ) )
16 5 ltnrd 
 |-  ( x e. ZZ -> -. ( x - 1 ) < ( x - 1 ) )
17 peano2zm 
 |-  ( x e. ZZ -> ( x - 1 ) e. ZZ )
18 zlem1lt 
 |-  ( ( x e. ZZ /\ ( x - 1 ) e. ZZ ) -> ( x <_ ( x - 1 ) <-> ( x - 1 ) < ( x - 1 ) ) )
19 17 18 mpdan 
 |-  ( x e. ZZ -> ( x <_ ( x - 1 ) <-> ( x - 1 ) < ( x - 1 ) ) )
20 16 19 mtbird 
 |-  ( x e. ZZ -> -. x <_ ( x - 1 ) )
21 20 ad2antrr 
 |-  ( ( ( x e. ZZ /\ A e. RR ) /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) -> -. x <_ ( x - 1 ) )
22 lenlt 
 |-  ( ( A e. RR /\ ( x - 1 ) e. RR ) -> ( A <_ ( x - 1 ) <-> -. ( x - 1 ) < A ) )
23 5 22 sylan2 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( A <_ ( x - 1 ) <-> -. ( x - 1 ) < A ) )
24 23 ancoms 
 |-  ( ( x e. ZZ /\ A e. RR ) -> ( A <_ ( x - 1 ) <-> -. ( x - 1 ) < A ) )
25 24 adantr 
 |-  ( ( ( x e. ZZ /\ A e. RR ) /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) -> ( A <_ ( x - 1 ) <-> -. ( x - 1 ) < A ) )
26 breq2 
 |-  ( y = ( x - 1 ) -> ( A <_ y <-> A <_ ( x - 1 ) ) )
27 breq2 
 |-  ( y = ( x - 1 ) -> ( x <_ y <-> x <_ ( x - 1 ) ) )
28 26 27 imbi12d 
 |-  ( y = ( x - 1 ) -> ( ( A <_ y -> x <_ y ) <-> ( A <_ ( x - 1 ) -> x <_ ( x - 1 ) ) ) )
29 28 rspcv 
 |-  ( ( x - 1 ) e. ZZ -> ( A. y e. ZZ ( A <_ y -> x <_ y ) -> ( A <_ ( x - 1 ) -> x <_ ( x - 1 ) ) ) )
30 17 29 syl 
 |-  ( x e. ZZ -> ( A. y e. ZZ ( A <_ y -> x <_ y ) -> ( A <_ ( x - 1 ) -> x <_ ( x - 1 ) ) ) )
31 30 imp 
 |-  ( ( x e. ZZ /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) -> ( A <_ ( x - 1 ) -> x <_ ( x - 1 ) ) )
32 31 adantlr 
 |-  ( ( ( x e. ZZ /\ A e. RR ) /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) -> ( A <_ ( x - 1 ) -> x <_ ( x - 1 ) ) )
33 25 32 sylbird 
 |-  ( ( ( x e. ZZ /\ A e. RR ) /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) -> ( -. ( x - 1 ) < A -> x <_ ( x - 1 ) ) )
34 21 33 mt3d 
 |-  ( ( ( x e. ZZ /\ A e. RR ) /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) -> ( x - 1 ) < A )
35 34 ex 
 |-  ( ( x e. ZZ /\ A e. RR ) -> ( A. y e. ZZ ( A <_ y -> x <_ y ) -> ( x - 1 ) < A ) )
36 15 35 impbid 
 |-  ( ( x e. ZZ /\ A e. RR ) -> ( ( x - 1 ) < A <-> A. y e. ZZ ( A <_ y -> x <_ y ) ) )
37 1re 
 |-  1 e. RR
38 ltsubadd 
 |-  ( ( x e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( x - 1 ) < A <-> x < ( A + 1 ) ) )
39 37 38 mp3an2 
 |-  ( ( x e. RR /\ A e. RR ) -> ( ( x - 1 ) < A <-> x < ( A + 1 ) ) )
40 3 39 sylan 
 |-  ( ( x e. ZZ /\ A e. RR ) -> ( ( x - 1 ) < A <-> x < ( A + 1 ) ) )
41 36 40 bitr3d 
 |-  ( ( x e. ZZ /\ A e. RR ) -> ( A. y e. ZZ ( A <_ y -> x <_ y ) <-> x < ( A + 1 ) ) )
42 41 ancoms 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( A. y e. ZZ ( A <_ y -> x <_ y ) <-> x < ( A + 1 ) ) )
43 42 anbi2d 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) <-> ( A <_ x /\ x < ( A + 1 ) ) ) )
44 43 reubidva 
 |-  ( A e. RR -> ( E! x e. ZZ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) <-> E! x e. ZZ ( A <_ x /\ x < ( A + 1 ) ) ) )
45 1 44 mpbid 
 |-  ( A e. RR -> E! x e. ZZ ( A <_ x /\ x < ( A + 1 ) ) )