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	$$⊢\left(1\dots 0\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0lt1	$$⊢0<1$$
2		1z	$$⊢1\in \mathbb{Z}$$
3		0z	$$⊢0\in \mathbb{Z}$$
4		fzn	$$⊢\left(1\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to \left(0<1\leftrightarrow \left(1\dots 0\right)=\varnothing \right)$$
5	2 3 4	mp2an	$$⊢0<1\leftrightarrow \left(1\dots 0\right)=\varnothing$$
6	1 5	mpbi	$$⊢\left(1\dots 0\right)=\varnothing$$