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	|- ( ph -> A e. RR )
	negelrpd.2	|- ( ph -> A < 0 )
Assertion	negelrpd	|- ( ph -> -u A e. RR+ )

Proof

Step	Hyp	Ref	Expression
1		negelrpd.1	|- ( ph -> A e. RR )
2		negelrpd.2	|- ( ph -> A < 0 )
3		negelrp	|- ( A e. RR -> ( -u A e. RR+ <-> A < 0 ) )
4	1 3	syl	|- ( ph -> ( -u A e. RR+ <-> A < 0 ) )
5	2 4	mpbird	|- ( ph -> -u A e. RR+ )