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	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cjval	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) )
2		replim	⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
3	2	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
4		recl	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
5	4	recnd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
6		ax-icn	⊢ i ∈ ℂ
7		imcl	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℂ )
9		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
10	6 8 9	sylancr	⊢ ( 𝐴 ∈ ℂ → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
11	5 10 5	ppncand	⊢ ( 𝐴 ∈ ℂ → ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) )
12	3 11	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) )
13	4 4	readdcld	⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
14	12 13	eqeltrd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ )
15	5 10 10	pnncand	⊢ ( 𝐴 ∈ ℂ → ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
16	2	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
17	6	a1i	⊢ ( 𝐴 ∈ ℂ → i ∈ ℂ )
18	17 8 8	adddid	⊢ ( 𝐴 ∈ ℂ → ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
19	15 16 18	3eqtr4d	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) )
20	19	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( i · ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ) )
21	7 7	readdcld	⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ∈ ℝ )
22	21	recnd	⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
23		mulass	⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ∧ ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ∈ ℂ ) → ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) = ( i · ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ) )
24	6 6 22 23	mp3an12i	⊢ ( 𝐴 ∈ ℂ → ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) = ( i · ( i · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ) )
25	20 24	eqtr4d	⊢ ( 𝐴 ∈ ℂ → ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) )
26		ixi	⊢ ( i · i ) = - 1
27		neg1rr	⊢ - 1 ∈ ℝ
28	26 27	eqeltri	⊢ ( i · i ) ∈ ℝ
29		remulcl	⊢ ( ( ( i · i ) ∈ ℝ ∧ ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ∈ ℝ ) → ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ∈ ℝ )
30	28 21 29	sylancr	⊢ ( 𝐴 ∈ ℂ → ( ( i · i ) · ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐴 ) ) ) ∈ ℝ )
31	25 30	eqeltrd	⊢ ( 𝐴 ∈ ℂ → ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ )
32	5 10	subcld	⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ )
33		cju	⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) )
34		oveq2	⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( 𝐴 + 𝑥 ) = ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
35	34	eleq1d	⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( ( 𝐴 + 𝑥 ) ∈ ℝ ↔ ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ ) )
36		oveq2	⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( 𝐴 − 𝑥 ) = ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
37	36	oveq2d	⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( i · ( 𝐴 − 𝑥 ) ) = ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
38	37	eleq1d	⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ↔ ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ ) )
39	35 38	anbi12d	⊢ ( 𝑥 = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) → ( ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ↔ ( ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ ) ) )
40	39	riota2	⊢ ( ( ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ ∧ ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) → ( ( ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
41	32 33 40	syl2anc	⊢ ( 𝐴 ∈ ℂ → ( ( ( 𝐴 + ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℝ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
42	14 31 41	mpbi2and	⊢ ( 𝐴 ∈ ℂ → ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )
43	1 42	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )