Metamath Proof Explorer


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+ )