Definition df-odd 41540

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

Assertion

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

Detailed syntax breakdown of Definition df-odd

Step	Hyp	Ref	Expression
1		codd 41538	. 2 class Odd
2		vz	. . . . . . 7 setvar z
3	2	cv 1482	. . . . . 6 class z
4		c1 9937	. . . . . 6 class 1
5		caddc 9939	. . . . . 6 class +
6	3, 4, 5	co 6650	. . . . 5 class ( z + 1 )
7		c2 11070	. . . . 5 class 2
8		cdiv 10684	. . . . 5 class /
9	6, 7, 8	co 6650	. . . 4 class ( ( z + 1 ) / 2 )
10		cz 11377	. . . 4 class ZZ
11	9, 10	wcel 1990	. . 3 wff ( ( z + 1 ) / 2 ) e. ZZ
12	11, 2, 10	crab 2916	. 2 class { z e. ZZ | ( ( z + 1 ) / 2 ) e. ZZ }
13	1, 12	wceq 1483	1 wff Odd = { z e. ZZ | ( ( z + 1 ) / 2 ) e. ZZ }

This definition is referenced by:  isodd  41542