Metamath Proof Explorer

Theorem xlesubadd

Description: Under certain conditions, the conclusion of lesubadd is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> A e. RR* )
2 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> B e. RR* )
3 xnegcl 
 |-  ( B e. RR* -> -e B e. RR* )
4 2 3 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> -e B e. RR* )
5 xaddcl 
 |-  ( ( A e. RR* /\ -e B e. RR* ) -> ( A +e -e B ) e. RR* )
6 1 4 5 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( A +e -e B ) e. RR* )
7 6 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) /\ B e. RR ) -> ( A +e -e B ) e. RR* )
8 simpll3 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) /\ B e. RR ) -> C e. RR* )
9 simpr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) /\ B e. RR ) -> B e. RR )
10 xleadd1 
 |-  ( ( ( A +e -e B ) e. RR* /\ C e. RR* /\ B e. RR ) -> ( ( A +e -e B ) <_ C <-> ( ( A +e -e B ) +e B ) <_ ( C +e B ) ) )
11 7 8 9 10 syl3anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) /\ B e. RR ) -> ( ( A +e -e B ) <_ C <-> ( ( A +e -e B ) +e B ) <_ ( C +e B ) ) )
12 xnpcan 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( A +e -e B ) +e B ) = A )
13 1 12 sylan 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) /\ B e. RR ) -> ( ( A +e -e B ) +e B ) = A )
14 13 breq1d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) /\ B e. RR ) -> ( ( ( A +e -e B ) +e B ) <_ ( C +e B ) <-> A <_ ( C +e B ) ) )
15 11 14 bitrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) /\ B e. RR ) -> ( ( A +e -e B ) <_ C <-> A <_ ( C +e B ) ) )
16 simpr3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> 0 <_ C )
17 oveq1 
 |-  ( A = +oo -> ( A +e -oo ) = ( +oo +e -oo ) )
18 pnfaddmnf 
 |-  ( +oo +e -oo ) = 0
19 17 18 eqtrdi 
 |-  ( A = +oo -> ( A +e -oo ) = 0 )
20 19 breq1d 
 |-  ( A = +oo -> ( ( A +e -oo ) <_ C <-> 0 <_ C ) )
21 16 20 syl5ibrcom 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( A = +oo -> ( A +e -oo ) <_ C ) )
22 xaddmnf1 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> ( A +e -oo ) = -oo )
23 22 ex 
 |-  ( A e. RR* -> ( A =/= +oo -> ( A +e -oo ) = -oo ) )
24 1 23 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( A =/= +oo -> ( A +e -oo ) = -oo ) )
25 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> C e. RR* )
26 mnfle 
 |-  ( C e. RR* -> -oo <_ C )
27 25 26 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> -oo <_ C )
28 breq1 
 |-  ( ( A +e -oo ) = -oo -> ( ( A +e -oo ) <_ C <-> -oo <_ C ) )
29 27 28 syl5ibrcom 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( ( A +e -oo ) = -oo -> ( A +e -oo ) <_ C ) )
30 24 29 syld 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( A =/= +oo -> ( A +e -oo ) <_ C ) )
31 21 30 pm2.61dne 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( A +e -oo ) <_ C )
32 pnfge 
 |-  ( A e. RR* -> A <_ +oo )
33 1 32 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> A <_ +oo )
34 ge0nemnf 
 |-  ( ( C e. RR* /\ 0 <_ C ) -> C =/= -oo )
35 25 16 34 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> C =/= -oo )
36 xaddpnf1 
 |-  ( ( C e. RR* /\ C =/= -oo ) -> ( C +e +oo ) = +oo )
37 25 35 36 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( C +e +oo ) = +oo )
38 33 37 breqtrrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> A <_ ( C +e +oo ) )
39 31 38 2thd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( ( A +e -oo ) <_ C <-> A <_ ( C +e +oo ) ) )
40 xnegeq 
 |-  ( B = +oo -> -e B = -e +oo )
41 xnegpnf 
 |-  -e +oo = -oo
42 40 41 eqtrdi 
 |-  ( B = +oo -> -e B = -oo )
43 42 oveq2d 
 |-  ( B = +oo -> ( A +e -e B ) = ( A +e -oo ) )
44 43 breq1d 
 |-  ( B = +oo -> ( ( A +e -e B ) <_ C <-> ( A +e -oo ) <_ C ) )
45 oveq2 
 |-  ( B = +oo -> ( C +e B ) = ( C +e +oo ) )
46 45 breq2d 
 |-  ( B = +oo -> ( A <_ ( C +e B ) <-> A <_ ( C +e +oo ) ) )
47 44 46 bibi12d 
 |-  ( B = +oo -> ( ( ( A +e -e B ) <_ C <-> A <_ ( C +e B ) ) <-> ( ( A +e -oo ) <_ C <-> A <_ ( C +e +oo ) ) ) )
48 39 47 syl5ibrcom 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( B = +oo -> ( ( A +e -e B ) <_ C <-> A <_ ( C +e B ) ) ) )
49 48 imp 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) /\ B = +oo ) -> ( ( A +e -e B ) <_ C <-> A <_ ( C +e B ) ) )
50 simpr2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> B =/= -oo )
51 2 50 jca 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( B e. RR* /\ B =/= -oo ) )
52 xrnemnf 
 |-  ( ( B e. RR* /\ B =/= -oo ) <-> ( B e. RR \/ B = +oo ) )
53 51 52 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( B e. RR \/ B = +oo ) )
54 15 49 53 mpjaodan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( ( A +e -e B ) <_ C <-> A <_ ( C +e B ) ) )