Metamath Proof Explorer

Theorem dfeven2

Description: Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020)

Ref Expression
Assertion dfeven2 ⊢ Even = z ∈ ℤ | 2 ∥ z

Proof

Step Hyp Ref Expression
1 dfeven4 ⊢ Even = z ∈ ℤ | ∃ i ∈ ℤ z = 2 ⁢ i
2 eqcom ⊢ z = 2 ⁢ i ↔ 2 ⁢ i = z
3 2cnd ⊢ z ∈ ℤ ∧ i ∈ ℤ → 2 ∈ ℂ
4 zcn ⊢ i ∈ ℤ → i ∈ ℂ
5 4 adantl ⊢ z ∈ ℤ ∧ i ∈ ℤ → i ∈ ℂ
6 3 5 mulcomd ⊢ z ∈ ℤ ∧ i ∈ ℤ → 2 ⁢ i = i ⋅ 2
7 6 eqeq1d ⊢ z ∈ ℤ ∧ i ∈ ℤ → 2 ⁢ i = z ↔ i ⋅ 2 = z
8 2 7 bitrid ⊢ z ∈ ℤ ∧ i ∈ ℤ → z = 2 ⁢ i ↔ i ⋅ 2 = z
9 8 rexbidva ⊢ z ∈ ℤ → ∃ i ∈ ℤ z = 2 ⁢ i ↔ ∃ i ∈ ℤ i ⋅ 2 = z
10 2z ⊢ 2 ∈ ℤ
11 divides ⊢ 2 ∈ ℤ ∧ z ∈ ℤ → 2 ∥ z ↔ ∃ i ∈ ℤ i ⋅ 2 = z
12 10 11 mpan ⊢ z ∈ ℤ → 2 ∥ z ↔ ∃ i ∈ ℤ i ⋅ 2 = z
13 9 12 bitr4d ⊢ z ∈ ℤ → ∃ i ∈ ℤ z = 2 ⁢ i ↔ 2 ∥ z
14 13 rabbiia ⊢ z ∈ ℤ | ∃ i ∈ ℤ z = 2 ⁢ i = z ∈ ℤ | 2 ∥ z
15 1 14 eqtri ⊢ Even = z ∈ ℤ | 2 ∥ z