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

Metamath Proof Explorer

Theorem 3exp3

Description: Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 3exp3 ( 3 ↑ 3 ) = 2 7

Proof

Step Hyp Ref Expression
1 3nn0 ⊢ 3 ∈ ℕ0
2 2nn0 ⊢ 2 ∈ ℕ0
3 2p1e3 ⊢ ( 2 + 1 ) = 3
4 sq3 ⊢ ( 3 ↑ 2 ) = 9
5 4 oveq1i ⊢ ( ( 3 ↑ 2 ) · 3 ) = ( 9 · 3 )
6 9t3e27 ⊢ ( 9 · 3 ) = 2 7
7 5 6 eqtri ⊢ ( ( 3 ↑ 2 ) · 3 ) = 2 7
8 1 2 3 7 numexpp1 ⊢ ( 3 ↑ 3 ) = 2 7