Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xlt2addrd Structured version   Unicode version

 Description: If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)

StepHypRef Expression
1 xlt2addrd.1 . . . . . 6
21rexrd 9697 . . . . 5
32ad2antrr 730 . . . 4
4 0xr 9694 . . . . 5
54a1i 11 . . . 4
6 xaddid1 11539 . . . . . 6
76eqcomd 2430 . . . . 5
83, 7syl 17 . . . 4
91ad2antrr 730 . . . . . 6
10 ltpnf 11429 . . . . . 6
119, 10syl 17 . . . . 5
12 simplr 760 . . . . 5
1311, 12breqtrrd 4450 . . . 4
14 0ltpnf 11431 . . . . 5
15 simpr 462 . . . . 5
1614, 15syl5breqr 4460 . . . 4
17 oveq1 6312 . . . . . . 7
1817eqeq2d 2436 . . . . . 6
19 breq1 4426 . . . . . 6
2018, 193anbi12d 1336 . . . . 5
21 oveq2 6313 . . . . . . 7
2221eqeq2d 2436 . . . . . 6
23 breq1 4426 . . . . . 6
2422, 233anbi13d 1337 . . . . 5
2520, 24rspc2ev 3193 . . . 4
263, 5, 8, 13, 16, 25syl113anc 1276 . . 3
272ad2antrr 730 . . . . 5
28 xlt2addrd.3 . . . . . . . 8
2928ad2antrr 730 . . . . . . 7
30 1re 9649 . . . . . . . . . 10
3130rexri 9700 . . . . . . . . 9
3231a1i 11 . . . . . . . 8
3332xnegcld 11593 . . . . . . 7
3429, 33xaddcld 11594 . . . . . 6
3534xnegcld 11593 . . . . 5
3627, 35xaddcld 11594 . . . 4
371ad2antrr 730 . . . . . . 7
3837renemnfd 9699 . . . . . 6
39 xrnepnf 11427 . . . . . . . . . . . . . . 15
4039biimpi 197 . . . . . . . . . . . . . 14
4129, 40sylancom 671 . . . . . . . . . . . . 13
4241orcomd 389 . . . . . . . . . . . 12
43 xlt2addrd.5 . . . . . . . . . . . . . 14
4443ad2antrr 730 . . . . . . . . . . . . 13
4544neneqd 2621 . . . . . . . . . . . 12
46 pm2.53 374 . . . . . . . . . . . 12
4742, 45, 46sylc 62 . . . . . . . . . . 11
48 rexsub 11533 . . . . . . . . . . 11
4947, 30, 48sylancl 666 . . . . . . . . . 10
50 resubcl 9945 . . . . . . . . . . 11
5147, 30, 50sylancl 666 . . . . . . . . . 10
5249, 51eqeltrd 2507 . . . . . . . . 9
53 rexneg 11511 . . . . . . . . 9
5452, 53syl 17 . . . . . . . 8
5552renegcld 10053 . . . . . . . 8
5654, 55eqeltrd 2507 . . . . . . 7
5756renemnfd 9699 . . . . . 6
5852renemnfd 9699 . . . . . 6
59 xaddass 11542 . . . . . 6
6027, 38, 35, 57, 34, 58, 59syl222anc 1280 . . . . 5
61 xaddcom 11538 . . . . . . . 8
6235, 34, 61syl2anc 665 . . . . . . 7
63 xnegid 11536 . . . . . . . 8
6434, 63syl 17 . . . . . . 7
6562, 64eqtrd 2463 . . . . . 6
6665oveq2d 6321 . . . . 5
6727, 6syl 17 . . . . 5
6860, 66, 673eqtrrd 2468 . . . 4
6937, 51resubcld 10054 . . . . . 6
70 ltpnf 11429 . . . . . 6
7169, 70syl 17 . . . . 5
72 rexsub 11533 . . . . . . 7
7337, 52, 72syl2anc 665 . . . . . 6
7449oveq2d 6321 . . . . . 6
7573, 74eqtrd 2463 . . . . 5
76 simplr 760 . . . . 5
7771, 75, 763brtr4d 4454 . . . 4
7847ltm1d 10546 . . . . 5
7949, 78eqbrtrd 4444 . . . 4
80 oveq1 6312 . . . . . . 7
8180eqeq2d 2436 . . . . . 6
82 breq1 4426 . . . . . 6
8381, 823anbi12d 1336 . . . . 5
84 oveq2 6313 . . . . . . 7
8584eqeq2d 2436 . . . . . 6
86 breq1 4426 . . . . . 6
8785, 863anbi13d 1337 . . . . 5
8883, 87rspc2ev 3193 . . . 4
8936, 34, 68, 77, 79, 88syl113anc 1276 . . 3
9026, 89pm2.61dane 2738 . 2
91 xlt2addrd.2 . . . . . 6
9291ad2antrr 730 . . . . 5
9331a1i 11 . . . . . 6
9493xnegcld 11593 . . . . 5
9592, 94xaddcld 11594 . . . 4
962ad2antrr 730 . . . . 5
9795xnegcld 11593 . . . . 5
9896, 97xaddcld 11594 . . . 4
99 xaddcom 11538 . . . . . 6
10095, 98, 99syl2anc 665 . . . . 5
1011ad2antrr 730 . . . . . . 7
102101renemnfd 9699 . . . . . 6
103 simplr 760 . . . . . . . . . . . . . 14
104 xrnepnf 11427 . . . . . . . . . . . . . . 15
105104biimpi 197 . . . . . . . . . . . . . 14
10692, 103, 105syl2anc 665 . . . . . . . . . . . . 13
107106orcomd 389 . . . . . . . . . . . 12
108 xlt2addrd.4 . . . . . . . . . . . . . 14
109108ad2antrr 730 . . . . . . . . . . . . 13
110109neneqd 2621 . . . . . . . . . . . 12
111 pm2.53 374 . . . . . . . . . . . 12
112107, 110, 111sylc 62 . . . . . . . . . . 11
113 rexsub 11533 . . . . . . . . . . 11
114112, 30, 113sylancl 666 . . . . . . . . . 10
115 resubcl 9945 . . . . . . . . . . 11
116112, 30, 115sylancl 666 . . . . . . . . . 10
117114, 116eqeltrd 2507 . . . . . . . . 9
118 rexneg 11511 . . . . . . . . 9
119117, 118syl 17 . . . . . . . 8
120117renegcld 10053 . . . . . . . 8
121119, 120eqeltrd 2507 . . . . . . 7
122121renemnfd 9699 . . . . . 6
123117renemnfd 9699 . . . . . 6
124 xaddass 11542 . . . . . 6
12596, 102, 97, 122, 95, 123, 124syl222anc 1280 . . . . 5
126 xaddcom 11538 . . . . . . . . 9
12797, 95, 126syl2anc 665 . . . . . . . 8
128 xnegid 11536 . . . . . . . . 9
12995, 128syl 17 . . . . . . . 8
130127, 129eqtrd 2463 . . . . . . 7
131130oveq2d 6321 . . . . . 6
13296, 6syl 17 . . . . . 6
133131, 132eqtrd 2463 . . . . 5
134100, 125, 1333eqtrrd 2468 . . . 4
135112ltm1d 10546 . . . . 5
136114, 135eqbrtrd 4444 . . . 4
137101, 116resubcld 10054 . . . . . 6
138 ltpnf 11429 . . . . . 6
139137, 138syl 17 . . . . 5
140 rexsub 11533 . . . . . . 7
141101, 117, 140syl2anc 665 . . . . . 6
142114oveq2d 6321 . . . . . 6
143141, 142eqtrd 2463 . . . . 5
144 simpr 462 . . . . 5
145139, 143, 1443brtr4d 4454 . . . 4
146 oveq1 6312 . . . . . . 7
147146eqeq2d 2436 . . . . . 6
148 breq1 4426 . . . . . 6
149147, 1483anbi12d 1336 . . . . 5
150 oveq2 6313 . . . . . . 7
151150eqeq2d 2436 . . . . . 6
152 breq1 4426 . . . . . 6
153151, 1523anbi13d 1337 . . . . 5
154149, 153rspc2ev 3193 . . . 4
15595, 98, 134, 136, 145, 154syl113anc 1276 . . 3
1561ad2antrr 730 . . . . . 6
15791ad2antrr 730 . . . . . . . . 9
158 simplr 760 . . . . . . . . 9
159157, 158, 105syl2anc 665 . . . . . . . 8
160159orcomd 389 . . . . . . 7
161108ad2antrr 730 . . . . . . . 8
162161neneqd 2621 . . . . . . 7
163160, 162, 111sylc 62 . . . . . 6
16428ad2antrr 730 . . . . . . . . 9
165164, 40sylancom 671 . . . . . . . 8
166165orcomd 389 . . . . . . 7
16743ad2antrr 730 . . . . . . . 8
168167neneqd 2621 . . . . . . 7
169166, 168, 46sylc 62 . . . . . 6
170 xlt2addrd.6 . . . . . . . 8
171170ad2antrr 730 . . . . . . 7
172 rexadd 11532 . . . . . . . 8
173163, 169, 172syl2anc 665 . . . . . . 7
174171, 173breqtrd 4448 . . . . . 6
175156, 163, 169, 174lt2addrd 28332 . . . . 5
176 rexadd 11532 . . . . . . . 8
177176eqeq2d 2436 . . . . . . 7
1781773anbi1d 1339 . . . . . 6
1791782rexbiia 2941 . . . . 5
180175, 179sylibr 215 . . . 4
181 ressxr 9691 . . . . . 6
182 ssrexv 3526 . . . . . 6
183181, 182ax-mp 5 . . . . 5
184183reximi 2890 . . . 4
185 ssrexv 3526 . . . . 5
186181, 185ax-mp 5 . . . 4
187180, 184, 1863syl 18 . . 3
188155, 187pm2.61dane 2738 . 2
18990, 188pm2.61dane 2738 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 369   wa 370   w3a 982   wceq 1437   wcel 1872   wne 2614  wrex 2772   wss 3436   class class class wbr 4423  (class class class)co 6305  cr 9545  cc0 9546  c1 9547   caddc 9549   cpnf 9679   cmnf 9680  cxr 9681   clt 9682   cmin 9867  cneg 9868   cxne 11413  cxad 11414 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 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623 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 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-div 10277  df-2 10675  df-rp 11310  df-xneg 11416  df-xadd 11417 This theorem is referenced by:  xrofsup  28359
 Copyright terms: Public domain W3C validator