Theorem 2exp5

Description: Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021)

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

Proof

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 {\mathbb{N}}_0$$
6		2nn0	$$⊢2\in {\mathbb{N}}_0$$
7		expadd	$$⊢\left(2\in ℂ\wedge 3\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\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$$