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 ) )