Description: _i cubed. (Contributed by NM, 31-Jan-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | i3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 | |
|
2 | 1 | oveq2i | |
3 | ax-icn | |
|
4 | 2nn0 | |
|
5 | expp1 | |
|
6 | 3 4 5 | mp2an | |
7 | i2 | |
|
8 | 7 | oveq1i | |
9 | 3 | mulm1i | |
10 | 8 9 | eqtri | |
11 | 6 10 | eqtri | |
12 | 2 11 | eqtri | |