Theorem negelrp

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

	Ref	Expression
Assertion	negelrp	⊢ ( 𝐴 ∈ ℝ → ( - 𝐴 ∈ ℝ+ ↔ 𝐴 < 0 ) )

Proof

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