Description: Define the set of odd numbers. (Contributed by AV, 14-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | df-odd |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | codd | ||
1 | vz | ||
2 | cz | ||
3 | 1 | cv | |
4 | caddc | ||
5 | c1 | ||
6 | 3 5 4 | co | |
7 | cdiv | ||
8 | c2 | ||
9 | 6 8 7 | co | |
10 | 9 2 | wcel | |
11 | 10 1 2 | crab | |
12 | 0 11 | wceq |