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

Metamath Proof Explorer

Theorem dfeven2

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

Ref Expression
Assertion dfeven2 Even = { 𝑧 ∈ ℤ ∣ 2 ∥ 𝑧 }

Proof

Step Hyp Ref Expression
1 dfeven4 ⊢ Even = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) }
2 eqcom ⊢ ( 𝑧 = ( 2 · 𝑖 ) ↔ ( 2 · 𝑖 ) = 𝑧 )
3 2cnd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 2 ∈ ℂ )
4 zcn ⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ )
5 4 adantl ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℂ )
6 3 5 mulcomd ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 2 · 𝑖 ) = ( 𝑖 · 2 ) )
7 6 eqeq1d ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 2 · 𝑖 ) = 𝑧 ↔ ( 𝑖 · 2 ) = 𝑧 ) )
8 2 7 bitrid ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑧 = ( 2 · 𝑖 ) ↔ ( 𝑖 · 2 ) = 𝑧 ) )
9 8 rexbidva ⊢ ( 𝑧 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) ↔ ∃ 𝑖 ∈ ℤ ( 𝑖 · 2 ) = 𝑧 ) )
10 2z ⊢ 2 ∈ ℤ
11 divides ⊢ ( ( 2 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 2 ∥ 𝑧 ↔ ∃ 𝑖 ∈ ℤ ( 𝑖 · 2 ) = 𝑧 ) )
12 10 11 mpan ⊢ ( 𝑧 ∈ ℤ → ( 2 ∥ 𝑧 ↔ ∃ 𝑖 ∈ ℤ ( 𝑖 · 2 ) = 𝑧 ) )
13 9 12 bitr4d ⊢ ( 𝑧 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) ↔ 2 ∥ 𝑧 ) )
14 13 rabbiia ⊢ { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( 2 · 𝑖 ) } = { 𝑧 ∈ ℤ ∣ 2 ∥ 𝑧 }
15 1 14 eqtri ⊢ Even = { 𝑧 ∈ ℤ ∣ 2 ∥ 𝑧 }