Metamath Proof Explorer


Theorem crred

Description: The real part of a complex number representation. Definition 10-3.1 of Gleason p. 132. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses crred.1 ( 𝜑𝐴 ∈ ℝ )
crred.2 ( 𝜑𝐵 ∈ ℝ )
Assertion crred ( 𝜑 → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 crred.1 ( 𝜑𝐴 ∈ ℝ )
2 crred.2 ( 𝜑𝐵 ∈ ℝ )
3 crre ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 )
4 1 2 3 syl2anc ( 𝜑 → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 )