MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xleadd1a Structured version   Unicode version

Theorem xleadd1a 11485
Description: Extended real version of leadd1 10028; note that the converse implication is not true, unlike the real version (for example  0  <  1 but  ( 1 +e +oo )  <_  ( 0 +e +oo )). (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xleadd1a  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  ( A +e C )  <_  ( B +e C ) )

Proof of Theorem xleadd1a
StepHypRef Expression
1 simplrr 769 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  e.  RR )  ->  A  e.  RR )
2 simpr 462 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  e.  RR )  ->  B  e.  RR )
3 simplrl 768 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  e.  RR )  ->  C  e.  RR )
4 simpllr 767 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  e.  RR )  ->  A  <_  B )
51, 2, 3, 4leadd1dd 10173 . . . . . 6  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  e.  RR )  ->  ( A  +  C
)  <_  ( B  +  C ) )
6 rexadd 11471 . . . . . . 7  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( A +e
C )  =  ( A  +  C ) )
71, 3, 6syl2anc 665 . . . . . 6  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  e.  RR )  ->  ( A +e
C )  =  ( A  +  C ) )
8 rexadd 11471 . . . . . . 7  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( B +e
C )  =  ( B  +  C ) )
92, 3, 8syl2anc 665 . . . . . 6  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  e.  RR )  ->  ( B +e
C )  =  ( B  +  C ) )
105, 7, 93brtr4d 4392 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  e.  RR )  ->  ( A +e
C )  <_  ( B +e C ) )
11 simpl1 1008 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  A  e.  RR* )
12 simpl3 1010 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  C  e.  RR* )
13 xaddcl 11476 . . . . . . . . 9  |-  ( ( A  e.  RR*  /\  C  e.  RR* )  ->  ( A +e C )  e.  RR* )
1411, 12, 13syl2anc 665 . . . . . . . 8  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  ( A +e C )  e.  RR* )
1514ad2antrr 730 . . . . . . 7  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  = +oo )  ->  ( A +e
C )  e.  RR* )
16 pnfge 11378 . . . . . . 7  |-  ( ( A +e C )  e.  RR*  ->  ( A +e C )  <_ +oo )
1715, 16syl 17 . . . . . 6  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  = +oo )  ->  ( A +e
C )  <_ +oo )
18 oveq1 6251 . . . . . . 7  |-  ( B  = +oo  ->  ( B +e C )  =  ( +oo +e C ) )
19 rexr 9632 . . . . . . . . 9  |-  ( C  e.  RR  ->  C  e.  RR* )
20 renemnf 9635 . . . . . . . . 9  |-  ( C  e.  RR  ->  C  =/= -oo )
21 xaddpnf2 11466 . . . . . . . . 9  |-  ( ( C  e.  RR*  /\  C  =/= -oo )  ->  ( +oo +e C )  = +oo )
2219, 20, 21syl2anc 665 . . . . . . . 8  |-  ( C  e.  RR  ->  ( +oo +e C )  = +oo )
2322ad2antrl 732 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  ( C  e.  RR  /\  A  e.  RR ) )  -> 
( +oo +e C )  = +oo )
2418, 23sylan9eqr 2479 . . . . . 6  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  = +oo )  ->  ( B +e
C )  = +oo )
2517, 24breqtrrd 4388 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  = +oo )  ->  ( A +e
C )  <_  ( B +e C ) )
2614adantr 466 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  ( A +e C )  e.  RR* )
27 xrleid 11395 . . . . . . . 8  |-  ( ( A +e C )  e.  RR*  ->  ( A +e C )  <_  ( A +e C ) )
2826, 27syl 17 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  ( A +e C )  <_  ( A +e C ) )
29 simplr 760 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  A  <_  B )
30 simpr 462 . . . . . . . . . 10  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  B  = -oo )
3111adantr 466 . . . . . . . . . . 11  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  A  e. 
RR* )
32 mnfle 11381 . . . . . . . . . . 11  |-  ( A  e.  RR*  -> -oo  <_  A )
3331, 32syl 17 . . . . . . . . . 10  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  -> -oo  <_  A )
3430, 33eqbrtrd 4382 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  B  <_  A )
35 simpl2 1009 . . . . . . . . . . 11  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  B  e.  RR* )
36 xrletri3 11397 . . . . . . . . . . 11  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  =  B  <->  ( A  <_  B  /\  B  <_  A ) ) )
3711, 35, 36syl2anc 665 . . . . . . . . . 10  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  ( A  =  B  <->  ( A  <_  B  /\  B  <_  A ) ) )
3837adantr 466 . . . . . . . . 9  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  ( A  =  B  <->  ( A  <_  B  /\  B  <_  A ) ) )
3929, 34, 38mpbir2and 930 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  A  =  B )
4039oveq1d 6259 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  ( A +e C )  =  ( B +e C ) )
4128, 40breqtrd 4386 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  B  = -oo )  ->  ( A +e C )  <_  ( B +e C ) )
4241adantlr 719 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  ( C  e.  RR  /\  A  e.  RR ) )  /\  B  = -oo )  ->  ( A +e
C )  <_  ( B +e C ) )
43 elxr 11362 . . . . . . 7  |-  ( B  e.  RR*  <->  ( B  e.  RR  \/  B  = +oo  \/  B  = -oo ) )
4435, 43sylib 199 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  ( B  e.  RR  \/  B  = +oo  \/  B  = -oo ) )
4544adantr 466 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  ( C  e.  RR  /\  A  e.  RR ) )  -> 
( B  e.  RR  \/  B  = +oo  \/  B  = -oo ) )
4610, 25, 42, 45mpjao3dan 1331 . . . 4  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  ( C  e.  RR  /\  A  e.  RR ) )  -> 
( A +e
C )  <_  ( B +e C ) )
4746anassrs 652 . . 3  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  e.  RR )  /\  A  e.  RR )  ->  ( A +e C )  <_  ( B +e C ) )
4814adantr 466 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  ( A +e C )  e.  RR* )
4948, 27syl 17 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  ( A +e C )  <_  ( A +e C ) )
50 simplr 760 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  A  <_  B )
51 pnfge 11378 . . . . . . . . . 10  |-  ( B  e.  RR*  ->  B  <_ +oo )
5235, 51syl 17 . . . . . . . . 9  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  B  <_ +oo )
5352adantr 466 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  B  <_ +oo )
54 simpr 462 . . . . . . . 8  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  A  = +oo )
5553, 54breqtrrd 4388 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  B  <_  A )
5637adantr 466 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  ( A  =  B  <->  ( A  <_  B  /\  B  <_  A ) ) )
5750, 55, 56mpbir2and 930 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  A  =  B )
5857oveq1d 6259 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  ( A +e C )  =  ( B +e C ) )
5949, 58breqtrd 4386 . . . 4  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  A  = +oo )  ->  ( A +e C )  <_  ( B +e C ) )
6059adantlr 719 . . 3  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  e.  RR )  /\  A  = +oo )  ->  ( A +e C )  <_  ( B +e C ) )
61 oveq1 6251 . . . . 5  |-  ( A  = -oo  ->  ( A +e C )  =  ( -oo +e C ) )
62 renepnf 9634 . . . . . . 7  |-  ( C  e.  RR  ->  C  =/= +oo )
63 xaddmnf2 11468 . . . . . . 7  |-  ( ( C  e.  RR*  /\  C  =/= +oo )  ->  ( -oo +e C )  = -oo )
6419, 62, 63syl2anc 665 . . . . . 6  |-  ( C  e.  RR  ->  ( -oo +e C )  = -oo )
6564adantl 467 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  C  e.  RR )  ->  ( -oo +e C )  = -oo )
6661, 65sylan9eqr 2479 . . . 4  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  e.  RR )  /\  A  = -oo )  ->  ( A +e C )  = -oo )
67 xaddcl 11476 . . . . . . 7  |-  ( ( B  e.  RR*  /\  C  e.  RR* )  ->  ( B +e C )  e.  RR* )
6835, 12, 67syl2anc 665 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  ( B +e C )  e.  RR* )
6968ad2antrr 730 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  e.  RR )  /\  A  = -oo )  ->  ( B +e C )  e.  RR* )
70 mnfle 11381 . . . . 5  |-  ( ( B +e C )  e.  RR*  -> -oo 
<_  ( B +e
C ) )
7169, 70syl 17 . . . 4  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  e.  RR )  /\  A  = -oo )  -> -oo  <_  ( B +e C ) )
7266, 71eqbrtrd 4382 . . 3  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  e.  RR )  /\  A  = -oo )  ->  ( A +e C )  <_  ( B +e C ) )
73 elxr 11362 . . . . 5  |-  ( A  e.  RR*  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
7411, 73sylib 199 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
7574adantr 466 . . 3  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  C  e.  RR )  ->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
7647, 60, 72, 75mpjao3dan 1331 . 2  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  C  e.  RR )  ->  ( A +e C )  <_  ( B +e C ) )
7741adantlr 719 . . 3  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = +oo )  /\  B  = -oo )  ->  ( A +e C )  <_  ( B +e C ) )
7814ad2antrr 730 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = +oo )  /\  B  =/= -oo )  ->  ( A +e C )  e.  RR* )
7978, 16syl 17 . . . 4  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = +oo )  /\  B  =/= -oo )  ->  ( A +e C )  <_ +oo )
80 simplr 760 . . . . . 6  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = +oo )  /\  B  =/= -oo )  ->  C  = +oo )
8180oveq2d 6260 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = +oo )  /\  B  =/= -oo )  ->  ( B +e C )  =  ( B +e +oo ) )
8235adantr 466 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  C  = +oo )  ->  B  e. 
RR* )
83 xaddpnf1 11465 . . . . . 6  |-  ( ( B  e.  RR*  /\  B  =/= -oo )  ->  ( B +e +oo )  = +oo )
8482, 83sylan 473 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = +oo )  /\  B  =/= -oo )  ->  ( B +e +oo )  = +oo )
8581, 84eqtrd 2457 . . . 4  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = +oo )  /\  B  =/= -oo )  ->  ( B +e C )  = +oo )
8679, 85breqtrrd 4388 . . 3  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = +oo )  /\  B  =/= -oo )  ->  ( A +e C )  <_  ( B +e C ) )
8777, 86pm2.61dane 2683 . 2  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  C  = +oo )  ->  ( A +e C )  <_  ( B +e C ) )
8859adantlr 719 . . 3  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = -oo )  /\  A  = +oo )  ->  ( A +e C )  <_  ( B +e C ) )
89 simplr 760 . . . . . 6  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = -oo )  /\  A  =/= +oo )  ->  C  = -oo )
9089oveq2d 6260 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = -oo )  /\  A  =/= +oo )  ->  ( A +e C )  =  ( A +e -oo ) )
9111adantr 466 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  C  = -oo )  ->  A  e. 
RR* )
92 xaddmnf1 11467 . . . . . 6  |-  ( ( A  e.  RR*  /\  A  =/= +oo )  ->  ( A +e -oo )  = -oo )
9391, 92sylan 473 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = -oo )  /\  A  =/= +oo )  ->  ( A +e -oo )  = -oo )
9490, 93eqtrd 2457 . . . 4  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = -oo )  /\  A  =/= +oo )  ->  ( A +e C )  = -oo )
9568ad2antrr 730 . . . . 5  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = -oo )  /\  A  =/= +oo )  ->  ( B +e C )  e.  RR* )
9695, 70syl 17 . . . 4  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = -oo )  /\  A  =/= +oo )  -> -oo  <_  ( B +e C ) )
9794, 96eqbrtrd 4382 . . 3  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  A  <_  B )  /\  C  = -oo )  /\  A  =/= +oo )  ->  ( A +e C )  <_  ( B +e C ) )
9888, 97pm2.61dane 2683 . 2  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  A  <_  B
)  /\  C  = -oo )  ->  ( A +e C )  <_  ( B +e C ) )
99 elxr 11362 . . 3  |-  ( C  e.  RR*  <->  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )
10012, 99sylib 199 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  ( C  e.  RR  \/  C  = +oo  \/  C  = -oo ) )
10176, 87, 98, 100mpjao3dan 1331 1  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  ( A +e C )  <_  ( B +e C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    \/ w3o 981    /\ w3a 982    = wceq 1437    e. wcel 1872    =/= wne 2594   class class class wbr 4361  (class class class)co 6244   RRcr 9484    + caddc 9488   +oocpnf 9618   -oocmnf 9619   RR*cxr 9620    <_ cle 9622   +ecxad 11353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-po 4712  df-so 4713  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-1st 6746  df-2nd 6747  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-xadd 11356
This theorem is referenced by:  xleadd2a  11486  xleadd1  11487  xaddge0  11490  xle2add  11491  imasdsf1olem  21325  xblss2ps  21353  xblss2  21354  stdbdxmet  21467  xrge0omnd  28420  measunl  28985  carsgclctunlem2  29098  xleadd1d  37449
  Copyright terms: Public domain W3C validator