Metamath Proof Explorer

Theorem xlt2add

Description: Extended real version of lt2add . Note that ltleadd , which has weaker assumptions, is not true for the extended reals (since 0 + +oo < 1 + +oo fails). (Contributed by Mario Carneiro, 23-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 xaddcl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) e. RR* )
2 1 3ad2ant1 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( A +e B ) e. RR* )
3 2 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> ( A +e B ) e. RR* )
4 simp1l 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> A e. RR* )
5 simp2r 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> D e. RR* )
6 xaddcl 
 |-  ( ( A e. RR* /\ D e. RR* ) -> ( A +e D ) e. RR* )
7 4 5 6 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( A +e D ) e. RR* )
8 7 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> ( A +e D ) e. RR* )
9 xaddcl 
 |-  ( ( C e. RR* /\ D e. RR* ) -> ( C +e D ) e. RR* )
10 9 3ad2ant2 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( C +e D ) e. RR* )
11 10 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> ( C +e D ) e. RR* )
12 simp3r 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> B < D )
13 12 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> B < D )
14 simp1r 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> B e. RR* )
15 14 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> B e. RR* )
16 5 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> D e. RR* )
17 simprl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> A e. RR )
18 xltadd2 
 |-  ( ( B e. RR* /\ D e. RR* /\ A e. RR ) -> ( B < D <-> ( A +e B ) < ( A +e D ) ) )
19 15 16 17 18 syl3anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> ( B < D <-> ( A +e B ) < ( A +e D ) ) )
20 13 19 mpbid 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> ( A +e B ) < ( A +e D ) )
21 simp3l 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> A < C )
22 21 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> A < C )
23 4 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> A e. RR* )
24 simp2l 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> C e. RR* )
25 24 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> C e. RR* )
26 simprr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> D e. RR )
27 xltadd1 
 |-  ( ( A e. RR* /\ C e. RR* /\ D e. RR ) -> ( A < C <-> ( A +e D ) < ( C +e D ) ) )
28 23 25 26 27 syl3anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> ( A < C <-> ( A +e D ) < ( C +e D ) ) )
29 22 28 mpbid 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> ( A +e D ) < ( C +e D ) )
30 3 8 11 20 29 xrlttrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ ( A e. RR /\ D e. RR ) ) -> ( A +e B ) < ( C +e D ) )
31 30 anassrs 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ A e. RR ) /\ D e. RR ) -> ( A +e B ) < ( C +e D ) )
32 pnfxr 
 |-  +oo e. RR*
33 32 a1i 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> +oo e. RR* )
34 pnfge 
 |-  ( C e. RR* -> C <_ +oo )
35 24 34 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> C <_ +oo )
36 4 24 33 21 35 xrltletrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> A < +oo )
37 nltpnft 
 |-  ( A e. RR* -> ( A = +oo <-> -. A < +oo ) )
38 37 necon2abid 
 |-  ( A e. RR* -> ( A < +oo <-> A =/= +oo ) )
39 4 38 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( A < +oo <-> A =/= +oo ) )
40 36 39 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> A =/= +oo )
41 pnfge 
 |-  ( D e. RR* -> D <_ +oo )
42 5 41 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> D <_ +oo )
43 14 5 33 12 42 xrltletrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> B < +oo )
44 nltpnft 
 |-  ( B e. RR* -> ( B = +oo <-> -. B < +oo ) )
45 44 necon2abid 
 |-  ( B e. RR* -> ( B < +oo <-> B =/= +oo ) )
46 14 45 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( B < +oo <-> B =/= +oo ) )
47 43 46 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> B =/= +oo )
48 xaddnepnf 
 |-  ( ( ( A e. RR* /\ A =/= +oo ) /\ ( B e. RR* /\ B =/= +oo ) ) -> ( A +e B ) =/= +oo )
49 4 40 14 47 48 syl22anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( A +e B ) =/= +oo )
50 nltpnft 
 |-  ( ( A +e B ) e. RR* -> ( ( A +e B ) = +oo <-> -. ( A +e B ) < +oo ) )
51 50 necon2abid 
 |-  ( ( A +e B ) e. RR* -> ( ( A +e B ) < +oo <-> ( A +e B ) =/= +oo ) )
52 2 51 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( ( A +e B ) < +oo <-> ( A +e B ) =/= +oo ) )
53 49 52 mpbird 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( A +e B ) < +oo )
54 53 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ D = +oo ) -> ( A +e B ) < +oo )
55 oveq2 
 |-  ( D = +oo -> ( C +e D ) = ( C +e +oo ) )
