Theorem cjth

Description: The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	cjth	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		cju	⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) )
2		riotasbc	⊢ ( ∃! 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) → [ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) / 𝑥 ] ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℂ → [ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) / 𝑥 ] ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) )
4		cjval	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) )
5	4	sbceq1d	⊢ ( 𝐴 ∈ ℂ → ( [ ( ∗ ‘ 𝐴 ) / 𝑥 ] ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ↔ [ ( ℩ 𝑥 ∈ ℂ ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) / 𝑥 ] ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ) )
6	3 5	mpbird	⊢ ( 𝐴 ∈ ℂ → [ ( ∗ ‘ 𝐴 ) / 𝑥 ] ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) )
7		fvex	⊢ ( ∗ ‘ 𝐴 ) ∈ V
8		oveq2	⊢ ( 𝑥 = ( ∗ ‘ 𝐴 ) → ( 𝐴 + 𝑥 ) = ( 𝐴 + ( ∗ ‘ 𝐴 ) ) )
9	8	eleq1d	⊢ ( 𝑥 = ( ∗ ‘ 𝐴 ) → ( ( 𝐴 + 𝑥 ) ∈ ℝ ↔ ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℝ ) )
10		oveq2	⊢ ( 𝑥 = ( ∗ ‘ 𝐴 ) → ( 𝐴 − 𝑥 ) = ( 𝐴 − ( ∗ ‘ 𝐴 ) ) )
11	10	oveq2d	⊢ ( 𝑥 = ( ∗ ‘ 𝐴 ) → ( i · ( 𝐴 − 𝑥 ) ) = ( i · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) )
12	11	eleq1d	⊢ ( 𝑥 = ( ∗ ‘ 𝐴 ) → ( ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ↔ ( i · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ ) )
13	9 12	anbi12d	⊢ ( 𝑥 = ( ∗ ‘ 𝐴 ) → ( ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ↔ ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ ) ) )
14	7 13	sbcie	⊢ ( [ ( ∗ ‘ 𝐴 ) / 𝑥 ] ( ( 𝐴 + 𝑥 ) ∈ ℝ ∧ ( i · ( 𝐴 − 𝑥 ) ) ∈ ℝ ) ↔ ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ ) )
15	6 14	sylib	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ ( i · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ ) )