Metamath Proof Explorer

Theorem dfeven4

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

Ref Expression
Assertion dfeven4 ⊢ Even = z ∈ ℤ | ∃ i ∈ ℤ z = 2 ⁢ i

Proof

Step Hyp Ref Expression
1 df-even ⊢ Even = z ∈ ℤ | z 2 ∈ ℤ
2 simpr ⊢ z ∈ ℤ ∧ z 2 ∈ ℤ → z 2 ∈ ℤ
3 oveq2 ⊢ i = z 2 → 2 ⁢ i = 2 ⁢ z 2
4 3 eqeq2d ⊢ i = z 2 → z = 2 ⁢ i ↔ z = 2 ⁢ z 2
5 4 adantl ⊢ z ∈ ℤ ∧ z 2 ∈ ℤ ∧ i = z 2 → z = 2 ⁢ i ↔ z = 2 ⁢ z 2
6 zcn ⊢ z ∈ ℤ → z ∈ ℂ
7 6 adantr ⊢ z ∈ ℤ ∧ z 2 ∈ ℤ → z ∈ ℂ
8 2cnd ⊢ z ∈ ℤ ∧ z 2 ∈ ℤ → 2 ∈ ℂ
9 2ne0 ⊢ 2 ≠ 0
10 9 a1i ⊢ z ∈ ℤ ∧ z 2 ∈ ℤ → 2 ≠ 0
11 7 8 10 divcan2d ⊢ z ∈ ℤ ∧ z 2 ∈ ℤ → 2 ⁢ z 2 = z
12 11 eqcomd ⊢ z ∈ ℤ ∧ z 2 ∈ ℤ → z = 2 ⁢ z 2
13 2 5 12 rspcedvd ⊢ z ∈ ℤ ∧ z 2 ∈ ℤ → ∃ i ∈ ℤ z = 2 ⁢ i
14 13 ex ⊢ z ∈ ℤ → z 2 ∈ ℤ → ∃ i ∈ ℤ z = 2 ⁢ i
15 oveq1 ⊢ z = 2 ⁢ i → z 2 = 2 ⁢ i 2
16 zcn ⊢ i ∈ ℤ → i ∈ ℂ
17 16 adantl ⊢ z ∈ ℤ ∧ i ∈ ℤ → i ∈ ℂ
18 2cnd ⊢ z ∈ ℤ ∧ i ∈ ℤ → 2 ∈ ℂ
19 9 a1i ⊢ z ∈ ℤ ∧ i ∈ ℤ → 2 ≠ 0
20 17 18 19 divcan3d ⊢ z ∈ ℤ ∧ i ∈ ℤ → 2 ⁢ i 2 = i
21 15 20 sylan9eqr ⊢ z ∈ ℤ ∧ i ∈ ℤ ∧ z = 2 ⁢ i → z 2 = i
22 simpr ⊢ z ∈ ℤ ∧ i ∈ ℤ → i ∈ ℤ
23 22 adantr ⊢ z ∈ ℤ ∧ i ∈ ℤ ∧ z = 2 ⁢ i → i ∈ ℤ
24 21 23 eqeltrd ⊢ z ∈ ℤ ∧ i ∈ ℤ ∧ z = 2 ⁢ i → z 2 ∈ ℤ
25 24 rexlimdva2 ⊢ z ∈ ℤ → ∃ i ∈ ℤ z = 2 ⁢ i → z 2 ∈ ℤ
26 14 25 impbid ⊢ z ∈ ℤ → z 2 ∈ ℤ ↔ ∃ i ∈ ℤ z = 2 ⁢ i
27 26 rabbiia ⊢ z ∈ ℤ | z 2 ∈ ℤ = z ∈ ℤ | ∃ i ∈ ℤ z = 2 ⁢ i
28 1 27 eqtri ⊢ Even = z ∈ ℤ | ∃ i ∈ ℤ z = 2 ⁢ i