Definition df-odd

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		codd	⊢ Odd
1		vz	⊢ 𝑧
2		cz	⊢ ℤ
3	1	cv	⊢ 𝑧
4		caddc	⊢ +
5		c1	⊢ 1
6	3 5 4	co	⊢ ( 𝑧 + 1 )
7		cdiv	⊢ /
8		c2	⊢ 2
9	6 8 7	co	⊢ ( ( 𝑧 + 1 ) / 2 )
10	9 2	wcel	⊢ ( ( 𝑧 + 1 ) / 2 ) ∈ ℤ
11	10 1 2	crab	⊢ { 𝑧 ∈ ℤ ∣ ( ( 𝑧 + 1 ) / 2 ) ∈ ℤ }
12	0 11	wceq	⊢ Odd = { 𝑧 ∈ ℤ ∣ ( ( 𝑧 + 1 ) / 2 ) ∈ ℤ }