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