This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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