Metamath Proof Explorer

Theorem exple2lt6

Description: A nonnegative integer to the power of itself is less than 6 if it is less than or equal to 2. (Contributed by AV, 16-Mar-2019)

Ref Expression
Assertion exple2lt6 
|- ( ( N e. NN0 /\ N <_ 2 ) -> ( N ^ N ) < 6 )

Proof

Step Hyp Ref Expression
1 nn0le2is012 
 |-  ( ( N e. NN0 /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) )
2 id 
 |-  ( N = 0 -> N = 0 )
3 2 2 oveq12d 
 |-  ( N = 0 -> ( N ^ N ) = ( 0 ^ 0 ) )
4 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
5 1lt6 
 |-  1 < 6
6 4 5 eqbrtri 
 |-  ( 0 ^ 0 ) < 6
7 3 6 eqbrtrdi 
 |-  ( N = 0 -> ( N ^ N ) < 6 )
8 id 
 |-  ( N = 1 -> N = 1 )
9 8 8 oveq12d 
 |-  ( N = 1 -> ( N ^ N ) = ( 1 ^ 1 ) )
10 ax-1cn 
 |-  1 e. CC
11 exp1 
 |-  ( 1 e. CC -> ( 1 ^ 1 ) = 1 )
12 10 11 ax-mp 
 |-  ( 1 ^ 1 ) = 1
13 12 5 eqbrtri 
 |-  ( 1 ^ 1 ) < 6
14 9 13 eqbrtrdi 
 |-  ( N = 1 -> ( N ^ N ) < 6 )
15 id 
 |-  ( N = 2 -> N = 2 )
16 15 15 oveq12d 
 |-  ( N = 2 -> ( N ^ N ) = ( 2 ^ 2 ) )
17 sq2 
 |-  ( 2 ^ 2 ) = 4
18 4lt6 
 |-  4 < 6
19 17 18 eqbrtri 
 |-  ( 2 ^ 2 ) < 6
20 16 19 eqbrtrdi 
 |-  ( N = 2 -> ( N ^ N ) < 6 )
21 7 14 20 3jaoi 
 |-  ( ( N = 0 \/ N = 1 \/ N = 2 ) -> ( N ^ N ) < 6 )
22 1 21 syl 
 |-  ( ( N e. NN0 /\ N <_ 2 ) -> ( N ^ N ) < 6 )