Metamath Proof Explorer

Theorem cu2

Description: The cube of 2 is 8. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion cu2 
|- ( 2 ^ 3 ) = 8

Proof

Step Hyp Ref Expression
1 df-3 
 |-  3 = ( 2 + 1 )
2 1 oveq2i 
 |-  ( 2 ^ 3 ) = ( 2 ^ ( 2 + 1 ) )
3 2cn 
 |-  2 e. CC
4 2nn0 
 |-  2 e. NN0
5 expp1 
 |-  ( ( 2 e. CC /\ 2 e. NN0 ) -> ( 2 ^ ( 2 + 1 ) ) = ( ( 2 ^ 2 ) x. 2 ) )
6 3 4 5 mp2an 
 |-  ( 2 ^ ( 2 + 1 ) ) = ( ( 2 ^ 2 ) x. 2 )
7 sq2 
 |-  ( 2 ^ 2 ) = 4
8 7 oveq1i 
 |-  ( ( 2 ^ 2 ) x. 2 ) = ( 4 x. 2 )
9 4t2e8 
 |-  ( 4 x. 2 ) = 8
10 8 9 eqtri 
 |-  ( ( 2 ^ 2 ) x. 2 ) = 8
11 6 10 eqtri 
 |-  ( 2 ^ ( 2 + 1 ) ) = 8
12 2 11 eqtri 
 |-  ( 2 ^ 3 ) = 8