Theorem i2

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

	Ref	Expression
Assertion	i2	⊢ ( i ↑ 2 ) = - 1

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2	1	sqvali	⊢ ( i ↑ 2 ) = ( i · i )
3		ixi	⊢ ( i · i ) = - 1
4	2 3	eqtri	⊢ ( i ↑ 2 ) = - 1