Metamath Proof Explorer


Theorem 0nn0m1nnn0

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 N=0N0¬N10

Proof

Step Hyp Ref Expression
1 0nn0 00
2 eleq1 N=0N000
3 1 2 mpbiri N=0N0
4 1nn 1
5 0mnnnnn0 1010
6 4 5 ax-mp 010
7 oveq1 N=0N1=01
8 neleq1 N1=01N10010
9 7 8 syl N=0N10010
10 6 9 mpbiri N=0N10
11 df-nel N10¬N10
12 10 11 sylib N=0¬N10
13 3 12 jca N=0N0¬N10
14 nn0z N0N
15 peano2zm NN1
16 14 15 syl N0N1
17 elnn0z N10N10N1
18 17 notbii ¬N10¬N10N1
19 18 biimpi ¬N10¬N10N1
20 annotanannot N1¬N10N1N1¬0N1
21 20 simprbi N1¬N10N1¬0N1
22 16 19 21 syl2an N0¬N10¬0N1
23 zre N1N1
24 14 15 23 3syl N0N1
25 0red N00
26 24 25 ltnled N0N1<0¬0N1
27 26 biimprd N0¬0N1N1<0
28 27 adantr N0¬N10¬0N1N1<0
29 22 28 mpd N0¬N10N1<0
30 0z 0
31 zlem1lt N0N0N1<0
32 14 30 31 sylancl N0N0N1<0
33 32 biimprd N0N1<0N0
34 33 adantr N0¬N10N1<0N0
35 29 34 mpd N0¬N10N0
36 nn0ge0 N00N
37 36 adantr N0¬N100N
38 nn0re N0N
39 38 25 letri3d N0N=0N00N
40 39 biimprd N0N00NN=0
41 40 adantr N0¬N10N00NN=0
42 35 37 41 mp2and N0¬N10N=0
43 13 42 impbii N=0N0¬N10