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 xaddid2
 |-  ( +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 xaddid1
 |-  ( 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 )