Theorem reval

Description: The value of the real part of a complex number. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	reval	$$⊢A\in ℂ\to \Re \left(A\right)=\frac{A+\bar{A}}{2}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢x=A\to \bar{x}=\bar{A}$$
2		oveq12	$$⊢\left(x=A\wedge \bar{x}=\bar{A}\right)\to x+\bar{x}=A+\bar{A}$$
3	1 2	mpdan	$$⊢x=A\to x+\bar{x}=A+\bar{A}$$
4	3	oveq1d	$$⊢x=A\to \frac{x+\bar{x}}{2}=\frac{A+\bar{A}}{2}$$
5		df-re	$$⊢\Re =\left(x\in ℂ⟼\frac{x+\bar{x}}{2}\right)$$
6		ovex	$$⊢\frac{A+\bar{A}}{2}\in \mathrm{V}$$
7	4 5 6	fvmpt	$$⊢A\in ℂ\to \Re \left(A\right)=\frac{A+\bar{A}}{2}$$