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

Metamath Proof Explorer

Theorem 1nevenALTV

Description: 1 is not an even number. (Contributed by AV, 12-Feb-2020) (Revised by AV, 18-Jun-2020)

		Ref	Expression
	Assertion	1nevenALTV	$⊢ 1 \notin Even$

Step	Hyp	Ref	Expression
1		1oddALTV	$⊢ 1 \in Odd$
2		1z	$⊢ 1 \in ℤ$
3		zeo2ALTV	$⊢ 1 \in ℤ \to (1 \in Even \leftrightarrow \neg 1 \in Odd)$
4	2 3	ax-mp	$⊢ 1 \in Even \leftrightarrow \neg 1 \in Odd$
5	4	con2bii	$⊢ 1 \in Odd \leftrightarrow \neg 1 \in Even$
6		df-nel	$⊢ 1 \notin Even \leftrightarrow \neg 1 \in Even$
7	5 6	bitr4i	$⊢ 1 \in Odd \leftrightarrow 1 \notin Even$
8	1 7	mpbi	$⊢ 1 \notin Even$