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 ∈ ℤ
3 0z 0 ∈ ℤ
4 fzn ( ( 1 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 0 < 1 ↔ ( 1 ... 0 ) = ∅ ) )
5 2 3 4 mp2an ( 0 < 1 ↔ ( 1 ... 0 ) = ∅ )
6 1 5 mpbi ( 1 ... 0 ) = ∅