Description: An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020) (Proof shortened by AV, 2-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nn0o | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0o1gt2 | |
|
2 | 1m1e0 | |
|
3 | 2 | oveq1i | |
4 | 2cn | |
|
5 | 2ne0 | |
|
6 | 4 5 | div0i | |
7 | 3 6 | eqtri | |
8 | 0nn0 | |
|
9 | 7 8 | eqeltri | |
10 | oveq1 | |
|
11 | 10 | oveq1d | |
12 | 11 | eleq1d | |
13 | 12 | adantr | |
14 | 9 13 | mpbiri | |
15 | 14 | ex | |
16 | 2z | |
|
17 | 16 | a1i | |
18 | nn0z | |
|
19 | 18 | ad2antrl | |
20 | 2re | |
|
21 | nn0re | |
|
22 | ltle | |
|
23 | 20 21 22 | sylancr | |
24 | 23 | adantr | |
25 | 24 | impcom | |
26 | eluz2 | |
|
27 | 17 19 25 26 | syl3anbrc | |
28 | simprr | |
|
29 | 27 28 | jca | |
30 | nno | |
|
31 | nnnn0 | |
|
32 | 29 30 31 | 3syl | |
33 | 32 | ex | |
34 | 15 33 | jaoi | |
35 | 1 34 | mpcom | |