Theorem lt0neg1dd

Description: If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	lt0neg1dd.1	$$⊢\phi \to A\in ℝ$$
	lt0neg1dd.2	$$⊢\phi \to A<0$$
Assertion	lt0neg1dd	$$⊢\phi \to 0<-A$$

Proof

Step	Hyp	Ref	Expression
1		lt0neg1dd.1	$$⊢\phi \to A\in ℝ$$
2		lt0neg1dd.2	$$⊢\phi \to A<0$$
3	1	lt0neg1d	$$⊢\phi \to \left(A<0\leftrightarrow 0<-A\right)$$
4	2 3	mpbid	$$⊢\phi \to 0<-A$$