ivthlem2 - Metamath Proof Explorer

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

Theorem ivthlem2 19306

Description: Lemma for ivth 19308. 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.

Step	Hyp	Ref	Expression
1		ivth.7	. . . . 5
2	1	adantr 452	. . . 4 $/\$
3		ivth.5	. . . . . 6
4		ivth.11	. . . . . . . 8
5		ivth.10	. . . . . . . . . . . 12
6		ssrab2 3392	. . . . . . . . . . . 12
7	5, 6	eqsstri 3342	. . . . . . . . . . 11
8		ivth.1	. . . . . . . . . . . 12
9		ivth.2	. . . . . . . . . . . 12
10		iccssre 10952	. . . . . . . . . . . 12 $/\$
11	8, 9, 10	syl2anc 643	. . . . . . . . . . 11
12	7, 11	syl5ss 3323	. . . . . . . . . 10
13		ivth.3	. . . . . . . . . . . . 13
14		ivth.4	. . . . . . . . . . . . 13
15		ivth.8	. . . . . . . . . . . . 13 $/\$
16		ivth.9	. . . . . . . . . . . . 13 $/\$
17	8, 9, 13, 14, 3, 1, 15, 16, 5	ivthlem1 19305	. . . . . . . . . . . 12 $/\$
18	17	simpld 446	. . . . . . . . . . 11
19		ne0i 3598	. . . . . . . . . . 11
20	18, 19	syl 16	. . . . . . . . . 10
21	17	simprd 450	. . . . . . . . . . 11
22		breq2 4180	. . . . . . . . . . . . 13
23	22	ralbidv 2690	. . . . . . . . . . . 12
24	23	rspcev 3016	. . . . . . . . . . 11 $/\$
25	9, 21, 24	syl2anc 643	. . . . . . . . . 10
26	12, 20, 25	3jca 1134	. . . . . . . . 9 $/\$ $/\$
27		suprcl 9928	. . . . . . . . 9 $/\$ $/\$
28	26, 27	syl 16	. . . . . . . 8
29	4, 28	syl5eqel 2492	. . . . . . 7
30		suprub 9929	. . . . . . . . 9 $/\$ $/\$ $/\$
31	26, 18, 30	syl2anc 643	. . . . . . . 8
32	31, 4	syl6breqr 4216	. . . . . . 7
33		suprleub 9932	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	26, 9, 33	syl2anc 643	. . . . . . . . 9
35	21, 34	mpbird 224	. . . . . . . 8
36	4, 35	syl5eqbr 4209	. . . . . . 7
37		elicc2 10935	. . . . . . . 8 $/\$ $/\$ $/\$
38	8, 9, 37	syl2anc 643	. . . . . . 7 $/\$ $/\$
39	29, 32, 36, 38	mpbir3and 1137	. . . . . 6
40	3, 39	sseldd 3313	. . . . 5
41	40	adantr 452	. . . 4 $/\$
42	15	ralrimiva 2753	. . . . . . 7
43		fveq2 5691	. . . . . . . . 9
44	43	eleq1d 2474	. . . . . . . 8
45	44	rspcv 3012	. . . . . . 7
46	39, 42, 45	sylc 58	. . . . . 6
47		difrp 10605	. . . . . 6 $/\$
48	46, 13, 47	syl2anc 643	. . . . 5
49	48	biimpa 471	. . . 4 $/\$
50		cncfi 18881	. . . 4 $/\$ $/\$
51	2, 41, 49, 50	syl3anc 1184	. . 3 $/\$
52		ssralv 3371	. . . . . . 7
53	3, 52	syl 16	. . . . . 6
54	53	ad2antrr 707	. . . . 5 $/\$ $/\$
55	9	ad2antrr 707	. . . . . . . . 9 $/\$ $/\$
56	29	ad2antrr 707	. . . . . . . . . 10 $/\$ $/\$
57		rphalfcl 10596	. . . . . . . . . . . 12
58	57	adantl 453	. . . . . . . . . . 11 $/\$ $/\$
59	58	rpred 10608	. . . . . . . . . 10 $/\$ $/\$
60	56, 59	readdcld 9075	. . . . . . . . 9 $/\$ $/\$
61		ifcl 3739	. . . . . . . . 9 $/\$
62	55, 60, 61	syl2anc 643	. . . . . . . 8 $/\$ $/\$
63	8	ad2antrr 707	. . . . . . . . 9 $/\$ $/\$
64	32	ad2antrr 707	. . . . . . . . 9 $/\$ $/\$
65	16	simprd 450	. . . . . . . . . . . . . . 15
66	8	rexrd 9094	. . . . . . . . . . . . . . . . . 18
67	9	rexrd 9094	. . . . . . . . . . . . . . . . . 18
68	8, 9, 14	ltled 9181	. . . . . . . . . . . . . . . . . 18
69		ubicc2 10974	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
70	66, 67, 68, 69	syl3anc 1184	. . . . . . . . . . . . . . . . 17
71		fveq2 5691	. . . . . . . . . . . . . . . . . . 19
72	71	eleq1d 2474	. . . . . . . . . . . . . . . . . 18
73	72	rspcv 3012	. . . . . . . . . . . . . . . . 17
74	70, 42, 73	sylc 58	. . . . . . . . . . . . . . . 16
75		lttr 9112	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76	46, 13, 74, 75	syl3anc 1184	. . . . . . . . . . . . . . 15 $/\$
77	65, 76	mpan2d 656	. . . . . . . . . . . . . 14
78	77	imp 419	. . . . . . . . . . . . 13 $/\$
79	78	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$
80	46	ltnrd 9167	. . . . . . . . . . . . . . . . 17
81		fveq2 5691	. . . . . . . . . . . . . . . . . . 19
82	81	breq2d 4188	. . . . . . . . . . . . . . . . . 18
83	82	notbid 286	. . . . . . . . . . . . . . . . 17
84	80, 83	syl5ibrcom 214	. . . . . . . . . . . . . . . 16
85	84	necon2ad 2619	. . . . . . . . . . . . . . 15
86	85, 36	jctild 528	. . . . . . . . . . . . . 14 $/\$
87	29, 9	ltlend 9178	. . . . . . . . . . . . . 14 $/\$
88	86, 87	sylibrd 226	. . . . . . . . . . . . 13
89	88	ad2antrr 707	. . . . . . . . . . . 12 $/\$ $/\$
90	79, 89	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
91	56, 58	ltaddrpd 10637	. . . . . . . . . . 11 $/\$ $/\$
92		breq2 4180	. . . . . . . . . . . 12
93		breq2 4180	. . . . . . . . . . . 12
94	92, 93	ifboth 3734	. . . . . . . . . . 11 $/\$
95	90, 91, 94	syl2anc 643	. . . . . . . . . 10 $/\$ $/\$
96	56, 62, 95	ltled 9181	. . . . . . . . 9 $/\$ $/\$
97	63, 56, 62, 64, 96	letrd 9187	. . . . . . . 8 $/\$ $/\$
98		min1 10736	. . . . . . . . 9 $/\$
99	55, 60, 98	syl2anc 643	. . . . . . . 8 $/\$ $/\$
100		elicc2 10935	. . . . . . . . . 10 $/\$ $/\$ $/\$
101	8, 9, 100	syl2anc 643	. . . . . . . . 9 $/\$ $/\$
102	101	ad2antrr 707	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
103	62, 97, 99, 102	mpbir3and 1137	. . . . . . 7 $/\$ $/\$
104	56, 62, 96	abssubge0d 12193	. . . . . . . 8 $/\$ $/\$
105		rpre 10578	. . . . . . . . . . . 12
106	105	adantl 453	. . . . . . . . . . 11 $/\$ $/\$
107	56, 106	readdcld 9075	. . . . . . . . . 10 $/\$ $/\$
108		min2 10737	. . . . . . . . . . 11 $/\$
109	55, 60, 108	syl2anc 643	. . . . . . . . . 10 $/\$ $/\$
110		rphalflt 10598	. . . . . . . . . . . 12
111	110	adantl 453	. . . . . . . . . . 11 $/\$ $/\$
112	59, 106, 56, 111	ltadd2dd 9189	. . . . . . . . . 10 $/\$ $/\$
113	62, 60, 107, 109, 112	lelttrd 9188	. . . . . . . . 9 $/\$ $/\$
114	62, 56, 106	ltsubadd2d 9584	. . . . . . . . 9 $/\$ $/\$
115	113, 114	mpbird 224	. . . . . . . 8 $/\$ $/\$
116	104, 115	eqbrtrd 4196	. . . . . . 7 $/\$ $/\$
117		oveq1 6051	. . . . . . . . . . 11
118	117	fveq2d 5695	. . . . . . . . . 10
119	118	breq1d 4186	. . . . . . . . 9
120		breq2 4180	. . . . . . . . 9
121	119, 120	anbi12d 692	. . . . . . . 8 $/\$ $/\$
122	121	rspcev 3016	. . . . . . 7 $/\$ $/\$ $/\$
123	103, 116, 95, 122	syl12anc 1182	. . . . . 6 $/\$ $/\$ $/\$
124		r19.29 2810	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
125		pm3.45 808	. . . . . . . . . 10 $/\$ $/\$
126	125	imp 419	. . . . . . . . 9 $/\$ $/\$ $/\$
127		simprr 734	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
128		simprl 733	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
129		simplll 735	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
130	129, 42	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
131		fveq2 5691	. . . . . . . . . . . . . . . . . . 19
132	131	eleq1d 2474	. . . . . . . . . . . . . . . . . 18
133	132	rspcv 3012	. . . . . . . . . . . . . . . . 17
134	128, 130, 133	sylc 58	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
135	129, 46	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
136	129, 13	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
137	136, 135	resubcld 9425	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
138	134, 135, 137	absdifltd 12195	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
139		ltle 9123	. . . . . . . . . . . . . . . . . . 19 $/\$
140	134, 136, 139	syl2anc 643	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
141	135	recnd 9074	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	136	recnd 9074	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
143	141, 142	pncan3d 9374	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
144	143	breq2d 4188	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
145	131	breq1d 4186	. . . . . . . . . . . . . . . . . . . . 21
146	145, 5	elrab2 3058	. . . . . . . . . . . . . . . . . . . 20 $/\$
147	146	baib 872	. . . . . . . . . . . . . . . . . . 19
148	147	ad2antrl 709	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
149	140, 144, 148	3imtr4d 260	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
150		suprub 9929	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
151	150, 4	syl6breqr 4216	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
152	151	ex 424	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
153	129, 26, 152	3syl 19	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
154	129, 11	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
155	154, 128	sseldd 3313	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
156	129, 29	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
157	155, 156	lenltd 9179	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
158	153, 157	sylibd 206	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
159	149, 158	syld 42	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
160	159	adantld 454	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
161	138, 160	sylbid 207	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
162	127, 161	mt2d 111	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
163	162	pm2.21d 100	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
164	163	expr 599	. . . . . . . . . . 11 $/\$ $/\$ $/\$
165	164	com23 74	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	165	imp3a 421	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
167	126, 166	syl5 30	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
168	167	rexlimdva 2794	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
169	124, 168	syl5 30	. . . . . 6 $/\$ $/\$ $/\$ $/\$
170	123, 169	mpan2d 656	. . . . 5 $/\$ $/\$
171	54, 170	syld 42	. . . 4 $/\$ $/\$
172	171	rexlimdva 2794	. . 3 $/\$
173	51, 172	mpd 15	. 2 $/\$
174	173	pm2.01da 430	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wne 2571

