Metamath Proof Explorer


Theorem i3

Description: _i cubed. (Contributed by NM, 31-Jan-2007)

Ref Expression
Assertion i3 i3=i

Proof

Step Hyp Ref Expression
1 df-3 3=2+1
2 1 oveq2i i3=i2+1
3 ax-icn i
4 2nn0 20
5 expp1 i20i2+1=i2i
6 3 4 5 mp2an i2+1=i2i
7 i2 i2=1
8 7 oveq1i i2i=-1i
9 3 mulm1i -1i=i
10 8 9 eqtri i2i=i
11 6 10 eqtri i2+1=i
12 2 11 eqtri i3=i