Theorem i3

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

	Ref	Expression
Assertion	i3	$$⊢{\mathrm{i}}^3=-\mathrm{i}$$

Proof

Step	Hyp	Ref	Expression
1		df-3	$$⊢3=2+1$$
2	1	oveq2i	$$⊢{\mathrm{i}}^3={\mathrm{i}}^{2+1}$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5		expp1	$$⊢\left(\mathrm{i}\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^{2+1}={\mathrm{i}}^2\mathrm{i}$$
6	3 4 5	mp2an	$$⊢{\mathrm{i}}^{2+1}={\mathrm{i}}^2\mathrm{i}$$
7		i2	$$⊢{\mathrm{i}}^2=-1$$
8	7	oveq1i	$$⊢{\mathrm{i}}^2\mathrm{i}=-1\mathrm{i}$$
9	3	mulm1i	$$⊢-1\mathrm{i}=-\mathrm{i}$$
10	8 9	eqtri	$$⊢{\mathrm{i}}^2\mathrm{i}=-\mathrm{i}$$
11	6 10	eqtri	$$⊢{\mathrm{i}}^{2+1}=-\mathrm{i}$$
12	2 11	eqtri	$$⊢{\mathrm{i}}^3=-\mathrm{i}$$