Theorem renegcld

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

	Ref	Expression
Hypothesis	renegcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
Assertion	renegcld	⊢ ( 𝜑 → - 𝐴 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		renegcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
3	1 2	syl	⊢ ( 𝜑 → - 𝐴 ∈ ℝ )