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

Metamath Proof Explorer

Theorem dfodd3

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

Ref Expression
Assertion dfodd3 Odd = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }

Proof

Step Hyp Ref Expression
1 dfodd6 ⊢ Odd = { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) }
2 eqcom ⊢ ( 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ↔ ( ( 2 · 𝑖 ) + 1 ) = 𝑧 )
3 2 a1i ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ↔ ( ( 2 · 𝑖 ) + 1 ) = 𝑧 ) )
4 3 rexbidva ⊢ ( 𝑧 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ↔ ∃ 𝑖 ∈ ℤ ( ( 2 · 𝑖 ) + 1 ) = 𝑧 ) )
5 odd2np1 ⊢ ( 𝑧 ∈ ℤ → ( ¬ 2 ∥ 𝑧 ↔ ∃ 𝑖 ∈ ℤ ( ( 2 · 𝑖 ) + 1 ) = 𝑧 ) )
6 4 5 bitr4d ⊢ ( 𝑧 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) ↔ ¬ 2 ∥ 𝑧 ) )
7 6 rabbiia ⊢ { 𝑧 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑧 = ( ( 2 · 𝑖 ) + 1 ) } = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
8 1 7 eqtri ⊢ Odd = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }