Definition df-odd

Description: Define the set of odd numbers. (Contributed by AV, 14-Jun-2020)

	Ref	Expression
Assertion	df-odd	$$⊢\mathrm{Odd}=\left\{z\in \mathbb{Z}|\frac{z+1}{2}\in \mathbb{Z}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		codd	$$class\mathrm{Odd}$$
1		vz	$$setvarz$$
2		cz	$$class\mathbb{Z}$$
3	1	cv	$$setvarz$$
4		caddc	$$class+$$
5		c1	$$class1$$
6	3 5 4	co	$$class\left(z+1\right)$$
7		cdiv	$$class÷$$
8		c2	$$class2$$
9	6 8 7	co	$$class\left(\frac{z+1}{2}\right)$$
10	9 2	wcel	$$wff\frac{z+1}{2}\in \mathbb{Z}$$
11	10 1 2	crab	$$class\left\{z\in \mathbb{Z}|\frac{z+1}{2}\in \mathbb{Z}\right\}$$
12	0 11	wceq	$$wff\mathrm{Odd}=\left\{z\in \mathbb{Z}|\frac{z+1}{2}\in \mathbb{Z}\right\}$$