resubeulem2

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

		Ref	Expression
	Assertion	resubeulem2	$⊢ (A \in ℝ \land B \in ℝ) \to A + (0 -_{ℝ} A) + ((0 -_{ℝ} (0 + 0)) + B) = B$

Proof

Step	Hyp	Ref	Expression
1		renegid	$⊢ A \in ℝ \to A + (0 -_{ℝ} A) = 0$
2	1	adantr	$⊢ (A \in ℝ \land B \in ℝ) \to A + (0 -_{ℝ} A) = 0$
3	2	oveq1d	$⊢ (A \in ℝ \land B \in ℝ) \to A + (0 -_{ℝ} A) + (0 -_{ℝ} (0 + 0)) + B = 0 + (0 -_{ℝ} (0 + 0)) + B$
4		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
5	4	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℂ$
6		rernegcl	$⊢ A \in ℝ \to 0 -_{ℝ} A \in ℝ$
7	6	adantr	$⊢ (A \in ℝ \land B \in ℝ) \to 0 -_{ℝ} A \in ℝ$
8	7	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to 0 -_{ℝ} A \in ℂ$
9		elre0re	$⊢ B \in ℝ \to 0 \in ℝ$
10	9 9	readdcld	$⊢ B \in ℝ \to 0 + 0 \in ℝ$
11		rernegcl	$⊢ 0 + 0 \in ℝ \to 0 -_{ℝ} (0 + 0) \in ℝ$
12	10 11	syl	$⊢ B \in ℝ \to 0 -_{ℝ} (0 + 0) \in ℝ$
13		id	$⊢ B \in ℝ \to B \in ℝ$
14	12 13	readdcld	$⊢ B \in ℝ \to (0 -_{ℝ} (0 + 0)) + B \in ℝ$
15	14	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to (0 -_{ℝ} (0 + 0)) + B \in ℝ$
16	15	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to (0 -_{ℝ} (0 + 0)) + B \in ℂ$
17	5 8 16	addassd	$⊢ (A \in ℝ \land B \in ℝ) \to A + (0 -_{ℝ} A) + (0 -_{ℝ} (0 + 0)) + B = A + (0 -_{ℝ} A) + ((0 -_{ℝ} (0 + 0)) + B)$
18		resubeulem1	$⊢ B \in ℝ \to 0 + (0 -_{ℝ} (0 + 0)) = 0 -_{ℝ} 0$
19	18	oveq1d	$⊢ B \in ℝ \to 0 + (0 -_{ℝ} (0 + 0)) + B = (0 -_{ℝ} 0) + B$
20	9	recnd	$⊢ B \in ℝ \to 0 \in ℂ$
21	12	recnd	$⊢ B \in ℝ \to 0 -_{ℝ} (0 + 0) \in ℂ$
22		recn	$⊢ B \in ℝ \to B \in ℂ$
23	20 21 22	addassd	$⊢ B \in ℝ \to 0 + (0 -_{ℝ} (0 + 0)) + B = 0 + (0 -_{ℝ} (0 + 0)) + B$
24		reneg0addid2	$⊢ B \in ℝ \to (0 -_{ℝ} 0) + B = B$
25	19 23 24	3eqtr3d	$⊢ B \in ℝ \to 0 + (0 -_{ℝ} (0 + 0)) + B = B$
26	25	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to 0 + (0 -_{ℝ} (0 + 0)) + B = B$
27	3 17 26	3eqtr3d	$⊢ (A \in ℝ \land B \in ℝ) \to A + (0 -_{ℝ} A) + ((0 -_{ℝ} (0 + 0)) + B) = B$

Metamath Proof Explorer

Theorem resubeulem2

Proof