Metamath Proof Explorer

Theorem xleadd1a

Description: Extended real version of leadd1 ; 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)

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

Proof

Step Hyp Ref Expression
1 simplrr 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ ( C e. RR /\ A e. RR ) ) /\ B e. RR ) -> A <_ B )
5 1 2 3 4 leadd1dd 
 |-  ( ( ( ( ( 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 1 3 rexaddd 
 |-  ( ( ( ( ( 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 ) )
7 2 3 rexaddd 
 |-  ( ( ( ( ( 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 ) )
8 5 6 7 3brtr4d 
 |-  ( ( ( ( ( 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 ) )
9 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> A e. RR* )
10 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> C e. RR* )
11 xaddcl 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A +e C ) e. RR* )
12 9 10 11 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A +e C ) e. RR* )
13 12 ad2antrr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ ( C e. RR /\ A e. RR ) ) /\ B = +oo ) -> ( A +e C ) e. RR* )
14 pnfge 
 |-  ( ( A +e C ) e. RR* -> ( A +e C ) <_ +oo )
15 13 14 syl 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ ( C e. RR /\ A e. RR ) ) /\ B = +oo ) -> ( A +e C ) <_ +oo )
16 oveq1 
 |-  ( B = +oo -> ( B +e C ) = ( +oo +e C ) )
17 rexr 
 |-  ( C e. RR -> C e. RR* )
18 renemnf 
 |-  ( C e. RR -> C =/= -oo )
19 xaddpnf2 
 |-  ( ( C e. RR* /\ C =/= -oo ) -> ( +oo +e C ) = +oo )
20 17 18 19 syl2anc 
 |-  ( C e. RR -> ( +oo +e C ) = +oo )
21 20 ad2antrl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ ( C e. RR /\ A e. RR ) ) -> ( +oo +e C ) = +oo )
22 16 21 sylan9eqr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ ( C e. RR /\ A e. RR ) ) /\ B = +oo ) -> ( B +e C ) = +oo )
23 15 22 breqtrrd 
 |-  ( ( ( ( ( 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 ) )
24 12 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> ( A +e C ) e. RR* )
25 24 xrleidd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> ( A +e C ) <_ ( A +e C ) )
26 simplr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> A <_ B )
27 simpr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> B = -oo )
28 9 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> A e. RR* )
29 mnfle 
 |-  ( A e. RR* -> -oo <_ A )
30 28 29 syl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> -oo <_ A )
31 27 30 eqbrtrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> B <_ A )
32 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> B e. RR* )
33 xrletri3 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
34 9 32 33 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
35 34 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
36 26 31 35 mpbir2and 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> A = B )
37 36 oveq1d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> ( A +e C ) = ( B +e C ) )
38 25 37 breqtrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ B = -oo ) -> ( A +e C ) <_ ( B +e C ) )
39 38 adantlr 
 |-  ( ( ( ( ( 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 ) )
40 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
41 32 40 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( B e. RR \/ B = +oo \/ B = -oo ) )
42 41 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ ( C e. RR /\ A e. RR ) ) -> ( B e. RR \/ B = +oo \/ B = -oo ) )
43 8 23 39 42 mpjao3dan 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ ( C e. RR /\ A e. RR ) ) -> ( A +e C ) <_ ( B +e C ) )
44 43 anassrs 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C e. RR ) /\ A e. RR ) -> ( A +e C ) <_ ( B +e C ) )
45 12 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> ( A +e C ) e. RR* )
46 45 xrleidd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> ( A +e C ) <_ ( A +e C ) )
47 simplr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> A <_ B )
48 pnfge 
 |-  ( B e. RR* -> B <_ +oo )
49 32 48 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> B <_ +oo )
50 49 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> B <_ +oo )
51 simpr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> A = +oo )
52 50 51 breqtrrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> B <_ A )
53 34 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
54 47 52 53 mpbir2and 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> A = B )
55 54 oveq1d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> ( A +e C ) = ( B +e C ) )
56 46 55 breqtrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ A = +oo ) -> ( A +e C ) <_ ( B +e C ) )
57 56 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C e. RR ) /\ A = +oo ) -> ( A +e C ) <_ ( B +e C ) )
58 oveq1 
 |-  ( A = -oo -> ( A +e C ) = ( -oo +e C ) )
