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