Theorem xnegrecl

Description: The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	xnegrecl	⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		rexneg	⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 = - 𝐴 )
2		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
3	1 2	eqeltrd	⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 ∈ ℝ )