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 |