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 ) = ∅