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	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\le 2\right)\to N^N<6$$

Proof

Step	Hyp	Ref	Expression
1		nn0le2is012	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\le 2\right)\to \left(N=0\vee N=1\vee N=2\right)$$
2		id	$$⊢N=0\to N=0$$
3	2 2	oveq12d	$$⊢N=0\to 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\to N^N<6$$
8		id	$$⊢N=1\to N=1$$
9	8 8	oveq12d	$$⊢N=1\to N^N=1^1$$
10		ax-1cn	$$⊢1\in ℂ$$
11		exp1	$$⊢1\in ℂ\to 1^1=1$$
12	10 11	ax-mp	$$⊢1^1=1$$
13	12 5	eqbrtri	$$⊢1^1<6$$
14	9 13	eqbrtrdi	$$⊢N=1\to N^N<6$$
15		id	$$⊢N=2\to N=2$$
16	15 15	oveq12d	$$⊢N=2\to 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\to N^N<6$$
21	7 14 20	3jaoi	$$⊢\left(N=0\vee N=1\vee N=2\right)\to N^N<6$$
22	1 21	syl	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\le 2\right)\to N^N<6$$