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

Metamath Proof Explorer

Theorem negreb

Description: The negative of a real is real. (Contributed by NM, 11-Aug-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion negreb ⊢ A ∈ ℂ → − A ∈ ℝ ↔ A ∈ ℝ

Proof

Step Hyp Ref Expression
1 renegcl ⊢ − A ∈ ℝ → − − A ∈ ℝ
2 negneg ⊢ A ∈ ℂ → − − A = A
3 2 eleq1d ⊢ A ∈ ℂ → − − A ∈ ℝ ↔ A ∈ ℝ
4 1 3 imbitrid ⊢ A ∈ ℂ → − A ∈ ℝ → A ∈ ℝ
5 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
6 4 5 impbid1 ⊢ A ∈ ℂ → − A ∈ ℝ ↔ A ∈ ℝ