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

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 = 64
9 1 2 6 7 8 numexp2x 2 6 = 64