Theorem negelrp

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

	Ref	Expression
Assertion	negelrp	$$⊢A\in ℝ\to \left(-A\in {ℝ}^{+}\leftrightarrow A<0\right)$$

Proof

Step	Hyp	Ref	Expression
1		elrp	$$⊢-A\in {ℝ}^{+}\leftrightarrow \left(-A\in ℝ\wedge 0<-A\right)$$
2		lt0neg1	$$⊢A\in ℝ\to \left(A<0\leftrightarrow 0<-A\right)$$
3		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
4	3	biantrurd	$$⊢A\in ℝ\to \left(0<-A\leftrightarrow \left(-A\in ℝ\wedge 0<-A\right)\right)$$
5	2 4	bitr2d	$$⊢A\in ℝ\to \left(\left(-A\in ℝ\wedge 0<-A\right)\leftrightarrow A<0\right)$$
6	1 5	bitrid	$$⊢A\in ℝ\to \left(-A\in {ℝ}^{+}\leftrightarrow A<0\right)$$