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

Metamath Proof Explorer

Theorem renegi

Description: Real part of negative. (Contributed by NM, 2-Aug-1999)

Ref Expression
Hypothesis recl.1 ⊢ A ∈ ℂ
Assertion renegi ⊢ ℜ ⁡ − A = − ℜ ⁡ A

Proof

Step Hyp Ref Expression
1 recl.1 ⊢ A ∈ ℂ
2 reneg ⊢ A ∈ ℂ → ℜ ⁡ − A = − ℜ ⁡ A
3 1 2 ax-mp ⊢ ℜ ⁡ − A = − ℜ ⁡ A