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

Proof

Step	Hyp	Ref	Expression
1		df-neg	⊢ - 1 = ( 0 − 1 )
2		ax-i2m1	⊢ ( ( i · i ) + 1 ) = 0
3		0cn	⊢ 0 ∈ ℂ
4		ax-1cn	⊢ 1 ∈ ℂ
5		ax-icn	⊢ i ∈ ℂ
6	5 5	mulcli	⊢ ( i · i ) ∈ ℂ
7	3 4 6	subadd2i	⊢ ( ( 0 − 1 ) = ( i · i ) ↔ ( ( i · i ) + 1 ) = 0 )
8	2 7	mpbir	⊢ ( 0 − 1 ) = ( i · i )
9	1 8	eqtr2i	⊢ ( i · i ) = - 1