| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ax-icn |
|- _i e. CC |
| 2 |
|
2nn0 |
|- 2 e. NN0 |
| 3 |
|
expadd |
|- ( ( _i e. CC /\ 2 e. NN0 /\ 2 e. NN0 ) -> ( _i ^ ( 2 + 2 ) ) = ( ( _i ^ 2 ) x. ( _i ^ 2 ) ) ) |
| 4 |
1 2 2 3
|
mp3an |
|- ( _i ^ ( 2 + 2 ) ) = ( ( _i ^ 2 ) x. ( _i ^ 2 ) ) |
| 5 |
|
2p2e4 |
|- ( 2 + 2 ) = 4 |
| 6 |
5
|
oveq2i |
|- ( _i ^ ( 2 + 2 ) ) = ( _i ^ 4 ) |
| 7 |
|
i2 |
|- ( _i ^ 2 ) = -u 1 |
| 8 |
7 7
|
oveq12i |
|- ( ( _i ^ 2 ) x. ( _i ^ 2 ) ) = ( -u 1 x. -u 1 ) |
| 9 |
|
ax-1cn |
|- 1 e. CC |
| 10 |
9 9
|
mul2negi |
|- ( -u 1 x. -u 1 ) = ( 1 x. 1 ) |
| 11 |
|
1t1e1 |
|- ( 1 x. 1 ) = 1 |
| 12 |
8 10 11
|
3eqtri |
|- ( ( _i ^ 2 ) x. ( _i ^ 2 ) ) = 1 |
| 13 |
4 6 12
|
3eqtr3i |
|- ( _i ^ 4 ) = 1 |