Theorem cji

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

	Ref	Expression
Assertion	cji	⊢ ( ∗ ‘ i ) = - i

Proof

Step	Hyp	Ref	Expression
1		rei	⊢ ( ℜ ‘ i ) = 0
2		imi	⊢ ( ℑ ‘ i ) = 1
3	2	oveq2i	⊢ ( i · ( ℑ ‘ i ) ) = ( i · 1 )
4		ax-icn	⊢ i ∈ ℂ
5	4	mulridi	⊢ ( i · 1 ) = i
6	3 5	eqtri	⊢ ( i · ( ℑ ‘ i ) ) = i
7	1 6	oveq12i	⊢ ( ( ℜ ‘ i ) − ( i · ( ℑ ‘ i ) ) ) = ( 0 − i )
8		remim	⊢ ( i ∈ ℂ → ( ∗ ‘ i ) = ( ( ℜ ‘ i ) − ( i · ( ℑ ‘ i ) ) ) )
9	4 8	ax-mp	⊢ ( ∗ ‘ i ) = ( ( ℜ ‘ i ) − ( i · ( ℑ ‘ i ) ) )
10		df-neg	⊢ - i = ( 0 − i )
11	7 9 10	3eqtr4i	⊢ ( ∗ ‘ i ) = - i