Metamath Proof Explorer

Theorem xnn0le2is012

Description: An extended nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 24-Nov-2021)

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

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 xnn0lenn0nn0 
 |-  ( ( N e. NN0* /\ 2 e. NN0 /\ N <_ 2 ) -> N e. NN0 )
3 1 2 mp3an2 
 |-  ( ( N e. NN0* /\ N <_ 2 ) -> N e. NN0 )
4 nn0le2is012 
 |-  ( ( N e. NN0 /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) )
5 3 4 sylancom 
 |-  ( ( N e. NN0* /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) )