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

Metamath Proof Explorer

Theorem 2exp5

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

Ref Expression
Assertion 2exp5 ( 2 ↑ 5 ) = 3 2

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 ∈ ℂ
5 3nn0 ⊢ 3 ∈ ℕ0
6 2nn0 ⊢ 2 ∈ ℕ0
7 expadd ⊢ ( ( 2 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 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 · 4 )
12 8 11 eqtri ⊢ ( 2 ↑ ( 3 + 2 ) ) = ( 8 · 4 )
13 3 12 eqtri ⊢ ( 2 ↑ 5 ) = ( 8 · 4 )
14 8t4e32 ⊢ ( 8 · 4 ) = 3 2
15 13 14 eqtri ⊢ ( 2 ↑ 5 ) = 3 2