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

Metamath Proof Explorer

Theorem crimi

Description: The imaginary part of a complex number representation. Definition 10-3.1 of Gleason p. 132. (Contributed by NM, 10-May-1999)

Ref Expression
Hypotheses crre.1 ⊢ 𝐴 ∈ ℝ
crre.2 ⊢ 𝐵 ∈ ℝ
Assertion crimi ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵

Proof

Step Hyp Ref Expression
1 crre.1 ⊢ 𝐴 ∈ ℝ
2 crre.2 ⊢ 𝐵 ∈ ℝ
3 crim ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵 )
4 1 2 3 mp2an ⊢ ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