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 2t3e6 
 |-  ( 2 x. 3 ) = 6
4 cu2 
 |-  ( 2 ^ 3 ) = 8
5 8t8e64 
 |-  ( 8 x. 8 ) = ; 6 4
6 1 2 3 4 5 numexp2x 
 |-  ( 2 ^ 6 ) = ; 6 4