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