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

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 )