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 = 0 <-> ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) )

Proof

Step Hyp Ref Expression
1 0nn0 
 |-  0 e. NN0
2 eleq1 
 |-  ( N = 0 -> ( N e. NN0 <-> 0 e. NN0 ) )
3 1 2 mpbiri 
 |-  ( N = 0 -> N e. NN0 )
4 1nn 
 |-  1 e. NN
5 0mnnnnn0 
 |-  ( 1 e. NN -> ( 0 - 1 ) e/ NN0 )
6 4 5 ax-mp 
 |-  ( 0 - 1 ) e/ NN0
7 oveq1 
 |-  ( N = 0 -> ( N - 1 ) = ( 0 - 1 ) )
8 neleq1 
 |-  ( ( N - 1 ) = ( 0 - 1 ) -> ( ( N - 1 ) e/ NN0 <-> ( 0 - 1 ) e/ NN0 ) )
9 7 8 syl 
 |-  ( N = 0 -> ( ( N - 1 ) e/ NN0 <-> ( 0 - 1 ) e/ NN0 ) )
10 6 9 mpbiri 
 |-  ( N = 0 -> ( N - 1 ) e/ NN0 )
11 df-nel 
 |-  ( ( N - 1 ) e/ NN0 <-> -. ( N - 1 ) e. NN0 )
12 10 11 sylib 
 |-  ( N = 0 -> -. ( N - 1 ) e. NN0 )
13 3 12 jca 
 |-  ( N = 0 -> ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) )
14 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
15 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
16 14 15 syl 
 |-  ( N e. NN0 -> ( N - 1 ) e. ZZ )
17 elnn0z 
 |-  ( ( N - 1 ) e. NN0 <-> ( ( N - 1 ) e. ZZ /\ 0 <_ ( N - 1 ) ) )
18 17 notbii 
 |-  ( -. ( N - 1 ) e. NN0 <-> -. ( ( N - 1 ) e. ZZ /\ 0 <_ ( N - 1 ) ) )
19 18 biimpi 
 |-  ( -. ( N - 1 ) e. NN0 -> -. ( ( N - 1 ) e. ZZ /\ 0 <_ ( N - 1 ) ) )
20 annotanannot 
 |-  ( ( ( N - 1 ) e. ZZ /\ -. ( ( N - 1 ) e. ZZ /\ 0 <_ ( N - 1 ) ) ) <-> ( ( N - 1 ) e. ZZ /\ -. 0 <_ ( N - 1 ) ) )
21 20 simprbi 
 |-  ( ( ( N - 1 ) e. ZZ /\ -. ( ( N - 1 ) e. ZZ /\ 0 <_ ( N - 1 ) ) ) -> -. 0 <_ ( N - 1 ) )
22 16 19 21 syl2an 
 |-  ( ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) -> -. 0 <_ ( N - 1 ) )
23 zre 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. RR )
24 14 15 23 3syl 
 |-  ( N e. NN0 -> ( N - 1 ) e. RR )
25 0red 
 |-  ( N e. NN0 -> 0 e. RR )
26 24 25 ltnled 
 |-  ( N e. NN0 -> ( ( N - 1 ) < 0 <-> -. 0 <_ ( N - 1 ) ) )
27 26 biimprd 
 |-  ( N e. NN0 -> ( -. 0 <_ ( N - 1 ) -> ( N - 1 ) < 0 ) )
28 27 adantr 
 |-  ( ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) -> ( -. 0 <_ ( N - 1 ) -> ( N - 1 ) < 0 ) )
29 22 28 mpd 
 |-  ( ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) -> ( N - 1 ) < 0 )
30 0z 
 |-  0 e. ZZ
31 zlem1lt 
 |-  ( ( N e. ZZ /\ 0 e. ZZ ) -> ( N <_ 0 <-> ( N - 1 ) < 0 ) )
32 14 30 31 sylancl 
 |-  ( N e. NN0 -> ( N <_ 0 <-> ( N - 1 ) < 0 ) )
33 32 biimprd 
 |-  ( N e. NN0 -> ( ( N - 1 ) < 0 -> N <_ 0 ) )
34 33 adantr 
 |-  ( ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) -> ( ( N - 1 ) < 0 -> N <_ 0 ) )
35 29 34 mpd 
 |-  ( ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) -> N <_ 0 )
36 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
37 36 adantr 
 |-  ( ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) -> 0 <_ N )
38 nn0re 
 |-  ( N e. NN0 -> N e. RR )
39 38 25 letri3d 
 |-  ( N e. NN0 -> ( N = 0 <-> ( N <_ 0 /\ 0 <_ N ) ) )
40 39 biimprd 
 |-  ( N e. NN0 -> ( ( N <_ 0 /\ 0 <_ N ) -> N = 0 ) )
41 40 adantr 
 |-  ( ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) -> ( ( N <_ 0 /\ 0 <_ N ) -> N = 0 ) )
42 35 37 41 mp2and 
 |-  ( ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) -> N = 0 )
43 13 42 impbii 
 |-  ( N = 0 <-> ( N e. NN0 /\ -. ( N - 1 ) e. NN0 ) )