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 ) = ; 6 4

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 3nn0 
 |-  3 e. NN0
3 3cn 
 |-  3 e. CC
4 2cn 
 |-  2 e. CC
5 3t2e6 
 |-  ( 3 x. 2 ) = 6
6 3 4 5 mulcomli 
 |-  ( 2 x. 3 ) = 6
7 cu2 
 |-  ( 2 ^ 3 ) = 8
8 8t8e64 
 |-  ( 8 x. 8 ) = ; 6 4
9 1 2 6 7 8 numexp2x 
 |-  ( 2 ^ 6 ) = ; 6 4