Theorem 2even

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

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

Proof

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