# 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}\in ℂ\to \stackrel{‾}{{A}}=\left(\iota {x}\in ℂ|\left({A}+{x}\in ℝ\wedge \mathrm{i}\left({A}-{x}\right)\in ℝ\right)\right)$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{y}={A}\to {y}+{x}={A}+{x}$
2 1 eleq1d ${⊢}{y}={A}\to \left({y}+{x}\in ℝ↔{A}+{x}\in ℝ\right)$
3 oveq1 ${⊢}{y}={A}\to {y}-{x}={A}-{x}$
4 3 oveq2d ${⊢}{y}={A}\to \mathrm{i}\left({y}-{x}\right)=\mathrm{i}\left({A}-{x}\right)$
5 4 eleq1d ${⊢}{y}={A}\to \left(\mathrm{i}\left({y}-{x}\right)\in ℝ↔\mathrm{i}\left({A}-{x}\right)\in ℝ\right)$
6 2 5 anbi12d ${⊢}{y}={A}\to \left(\left({y}+{x}\in ℝ\wedge \mathrm{i}\left({y}-{x}\right)\in ℝ\right)↔\left({A}+{x}\in ℝ\wedge \mathrm{i}\left({A}-{x}\right)\in ℝ\right)\right)$
7 6 riotabidv ${⊢}{y}={A}\to \left(\iota {x}\in ℂ|\left({y}+{x}\in ℝ\wedge \mathrm{i}\left({y}-{x}\right)\in ℝ\right)\right)=\left(\iota {x}\in ℂ|\left({A}+{x}\in ℝ\wedge \mathrm{i}\left({A}-{x}\right)\in ℝ\right)\right)$
8 df-cj ${⊢}*=\left({y}\in ℂ⟼\left(\iota {x}\in ℂ|\left({y}+{x}\in ℝ\wedge \mathrm{i}\left({y}-{x}\right)\in ℝ\right)\right)\right)$
9 riotaex ${⊢}\left(\iota {x}\in ℂ|\left({A}+{x}\in ℝ\wedge \mathrm{i}\left({A}-{x}\right)\in ℝ\right)\right)\in \mathrm{V}$
10 7 8 9 fvmpt ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}=\left(\iota {x}\in ℂ|\left({A}+{x}\in ℝ\wedge \mathrm{i}\left({A}-{x}\right)\in ℝ\right)\right)$