Theorem dfodd7

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

	Ref	Expression
Assertion	dfodd7	$$⊢\mathrm{Odd}=\left\{z\in \mathbb{Z}|2\gcd z=1\right\}$$

Proof

Step	Hyp	Ref	Expression
1		isodd7	$$⊢x\in \mathrm{Odd}\leftrightarrow \left(x\in \mathbb{Z}\wedge 2\gcd x=1\right)$$
2		oveq2	$$⊢z=x\to 2\gcd z=2\gcd x$$
3	2	eqeq1d	$$⊢z=x\to \left(2\gcd z=1\leftrightarrow 2\gcd x=1\right)$$
4	3	elrab	$$⊢x\in \left\{z\in \mathbb{Z}|2\gcd z=1\right\}\leftrightarrow \left(x\in \mathbb{Z}\wedge 2\gcd x=1\right)$$
5	1 4	bitr4i	$$⊢x\in \mathrm{Odd}\leftrightarrow x\in \left\{z\in \mathbb{Z}|2\gcd z=1\right\}$$
6	5	eqriv	$$⊢\mathrm{Odd}=\left\{z\in \mathbb{Z}|2\gcd z=1\right\}$$