Theorem 2exp7

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

	Ref	Expression
Assertion	2exp7	$$⊢2^7=128$$

Proof

Step	Hyp	Ref	Expression
1		df-7	$$⊢7=6+1$$
2	1	oveq2i	$$⊢2^7=2^{6+1}$$
3		2cn	$$⊢2\in ℂ$$
4		6nn0	$$⊢6\in {\mathbb{N}}_0$$
5		expp1	$$⊢\left(2\in ℂ\wedge 6\in {\mathbb{N}}_0\right)\to 2^{6+1}=2^6\cdot 2$$
6	3 4 5	mp2an	$$⊢2^{6+1}=2^6\cdot 2$$
7		2exp6	$$⊢2^6=64$$
8	7	oveq1i	$$⊢2^6\cdot 2=64\cdot 2$$
9	6 8	eqtri	$$⊢2^{6+1}=64\cdot 2$$
10	2 9	eqtri	$$⊢2^7=64\cdot 2$$
11		2nn0	$$⊢2\in {\mathbb{N}}_0$$
12		4nn0	$$⊢4\in {\mathbb{N}}_0$$
13		eqid	$$⊢64=64$$
14		6t2e12	$$⊢6\cdot 2=12$$
15		4t2e8	$$⊢4\cdot 2=8$$
16	11 4 12 13 14 15	decmul1	$$⊢64\cdot 2=128$$
17	10 16	eqtri	$$⊢2^7=128$$