Description: Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nn0ob | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0o | |
|
2 | nn0cn | |
|
3 | xp1d2m1eqxm1d2 | |
|
4 | 3 | eqcomd | |
5 | 2 4 | syl | |
6 | peano2cnm | |
|
7 | 2 6 | syl | |
8 | 7 | halfcld | |
9 | 1cnd | |
|
10 | peano2nn0 | |
|
11 | 10 | nn0cnd | |
12 | 11 | halfcld | |
13 | 8 9 12 | addlsub | |
14 | 5 13 | mpbird | |
15 | 14 | adantr | |
16 | peano2nn0 | |
|
17 | 16 | adantl | |
18 | 15 17 | eqeltrrd | |
19 | 1 18 | impbida | |