Theorem dfodd5

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

	Ref	Expression
Assertion	dfodd5	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) ≠ 0 }

Proof

Step	Hyp	Ref	Expression
1		dfodd4	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) = 1 }
2		elmod2	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 mod 2 ) ∈ { 0 , 1 } )
3		prcom	⊢ { 0 , 1 } = { 1 , 0 }
4	3	eleq2i	⊢ ( ( 𝑧 mod 2 ) ∈ { 0 , 1 } ↔ ( 𝑧 mod 2 ) ∈ { 1 , 0 } )
5	4	biimpi	⊢ ( ( 𝑧 mod 2 ) ∈ { 0 , 1 } → ( 𝑧 mod 2 ) ∈ { 1 , 0 } )
6		ax-1ne0	⊢ 1 ≠ 0
7		elprneb	⊢ ( ( ( 𝑧 mod 2 ) ∈ { 1 , 0 } ∧ 1 ≠ 0 ) → ( ( 𝑧 mod 2 ) = 1 ↔ ( 𝑧 mod 2 ) ≠ 0 ) )
8	5 6 7	sylancl	⊢ ( ( 𝑧 mod 2 ) ∈ { 0 , 1 } → ( ( 𝑧 mod 2 ) = 1 ↔ ( 𝑧 mod 2 ) ≠ 0 ) )
9	2 8	syl	⊢ ( 𝑧 ∈ ℤ → ( ( 𝑧 mod 2 ) = 1 ↔ ( 𝑧 mod 2 ) ≠ 0 ) )
10	9	rabbiia	⊢ { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) = 1 } = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) ≠ 0 }
11	1 10	eqtri	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( 𝑧 mod 2 ) ≠ 0 }