1neven

		Ref	Expression
	Hypothesis	2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
	Assertion	1neven	$⊢ 1 \notin E$

Step	Hyp	Ref	Expression
1		2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
2		halfnz	$⊢ \neg \frac{1}{2} \in ℤ$
3		eleq1a	$⊢ x \in ℤ \to (\frac{1}{2} = x \to \frac{1}{2} \in ℤ)$
4	2 3	mtoi	$⊢ x \in ℤ \to \neg \frac{1}{2} = x$
5		1cnd	$⊢ x \in ℤ \to 1 \in ℂ$
6		zcn	$⊢ x \in ℤ \to x \in ℂ$
7		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
8	7	a1i	$⊢ x \in ℤ \to (2 \in ℂ \land 2 \neq 0)$
9		divmul2	$⊢ (1 \in ℂ \land x \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to (\frac{1}{2} = x \leftrightarrow 1 = 2 x)$
10	5 6 8 9	syl3anc	$⊢ x \in ℤ \to (\frac{1}{2} = x \leftrightarrow 1 = 2 x)$
11	4 10	mtbid	$⊢ x \in ℤ \to \neg 1 = 2 x$
12	11	nrex	$⊢ \neg \exists x \in ℤ 1 = 2 x$
13	12	intnan	$⊢ \neg (1 \in ℤ \land \exists x \in ℤ 1 = 2 x)$
14		eqeq1	$⊢ z = 1 \to (z = 2 x \leftrightarrow 1 = 2 x)$
15	14	rexbidv	$⊢ z = 1 \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ 1 = 2 x)$
16	15 1	elrab2	$⊢ 1 \in E \leftrightarrow (1 \in ℤ \land \exists x \in ℤ 1 = 2 x)$
17	13 16	mtbir	$⊢ \neg 1 \in E$
18	17	nelir	$⊢ 1 \notin E$

Metamath Proof Explorer