Metamath Proof Explorer

Theorem i3

Description: _i cubed. (Contributed by NM, 31-Jan-2007)

Ref Expression
Assertion i3 
|- ( _i ^ 3 ) = -u _i

Proof

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