Theorem i2

Description: _i squared. (Contributed by NM, 6-May-1999)

	Ref	Expression
Assertion	i2	$$⊢{\mathrm{i}}^2=-1$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2	1	sqvali	$$⊢{\mathrm{i}}^2=\mathrm{i}\mathrm{i}$$
3		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
4	2 3	eqtri	$$⊢{\mathrm{i}}^2=-1$$