| 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 |