56 mnfxr 
 |-  -oo e. RR*
57 56 a1i 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> -oo e. RR* )
58 mnfle 
 |-  ( A e. RR* -> -oo <_ A )
59 4 58 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> -oo <_ A )
60 57 4 24 59 21 xrlelttrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> -oo < C )
61 ngtmnft 
 |-  ( C e. RR* -> ( C = -oo <-> -. -oo < C ) )
62 61 necon2abid 
 |-  ( C e. RR* -> ( -oo < C <-> C =/= -oo ) )
63 24 62 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( -oo < C <-> C =/= -oo ) )
64 60 63 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> C =/= -oo )
65 xaddpnf1 
 |-  ( ( C e. RR* /\ C =/= -oo ) -> ( C +e +oo ) = +oo )
66 24 64 65 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( C +e +oo ) = +oo )
67 55 66 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ D = +oo ) -> ( C +e D ) = +oo )
68 54 67 breqtrrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ D = +oo ) -> ( A +e B ) < ( C +e D ) )
69 68 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ A e. RR ) /\ D = +oo ) -> ( A +e B ) < ( C +e D ) )
70 mnfle 
 |-  ( B e. RR* -> -oo <_ B )
71 14 70 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> -oo <_ B )
72 57 14 5 71 12 xrlelttrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> -oo < D )
73 ngtmnft 
 |-  ( D e. RR* -> ( D = -oo <-> -. -oo < D ) )
74 73 necon2abid 
 |-  ( D e. RR* -> ( -oo < D <-> D =/= -oo ) )
75 5 74 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( -oo < D <-> D =/= -oo ) )
76 72 75 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> D =/= -oo )
77 76 a1d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( -. ( A +e B ) < ( C +e D ) -> D =/= -oo ) )
78 77 necon4bd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( D = -oo -> ( A +e B ) < ( C +e D ) ) )
79 78 imp 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ D = -oo ) -> ( A +e B ) < ( C +e D ) )
80 79 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ A e. RR ) /\ D = -oo ) -> ( A +e B ) < ( C +e D ) )
81 elxr 
 |-  ( D e. RR* <-> ( D e. RR \/ D = +oo \/ D = -oo ) )
82 5 81 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( D e. RR \/ D = +oo \/ D = -oo ) )
83 82 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ A e. RR ) -> ( D e. RR \/ D = +oo \/ D = -oo ) )
84 31 69 80 83 mpjao3dan 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ A e. RR ) -> ( A +e B ) < ( C +e D ) )
85 40 a1d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( -. ( A +e B ) < ( C +e D ) -> A =/= +oo ) )
86 85 necon4bd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( A = +oo -> ( A +e B ) < ( C +e D ) ) )
87 86 imp 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ A = +oo ) -> ( A +e B ) < ( C +e D ) )
88 oveq1 
 |-  ( A = -oo -> ( A +e B ) = ( -oo +e B ) )
89 xaddmnf2 
 |-  ( ( B e. RR* /\ B =/= +oo ) -> ( -oo +e B ) = -oo )
90 14 47 89 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( -oo +e B ) = -oo )
91 88 90 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ A = -oo ) -> ( A +e B ) = -oo )
92 xaddnemnf 
 |-  ( ( ( C e. RR* /\ C =/= -oo ) /\ ( D e. RR* /\ D =/= -oo ) ) -> ( C +e D ) =/= -oo )
93 24 64 5 76 92 syl22anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( C +e D ) =/= -oo )
94 ngtmnft 
 |-  ( ( C +e D ) e. RR* -> ( ( C +e D ) = -oo <-> -. -oo < ( C +e D ) ) )
95 94 necon2abid 
 |-  ( ( C +e D ) e. RR* -> ( -oo < ( C +e D ) <-> ( C +e D ) =/= -oo ) )
96 10 95 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( -oo < ( C +e D ) <-> ( C +e D ) =/= -oo ) )
97 93 96 mpbird 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> -oo < ( C +e D ) )
98 97 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ A = -oo ) -> -oo < ( C +e D ) )
99 91 98 eqbrtrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) /\ A = -oo ) -> ( A +e B ) < ( C +e D ) )
100 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
101 4 100 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( A e. RR \/ A = +oo \/ A = -oo ) )
102 84 87 99 101 mpjao3dan 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) /\ ( A < C /\ B < D ) ) -> ( A +e B ) < ( C +e D ) )
103 102 3expia 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A < C /\ B < D ) -> ( A +e B ) < ( C +e D ) ) )