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\in ℝ\to -A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		rexneg	$$⊢A\in ℝ\to -A=-A$$
2		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
3	1 2	eqeltrd	$$⊢A\in ℝ\to -A\in ℝ$$