Definition df-odd

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

	Ref	Expression
Assertion	df-odd	|- Odd = { z e. ZZ | ( ( z + 1 ) / 2 ) e. ZZ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		codd	|- Odd
1		vz	|- z
2		cz	|- ZZ
3	1	cv	|- z
4		caddc	|- +
5		c1	|- 1
6	3 5 4	co	|- ( z + 1 )
7		cdiv	|- /
8		c2	|- 2
9	6 8 7	co	|- ( ( z + 1 ) / 2 )
10	9 2	wcel	|- ( ( z + 1 ) / 2 ) e. ZZ
11	10 1 2	crab	|- { z e. ZZ | ( ( z + 1 ) / 2 ) e. ZZ }
12	0 11	wceq	|- Odd = { z e. ZZ | ( ( z + 1 ) / 2 ) e. ZZ }