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\in ℂ$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5		expp1	$$⊢\left(2\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to 2^{2+1}=2^2\cdot 2$$
6	3 4 5	mp2an	$$⊢2^{2+1}=2^2\cdot 2$$
7		sq2	$$⊢2^2=4$$
8	7	oveq1i	$$⊢2^2\cdot 2=4\cdot 2$$
9		4t2e8	$$⊢4\cdot 2=8$$
10	8 9	eqtri	$$⊢2^2\cdot 2=8$$
11	6 10	eqtri	$$⊢2^{2+1}=8$$
12	2 11	eqtri	$$⊢2^3=8$$