0even

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

Step	Hyp	Ref	Expression
1		2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
2		0z	$⊢ 0 \in ℤ$
3		2cn	$⊢ 2 \in ℂ$
4		0zd	$⊢ 2 \in ℂ \to 0 \in ℤ$
5		oveq2	$⊢ x = 0 \to 2 x = 2 \cdot 0$
6	5	eqeq2d	$⊢ x = 0 \to (0 = 2 x \leftrightarrow 0 = 2 \cdot 0)$
7	6	adantl	$⊢ (2 \in ℂ \land x = 0) \to (0 = 2 x \leftrightarrow 0 = 2 \cdot 0)$
8		mul01	$⊢ 2 \in ℂ \to 2 \cdot 0 = 0$
9	8	eqcomd	$⊢ 2 \in ℂ \to 0 = 2 \cdot 0$
10	4 7 9	rspcedvd	$⊢ 2 \in ℂ \to \exists x \in ℤ 0 = 2 x$
11	3 10	ax-mp	$⊢ \exists x \in ℤ 0 = 2 x$
12		eqeq1	$⊢ z = 0 \to (z = 2 x \leftrightarrow 0 = 2 x)$
13	12	rexbidv	$⊢ z = 0 \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ 0 = 2 x)$
14	13	elrab	$⊢ 0 \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \leftrightarrow (0 \in ℤ \land \exists x \in ℤ 0 = 2 x)$
15	2 11 14	mpbir2an	$⊢ 0 \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
16	15 1	eleqtrri	$⊢ 0 \in E$

Metamath Proof Explorer