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

Metamath Proof Explorer

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	$⊢ i i = - 1$

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