Metamath Proof Explorer

Theorem xrge0npcan

Description: Extended nonnegative real version of npcan . (Contributed by Thierry Arnoux, 9-Jun-2017)

Ref Expression
Assertion xrge0npcan 
|- ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) -> ( ( A +e -e B ) +e B ) = A )

Proof

Step Hyp Ref Expression
1 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
2 simpl1 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> A e. ( 0 [,] +oo ) )
3 1 2 sselid 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> A e. RR* )
4 simpr 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> B = +oo )
5 simpl3 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> B <_ A )
6 4 5 eqbrtrrd 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> +oo <_ A )
7 xgepnf 
 |-  ( A e. RR* -> ( +oo <_ A <-> A = +oo ) )
8 7 biimpa 
 |-  ( ( A e. RR* /\ +oo <_ A ) -> A = +oo )
9 3 6 8 syl2anc 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> A = +oo )
10 xnegeq 
 |-  ( B = +oo -> -e B = -e +oo )
11 4 10 syl 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> -e B = -e +oo )
12 9 11 oveq12d 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( A +e -e B ) = ( +oo +e -e +oo ) )
13 pnfxr 
 |-  +oo e. RR*
14 xnegid 
 |-  ( +oo e. RR* -> ( +oo +e -e +oo ) = 0 )
15 13 14 ax-mp 
 |-  ( +oo +e -e +oo ) = 0
16 12 15 eqtrdi 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( A +e -e B ) = 0 )
17 16 oveq1d 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( ( A +e -e B ) +e B ) = ( 0 +e B ) )
18 4 oveq2d 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( 0 +e B ) = ( 0 +e +oo ) )
19 xaddlid 
 |-  ( +oo e. RR* -> ( 0 +e +oo ) = +oo )
20 13 19 mp1i 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( 0 +e +oo ) = +oo )
21 17 18 20 3eqtrd 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( ( A +e -e B ) +e B ) = +oo )
22 21 9 eqtr4d 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( ( A +e -e B ) +e B ) = A )
23 simpl1 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> A e. ( 0 [,] +oo ) )
24 1 23 sselid 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> A e. RR* )
25 xrge0neqmnf 
 |-  ( A e. ( 0 [,] +oo ) -> A =/= -oo )
26 23 25 syl 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> A =/= -oo )
27 simpl2 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> B e. ( 0 [,] +oo ) )
28 1 27 sselid 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> B e. RR* )
29 28 xnegcld 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> -e B e. RR* )
30 simpr 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> -. B = +oo )
31 xnegneg 
 |-  ( B e. RR* -> -e -e B = B )
32 xnegeq 
 |-  ( -e B = -oo -> -e -e B = -e -oo )
33 31 32 sylan9req 
 |-  ( ( B e. RR* /\ -e B = -oo ) -> B = -e -oo )
34 xnegmnf 
 |-  -e -oo = +oo
35 33 34 eqtrdi 
 |-  ( ( B e. RR* /\ -e B = -oo ) -> B = +oo )
36 35 stoic1a 
 |-  ( ( B e. RR* /\ -. B = +oo ) -> -. -e B = -oo )
37 36 neqned 
 |-  ( ( B e. RR* /\ -. B = +oo ) -> -e B =/= -oo )
38 28 30 37 syl2anc 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> -e B =/= -oo )
39 xrge0neqmnf 
 |-  ( B e. ( 0 [,] +oo ) -> B =/= -oo )
40 27 39 syl 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> B =/= -oo )
41 xaddass 
 |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( -e B e. RR* /\ -e B =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) ) -> ( ( A +e -e B ) +e B ) = ( A +e ( -e B +e B ) ) )
42 24 26 29 38 28 40 41 syl222anc 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> ( ( A +e -e B ) +e B ) = ( A +e ( -e B +e B ) ) )
43 xnegcl 
 |-  ( B e. RR* -> -e B e. RR* )
44 xaddcom 
 |-  ( ( -e B e. RR* /\ B e. RR* ) -> ( -e B +e B ) = ( B +e -e B ) )
45 43 44 mpancom 
 |-  ( B e. RR* -> ( -e B +e B ) = ( B +e -e B ) )
46 xnegid 
 |-  ( B e. RR* -> ( B +e -e B ) = 0 )
47 45 46 eqtrd 
 |-  ( B e. RR* -> ( -e B +e B ) = 0 )
48 47 oveq2d 
 |-  ( B e. RR* -> ( A +e ( -e B +e B ) ) = ( A +e 0 ) )
49 xaddrid 
 |-  ( A e. RR* -> ( A +e 0 ) = A )
50 48 49 sylan9eqr 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e ( -e B +e B ) ) = A )
51 24 28 50 syl2anc 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> ( A +e ( -e B +e B ) ) = A )
52 42 51 eqtrd 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> ( ( A +e -e B ) +e B ) = A )
53 22 52 pm2.61dan 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) -> ( ( A +e -e B ) +e B ) = A )