This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 · 𝐵 ) ) ) = 𝐴 )