Theorem 2exp7

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

	Ref	Expression
Assertion	2exp7	⊢ ( 2 ↑ 7 ) = ; ; 1 2 8

Proof

Step	Hyp	Ref	Expression
1		df-7	⊢ 7 = ( 6 + 1 )
2	1	oveq2i	⊢ ( 2 ↑ 7 ) = ( 2 ↑ ( 6 + 1 ) )
3		2cn	⊢ 2 ∈ ℂ
4		6nn0	⊢ 6 ∈ ℕ0
5		expp1	⊢ ( ( 2 ∈ ℂ ∧ 6 ∈ ℕ0 ) → ( 2 ↑ ( 6 + 1 ) ) = ( ( 2 ↑ 6 ) · 2 ) )
6	3 4 5	mp2an	⊢ ( 2 ↑ ( 6 + 1 ) ) = ( ( 2 ↑ 6 ) · 2 )
7		2exp6	⊢ ( 2 ↑ 6 ) = ; 6 4
8	7	oveq1i	⊢ ( ( 2 ↑ 6 ) · 2 ) = ( ; 6 4 · 2 )
9	6 8	eqtri	⊢ ( 2 ↑ ( 6 + 1 ) ) = ( ; 6 4 · 2 )
10	2 9	eqtri	⊢ ( 2 ↑ 7 ) = ( ; 6 4 · 2 )
11		2nn0	⊢ 2 ∈ ℕ0
12		4nn0	⊢ 4 ∈ ℕ0
13		eqid	⊢ ; 6 4 = ; 6 4
14		6t2e12	⊢ ( 6 · 2 ) = ; 1 2
15		4t2e8	⊢ ( 4 · 2 ) = 8
16	11 4 12 13 14 15	decmul1	⊢ ( ; 6 4 · 2 ) = ; ; 1 2 8
17	10 16	eqtri	⊢ ( 2 ↑ 7 ) = ; ; 1 2 8