Metamath Proof Explorer


Theorem i4

Description: _i to the fourth power. (Contributed by NM, 31-Jan-2007)

Ref Expression
Assertion i4 i4=1

Proof

Step Hyp Ref Expression
1 ax-icn i
2 2nn0 20
3 expadd i2020i2+2=i2i2
4 1 2 2 3 mp3an i2+2=i2i2
5 2p2e4 2+2=4
6 5 oveq2i i2+2=i4
7 i2 i2=1
8 7 7 oveq12i i2i2=-1-1
9 ax-1cn 1
10 9 9 mul2negi -1-1=11
11 1t1e1 11=1
12 8 10 11 3eqtri i2i2=1
13 4 6 12 3eqtr3i i4=1