Theorem imf

Description: Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007) (Revised by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	imf	⊢ ℑ : ℂ ⟶ ℝ

Proof

Step	Hyp	Ref	Expression
1		df-im	⊢ ℑ = ( 𝑥 ∈ ℂ ↦ ( ℜ ‘ ( 𝑥 / i ) ) )
2		imval	⊢ ( 𝑥 ∈ ℂ → ( ℑ ‘ 𝑥 ) = ( ℜ ‘ ( 𝑥 / i ) ) )
3		imcl	⊢ ( 𝑥 ∈ ℂ → ( ℑ ‘ 𝑥 ) ∈ ℝ )
4	2 3	eqeltrrd	⊢ ( 𝑥 ∈ ℂ → ( ℜ ‘ ( 𝑥 / i ) ) ∈ ℝ )
5	1 4	fmpti	⊢ ℑ : ℂ ⟶ ℝ