Metamath Proof Explorer

Theorem 0even

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

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

Proof

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