Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-odd | Structured version Visualization version GIF version |
Description: Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.) |
Ref | Expression |
---|---|
df-odd | ⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | codd 45572 | . 2 class Odd | |
2 | vz | . . . . . . 7 setvar 𝑧 | |
3 | 2 | cv 1541 | . . . . . 6 class 𝑧 |
4 | c1 10986 | . . . . . 6 class 1 | |
5 | caddc 10988 | . . . . . 6 class + | |
6 | 3, 4, 5 | co 7350 | . . . . 5 class (𝑧 + 1) |
7 | c2 12142 | . . . . 5 class 2 | |
8 | cdiv 11746 | . . . . 5 class / | |
9 | 6, 7, 8 | co 7350 | . . . 4 class ((𝑧 + 1) / 2) |
10 | cz 12433 | . . . 4 class ℤ | |
11 | 9, 10 | wcel 2107 | . . 3 wff ((𝑧 + 1) / 2) ∈ ℤ |
12 | 11, 2, 10 | crab 3406 | . 2 class {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ} |
13 | 1, 12 | wceq 1542 | 1 wff Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ} |
Colors of variables: wff setvar class |
This definition is referenced by: isodd 45576 |
Copyright terms: Public domain | W3C validator |