Theorem cji

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

	Ref	Expression
Assertion	cji	$$⊢\bar{\mathrm{i}}=-\mathrm{i}$$

Proof

Step	Hyp	Ref	Expression
1		rei	$$⊢\Re \left(\mathrm{i}\right)=0$$
2		imi	$$⊢\Im \left(\mathrm{i}\right)=1$$
3	2	oveq2i	$$⊢\mathrm{i}\Im \left(\mathrm{i}\right)=\mathrm{i}\cdot 1$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5	4	mulid1i	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$
6	3 5	eqtri	$$⊢\mathrm{i}\Im \left(\mathrm{i}\right)=\mathrm{i}$$
7	1 6	oveq12i	$$⊢\Re \left(\mathrm{i}\right)-\mathrm{i}\Im \left(\mathrm{i}\right)=0-\mathrm{i}$$
8		remim	$$⊢\mathrm{i}\in ℂ\to \bar{\mathrm{i}}=\Re \left(\mathrm{i}\right)-\mathrm{i}\Im \left(\mathrm{i}\right)$$
9	4 8	ax-mp	$$⊢\bar{\mathrm{i}}=\Re \left(\mathrm{i}\right)-\mathrm{i}\Im \left(\mathrm{i}\right)$$
10		df-neg	$$⊢-\mathrm{i}=0-\mathrm{i}$$
11	7 9 10	3eqtr4i	$$⊢\bar{\mathrm{i}}=-\mathrm{i}$$