Definition df-odd 44967

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

Assertion

Ref	Expression
df-odd	⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}

Detailed syntax breakdown of Definition df-odd

Step	Hyp	Ref	Expression
1		codd 44965	. 2 class Odd
2		vz	. . . . . . 7 setvar 𝑧
3	2	cv 1538	. . . . . 6 class 𝑧
4		c1 10803	. . . . . 6 class 1
5		caddc 10805	. . . . . 6 class +
6	3, 4, 5	co 7255	. . . . 5 class (𝑧 + 1)
7		c2 11958	. . . . 5 class 2
8		cdiv 11562	. . . . 5 class /
9	6, 7, 8	co 7255	. . . 4 class ((𝑧 + 1) / 2)
10		cz 12249	. . . 4 class ℤ
11	9, 10	wcel 2108	. . 3 wff ((𝑧 + 1) / 2) ∈ ℤ
12	11, 2, 10	crab 3067	. 2 class {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}
13	1, 12	wceq 1539	1 wff Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}

This definition is referenced by:  isodd  44969