This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 reneg0addlid ⊢ ( 𝐵 ∈ ℝ → ( ( 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 ) ) + 𝐵 ) ) ) = 𝐵 )