This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem i3

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

Ref Expression
Assertion i3 ⊢ i 3 = − i

Proof

Step Hyp Ref Expression
1 df-3 ⊢ 3 = 2 + 1
2 1 oveq2i ⊢ i 3 = i 2 + 1
3 ax-icn ⊢ i ∈ ℂ
4 2nn0 ⊢ 2 ∈ ℕ 0
5 expp1 ⊢ i ∈ ℂ ∧ 2 ∈ ℕ 0 → i 2 + 1 = i 2 ⁢ i
6 3 4 5 mp2an ⊢ i 2 + 1 = i 2 ⁢ i
7 i2 ⊢ i 2 = − 1
8 7 oveq1i ⊢ i 2 ⁢ i = -1 ⁢ i
9 3 mulm1i ⊢ -1 ⁢ i = − i
10 8 9 eqtri ⊢ i 2 ⁢ i = − i
11 6 10 eqtri ⊢ i 2 + 1 = − i
12 2 11 eqtri ⊢ i 3 = − i