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