Description: _i to the fourth power. (Contributed by NM, 31-Jan-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | i4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-icn | |
|
2 | 2nn0 | |
|
3 | expadd | |
|
4 | 1 2 2 3 | mp3an | |
5 | 2p2e4 | |
|
6 | 5 | oveq2i | |
7 | i2 | |
|
8 | 7 7 | oveq12i | |
9 | ax-1cn | |
|
10 | 9 9 | mul2negi | |
11 | 1t1e1 | |
|
12 | 8 10 11 | 3eqtri | |
13 | 4 6 12 | 3eqtr3i | |