Metamath Proof Explorer

Theorem cjval

Description: The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion cjval ⊢ A ∈ ℂ → A ‾ = ι x ∈ ℂ | A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ y = A → y + x = A + x
2 1 eleq1d ⊢ y = A → y + x ∈ ℝ ↔ A + x ∈ ℝ
3 oveq1 ⊢ y = A → y − x = A − x
4 3 oveq2d ⊢ y = A → i ⁢ y − x = i ⁢ A − x
5 4 eleq1d ⊢ y = A → i ⁢ y − x ∈ ℝ ↔ i ⁢ A − x ∈ ℝ
6 2 5 anbi12d ⊢ y = A → y + x ∈ ℝ ∧ i ⁢ y − x ∈ ℝ ↔ A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ
7 6 riotabidv ⊢ y = A → ι x ∈ ℂ | y + x ∈ ℝ ∧ i ⁢ y − x ∈ ℝ = ι x ∈ ℂ | A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ
8 df-cj ⊢ * = y ∈ ℂ ⟼ ι x ∈ ℂ | y + x ∈ ℝ ∧ i ⁢ y − x ∈ ℝ
9 riotaex ⊢ ι x ∈ ℂ | A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ ∈ V
10 7 8 9 fvmpt ⊢ A ∈ ℂ → A ‾ = ι x ∈ ℂ | A + x ∈ ℝ ∧ i ⁢ A − x ∈ ℝ