Description: A number is zero if and only if it's a nonnegative integer that becomes negative after subtracting 1. (Contributed by BTernaryTau, 30-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | 0nn0m1nnn0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0nn0 | |
|
2 | eleq1 | |
|
3 | 1 2 | mpbiri | |
4 | 1nn | |
|
5 | 0mnnnnn0 | |
|
6 | 4 5 | ax-mp | |
7 | oveq1 | |
|
8 | neleq1 | |
|
9 | 7 8 | syl | |
10 | 6 9 | mpbiri | |
11 | df-nel | |
|
12 | 10 11 | sylib | |
13 | 3 12 | jca | |
14 | nn0z | |
|
15 | peano2zm | |
|
16 | 14 15 | syl | |
17 | elnn0z | |
|
18 | 17 | notbii | |
19 | 18 | biimpi | |
20 | annotanannot | |
|
21 | 20 | simprbi | |
22 | 16 19 21 | syl2an | |
23 | zre | |
|
24 | 14 15 23 | 3syl | |
25 | 0red | |
|
26 | 24 25 | ltnled | |
27 | 26 | biimprd | |
28 | 27 | adantr | |
29 | 22 28 | mpd | |
30 | 0z | |
|
31 | zlem1lt | |
|
32 | 14 30 31 | sylancl | |
33 | 32 | biimprd | |
34 | 33 | adantr | |
35 | 29 34 | mpd | |
36 | nn0ge0 | |
|
37 | 36 | adantr | |
38 | nn0re | |
|
39 | 38 25 | letri3d | |
40 | 39 | biimprd | |
41 | 40 | adantr | |
42 | 35 37 41 | mp2and | |
43 | 13 42 | impbii | |