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