Theorem rernegcl

Description: Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	rernegcl	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		elre0re	⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
2		resubval	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 −ℝ 𝐴 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 ) )
3	1 2	mpancom	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 ) )
4		renegeu	⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )
5		riotacl	⊢ ( ∃! 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 → ( ℩ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 ) ∈ ℝ )
6	4 5	syl	⊢ ( 𝐴 ∈ ℝ → ( ℩ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 ) ∈ ℝ )
7	3 6	eqeltrd	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℝ )