Theorem lt0neg1dd

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

	Ref	Expression
Hypotheses	lt0neg1dd.1	|- ( ph -> A e. RR )
	lt0neg1dd.2	|- ( ph -> A < 0 )
Assertion	lt0neg1dd	|- ( ph -> 0 < -u A )

Proof

Step	Hyp	Ref	Expression
1		lt0neg1dd.1	|- ( ph -> A e. RR )
2		lt0neg1dd.2	|- ( ph -> A < 0 )
3	1	lt0neg1d	|- ( ph -> ( A < 0 <-> 0 < -u A ) )
4	2 3	mpbid	|- ( ph -> 0 < -u A )