Metamath Proof Explorer

Theorem xpncan

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

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

Proof

Step Hyp Ref Expression
1 rexneg 
 |-  ( B e. RR -> -e B = -u B )
2 1 adantl 
 |-  ( ( A e. RR* /\ B e. RR ) -> -e B = -u B )
3 2 oveq2d 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( A +e B ) +e -e B ) = ( ( A +e B ) +e -u B ) )
4 renegcl 
 |-  ( B e. RR -> -u B e. RR )
5 4 ad2antlr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A = -oo ) -> -u B e. RR )
6 rexr 
 |-  ( -u B e. RR -> -u B e. RR* )
7 renepnf 
 |-  ( -u B e. RR -> -u B =/= +oo )
8 xaddmnf2 
 |-  ( ( -u B e. RR* /\ -u B =/= +oo ) -> ( -oo +e -u B ) = -oo )
9 6 7 8 syl2anc 
 |-  ( -u B e. RR -> ( -oo +e -u B ) = -oo )
10 5 9 syl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A = -oo ) -> ( -oo +e -u B ) = -oo )
11 oveq1 
 |-  ( A = -oo -> ( A +e B ) = ( -oo +e B ) )
12 rexr 
 |-  ( B e. RR -> B e. RR* )
13 renepnf 
 |-  ( B e. RR -> B =/= +oo )
14 xaddmnf2 
 |-  ( ( B e. RR* /\ B =/= +oo ) -> ( -oo +e B ) = -oo )
15 12 13 14 syl2anc 
 |-  ( B e. RR -> ( -oo +e B ) = -oo )
16 15 adantl 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( -oo +e B ) = -oo )
17 11 16 sylan9eqr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A = -oo ) -> ( A +e B ) = -oo )
18 17 oveq1d 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A = -oo ) -> ( ( A +e B ) +e -u B ) = ( -oo +e -u B ) )
19 simpr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A = -oo ) -> A = -oo )
20 10 18 19 3eqtr4d 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A = -oo ) -> ( ( A +e B ) +e -u B ) = A )
21 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> A e. RR* )
22 simpr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> A =/= -oo )
23 12 ad2antlr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> B e. RR* )
24 renemnf 
 |-  ( B e. RR -> B =/= -oo )
25 24 ad2antlr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> B =/= -oo )
26 4 ad2antlr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> -u B e. RR )
27 26 6 syl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> -u B e. RR* )
28 renemnf 
 |-  ( -u B e. RR -> -u B =/= -oo )
29 26 28 syl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> -u B =/= -oo )
30 xaddass 
 |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( -u B e. RR* /\ -u B =/= -oo ) ) -> ( ( A +e B ) +e -u B ) = ( A +e ( B +e -u B ) ) )
31 21 22 23 25 27 29 30 syl222anc 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> ( ( A +e B ) +e -u B ) = ( A +e ( B +e -u B ) ) )
32 simplr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> B e. RR )
33 32 26 rexaddd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> ( B +e -u B ) = ( B + -u B ) )
34 32 recnd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> B e. CC )
35 34 negidd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> ( B + -u B ) = 0 )
36 33 35 eqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> ( B +e -u B ) = 0 )
37 36 oveq2d 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> ( A +e ( B +e -u B ) ) = ( A +e 0 ) )
38 xaddrid 
 |-  ( A e. RR* -> ( A +e 0 ) = A )
39 38 ad2antrr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> ( A +e 0 ) = A )
40 37 39 eqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> ( A +e ( B +e -u B ) ) = A )
41 31 40 eqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A =/= -oo ) -> ( ( A +e B ) +e -u B ) = A )
42 20 41 pm2.61dane 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( A +e B ) +e -u B ) = A )
43 3 42 eqtrd 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( A +e B ) +e -e B ) = A )