Definition df-i

Description: Define the complex number _i (the imaginary unit). (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	df-i	|- _i = <. 0R , 1R >.

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ci	|- _i
1		c0r	|- 0R
2		c1r	|- 1R
3	1 2	cop	|- <. 0R , 1R >.
4	0 3	wceq	|- _i = <. 0R , 1R >.