2exp5

		Ref	Expression
	Assertion	2exp5	$⊢ 2^{5} = 32$

Step	Hyp	Ref	Expression
1		3p2e5	$⊢ 3 + 2 = 5$
2	1	eqcomi	$⊢ 5 = 3 + 2$
3	2	oveq2i	$⊢ 2^{5} = 2^{3 + 2}$
4		2cn	$⊢ 2 \in ℂ$
5		3nn0	$⊢ 3 \in ℕ_{0}$
6		2nn0	$⊢ 2 \in ℕ_{0}$
7		expadd	$⊢ (2 \in ℂ \land 3 \in ℕ_{0} \land 2 \in ℕ_{0}) \to 2^{3 + 2} = 2^{3} 2^{2}$
8	4 5 6 7	mp3an	$⊢ 2^{3 + 2} = 2^{3} 2^{2}$
9		cu2	$⊢ 2^{3} = 8$
10		sq2	$⊢ 2^{2} = 4$
11	9 10	oveq12i	$⊢ 2^{3} 2^{2} = 8 \cdot 4$
12	8 11	eqtri	$⊢ 2^{3 + 2} = 8 \cdot 4$
13	3 12	eqtri	$⊢ 2^{5} = 8 \cdot 4$
14		8t4e32	$⊢ 8 \cdot 4 = 32$
15	13 14	eqtri	$⊢ 2^{5} = 32$

Metamath Proof Explorer