Metamath Proof Explorer


Theorem nn0lt2

Description: A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018)

Ref Expression
Assertion nn0lt2
|- ( ( N e. NN0 /\ N < 2 ) -> ( N = 0 \/ N = 1 ) )

Proof

Step Hyp Ref Expression
1 olc
 |-  ( N = 1 -> ( N = 0 \/ N = 1 ) )
2 1 a1d
 |-  ( N = 1 -> ( ( N e. NN0 /\ N < 2 ) -> ( N = 0 \/ N = 1 ) ) )
3 nn0z
 |-  ( N e. NN0 -> N e. ZZ )
4 2z
 |-  2 e. ZZ
5 zltlem1
 |-  ( ( N e. ZZ /\ 2 e. ZZ ) -> ( N < 2 <-> N <_ ( 2 - 1 ) ) )
6 3 4 5 sylancl
 |-  ( N e. NN0 -> ( N < 2 <-> N <_ ( 2 - 1 ) ) )
7 2m1e1
 |-  ( 2 - 1 ) = 1
8 7 breq2i
 |-  ( N <_ ( 2 - 1 ) <-> N <_ 1 )
9 6 8 bitrdi
 |-  ( N e. NN0 -> ( N < 2 <-> N <_ 1 ) )
10 necom
 |-  ( N =/= 1 <-> 1 =/= N )
11 nn0re
 |-  ( N e. NN0 -> N e. RR )
12 1re
 |-  1 e. RR
13 ltlen
 |-  ( ( N e. RR /\ 1 e. RR ) -> ( N < 1 <-> ( N <_ 1 /\ 1 =/= N ) ) )
14 11 12 13 sylancl
 |-  ( N e. NN0 -> ( N < 1 <-> ( N <_ 1 /\ 1 =/= N ) ) )
15 nn0lt10b
 |-  ( N e. NN0 -> ( N < 1 <-> N = 0 ) )
16 15 biimpa
 |-  ( ( N e. NN0 /\ N < 1 ) -> N = 0 )
17 16 orcd
 |-  ( ( N e. NN0 /\ N < 1 ) -> ( N = 0 \/ N = 1 ) )
18 17 ex
 |-  ( N e. NN0 -> ( N < 1 -> ( N = 0 \/ N = 1 ) ) )
19 14 18 sylbird
 |-  ( N e. NN0 -> ( ( N <_ 1 /\ 1 =/= N ) -> ( N = 0 \/ N = 1 ) ) )
20 19 expd
 |-  ( N e. NN0 -> ( N <_ 1 -> ( 1 =/= N -> ( N = 0 \/ N = 1 ) ) ) )
21 10 20 syl7bi
 |-  ( N e. NN0 -> ( N <_ 1 -> ( N =/= 1 -> ( N = 0 \/ N = 1 ) ) ) )
22 9 21 sylbid
 |-  ( N e. NN0 -> ( N < 2 -> ( N =/= 1 -> ( N = 0 \/ N = 1 ) ) ) )
23 22 imp
 |-  ( ( N e. NN0 /\ N < 2 ) -> ( N =/= 1 -> ( N = 0 \/ N = 1 ) ) )
24 23 com12
 |-  ( N =/= 1 -> ( ( N e. NN0 /\ N < 2 ) -> ( N = 0 \/ N = 1 ) ) )
25 2 24 pm2.61ine
 |-  ( ( N e. NN0 /\ N < 2 ) -> ( N = 0 \/ N = 1 ) )