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 
|- ( ( A e. RR /\ B e. RR ) -> ( A + ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) ) = B )

Proof

Step Hyp Ref Expression
1 renegid 
 |-  ( A e. RR -> ( A + ( 0 -R A ) ) = 0 )
2 1 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + ( 0 -R A ) ) = 0 )
3 2 oveq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + ( 0 -R A ) ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) = ( 0 + ( ( 0 -R ( 0 + 0 ) ) + B ) ) )
4 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
5 4 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. CC )
6 rernegcl 
 |-  ( A e. RR -> ( 0 -R A ) e. RR )
7 6 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 -R A ) e. RR )
8 7 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 -R A ) e. CC )
9 elre0re 
 |-  ( B e. RR -> 0 e. RR )
10 9 9 readdcld 
 |-  ( B e. RR -> ( 0 + 0 ) e. RR )
11 rernegcl 
 |-  ( ( 0 + 0 ) e. RR -> ( 0 -R ( 0 + 0 ) ) e. RR )
12 10 11 syl 
 |-  ( B e. RR -> ( 0 -R ( 0 + 0 ) ) e. RR )
13 id 
 |-  ( B e. RR -> B e. RR )
14 12 13 readdcld 
 |-  ( B e. RR -> ( ( 0 -R ( 0 + 0 ) ) + B ) e. RR )
15 14 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 -R ( 0 + 0 ) ) + B ) e. RR )
16 15 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 -R ( 0 + 0 ) ) + B ) e. CC )
17 5 8 16 addassd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + ( 0 -R A ) ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) = ( A + ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) ) )
18 resubeulem1 
 |-  ( B e. RR -> ( 0 + ( 0 -R ( 0 + 0 ) ) ) = ( 0 -R 0 ) )
19 18 oveq1d 
 |-  ( B e. RR -> ( ( 0 + ( 0 -R ( 0 + 0 ) ) ) + B ) = ( ( 0 -R 0 ) + B ) )
20 9 recnd 
 |-  ( B e. RR -> 0 e. CC )
21 12 recnd 
 |-  ( B e. RR -> ( 0 -R ( 0 + 0 ) ) e. CC )
22 recn 
 |-  ( B e. RR -> B e. CC )
23 20 21 22 addassd 
 |-  ( B e. RR -> ( ( 0 + ( 0 -R ( 0 + 0 ) ) ) + B ) = ( 0 + ( ( 0 -R ( 0 + 0 ) ) + B ) ) )
24 reneg0addlid 
 |-  ( B e. RR -> ( ( 0 -R 0 ) + B ) = B )
25 19 23 24 3eqtr3d 
 |-  ( B e. RR -> ( 0 + ( ( 0 -R ( 0 + 0 ) ) + B ) ) = B )
26 25 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 + ( ( 0 -R ( 0 + 0 ) ) + B ) ) = B )
27 3 17 26 3eqtr3d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + ( ( 0 -R A ) + ( ( 0 -R ( 0 + 0 ) ) + B ) ) ) = B )