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