Metamath Proof Explorer

Theorem xnegrecl

Description: The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion xnegrecl 
|- ( A e. RR -> -e A e. RR )

Proof

Step Hyp Ref Expression
1 rexneg 
 |-  ( A e. RR -> -e A = -u A )
2 renegcl 
 |-  ( A e. RR -> -u A e. RR )
3 1 2 eqeltrd 
 |-  ( A e. RR -> -e A e. RR )