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 ) ) )