Theorem negelrpd

Description: The negation of a negative number is in the positive real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	negelrpd.1	$$⊢\phi \to A\in ℝ$$
	negelrpd.2	$$⊢\phi \to A<0$$
Assertion	negelrpd	$$⊢\phi \to -A\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		negelrpd.1	$$⊢\phi \to A\in ℝ$$
2		negelrpd.2	$$⊢\phi \to A<0$$
3		negelrp	$$⊢A\in ℝ\to \left(-A\in {ℝ}^{+}\leftrightarrow A<0\right)$$
4	1 3	syl	$$⊢\phi \to \left(-A\in {ℝ}^{+}\leftrightarrow A<0\right)$$
5	2 4	mpbird	$$⊢\phi \to -A\in {ℝ}^{+}$$