Theorem cji

Description: The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005)

	Ref	Expression
Assertion	cji	|- ( * ` _i ) = -u _i

Proof

Step	Hyp	Ref	Expression
1		rei	|- ( Re ` _i ) = 0
2		imi	|- ( Im ` _i ) = 1
3	2	oveq2i	|- ( _i x. ( Im ` _i ) ) = ( _i x. 1 )
4		ax-icn	|- _i e. CC
5	4	mulid1i	|- ( _i x. 1 ) = _i
6	3 5	eqtri	|- ( _i x. ( Im ` _i ) ) = _i
7	1 6	oveq12i	|- ( ( Re ` _i ) - ( _i x. ( Im ` _i ) ) ) = ( 0 - _i )
8		remim	|- ( _i e. CC -> ( * ` _i ) = ( ( Re ` _i ) - ( _i x. ( Im ` _i ) ) ) )
9	4 8	ax-mp	|- ( * ` _i ) = ( ( Re ` _i ) - ( _i x. ( Im ` _i ) ) )
10		df-neg	|- -u _i = ( 0 - _i )
11	7 9 10	3eqtr4i	|- ( * ` _i ) = -u _i