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