Theorem resubeulem1

Description: Lemma for resubeu . A value which when added to zero, results in negative zero. (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	resubeulem1	$$⊢A\in ℝ\to 0+\left(0{-}_{ℝ}\left(0+0\right)\right)=0{-}_{ℝ}0$$

Proof

Step	Hyp	Ref	Expression
1		elre0re	$$⊢A\in ℝ\to 0\in ℝ$$
2	1	recnd	$$⊢A\in ℝ\to 0\in ℂ$$
3	1 1	readdcld	$$⊢A\in ℝ\to 0+0\in ℝ$$
4		rernegcl	$$⊢0+0\in ℝ\to 0{-}_{ℝ}\left(0+0\right)\in ℝ$$
5	3 4	syl	$$⊢A\in ℝ\to 0{-}_{ℝ}\left(0+0\right)\in ℝ$$
6	5	recnd	$$⊢A\in ℝ\to 0{-}_{ℝ}\left(0+0\right)\in ℂ$$
7	2 2 6	addassd	$$⊢A\in ℝ\to 0+0+\left(0{-}_{ℝ}\left(0+0\right)\right)=0+0+\left(0{-}_{ℝ}\left(0+0\right)\right)$$
8		renegid	$$⊢0+0\in ℝ\to 0+0+\left(0{-}_{ℝ}\left(0+0\right)\right)=0$$
9	3 8	syl	$$⊢A\in ℝ\to 0+0+\left(0{-}_{ℝ}\left(0+0\right)\right)=0$$
10	7 9	eqtr3d	$$⊢A\in ℝ\to 0+0+\left(0{-}_{ℝ}\left(0+0\right)\right)=0$$
11	1 5	readdcld	$$⊢A\in ℝ\to 0+\left(0{-}_{ℝ}\left(0+0\right)\right)\in ℝ$$
12		renegadd	$$⊢\left(0\in ℝ\wedge 0+\left(0{-}_{ℝ}\left(0+0\right)\right)\in ℝ\right)\to \left(0{-}_{ℝ}0=0+\left(0{-}_{ℝ}\left(0+0\right)\right)\leftrightarrow 0+0+\left(0{-}_{ℝ}\left(0+0\right)\right)=0\right)$$
13	1 11 12	syl2anc	$$⊢A\in ℝ\to \left(0{-}_{ℝ}0=0+\left(0{-}_{ℝ}\left(0+0\right)\right)\leftrightarrow 0+0+\left(0{-}_{ℝ}\left(0+0\right)\right)=0\right)$$
14	10 13	mpbird	$$⊢A\in ℝ\to 0{-}_{ℝ}0=0+\left(0{-}_{ℝ}\left(0+0\right)\right)$$
15	14	eqcomd	$$⊢A\in ℝ\to 0+\left(0{-}_{ℝ}\left(0+0\right)\right)=0{-}_{ℝ}0$$