59 renepnf 
 |-  ( C e. RR -> C =/= +oo )
60 xaddmnf2 
 |-  ( ( C e. RR* /\ C =/= +oo ) -> ( -oo +e C ) = -oo )
61 17 59 60 syl2anc 
 |-  ( C e. RR -> ( -oo +e C ) = -oo )
62 61 adantl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C e. RR ) -> ( -oo +e C ) = -oo )
63 58 62 sylan9eqr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C e. RR ) /\ A = -oo ) -> ( A +e C ) = -oo )
64 xaddcl 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B +e C ) e. RR* )
65 32 10 64 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( B +e C ) e. RR* )
66 65 ad2antrr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C e. RR ) /\ A = -oo ) -> ( B +e C ) e. RR* )
67 mnfle 
 |-  ( ( B +e C ) e. RR* -> -oo <_ ( B +e C ) )
68 66 67 syl 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C e. RR ) /\ A = -oo ) -> -oo <_ ( B +e C ) )
69 63 68 eqbrtrd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C e. RR ) /\ A = -oo ) -> ( A +e C ) <_ ( B +e C ) )
70 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
71 9 70 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A e. RR \/ A = +oo \/ A = -oo ) )
72 71 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C e. RR ) -> ( A e. RR \/ A = +oo \/ A = -oo ) )
73 44 57 69 72 mpjao3dan 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C e. RR ) -> ( A +e C ) <_ ( B +e C ) )
74 38 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) /\ B = -oo ) -> ( A +e C ) <_ ( B +e C ) )
75 12 ad2antrr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) /\ B =/= -oo ) -> ( A +e C ) e. RR* )
76 75 14 syl 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) /\ B =/= -oo ) -> ( A +e C ) <_ +oo )
77 simplr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) /\ B =/= -oo ) -> C = +oo )
78 77 oveq2d 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) /\ B =/= -oo ) -> ( B +e C ) = ( B +e +oo ) )
79 32 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) -> B e. RR* )
80 xaddpnf1 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( B +e +oo ) = +oo )
81 79 80 sylan 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) /\ B =/= -oo ) -> ( B +e +oo ) = +oo )
82 78 81 eqtrd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) /\ B =/= -oo ) -> ( B +e C ) = +oo )
83 76 82 breqtrrd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) /\ B =/= -oo ) -> ( A +e C ) <_ ( B +e C ) )
84 74 83 pm2.61dane 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = +oo ) -> ( A +e C ) <_ ( B +e C ) )
85 56 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) /\ A = +oo ) -> ( A +e C ) <_ ( B +e C ) )
86 simplr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) /\ A =/= +oo ) -> C = -oo )
87 86 oveq2d 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) /\ A =/= +oo ) -> ( A +e C ) = ( A +e -oo ) )
88 9 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) -> A e. RR* )
89 xaddmnf1 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> ( A +e -oo ) = -oo )
90 88 89 sylan 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) /\ A =/= +oo ) -> ( A +e -oo ) = -oo )
91 87 90 eqtrd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) /\ A =/= +oo ) -> ( A +e C ) = -oo )
92 65 ad2antrr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) /\ A =/= +oo ) -> ( B +e C ) e. RR* )
93 92 67 syl 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) /\ A =/= +oo ) -> -oo <_ ( B +e C ) )
94 91 93 eqbrtrd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) /\ A =/= +oo ) -> ( A +e C ) <_ ( B +e C ) )
95 85 94 pm2.61dane 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) /\ C = -oo ) -> ( A +e C ) <_ ( B +e C ) )
96 elxr 
 |-  ( C e. RR* <-> ( C e. RR \/ C = +oo \/ C = -oo ) )
97 10 96 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( C e. RR \/ C = +oo \/ C = -oo ) )
98 73 84 95 97 mpjao3dan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A +e C ) <_ ( B +e C ) )