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

Metamath Proof Explorer

Theorem imval

Description: The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion imval ⊢ A ∈ ℂ → ℑ ⁡ A = ℜ ⁡ A i

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ x = A → ℜ ⁡ x i = ℜ ⁡ A i
2 df-im ⊢ ℑ = x ∈ ℂ ⟼ ℜ ⁡ x i
3 fvex ⊢ ℜ ⁡ A i ∈ V
4 1 2 3 fvmpt ⊢ A ∈ ℂ → ℑ ⁡ A = ℜ ⁡ A i