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

Metamath Proof Explorer

Theorem 1nuz2

Description: 1 is not in ( ZZ>=2 ) . (Contributed by Paul Chapman, 21-Nov-2012)

		Ref	Expression
	Assertion	1nuz2	$⊢ \neg 1 \in ℤ_{\geq 2}$

Step	Hyp	Ref	Expression
1		neirr	$⊢ \neg 1 \neq 1$
2		eluz2b3	$⊢ 1 \in ℤ_{\geq 2} \leftrightarrow (1 \in ℕ \land 1 \neq 1)$
3	2	simprbi	$⊢ 1 \in ℤ_{\geq 2} \to 1 \neq 1$
4	1 3	mto	$⊢ \neg 1 \in ℤ_{\geq 2}$