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