Metamath Proof Explorer


Theorem renegcld

Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 renegcld.1
 |-  ( ph -> A e. RR )
2 renegcl
 |-  ( A e. RR -> -u A e. RR )
3 1 2 syl
 |-  ( ph -> -u A e. RR )