Theorem dfodd2

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

	Ref	Expression
Assertion	dfodd2	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ }

Proof

Step	Hyp	Ref	Expression
1		isodd2	⊢ ( 𝑥 ∈ Odd ↔ ( 𝑥 ∈ ℤ ∧ ( ( 𝑥 − 1 ) / 2 ) ∈ ℤ ) )
2		oveq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 − 1 ) = ( 𝑥 − 1 ) )
3	2	oveq1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 − 1 ) / 2 ) = ( ( 𝑥 − 1 ) / 2 ) )
4	3	eleq1d	⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑥 − 1 ) / 2 ) ∈ ℤ ) )
5	4	elrab	⊢ ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ } ↔ ( 𝑥 ∈ ℤ ∧ ( ( 𝑥 − 1 ) / 2 ) ∈ ℤ ) )
6	1 5	bitr4i	⊢ ( 𝑥 ∈ Odd ↔ 𝑥 ∈ { 𝑧 ∈ ℤ ∣ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ } )
7	6	eqriv	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( ( 𝑧 − 1 ) / 2 ) ∈ ℤ }