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

Metamath Proof Explorer

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} = 64$

Step	Hyp	Ref	Expression
1		2nn0	$⊢ 2 \in ℕ_{0}$
2		3nn0	$⊢ 3 \in ℕ_{0}$
3		3cn	$⊢ 3 \in ℂ$
4		2cn	$⊢ 2 \in ℂ$
5		3t2e6	$⊢ 3 \cdot 2 = 6$
6	3 4 5	mulcomli	$⊢ 2 \cdot 3 = 6$
7		cu2	$⊢ 2^{3} = 8$
8		8t8e64	$⊢ 8 \cdot 8 = 64$
9	1 2 6 7 8	numexp2x	$⊢ 2^{6} = 64$