Metamath Proof Explorer

Theorem rexnegd

Description: Minus a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis rexnegd.1 
|- ( ph -> A e. RR )
Assertion rexnegd 
|- ( ph -> -e A = -u A )

Proof

Step Hyp Ref Expression
1 rexnegd.1 
 |-  ( ph -> A e. RR )
2 rexneg 
 |-  ( A e. RR -> -e A = -u A )
3 1 2 syl 
 |-  ( ph -> -e A = -u A )