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

Metamath Proof Explorer

Theorem reim

Description: The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 mulcl ⊢ i ∈ ℂ ∧ A ∈ ℂ → i ⁢ A ∈ ℂ
3 1 2 mpan ⊢ A ∈ ℂ → i ⁢ A ∈ ℂ
4 imval ⊢ i ⁢ A ∈ ℂ → ℑ ⁡ i ⁢ A = ℜ ⁡ i ⁢ A i
5 3 4 syl ⊢ A ∈ ℂ → ℑ ⁡ i ⁢ A = ℜ ⁡ i ⁢ A i
6 ine0 ⊢ i ≠ 0
7 divcan3 ⊢ A ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 → i ⁢ A i = A
8 1 6 7 mp3an23 ⊢ A ∈ ℂ → i ⁢ A i = A
9 8 fveq2d ⊢ A ∈ ℂ → ℜ ⁡ i ⁢ A i = ℜ ⁡ A
10 5 9 eqtr2d ⊢ A ∈ ℂ → ℜ ⁡ A = ℑ ⁡ i ⁢ A