Metamath Proof Explorer

Theorem xsubge0

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

Ref Expression
Assertion xsubge0 
|- ( ( A e. RR* /\ B e. RR* ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )

Proof

Step Hyp Ref Expression
1 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
2 0xr 
 |-  0 e. RR*
3 rexr 
 |-  ( B e. RR -> B e. RR* )
4 xnegcl 
 |-  ( B e. RR* -> -e B e. RR* )
5 xaddcl 
 |-  ( ( A e. RR* /\ -e B e. RR* ) -> ( A +e -e B ) e. RR* )
6 4 5 sylan2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e -e B ) e. RR* )
7 3 6 sylan2 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A +e -e B ) e. RR* )
8 simpr 
 |-  ( ( A e. RR* /\ B e. RR ) -> B e. RR )
9 xleadd1 
 |-  ( ( 0 e. RR* /\ ( A +e -e B ) e. RR* /\ B e. RR ) -> ( 0 <_ ( A +e -e B ) <-> ( 0 +e B ) <_ ( ( A +e -e B ) +e B ) ) )
10 2 7 8 9 mp3an2i 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( 0 <_ ( A +e -e B ) <-> ( 0 +e B ) <_ ( ( A +e -e B ) +e B ) ) )
11 3 adantl 
 |-  ( ( A e. RR* /\ B e. RR ) -> B e. RR* )
12 xaddlid 
 |-  ( B e. RR* -> ( 0 +e B ) = B )
13 11 12 syl 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( 0 +e B ) = B )
14 xnpcan 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( A +e -e B ) +e B ) = A )
15 13 14 breq12d 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( 0 +e B ) <_ ( ( A +e -e B ) +e B ) <-> B <_ A ) )
16 10 15 bitrd 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )
17 pnfxr 
 |-  +oo e. RR*
18 xrletri3 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( A = +oo <-> ( A <_ +oo /\ +oo <_ A ) ) )
19 17 18 mpan2 
 |-  ( A e. RR* -> ( A = +oo <-> ( A <_ +oo /\ +oo <_ A ) ) )
20 mnflt0 
 |-  -oo < 0
21 mnfxr 
 |-  -oo e. RR*
22 xrltnle 
 |-  ( ( -oo e. RR* /\ 0 e. RR* ) -> ( -oo < 0 <-> -. 0 <_ -oo ) )
23 21 2 22 mp2an 
 |-  ( -oo < 0 <-> -. 0 <_ -oo )
24 20 23 mpbi 
 |-  -. 0 <_ -oo
25 xaddmnf1 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> ( A +e -oo ) = -oo )
26 25 breq2d 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> ( 0 <_ ( A +e -oo ) <-> 0 <_ -oo ) )
27 24 26 mtbiri 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> -. 0 <_ ( A +e -oo ) )
28 27 ex 
 |-  ( A e. RR* -> ( A =/= +oo -> -. 0 <_ ( A +e -oo ) ) )
29 28 necon4ad 
 |-  ( A e. RR* -> ( 0 <_ ( A +e -oo ) -> A = +oo ) )
30 0le0 
 |-  0 <_ 0
31 oveq1 
 |-  ( A = +oo -> ( A +e -oo ) = ( +oo +e -oo ) )
32 pnfaddmnf 
 |-  ( +oo +e -oo ) = 0
33 31 32 eqtrdi 
 |-  ( A = +oo -> ( A +e -oo ) = 0 )
34 30 33 breqtrrid 
 |-  ( A = +oo -> 0 <_ ( A +e -oo ) )
35 29 34 impbid1 
 |-  ( A e. RR* -> ( 0 <_ ( A +e -oo ) <-> A = +oo ) )
36 pnfge 
 |-  ( A e. RR* -> A <_ +oo )
37 36 biantrurd 
 |-  ( A e. RR* -> ( +oo <_ A <-> ( A <_ +oo /\ +oo <_ A ) ) )
