dfodd2

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

		Ref	Expression
	Assertion	dfodd2	$⊢ Odd = \{z \in ℤ \| \frac{z - 1}{2} \in ℤ\}$

Step	Hyp	Ref	Expression
1		isodd2	$⊢ x \in Odd \leftrightarrow (x \in ℤ \land \frac{x - 1}{2} \in ℤ)$
2		oveq1	$⊢ z = x \to z - 1 = x - 1$
3	2	oveq1d	$⊢ z = x \to \frac{z - 1}{2} = \frac{x - 1}{2}$
4	3	eleq1d	$⊢ z = x \to (\frac{z - 1}{2} \in ℤ \leftrightarrow \frac{x - 1}{2} \in ℤ)$
5	4	elrab	$⊢ x \in \{z \in ℤ \| \frac{z - 1}{2} \in ℤ\} \leftrightarrow (x \in ℤ \land \frac{x - 1}{2} \in ℤ)$
6	1 5	bitr4i	$⊢ x \in Odd \leftrightarrow x \in \{z \in ℤ \| \frac{z - 1}{2} \in ℤ\}$
7	6	eqriv	$⊢ Odd = \{z \in ℤ \| \frac{z - 1}{2} \in ℤ\}$

Metamath Proof Explorer