Theorem i2

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

	Ref	Expression
Assertion	i2	|- ( _i ^ 2 ) = -u 1

Proof

Step	Hyp	Ref	Expression
1		ax-icn	|- _i e. CC
2	1	sqvali	|- ( _i ^ 2 ) = ( _i x. _i )
3		ixi	|- ( _i x. _i ) = -u 1
4	2 3	eqtri	|- ( _i ^ 2 ) = -u 1