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 + (0 -_{ℝ} (0 + 0)) = 0 -_{ℝ} 0$

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 -_{ℝ} (0 + 0) \in ℝ$
5	3 4	syl	$⊢ A \in ℝ \to 0 -_{ℝ} (0 + 0) \in ℝ$
6	5	recnd	$⊢ A \in ℝ \to 0 -_{ℝ} (0 + 0) \in ℂ$
7	2 2 6	addassd	$⊢ A \in ℝ \to 0 + 0 + (0 -_{ℝ} (0 + 0)) = 0 + 0 + (0 -_{ℝ} (0 + 0))$
8		renegid	$⊢ 0 + 0 \in ℝ \to 0 + 0 + (0 -_{ℝ} (0 + 0)) = 0$
9	3 8	syl	$⊢ A \in ℝ \to 0 + 0 + (0 -_{ℝ} (0 + 0)) = 0$
10	7 9	eqtr3d	$⊢ A \in ℝ \to 0 + 0 + (0 -_{ℝ} (0 + 0)) = 0$
11	1 5	readdcld	$⊢ A \in ℝ \to 0 + (0 -_{ℝ} (0 + 0)) \in ℝ$
12		renegadd	$⊢ (0 \in ℝ \land 0 + (0 -_{ℝ} (0 + 0)) \in ℝ) \to (0 -_{ℝ} 0 = 0 + (0 -_{ℝ} (0 + 0)) \leftrightarrow 0 + 0 + (0 -_{ℝ} (0 + 0)) = 0)$
13	1 11 12	syl2anc	$⊢ A \in ℝ \to (0 -_{ℝ} 0 = 0 + (0 -_{ℝ} (0 + 0)) \leftrightarrow 0 + 0 + (0 -_{ℝ} (0 + 0)) = 0)$
14	10 13	mpbird	$⊢ A \in ℝ \to 0 -_{ℝ} 0 = 0 + (0 -_{ℝ} (0 + 0))$
15	14	eqcomd	$⊢ A \in ℝ \to 0 + (0 -_{ℝ} (0 + 0)) = 0 -_{ℝ} 0$

Metamath Proof Explorer