Metamath Proof Explorer


Theorem dfeven4

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

Ref Expression
Assertion dfeven4 Even = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) }

Proof

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