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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2 ) → ( 𝑁 ↑ 𝑁 ) < 6 )

Proof

Step	Hyp	Ref	Expression
1		nn0le2is012	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) )
2		id	⊢ ( 𝑁 = 0 → 𝑁 = 0 )
3	2 2	oveq12d	⊢ ( 𝑁 = 0 → ( 𝑁 ↑ 𝑁 ) = ( 0 ↑ 0 ) )
4		0exp0e1	⊢ ( 0 ↑ 0 ) = 1
5		1lt6	⊢ 1 < 6
6	4 5	eqbrtri	⊢ ( 0 ↑ 0 ) < 6
7	3 6	eqbrtrdi	⊢ ( 𝑁 = 0 → ( 𝑁 ↑ 𝑁 ) < 6 )
8		id	⊢ ( 𝑁 = 1 → 𝑁 = 1 )
9	8 8	oveq12d	⊢ ( 𝑁 = 1 → ( 𝑁 ↑ 𝑁 ) = ( 1 ↑ 1 ) )
10		ax-1cn	⊢ 1 ∈ ℂ
11		exp1	⊢ ( 1 ∈ ℂ → ( 1 ↑ 1 ) = 1 )
12	10 11	ax-mp	⊢ ( 1 ↑ 1 ) = 1
13	12 5	eqbrtri	⊢ ( 1 ↑ 1 ) < 6
14	9 13	eqbrtrdi	⊢ ( 𝑁 = 1 → ( 𝑁 ↑ 𝑁 ) < 6 )
15		id	⊢ ( 𝑁 = 2 → 𝑁 = 2 )
16	15 15	oveq12d	⊢ ( 𝑁 = 2 → ( 𝑁 ↑ 𝑁 ) = ( 2 ↑ 2 ) )
17		sq2	⊢ ( 2 ↑ 2 ) = 4
18		4lt6	⊢ 4 < 6
19	17 18	eqbrtri	⊢ ( 2 ↑ 2 ) < 6
20	16 19	eqbrtrdi	⊢ ( 𝑁 = 2 → ( 𝑁 ↑ 𝑁 ) < 6 )
21	7 14 20	3jaoi	⊢ ( ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) → ( 𝑁 ↑ 𝑁 ) < 6 )
22	1 21	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2 ) → ( 𝑁 ↑ 𝑁 ) < 6 )