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