38 19 35 37 3bitr4d 
 |-  ( A e. RR* -> ( 0 <_ ( A +e -oo ) <-> +oo <_ A ) )
39 38 adantr 
 |-  ( ( A e. RR* /\ B = +oo ) -> ( 0 <_ ( A +e -oo ) <-> +oo <_ A ) )
40 xnegeq 
 |-  ( B = +oo -> -e B = -e +oo )
41 xnegpnf 
 |-  -e +oo = -oo
42 40 41 eqtrdi 
 |-  ( B = +oo -> -e B = -oo )
43 42 adantl 
 |-  ( ( A e. RR* /\ B = +oo ) -> -e B = -oo )
44 43 oveq2d 
 |-  ( ( A e. RR* /\ B = +oo ) -> ( A +e -e B ) = ( A +e -oo ) )
45 44 breq2d 
 |-  ( ( A e. RR* /\ B = +oo ) -> ( 0 <_ ( A +e -e B ) <-> 0 <_ ( A +e -oo ) ) )
46 breq1 
 |-  ( B = +oo -> ( B <_ A <-> +oo <_ A ) )
47 46 adantl 
 |-  ( ( A e. RR* /\ B = +oo ) -> ( B <_ A <-> +oo <_ A ) )
48 39 45 47 3bitr4d 
 |-  ( ( A e. RR* /\ B = +oo ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )
49 oveq1 
 |-  ( A = -oo -> ( A +e +oo ) = ( -oo +e +oo ) )
50 mnfaddpnf 
 |-  ( -oo +e +oo ) = 0
51 49 50 eqtrdi 
 |-  ( A = -oo -> ( A +e +oo ) = 0 )
52 51 adantl 
 |-  ( ( A e. RR* /\ A = -oo ) -> ( A +e +oo ) = 0 )
53 30 52 breqtrrid 
 |-  ( ( A e. RR* /\ A = -oo ) -> 0 <_ ( A +e +oo ) )
54 0lepnf 
 |-  0 <_ +oo
55 xaddpnf1 
 |-  ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )
56 54 55 breqtrrid 
 |-  ( ( A e. RR* /\ A =/= -oo ) -> 0 <_ ( A +e +oo ) )
57 53 56 pm2.61dane 
 |-  ( A e. RR* -> 0 <_ ( A +e +oo ) )
58 mnfle 
 |-  ( A e. RR* -> -oo <_ A )
59 57 58 2thd 
 |-  ( A e. RR* -> ( 0 <_ ( A +e +oo ) <-> -oo <_ A ) )
60 59 adantr 
 |-  ( ( A e. RR* /\ B = -oo ) -> ( 0 <_ ( A +e +oo ) <-> -oo <_ A ) )
61 xnegeq 
 |-  ( B = -oo -> -e B = -e -oo )
62 xnegmnf 
 |-  -e -oo = +oo
63 61 62 eqtrdi 
 |-  ( B = -oo -> -e B = +oo )
64 63 adantl 
 |-  ( ( A e. RR* /\ B = -oo ) -> -e B = +oo )
65 64 oveq2d 
 |-  ( ( A e. RR* /\ B = -oo ) -> ( A +e -e B ) = ( A +e +oo ) )
66 65 breq2d 
 |-  ( ( A e. RR* /\ B = -oo ) -> ( 0 <_ ( A +e -e B ) <-> 0 <_ ( A +e +oo ) ) )
67 breq1 
 |-  ( B = -oo -> ( B <_ A <-> -oo <_ A ) )
68 67 adantl 
 |-  ( ( A e. RR* /\ B = -oo ) -> ( B <_ A <-> -oo <_ A ) )
69 60 66 68 3bitr4d 
 |-  ( ( A e. RR* /\ B = -oo ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )
70 16 48 69 3jaodan 
 |-  ( ( A e. RR* /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )
71 1 70 sylan2b 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )