Theorem cu2

Description: The cube of 2 is 8. (Contributed by NM, 2-Aug-2004)

	Ref	Expression
Assertion	cu2	⊢ ( 2 ↑ 3 ) = 8

Proof

Step	Hyp	Ref	Expression
1		df-3	⊢ 3 = ( 2 + 1 )
2	1	oveq2i	⊢ ( 2 ↑ 3 ) = ( 2 ↑ ( 2 + 1 ) )
3		2cn	⊢ 2 ∈ ℂ
4		2nn0	⊢ 2 ∈ ℕ0
5		expp1	⊢ ( ( 2 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 2 ↑ ( 2 + 1 ) ) = ( ( 2 ↑ 2 ) · 2 ) )
6	3 4 5	mp2an	⊢ ( 2 ↑ ( 2 + 1 ) ) = ( ( 2 ↑ 2 ) · 2 )
7		sq2	⊢ ( 2 ↑ 2 ) = 4
8	7	oveq1i	⊢ ( ( 2 ↑ 2 ) · 2 ) = ( 4 · 2 )
9		4t2e8	⊢ ( 4 · 2 ) = 8
10	8 9	eqtri	⊢ ( ( 2 ↑ 2 ) · 2 ) = 8
11	6 10	eqtri	⊢ ( 2 ↑ ( 2 + 1 ) ) = 8
12	2 11	eqtri	⊢ ( 2 ↑ 3 ) = 8