Theorem remim

Description: Value of the conjugate of a complex number. The value is the real part minus _i times the imaginary part. Definition 10-3.2 of Gleason p. 132. (Contributed by NM, 10-May-1999) (Revised by Mario Carneiro, 7-Nov-2013)

	Ref	Expression
Assertion	remim	$$⊢A\in ℂ\to \bar{A}=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cjval	$$⊢A\in ℂ\to \bar{A}=\left(\iota x\in ℂ|\left(A+x\in ℝ\wedge \mathrm{i}\left(A-x\right)\in ℝ\right)\right)$$
2		replim	$$⊢A\in ℂ\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
3	2	oveq1d	$$⊢A\in ℂ\to A+\Re \left(A\right)-\mathrm{i}\Im \left(A\right)=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)+\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)$$
4		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
5	4	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
6		ax-icn	$$⊢\mathrm{i}\in ℂ$$
7		imcl	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$
8	7	recnd	$$⊢A\in ℂ\to \Im \left(A\right)\in ℂ$$
9		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to \mathrm{i}\Im \left(A\right)\in ℂ$$
10	6 8 9	sylancr	$$⊢A\in ℂ\to \mathrm{i}\Im \left(A\right)\in ℂ$$
11	5 10 5	ppncand	$$⊢A\in ℂ\to \Re \left(A\right)+\mathrm{i}\Im \left(A\right)+\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)=\Re \left(A\right)+\Re \left(A\right)$$
12	3 11	eqtrd	$$⊢A\in ℂ\to A+\Re \left(A\right)-\mathrm{i}\Im \left(A\right)=\Re \left(A\right)+\Re \left(A\right)$$
13	4 4	readdcld	$$⊢A\in ℂ\to \Re \left(A\right)+\Re \left(A\right)\in ℝ$$
14	12 13	eqeltrd	$$⊢A\in ℂ\to A+\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\in ℝ$$
15	5 10 10	pnncand	$$⊢A\in ℂ\to \Re \left(A\right)+\mathrm{i}\Im \left(A\right)-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)=\mathrm{i}\Im \left(A\right)+\mathrm{i}\Im \left(A\right)$$
16	2	oveq1d	$$⊢A\in ℂ\to A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)$$
17	6	a1i	$$⊢A\in ℂ\to \mathrm{i}\in ℂ$$
18	17 8 8	adddid	$$⊢A\in ℂ\to \mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)=\mathrm{i}\Im \left(A\right)+\mathrm{i}\Im \left(A\right)$$
19	15 16 18	3eqtr4d	$$⊢A\in ℂ\to A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)=\mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)$$
20	19	oveq2d	$$⊢A\in ℂ\to \mathrm{i}\left(A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)\right)=\mathrm{i}\mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)$$
21	7 7	readdcld	$$⊢A\in ℂ\to \Im \left(A\right)+\Im \left(A\right)\in ℝ$$
22	21	recnd	$$⊢A\in ℂ\to \Im \left(A\right)+\Im \left(A\right)\in ℂ$$
23		mulass	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\in ℂ\wedge \Im \left(A\right)+\Im \left(A\right)\in ℂ\right)\to \mathrm{i}\mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)=\mathrm{i}\mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)$$
24	6 6 22 23	mp3an12i	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)=\mathrm{i}\mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)$$
25	20 24	eqtr4d	$$⊢A\in ℂ\to \mathrm{i}\left(A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)\right)=\mathrm{i}\mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)$$
26		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
27		neg1rr	$$⊢-1\in ℝ$$
28	26 27	eqeltri	$$⊢\mathrm{i}\mathrm{i}\in ℝ$$
29		remulcl	$$⊢\left(\mathrm{i}\mathrm{i}\in ℝ\wedge \Im \left(A\right)+\Im \left(A\right)\in ℝ\right)\to \mathrm{i}\mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)\in ℝ$$
30	28 21 29	sylancr	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}\left(\Im \left(A\right)+\Im \left(A\right)\right)\in ℝ$$
31	25 30	eqeltrd	$$⊢A\in ℂ\to \mathrm{i}\left(A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)\right)\in ℝ$$
32	5 10	subcld	$$⊢A\in ℂ\to \Re \left(A\right)-\mathrm{i}\Im \left(A\right)\in ℂ$$
33		cju	$$⊢A\in ℂ\to \exists !x\in ℂ\left(A+x\in ℝ\wedge \mathrm{i}\left(A-x\right)\in ℝ\right)$$
34		oveq2	$$⊢x=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\to A+x=A+\Re \left(A\right)-\mathrm{i}\Im \left(A\right)$$
35	34	eleq1d	$$⊢x=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\to \left(A+x\in ℝ\leftrightarrow A+\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\in ℝ\right)$$
36		oveq2	$$⊢x=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\to A-x=A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)$$
37	36	oveq2d	$$⊢x=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\to \mathrm{i}\left(A-x\right)=\mathrm{i}\left(A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)\right)$$
38	37	eleq1d	$$⊢x=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\to \left(\mathrm{i}\left(A-x\right)\in ℝ\leftrightarrow \mathrm{i}\left(A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)\right)\in ℝ\right)$$
39	35 38	anbi12d	$$⊢x=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\to \left(\left(A+x\in ℝ\wedge \mathrm{i}\left(A-x\right)\in ℝ\right)\leftrightarrow \left(A+\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\in ℝ\wedge \mathrm{i}\left(A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)\right)\in ℝ\right)\right)$$
40	39	riota2	$$⊢\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\in ℂ\wedge \exists !x\in ℂ\left(A+x\in ℝ\wedge \mathrm{i}\left(A-x\right)\in ℝ\right)\right)\to \left(\left(A+\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\in ℝ\wedge \mathrm{i}\left(A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)\right)\in ℝ\right)\leftrightarrow \left(\iota x\in ℂ|\left(A+x\in ℝ\wedge \mathrm{i}\left(A-x\right)\in ℝ\right)\right)=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)$$
41	32 33 40	syl2anc	$$⊢A\in ℂ\to \left(\left(A+\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\in ℝ\wedge \mathrm{i}\left(A-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)\right)\in ℝ\right)\leftrightarrow \left(\iota x\in ℂ|\left(A+x\in ℝ\wedge \mathrm{i}\left(A-x\right)\in ℝ\right)\right)=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)$$
42	14 31 41	mpbi2and	$$⊢A\in ℂ\to \left(\iota x\in ℂ|\left(A+x\in ℝ\wedge \mathrm{i}\left(A-x\right)\in ℝ\right)\right)=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)$$
43	1 42	eqtrd	$$⊢A\in ℂ\to \bar{A}=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)$$