2exp7

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

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

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 ℕ_{0}$
5		expp1	$⊢ (2 \in ℂ \land 6 \in ℕ_{0}) \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 ℕ_{0}$
12		4nn0	$⊢ 4 \in ℕ_{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$

Metamath Proof Explorer