Metamath Proof Explorer


Theorem rexnegd

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

Ref Expression
Hypothesis rexnegd.1 ( 𝜑𝐴 ∈ ℝ )
Assertion rexnegd ( 𝜑 → -𝑒 𝐴 = - 𝐴 )

Proof

Step Hyp Ref Expression
1 rexnegd.1 ( 𝜑𝐴 ∈ ℝ )
2 rexneg ( 𝐴 ∈ ℝ → -𝑒 𝐴 = - 𝐴 )
3 1 2 syl ( 𝜑 → -𝑒 𝐴 = - 𝐴 )