Theorem btwnnz

Description: A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005)

	Ref	Expression
Assertion	btwnnz	|- ( ( A e. ZZ /\ A < B /\ B < ( A + 1 ) ) -> -. B e. ZZ )

Proof

Step	Hyp	Ref	Expression
1		zltp1le	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( A + 1 ) <_ B ) )
2		peano2z	|- ( A e. ZZ -> ( A + 1 ) e. ZZ )
3		zre	|- ( ( A + 1 ) e. ZZ -> ( A + 1 ) e. RR )
4	2 3	syl	|- ( A e. ZZ -> ( A + 1 ) e. RR )
5		zre	|- ( B e. ZZ -> B e. RR )
6		lenlt	|- ( ( ( A + 1 ) e. RR /\ B e. RR ) -> ( ( A + 1 ) <_ B <-> -. B < ( A + 1 ) ) )
7	4 5 6	syl2an	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A + 1 ) <_ B <-> -. B < ( A + 1 ) ) )
8	1 7	bitrd	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B <-> -. B < ( A + 1 ) ) )
9	8	biimpd	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B -> -. B < ( A + 1 ) ) )
10	9	impancom	|- ( ( A e. ZZ /\ A < B ) -> ( B e. ZZ -> -. B < ( A + 1 ) ) )
11	10	con2d	|- ( ( A e. ZZ /\ A < B ) -> ( B < ( A + 1 ) -> -. B e. ZZ ) )
12	11	3impia	|- ( ( A e. ZZ /\ A < B /\ B < ( A + 1 ) ) -> -. B e. ZZ )