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

Metamath Proof Explorer

Theorem negelrp

Description: Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018)

Ref Expression
Assertion negelrp ⊢ A ∈ ℝ → − A ∈ ℝ + ↔ A < 0

Proof

Step Hyp Ref Expression
1 elrp ⊢ − A ∈ ℝ + ↔ − A ∈ ℝ ∧ 0 < − A
2 lt0neg1 ⊢ A ∈ ℝ → A < 0 ↔ 0 < − A
3 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
4 3 biantrurd ⊢ A ∈ ℝ → 0 < − A ↔ − A ∈ ℝ ∧ 0 < − A
5 2 4 bitr2d ⊢ A ∈ ℝ → − A ∈ ℝ ∧ 0 < − A ↔ A < 0
6 1 5 bitrid ⊢ A ∈ ℝ → − A ∈ ℝ + ↔ A < 0