Detailed syntax breakdown of Definition df-odd
Step | Hyp | Ref
| Expression |
1 | | codd 45088 |
. 2
class
Odd |
2 | | vz |
. . . . . . 7
setvar 𝑧 |
3 | 2 | cv 1538 |
. . . . . 6
class 𝑧 |
4 | | c1 10881 |
. . . . . 6
class
1 |
5 | | caddc 10883 |
. . . . . 6
class
+ |
6 | 3, 4, 5 | co 7284 |
. . . . 5
class (𝑧 + 1) |
7 | | c2 12037 |
. . . . 5
class
2 |
8 | | cdiv 11641 |
. . . . 5
class
/ |
9 | 6, 7, 8 | co 7284 |
. . . 4
class ((𝑧 + 1) / 2) |
10 | | cz 12328 |
. . . 4
class
ℤ |
11 | 9, 10 | wcel 2107 |
. . 3
wff ((𝑧 + 1) / 2) ∈
ℤ |
12 | 11, 2, 10 | crab 3069 |
. 2
class {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈
ℤ} |
13 | 1, 12 | wceq 1539 |
1
wff Odd =
{𝑧 ∈ ℤ ∣
((𝑧 + 1) / 2) ∈
ℤ} |