Metamath Proof Explorer

Theorem 2exp4

Description: Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 2exp4 
|- ( 2 ^ 4 ) = ; 1 6

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 2t2e4 
 |-  ( 2 x. 2 ) = 4
3 sq2 
 |-  ( 2 ^ 2 ) = 4
4 4t4e16 
 |-  ( 4 x. 4 ) = ; 1 6
5 1 1 2 3 4 numexp2x 
 |-  ( 2 ^ 4 ) = ; 1 6