Metamath Proof Explorer


Theorem xnegcli

Description: Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis xnegcli.1
|- A e. RR*
Assertion xnegcli
|- -e A e. RR*

Proof

Step Hyp Ref Expression
1 xnegcli.1
 |-  A e. RR*
2 xnegcl
 |-  ( A e. RR* -> -e A e. RR* )
3 1 2 ax-mp
 |-  -e A e. RR*