Metamath Proof Explorer

Theorem cjth

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

Ref Expression
Assertion cjth ⊢ A ∈ ℂ → A + A ‾ ∈ ℝ ∧ i ⁢ A − A ‾ ∈ ℝ

Proof

Step Hyp Ref Expression
1 cju ⊢ A ∈ ℂ → ∃! x ∈ ℂ A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ
2 riotasbc ⊢ ∃! x ∈ ℂ A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ → [˙ ι x ∈ ℂ | A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ / x]˙ A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ
3 1 2 syl ⊢ A ∈ ℂ → [˙ ι x ∈ ℂ | A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ / x]˙ A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ
4 cjval ⊢ A ∈ ℂ → A ‾ = ι x ∈ ℂ | A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ
5 4 sbceq1d ⊢ A ∈ ℂ → [˙ A ‾ / x]˙ A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ ↔ [˙ ι x ∈ ℂ | A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ / x]˙ A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ
6 3 5 mpbird ⊢ A ∈ ℂ → [˙ A ‾ / x]˙ A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ
7 fvex ⊢ A ‾ ∈ V
8 oveq2 ⊢ x = A ‾ → A + x = A + A ‾
9 8 eleq1d ⊢ x = A ‾ → A + x ∈ ℝ ↔ A + A ‾ ∈ ℝ
10 oveq2 ⊢ x = A ‾ → A − x = A − A ‾
11 10 oveq2d ⊢ x = A ‾ → i ⁢ A − x = i ⁢ A − A ‾
12 11 eleq1d ⊢ x = A ‾ → i ⁢ A − x ∈ ℝ ↔ i ⁢ A − A ‾ ∈ ℝ
13 9 12 anbi12d ⊢ x = A ‾ → A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ ↔ A + A ‾ ∈ ℝ ∧ i ⁢ A − A ‾ ∈ ℝ
14 7 13 sbcie ⊢ [˙ A ‾ / x]˙ A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ ↔ A + A ‾ ∈ ℝ ∧ i ⁢ A − A ‾ ∈ ℝ
15 6 14 sylib ⊢ A ∈ ℂ → A + A ‾ ∈ ℝ ∧ i ⁢ A − A ‾ ∈ ℝ