Step |
Hyp |
Ref |
Expression |
1 |
|
rexr |
|- ( B e. RR -> B e. RR* ) |
2 |
|
xnegneg |
|- ( B e. RR* -> -e -e B = B ) |
3 |
1 2
|
syl |
|- ( B e. RR -> -e -e B = B ) |
4 |
3
|
adantl |
|- ( ( A e. RR* /\ B e. RR ) -> -e -e B = B ) |
5 |
4
|
oveq2d |
|- ( ( A e. RR* /\ B e. RR ) -> ( ( A +e -e B ) +e -e -e B ) = ( ( A +e -e B ) +e B ) ) |
6 |
|
rexneg |
|- ( B e. RR -> -e B = -u B ) |
7 |
|
renegcl |
|- ( B e. RR -> -u B e. RR ) |
8 |
6 7
|
eqeltrd |
|- ( B e. RR -> -e B e. RR ) |
9 |
|
xpncan |
|- ( ( A e. RR* /\ -e B e. RR ) -> ( ( A +e -e B ) +e -e -e B ) = A ) |
10 |
8 9
|
sylan2 |
|- ( ( A e. RR* /\ B e. RR ) -> ( ( A +e -e B ) +e -e -e B ) = A ) |
11 |
5 10
|
eqtr3d |
|- ( ( A e. RR* /\ B e. RR ) -> ( ( A +e -e B ) +e B ) = A ) |