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*