Metamath Proof Explorer

Theorem imre

Description: The imaginary part of a complex number in terms of the real part function. (Contributed by NM, 12-May-2005) (Revised by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion imre ⊢ A ∈ ℂ → ℑ ⁡ A = ℜ ⁡ − i ⁢ A

Proof

Step Hyp Ref Expression
1 imval ⊢ A ∈ ℂ → ℑ ⁡ A = ℜ ⁡ A i
2 ax-icn ⊢ i ∈ ℂ
3 ine0 ⊢ i ≠ 0
4 divrec2 ⊢ A ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 → A i = 1 i ⁢ A
5 2 3 4 mp3an23 ⊢ A ∈ ℂ → A i = 1 i ⁢ A
6 irec ⊢ 1 i = − i
7 6 oveq1i ⊢ 1 i ⁢ A = − i ⁢ A
8 5 7 eqtrdi ⊢ A ∈ ℂ → A i = − i ⁢ A
9 8 fveq2d ⊢ A ∈ ℂ → ℜ ⁡ A i = ℜ ⁡ − i ⁢ A
10 1 9 eqtrd ⊢ A ∈ ℂ → ℑ ⁡ A = ℜ ⁡ − i ⁢ A