Metamath Proof Explorer

Theorem nn0le2is012

Description: A nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 16-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( N e. NN0 -> N e. RR )
2 2re 
 |-  2 e. RR
3 2 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
4 1 3 leloed 
 |-  ( N e. NN0 -> ( N <_ 2 <-> ( N < 2 \/ N = 2 ) ) )
5 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
6 2z 
 |-  2 e. ZZ
7 zltlem1 
 |-  ( ( N e. ZZ /\ 2 e. ZZ ) -> ( N < 2 <-> N <_ ( 2 - 1 ) ) )
8 5 6 7 sylancl 
 |-  ( N e. NN0 -> ( N < 2 <-> N <_ ( 2 - 1 ) ) )
9 2m1e1 
 |-  ( 2 - 1 ) = 1
10 9 a1i 
 |-  ( N e. NN0 -> ( 2 - 1 ) = 1 )
11 10 breq2d 
 |-  ( N e. NN0 -> ( N <_ ( 2 - 1 ) <-> N <_ 1 ) )
12 8 11 bitrd 
 |-  ( N e. NN0 -> ( N < 2 <-> N <_ 1 ) )
13 1red 
 |-  ( N e. NN0 -> 1 e. RR )
14 1 13 leloed 
 |-  ( N e. NN0 -> ( N <_ 1 <-> ( N < 1 \/ N = 1 ) ) )
15 nn0lt10b 
 |-  ( N e. NN0 -> ( N < 1 <-> N = 0 ) )
16 3mix1 
 |-  ( N = 0 -> ( N = 0 \/ N = 1 \/ N = 2 ) )
17 15 16 biimtrdi 
 |-  ( N e. NN0 -> ( N < 1 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
18 17 com12 
 |-  ( N < 1 -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
19 3mix2 
 |-  ( N = 1 -> ( N = 0 \/ N = 1 \/ N = 2 ) )
20 19 a1d 
 |-  ( N = 1 -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
21 18 20 jaoi 
 |-  ( ( N < 1 \/ N = 1 ) -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
22 21 com12 
 |-  ( N e. NN0 -> ( ( N < 1 \/ N = 1 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
23 14 22 sylbid 
 |-  ( N e. NN0 -> ( N <_ 1 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
24 12 23 sylbid 
 |-  ( N e. NN0 -> ( N < 2 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
25 24 com12 
 |-  ( N < 2 -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
26 3mix3 
 |-  ( N = 2 -> ( N = 0 \/ N = 1 \/ N = 2 ) )
27 26 a1d 
 |-  ( N = 2 -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
28 25 27 jaoi 
 |-  ( ( N < 2 \/ N = 2 ) -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
29 28 com12 
 |-  ( N e. NN0 -> ( ( N < 2 \/ N = 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
30 4 29 sylbid 
 |-  ( N e. NN0 -> ( N <_ 2 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) )
31 30 imp 
 |-  ( ( N e. NN0 /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) )