Theorem ixi

Description: _i times itself is minus 1. (Contributed by NM, 6-May-1999) (Proof shortened by Andrew Salmon, 19-Nov-2011)

	Ref	Expression
Assertion	ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$

Proof

Step	Hyp	Ref	Expression
1		df-neg	$$⊢-1=0-1$$
2		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
3		0cn	$$⊢0\in ℂ$$
4		ax-1cn	$$⊢1\in ℂ$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6	5 5	mulcli	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
7	3 4 6	subadd2i	$$⊢0-1=\mathrm{i}\mathrm{i}\leftrightarrow \mathrm{i}\mathrm{i}+1=0$$
8	2 7	mpbir	$$⊢0-1=\mathrm{i}\mathrm{i}$$
9	1 8	eqtr2i	$$⊢\mathrm{i}\mathrm{i}=-1$$