Theorem 2exp6

Description: Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015) (Proof shortened by OpenAI, 25-Mar-2020)

	Ref	Expression
Assertion	2exp6	⊢ ( 2 ↑ 6 ) = ; 6 4

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2		3nn0	⊢ 3 ∈ ℕ0
3		3cn	⊢ 3 ∈ ℂ
4		2cn	⊢ 2 ∈ ℂ
5		3t2e6	⊢ ( 3 · 2 ) = 6
6	3 4 5	mulcomli	⊢ ( 2 · 3 ) = 6
7		cu2	⊢ ( 2 ↑ 3 ) = 8
8		8t8e64	⊢ ( 8 · 8 ) = ; 6 4
9	1 2 6 7 8	numexp2x	⊢ ( 2 ↑ 6 ) = ; 6 4