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

Theorem ivthlem2 21594
 Description: Lemma for ivth 21596. Show that the supremum of cannot be less than . If it was, continuity of implies that there are points just above the supremum that are also less than , a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014.)
Hypotheses
Ref Expression
ivth.1
ivth.2
ivth.3
ivth.4
ivth.5
ivth.7
ivth.8
ivth.9
ivth.10
ivth.11
Assertion
Ref Expression
ivthlem2
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,

Proof of Theorem ivthlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ivth.7 . . . . 5
21adantr 465 . . . 4
3 ivth.5 . . . . . 6
4 ivth.11 . . . . . . . 8
5 ivth.10 . . . . . . . . . . . 12
6 ssrab2 3580 . . . . . . . . . . . 12
75, 6eqsstri 3529 . . . . . . . . . . 11
8 ivth.1 . . . . . . . . . . . 12
9 ivth.2 . . . . . . . . . . . 12
10 iccssre 11597 . . . . . . . . . . . 12
118, 9, 10syl2anc 661 . . . . . . . . . . 11
127, 11syl5ss 3510 . . . . . . . . . 10
13 ivth.3 . . . . . . . . . . . . 13
14 ivth.4 . . . . . . . . . . . . 13
15 ivth.8 . . . . . . . . . . . . 13
16 ivth.9 . . . . . . . . . . . . 13
178, 9, 13, 14, 3, 1, 15, 16, 5ivthlem1 21593 . . . . . . . . . . . 12
1817simpld 459 . . . . . . . . . . 11
19 ne0i 3786 . . . . . . . . . . 11
2018, 19syl 16 . . . . . . . . . 10
2117simprd 463 . . . . . . . . . . 11
22 breq2 4446 . . . . . . . . . . . . 13
2322ralbidv 2898 . . . . . . . . . . . 12
2423rspcev 3209 . . . . . . . . . . 11
259, 21, 24syl2anc 661 . . . . . . . . . 10
2612, 20, 253jca 1171 . . . . . . . . 9
27 suprcl 10494 . . . . . . . . 9
2826, 27syl 16 . . . . . . . 8
294, 28syl5eqel 2554 . . . . . . 7
30 suprub 10495 . . . . . . . . 9
3126, 18, 30syl2anc 661 . . . . . . . 8
3231, 4syl6breqr 4482 . . . . . . 7
33 suprleub 10498 . . . . . . . . . 10
3426, 9, 33syl2anc 661 . . . . . . . . 9
3521, 34mpbird 232 . . . . . . . 8
364, 35syl5eqbr 4475 . . . . . . 7
37 elicc2 11580 . . . . . . . 8
388, 9, 37syl2anc 661 . . . . . . 7
3929, 32, 36, 38mpbir3and 1174 . . . . . 6
403, 39sseldd 3500 . . . . 5
4140adantr 465 . . . 4
4215ralrimiva 2873 . . . . . . 7
43 fveq2 5859 . . . . . . . . 9
4443eleq1d 2531 . . . . . . . 8
4544rspcv 3205 . . . . . . 7
4639, 42, 45sylc 60 . . . . . 6
47 difrp 11244 . . . . . 6
4846, 13, 47syl2anc 661 . . . . 5
4948biimpa 484 . . . 4
50 cncfi 21128 . . . 4
512, 41, 49, 50syl3anc 1223 . . 3
52 ssralv 3559 . . . . . . 7
533, 52syl 16 . . . . . 6
5453ad2antrr 725 . . . . 5
559ad2antrr 725 . . . . . . . . 9
5629ad2antrr 725 . . . . . . . . . 10
57 rphalfcl 11235 . . . . . . . . . . . 12
5857adantl 466 . . . . . . . . . . 11
5958rpred 11247 . . . . . . . . . 10
6056, 59readdcld 9614 . . . . . . . . 9
61 ifcl 3976 . . . . . . . . 9
6255, 60, 61syl2anc 661 . . . . . . . 8
638ad2antrr 725 . . . . . . . . 9
6432ad2antrr 725 . . . . . . . . 9
6516simprd 463 . . . . . . . . . . . . . . 15
668rexrd 9634 . . . . . . . . . . . . . . . . . 18
679rexrd 9634 . . . . . . . . . . . . . . . . . 18
688, 9, 14ltled 9723 . . . . . . . . . . . . . . . . . 18
69 ubicc2 11628 . . . . . . . . . . . . . . . . . 18
7066, 67, 68, 69syl3anc 1223 . . . . . . . . . . . . . . . . 17
71 fveq2 5859 . . . . . . . . . . . . . . . . . . 19
7271eleq1d 2531 . . . . . . . . . . . . . . . . . 18
7372rspcv 3205 . . . . . . . . . . . . . . . . 17
7470, 42, 73sylc 60 . . . . . . . . . . . . . . . 16
75 lttr 9652 . . . . . . . . . . . . . . . 16
7646, 13, 74, 75syl3anc 1223 . . . . . . . . . . . . . . 15
7765, 76mpan2d 674 . . . . . . . . . . . . . 14
7877imp 429 . . . . . . . . . . . . 13
7978adantr 465 . . . . . . . . . . . 12
8046ltnrd 9709 . . . . . . . . . . . . . . . . 17
81 fveq2 5859 . . . . . . . . . . . . . . . . . . 19
8281breq2d 4454 . . . . . . . . . . . . . . . . . 18
8382notbid 294 . . . . . . . . . . . . . . . . 17
8480, 83syl5ibrcom 222 . . . . . . . . . . . . . . . 16
8584necon2ad 2675 . . . . . . . . . . . . . . 15
8685, 36jctild 543 . . . . . . . . . . . . . 14
8729, 9ltlend 9720 . . . . . . . . . . . . . 14
8886, 87sylibrd 234 . . . . . . . . . . . . 13
8988ad2antrr 725 . . . . . . . . . . . 12
9079, 89mpd 15 . . . . . . . . . . 11
9156, 58ltaddrpd 11276 . . . . . . . . . . 11
92 breq2 4446 . . . . . . . . . . . 12
93 breq2 4446 . . . . . . . . . . . 12
9492, 93ifboth 3970 . . . . . . . . . . 11
9590, 91, 94syl2anc 661 . . . . . . . . . 10
9656, 62, 95ltled 9723 . . . . . . . . 9
9763, 56, 62, 64, 96letrd 9729 . . . . . . . 8
98 min1 11380 . . . . . . . . 9
9955, 60, 98syl2anc 661 . . . . . . . 8
100 elicc2 11580 . . . . . . . . . 10
1018, 9, 100syl2anc 661 . . . . . . . . 9
102101ad2antrr 725 . . . . . . . 8
10362, 97, 99, 102mpbir3and 1174 . . . . . . 7
10456, 62, 96abssubge0d 13214 . . . . . . . 8
105 rpre 11217 . . . . . . . . . . . 12
106105adantl 466 . . . . . . . . . . 11
10756, 106readdcld 9614 . . . . . . . . . 10
108 min2 11381 . . . . . . . . . . 11
10955, 60, 108syl2anc 661 . . . . . . . . . 10
110 rphalflt 11237 . . . . . . . . . . . 12
111110adantl 466 . . . . . . . . . . 11
11259, 106, 56, 111ltadd2dd 9731 . . . . . . . . . 10
11362, 60, 107, 109, 112lelttrd 9730 . . . . . . . . 9
11462, 56, 106ltsubadd2d 10141 . . . . . . . . 9
115113, 114mpbird 232 . . . . . . . 8
116104, 115eqbrtrd 4462 . . . . . . 7
117 oveq1 6284 . . . . . . . . . . 11
118117fveq2d 5863 . . . . . . . . . 10
119118breq1d 4452 . . . . . . . . 9
120 breq2 4446 . . . . . . . . 9
121119, 120anbi12d 710 . . . . . . . 8
122121rspcev 3209 . . . . . . 7
123103, 116, 95, 122syl12anc 1221 . . . . . 6
124 r19.29 2992 . . . . . . 7
125 pm3.45 831 . . . . . . . . . 10
126125imp 429 . . . . . . . . 9
127 simprr 756 . . . . . . . . . . . . . 14
128 simprl 755 . . . . . . . . . . . . . . . . 17
129 simplll 757 . . . . . . . . . . . . . . . . . 18
130129, 42syl 16 . . . . . . . . . . . . . . . . 17
131 fveq2 5859 . . . . . . . . . . . . . . . . . . 19
132131eleq1d 2531 . . . . . . . . . . . . . . . . . 18
133132rspcv 3205 . . . . . . . . . . . . . . . . 17
134128, 130, 133sylc 60 . . . . . . . . . . . . . . . 16
135129, 46syl 16 . . . . . . . . . . . . . . . 16
136129, 13syl 16 . . . . . . . . . . . . . . . . 17
137136, 135resubcld 9978 . . . . . . . . . . . . . . . 16
138134, 135, 137absdifltd 13216 . . . . . . . . . . . . . . 15
139 ltle 9664 . . . . . . . . . . . . . . . . . . 19
140134, 136, 139syl2anc 661 . . . . . . . . . . . . . . . . . 18
141135recnd 9613 . . . . . . . . . . . . . . . . . . . 20
142136recnd 9613 . . . . . . . . . . . . . . . . . . . 20
143141, 142pncan3d 9924 . . . . . . . . . . . . . . . . . . 19
144143breq2d 4454 . . . . . . . . . . . . . . . . . 18
145131breq1d 4452 . . . . . . . . . . . . . . . . . . . . 21
146145, 5elrab2 3258 . . . . . . . . . . . . . . . . . . . 20
147146baib 898 . . . . . . . . . . . . . . . . . . 19
148147ad2antrl 727 . . . . . . . . . . . . . . . . . 18
149140, 144, 1483imtr4d 268 . . . . . . . . . . . . . . . . 17
150 suprub 10495 . . . . . . . . . . . . . . . . . . . . 21
151150, 4syl6breqr 4482 . . . . . . . . . . . . . . . . . . . 20
152151ex 434 . . . . . . . . . . . . . . . . . . 19
153129, 26, 1523syl 20 . . . . . . . . . . . . . . . . . 18
154129, 11syl 16 . . . . . . . . . . . . . . . . . . . 20
155154, 128sseldd 3500 . . . . . . . . . . . . . . . . . . 19
156129, 29syl 16 . . . . . . . . . . . . . . . . . . 19
157155, 156lenltd 9721 . . . . . . . . . . . . . . . . . 18
158153, 157sylibd 214 . . . . . . . . . . . . . . . . 17
159149, 158syld 44 . . . . . . . . . . . . . . . 16
160159adantld 467 . . . . . . . . . . . . . . 15
161138, 160sylbid 215 . . . . . . . . . . . . . 14
162127, 161mt2d 117 . . . . . . . . . . . . 13
163162pm2.21d 106 . . . . . . . . . . . 12
164163expr 615 . . . . . . . . . . 11
165164com23 78 . . . . . . . . . 10
166165impd 431 . . . . . . . . 9
167126, 166syl5 32 . . . . . . . 8
168167rexlimdva 2950 . . . . . . 7
169124, 168syl5 32 . . . . . 6
170123, 169mpan2d 674 . . . . 5
17154, 170syld 44 . . . 4
172171rexlimdva 2950 . . 3
17351, 172mpd 15 . 2
174173pm2.01da 442 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   w3a 968   wceq 1374   wcel 1762   wne 2657  wral 2809  wrex 2810  crab 2813   wss 3471  c0 3780  cif 3934   class class class wbr 4442  cfv 5581  (class class class)co 6277  csup 7891  cc 9481  cr 9482   caddc 9486  cxr 9618   clt 9619   cle 9620   cmin 9796   cdiv 10197  c2 10576  crp 11211  cicc 11523  cabs 13019  ccncf 21110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560  ax-pre-sup 9561 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-nel 2660  df-ral 2814  df-rex 2815  df-reu 2816  df-rmo 2817  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-tp 4027  df-op 4029  df-uni 4241  df-iun 4322  df-br 4443  df-opab 4501  df-mpt 4502  df-tr 4536  df-eprel 4786  df-id 4790  df-po 4795  df-so 4796  df-fr 4833  df-we 4835  df-ord 4876  df-on 4877  df-lim 4878  df-suc 4879  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6674  df-2nd 6777  df-recs 7034  df-rdg 7068  df-er 7303  df-map 7414  df-en 7509  df-dom 7510  df-sdom 7511  df-sup 7892  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9798  df-neg 9799  df-div 10198  df-nn 10528  df-2 10585  df-3 10586  df-n0 10787  df-z 10856  df-uz 11074  df-rp 11212  df-icc 11527  df-seq 12066  df-exp 12125  df-cj 12884  df-re 12885  df-im 12886  df-sqr 13020  df-abs 13021  df-cncf 21112 This theorem is referenced by:  ivthlem3  21595
 Copyright terms: Public domain W3C validator