Theorem 0even

Description: 0 is an even integer. (Contributed by AV, 11-Feb-2020)

	Ref	Expression
Hypothesis	2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
Assertion	0even	⊢ 0 ∈ 𝐸

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		0z	⊢ 0 ∈ ℤ
3		2cn	⊢ 2 ∈ ℂ
4		0zd	⊢ ( 2 ∈ ℂ → 0 ∈ ℤ )
5		oveq2	⊢ ( 𝑥 = 0 → ( 2 · 𝑥 ) = ( 2 · 0 ) )
6	5	eqeq2d	⊢ ( 𝑥 = 0 → ( 0 = ( 2 · 𝑥 ) ↔ 0 = ( 2 · 0 ) ) )
7	6	adantl	⊢ ( ( 2 ∈ ℂ ∧ 𝑥 = 0 ) → ( 0 = ( 2 · 𝑥 ) ↔ 0 = ( 2 · 0 ) ) )
8		mul01	⊢ ( 2 ∈ ℂ → ( 2 · 0 ) = 0 )
9	8	eqcomd	⊢ ( 2 ∈ ℂ → 0 = ( 2 · 0 ) )
10	4 7 9	rspcedvd	⊢ ( 2 ∈ ℂ → ∃ 𝑥 ∈ ℤ 0 = ( 2 · 𝑥 ) )
11	3 10	ax-mp	⊢ ∃ 𝑥 ∈ ℤ 0 = ( 2 · 𝑥 )
12		eqeq1	⊢ ( 𝑧 = 0 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 0 = ( 2 · 𝑥 ) ) )
13	12	rexbidv	⊢ ( 𝑧 = 0 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 0 = ( 2 · 𝑥 ) ) )
14	13	elrab	⊢ ( 0 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ↔ ( 0 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 0 = ( 2 · 𝑥 ) ) )
15	2 11 14	mpbir2an	⊢ 0 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
16	15 1	eleqtrri	⊢ 0 ∈ 𝐸