This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 · 𝑖 ) }