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 ∥ 𝑧 }