This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ ) )