Metamath Proof Explorer

Theorem nn0lt10b

Description: A nonnegative integer less than 1 is 0 . (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by OpenAI, 25-Mar-2020)

Ref Expression
Assertion nn0lt10b 
|- ( N e. NN0 -> ( N < 1 <-> N = 0 ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 nnnlt1 
 |-  ( N e. NN -> -. N < 1 )
3 2 pm2.21d 
 |-  ( N e. NN -> ( N < 1 -> N = 0 ) )
4 ax-1 
 |-  ( N = 0 -> ( N < 1 -> N = 0 ) )
5 3 4 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( N < 1 -> N = 0 ) )
6 1 5 sylbi 
 |-  ( N e. NN0 -> ( N < 1 -> N = 0 ) )
7 0lt1 
 |-  0 < 1
8 breq1 
 |-  ( N = 0 -> ( N < 1 <-> 0 < 1 ) )
9 7 8 mpbiri 
 |-  ( N = 0 -> N < 1 )
10 6 9 impbid1 
 |-  ( N e. NN0 -> ( N < 1 <-> N = 0 ) )