wral 2670

wrex 2671

crab 2674

wss 3284

c0 3592

cif 3703 class class class wbr 4176

cfv 5417 (class class class)co 6044

csup 7407

cc 8948

cr 8949

caddc 8953

cxr 9079

clt 9080

cle 9081

cmin 9251

cdiv 9637

c2 10009

crp 10572

cicc 10879

cabs 11998

ccncf 18863

This theorem is referenced by: ivthlem3 19307

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2389 ax-sep 4294 ax-nul 4302 ax-pow 4341 ax-pr 4367 ax-un 4664 ax-cnex 9006 ax-resscn 9007 ax-1cn 9008 ax-icn 9009 ax-addcl 9010 ax-addrcl 9011 ax-mulcl 9012 ax-mulrcl 9013 ax-mulcom 9014 ax-addass 9015 ax-mulass 9016 ax-distr 9017 ax-i2m1 9018 ax-1ne0 9019 ax-1rid 9020 ax-rnegex 9021 ax-rrecex 9022 ax-cnre 9023 ax-pre-lttri 9024 ax-pre-lttrn 9025 ax-pre-ltadd 9026 ax-pre-mulgt0 9027 ax-pre-sup 9028

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2262 df-mo 2263 df-clab 2395 df-cleq 2401 df-clel 2404 df-nfc 2533 df-ne 2573 df-nel 2574 df-ral 2675 df-rex 2676 df-reu 2677 df-rmo 2678 df-rab 2679 df-v 2922 df-sbc 3126 df-csb 3216 df-dif 3287 df-un 3289 df-in 3291 df-ss 3298 df-pss 3300 df-nul 3593 df-if 3704 df-pw 3765 df-sn 3784 df-pr 3785 df-tp 3786 df-op 3787 df-uni 3980 df-iun 4059 df-br 4177 df-opab 4231 df-mpt 4232 df-tr 4267 df-eprel 4458 df-id 4462 df-po 4467 df-so 4468 df-fr 4505 df-we 4507 df-ord 4548 df-on 4549 df-lim 4550 df-suc 4551 df-om 4809 df-xp 4847 df-rel 4848 df-cnv 4849 df-co 4850 df-dm 4851 df-rn 4852 df-res 4853 df-ima 4854 df-iota 5381 df-fun 5419 df-fn 5420 df-f 5421 df-f1 5422 df-fo 5423 df-f1o 5424 df-fv 5425 df-ov 6047 df-oprab 6048 df-mpt2 6049 df-2nd 6313 df-riota 6512 df-recs 6596 df-rdg 6631 df-er 6868 df-map 6983 df-en 7073 df-dom 7074 df-sdom 7075 df-sup 7408 df-pnf 9082 df-mnf 9083 df-xr 9084 df-ltxr 9085 df-le 9086 df-sub 9253 df-neg 9254 df-div 9638 df-nn 9961 df-2 10018 df-3 10019 df-n0 10182 df-z 10243 df-uz 10449 df-rp 10573 df-icc 10883 df-seq 11283 df-exp 11342 df-cj 11863 df-re 11864 df-im 11865 df-sqr 11999 df-abs 12000 df-cncf 18865

W3C validator