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 ABA+0-A+0-0+0+B=B

Proof

Step Hyp Ref Expression
1 renegid AA+0-A=0
2 1 adantr ABA+0-A=0
3 2 oveq1d ABA+0-A+0-0+0+B=0+0-0+0+B
4 simpl ABA
5 4 recnd ABA
6 rernegcl A0-A
7 6 adantr AB0-A
8 7 recnd AB0-A
9 elre0re B0
10 9 9 readdcld B0+0
11 rernegcl 0+00-0+0
12 10 11 syl B0-0+0
13 id BB
14 12 13 readdcld B0-0+0+B
15 14 adantl AB0-0+0+B
16 15 recnd AB0-0+0+B
17 5 8 16 addassd ABA+0-A+0-0+0+B=A+0-A+0-0+0+B
18 resubeulem1 B0+0-0+0=0-0
19 18 oveq1d B0+0-0+0+B=0-0+B
20 9 recnd B0
21 12 recnd B0-0+0
22 recn BB
23 20 21 22 addassd B0+0-0+0+B=0+0-0+0+B
24 reneg0addid2 B0-0+B=B
25 19 23 24 3eqtr3d B0+0-0+0+B=B
26 25 adantl AB0+0-0+0+B=B
27 3 17 26 3eqtr3d ABA+0-A+0-0+0+B=B