Theorem 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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		renegid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 0 −ℝ 𝐴 ) ) = 0 )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( 0 −ℝ 𝐴 ) ) = 0 )
3	2	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) = ( 0 + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) )
4		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
5	4	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ )
6		rernegcl	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℝ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 −ℝ 𝐴 ) ∈ ℝ )
8	7	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 −ℝ 𝐴 ) ∈ ℂ )
9		elre0re	⊢ ( 𝐵 ∈ ℝ → 0 ∈ ℝ )
10	9 9	readdcld	⊢ ( 𝐵 ∈ ℝ → ( 0 + 0 ) ∈ ℝ )
11		rernegcl	⊢ ( ( 0 + 0 ) ∈ ℝ → ( 0 −ℝ ( 0 + 0 ) ) ∈ ℝ )
12	10 11	syl	⊢ ( 𝐵 ∈ ℝ → ( 0 −ℝ ( 0 + 0 ) ) ∈ ℝ )
13		id	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ )
14	12 13	readdcld	⊢ ( 𝐵 ∈ ℝ → ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ∈ ℝ )
15	14	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ∈ ℝ )
16	15	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ∈ ℂ )
17	5 8 16	addassd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( 0 −ℝ 𝐴 ) ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) = ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) ) )
18		resubeulem1	⊢ ( 𝐵 ∈ ℝ → ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) = ( 0 −ℝ 0 ) )
19	18	oveq1d	⊢ ( 𝐵 ∈ ℝ → ( ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) + 𝐵 ) = ( ( 0 −ℝ 0 ) + 𝐵 ) )
20	9	recnd	⊢ ( 𝐵 ∈ ℝ → 0 ∈ ℂ )
21	12	recnd	⊢ ( 𝐵 ∈ ℝ → ( 0 −ℝ ( 0 + 0 ) ) ∈ ℂ )
22		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
23	20 21 22	addassd	⊢ ( 𝐵 ∈ ℝ → ( ( 0 + ( 0 −ℝ ( 0 + 0 ) ) ) + 𝐵 ) = ( 0 + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) )
24		reneg0addid2	⊢ ( 𝐵 ∈ ℝ → ( ( 0 −ℝ 0 ) + 𝐵 ) = 𝐵 )
25	19 23 24	3eqtr3d	⊢ ( 𝐵 ∈ ℝ → ( 0 + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) = 𝐵 )
26	25	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) = 𝐵 )
27	3 17 26	3eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ ( 0 + 0 ) ) + 𝐵 ) ) ) = 𝐵 )