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

Metamath Proof Explorer

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 )