Metamath Proof Explorer


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 mulid1 ( 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 ∈ 𝐸