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	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐴 → ( ∗ ‘ 𝑥 ) = ( ∗ ‘ 𝐴 ) )
2		oveq12	⊢ ( ( 𝑥 = 𝐴 ∧ ( ∗ ‘ 𝑥 ) = ( ∗ ‘ 𝐴 ) ) → ( 𝑥 + ( ∗ ‘ 𝑥 ) ) = ( 𝐴 + ( ∗ ‘ 𝐴 ) ) )
3	1 2	mpdan	⊢ ( 𝑥 = 𝐴 → ( 𝑥 + ( ∗ ‘ 𝑥 ) ) = ( 𝐴 + ( ∗ ‘ 𝐴 ) ) )
4	3	oveq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 + ( ∗ ‘ 𝑥 ) ) / 2 ) = ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) )
5		df-re	⊢ ℜ = ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 + ( ∗ ‘ 𝑥 ) ) / 2 ) )
6		ovex	⊢ ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) ∈ V
7	4 5 6	fvmpt	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) )