Metamath Proof Explorer

Theorem 2even

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

Ref Expression
Hypothesis 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
Assertion 2even ⊢ 2 ∈ E

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2 2z ⊢ 2 ∈ ℤ
3 2cn ⊢ 2 ∈ ℂ
4 1zzd ⊢ 2 ∈ ℂ → 1 ∈ ℤ
5 oveq2 ⊢ x = 1 → 2 ⁢ x = 2 ⋅ 1
6 5 eqeq2d ⊢ x = 1 → 2 = 2 ⁢ x ↔ 2 = 2 ⋅ 1
7 6 adantl ⊢ 2 ∈ ℂ ∧ x = 1 → 2 = 2 ⁢ x ↔ 2 = 2 ⋅ 1
8 mulid1 ⊢ 2 ∈ ℂ → 2 ⋅ 1 = 2
9 8 eqcomd ⊢ 2 ∈ ℂ → 2 = 2 ⋅ 1
10 4 7 9 rspcedvd ⊢ 2 ∈ ℂ → ∃ x ∈ ℤ 2 = 2 ⁢ x
11 3 10 ax-mp ⊢ ∃ x ∈ ℤ 2 = 2 ⁢ x
12 eqeq1 ⊢ z = 2 → z = 2 ⁢ x ↔ 2 = 2 ⁢ x
13 12 rexbidv ⊢ z = 2 → ∃ x ∈ ℤ z = 2 ⁢ x ↔ ∃ x ∈ ℤ 2 = 2 ⁢ x
14 13 elrab ⊢ 2 ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ↔ 2 ∈ ℤ ∧ ∃ x ∈ ℤ 2 = 2 ⁢ x
15 2 11 14 mpbir2an ⊢ 2 ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
16 15 1 eleqtrri ⊢ 2 ∈ E