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

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 \dots 0) = \emptyset$

Step	Hyp	Ref	Expression
1		0lt1	$⊢ 0 < 1$
2		1z	$⊢ 1 \in ℤ$
3		0z	$⊢ 0 \in ℤ$
4		fzn	$⊢ (1 \in ℤ \land 0 \in ℤ) \to (0 < 1 \leftrightarrow (1 \dots 0) = \emptyset)$
5	2 3 4	mp2an	$⊢ 0 < 1 \leftrightarrow (1 \dots 0) = \emptyset$
6	1 5	mpbi	$⊢ (1 \dots 0) = \emptyset$