This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem btwnz

Description: Any real number can be sandwiched between two integers. Exercise 2 of Apostol p. 28. (Contributed by NM, 10-Nov-2004)

Ref Expression
Assertion btwnz 
|- ( A e. RR -> ( E. x e. ZZ x < A /\ E. y e. ZZ A < y ) )

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( A e. RR -> -u A e. RR )
2 arch 
 |-  ( -u A e. RR -> E. z e. NN -u A < z )
3 1 2 syl 
 |-  ( A e. RR -> E. z e. NN -u A < z )
4 nnre 
 |-  ( z e. NN -> z e. RR )
5 ltnegcon1 
 |-  ( ( A e. RR /\ z e. RR ) -> ( -u A < z <-> -u z < A ) )
6 5 ex 
 |-  ( A e. RR -> ( z e. RR -> ( -u A < z <-> -u z < A ) ) )
7 4 6 syl5 
 |-  ( A e. RR -> ( z e. NN -> ( -u A < z <-> -u z < A ) ) )
8 7 pm5.32d 
 |-  ( A e. RR -> ( ( z e. NN /\ -u A < z ) <-> ( z e. NN /\ -u z < A ) ) )
9 nnnegz 
 |-  ( z e. NN -> -u z e. ZZ )
10 breq1 
 |-  ( x = -u z -> ( x < A <-> -u z < A ) )
11 10 rspcev 
 |-  ( ( -u z e. ZZ /\ -u z < A ) -> E. x e. ZZ x < A )
12 9 11 sylan 
 |-  ( ( z e. NN /\ -u z < A ) -> E. x e. ZZ x < A )
13 8 12 biimtrdi 
 |-  ( A e. RR -> ( ( z e. NN /\ -u A < z ) -> E. x e. ZZ x < A ) )
14 13 expd 
 |-  ( A e. RR -> ( z e. NN -> ( -u A < z -> E. x e. ZZ x < A ) ) )
15 14 rexlimdv 
 |-  ( A e. RR -> ( E. z e. NN -u A < z -> E. x e. ZZ x < A ) )
16 3 15 mpd 
 |-  ( A e. RR -> E. x e. ZZ x < A )
17 arch 
 |-  ( A e. RR -> E. y e. NN A < y )
18 nnz 
 |-  ( y e. NN -> y e. ZZ )
19 18 anim1i 
 |-  ( ( y e. NN /\ A < y ) -> ( y e. ZZ /\ A < y ) )
20 19 reximi2 
 |-  ( E. y e. NN A < y -> E. y e. ZZ A < y )
21 17 20 syl 
 |-  ( A e. RR -> E. y e. ZZ A < y )
22 16 21 jca 
 |-  ( A e. RR -> ( E. x e. ZZ x < A /\ E. y e. ZZ A < y ) )