Metamath Proof Explorer

Theorem fz10

Description: There are no integers between 1 and 0. (Contributed by Jeff Madsen, 16-Jun-2010) (Proof shortened by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fz10 
|- ( 1 ... 0 ) = (/)

Proof

Step Hyp Ref Expression
1 0lt1 
 |-  0 < 1
2 1z 
 |-  1 e. ZZ
3 0z 
 |-  0 e. ZZ
4 fzn 
 |-  ( ( 1 e. ZZ /\ 0 e. ZZ ) -> ( 0 < 1 <-> ( 1 ... 0 ) = (/) ) )
5 2 3 4 mp2an 
 |-  ( 0 < 1 <-> ( 1 ... 0 ) = (/) )
6 1 5 mpbi 
 |-  ( 1 ... 0 ) = (/)