Metamath Proof Explorer


Theorem xnpcan

Description: Extended real version of npcan . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xnpcan
|- ( ( A e. RR* /\ B e. RR ) -> ( ( A +e -e B ) +e B ) = A )

Proof

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 )