Theorem rernegcl

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

	Ref	Expression
Assertion	rernegcl	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		elre0re	$$⊢A\in ℝ\to 0\in ℝ$$
2		resubval	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to 0{-}_{ℝ}A=\left(\iota x\in ℝ|A+x=0\right)$$
3	1 2	mpancom	$$⊢A\in ℝ\to 0{-}_{ℝ}A=\left(\iota x\in ℝ|A+x=0\right)$$
4		renegeu	$$⊢A\in ℝ\to \exists !x\in ℝA+x=0$$
5		riotacl	$$⊢\exists !x\in ℝA+x=0\to \left(\iota x\in ℝ|A+x=0\right)\in ℝ$$
6	4 5	syl	$$⊢A\in ℝ\to \left(\iota x\in ℝ|A+x=0\right)\in ℝ$$
7	3 6	eqeltrd	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℝ$$