ivthlem2 - Metamath Proof Explorer

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

Theorem ivthlem2 19354

Description: Lemma for ivth 19356. 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 453	. . . 4 $/\$
3		ivth.5	. . . . . 6
4		ivth.11	. . . . . . . 8
5		ivth.10	. . . . . . . . . . . 12
6		ssrab2 3430	. . . . . . . . . . . 12
7	5, 6	eqsstri 3380	. . . . . . . . . . 11
8		ivth.1	. . . . . . . . . . . 12
9		ivth.2	. . . . . . . . . . . 12
10		iccssre 10997	. . . . . . . . . . . 12 $/\$
11	8, 9, 10	syl2anc 644	. . . . . . . . . . 11
12	7, 11	syl5ss 3361	. . . . . . . . . 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 19353	. . . . . . . . . . . 12 $/\$
18	17	simpld 447	. . . . . . . . . . 11
19		ne0i 3636	. . . . . . . . . . 11
20	18, 19	syl 16	. . . . . . . . . 10
21	17	simprd 451	. . . . . . . . . . 11
22		breq2 4219	. . . . . . . . . . . . 13
23	22	ralbidv 2727	. . . . . . . . . . . 12
24	23	rspcev 3054	. . . . . . . . . . 11 $/\$
25	9, 21, 24	syl2anc 644	. . . . . . . . . 10
26	12, 20, 25	3jca 1135	. . . . . . . . 9 $/\$ $/\$
27		suprcl 9973	. . . . . . . . 9 $/\$ $/\$
28	26, 27	syl 16	. . . . . . . 8
29	4, 28	syl5eqel 2522	. . . . . . 7
30		suprub 9974	. . . . . . . . 9 $/\$ $/\$ $/\$
31	26, 18, 30	syl2anc 644	. . . . . . . 8
32	31, 4	syl6breqr 4255	. . . . . . 7
33		suprleub 9977	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	26, 9, 33	syl2anc 644	. . . . . . . . 9
35	21, 34	mpbird 225	. . . . . . . 8
36	4, 35	syl5eqbr 4248	. . . . . . 7
37		elicc2 10980	. . . . . . . 8 $/\$ $/\$ $/\$
38	8, 9, 37	syl2anc 644	. . . . . . 7 $/\$ $/\$
39	29, 32, 36, 38	mpbir3and 1138	. . . . . 6
40	3, 39	sseldd 3351	. . . . 5
41	40	adantr 453	. . . 4 $/\$
42	15	ralrimiva 2791	. . . . . . 7
43		fveq2 5731	. . . . . . . . 9
44	43	eleq1d 2504	. . . . . . . 8
45	44	rspcv 3050	. . . . . . 7
46	39, 42, 45	sylc 59	. . . . . 6
47		difrp 10650	. . . . . 6 $/\$
48	46, 13, 47	syl2anc 644	. . . . 5
49	48	biimpa 472	. . . 4 $/\$
50		cncfi 18929	. . . 4 $/\$ $/\$
51	2, 41, 49, 50	syl3anc 1185	. . 3 $/\$
52		ssralv 3409	. . . . . . 7
53	3, 52	syl 16	. . . . . 6
54	53	ad2antrr 708	. . . . 5 $/\$ $/\$
55	9	ad2antrr 708	. . . . . . . . 9 $/\$ $/\$
56	29	ad2antrr 708	. . . . . . . . . 10 $/\$ $/\$
57		rphalfcl 10641	. . . . . . . . . . . 12
58	57	adantl 454	. . . . . . . . . . 11 $/\$ $/\$
59	58	rpred 10653	. . . . . . . . . 10 $/\$ $/\$
60	56, 59	readdcld 9120	. . . . . . . . 9 $/\$ $/\$
61		ifcl 3777	. . . . . . . . 9 $/\$
62	55, 60, 61	syl2anc 644	. . . . . . . 8 $/\$ $/\$
63	8	ad2antrr 708	. . . . . . . . 9 $/\$ $/\$
64	32	ad2antrr 708	. . . . . . . . 9 $/\$ $/\$
65	16	simprd 451	. . . . . . . . . . . . . . 15
66	8	rexrd 9139	. . . . . . . . . . . . . . . . . 18
67	9	rexrd 9139	. . . . . . . . . . . . . . . . . 18
68	8, 9, 14	ltled 9226	. . . . . . . . . . . . . . . . . 18
69		ubicc2 11019	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
70	66, 67, 68, 69	syl3anc 1185	. . . . . . . . . . . . . . . . 17
71		fveq2 5731	. . . . . . . . . . . . . . . . . . 19
72	71	eleq1d 2504	. . . . . . . . . . . . . . . . . 18
73	72	rspcv 3050	. . . . . . . . . . . . . . . . 17
74	70, 42, 73	sylc 59	. . . . . . . . . . . . . . . 16
75		lttr 9157	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
76	46, 13, 74, 75	syl3anc 1185	. . . . . . . . . . . . . . 15 $/\$
77	65, 76	mpan2d 657	. . . . . . . . . . . . . 14
78	77	imp 420	. . . . . . . . . . . . 13 $/\$
79	78	adantr 453	. . . . . . . . . . . 12 $/\$ $/\$
80	46	ltnrd 9212	. . . . . . . . . . . . . . . . 17
81		fveq2 5731	. . . . . . . . . . . . . . . . . . 19
82	81	breq2d 4227	. . . . . . . . . . . . . . . . . 18
83	82	notbid 287	. . . . . . . . . . . . . . . . 17
84	80, 83	syl5ibrcom 215	. . . . . . . . . . . . . . . 16
85	84	necon2ad 2654	. . . . . . . . . . . . . . 15
86	85, 36	jctild 529	. . . . . . . . . . . . . 14 $/\$
87	29, 9	ltlend 9223	. . . . . . . . . . . . . 14 $/\$
88	86, 87	sylibrd 227	. . . . . . . . . . . . 13
89	88	ad2antrr 708	. . . . . . . . . . . 12 $/\$ $/\$
90	79, 89	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
91	56, 58	ltaddrpd 10682	. . . . . . . . . . 11 $/\$ $/\$
92		breq2 4219	. . . . . . . . . . . 12
93		breq2 4219	. . . . . . . . . . . 12
94	92, 93	ifboth 3772	. . . . . . . . . . 11 $/\$
95	90, 91, 94	syl2anc 644	. . . . . . . . . 10 $/\$ $/\$
96	56, 62, 95	ltled 9226	. . . . . . . . 9 $/\$ $/\$
97	63, 56, 62, 64, 96	letrd 9232	. . . . . . . 8 $/\$ $/\$
98		min1 10781	. . . . . . . . 9 $/\$
99	55, 60, 98	syl2anc 644	. . . . . . . 8 $/\$ $/\$
100		elicc2 10980	. . . . . . . . . 10 $/\$ $/\$ $/\$
101	8, 9, 100	syl2anc 644	. . . . . . . . 9 $/\$ $/\$
102	101	ad2antrr 708	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
103	62, 97, 99, 102	mpbir3and 1138	. . . . . . 7 $/\$ $/\$
104	56, 62, 96	abssubge0d 12239	. . . . . . . 8 $/\$ $/\$
105		rpre 10623	. . . . . . . . . . . 12
106	105	adantl 454	. . . . . . . . . . 11 $/\$ $/\$
107	56, 106	readdcld 9120	. . . . . . . . . 10 $/\$ $/\$
108		min2 10782	. . . . . . . . . . 11 $/\$
109	55, 60, 108	syl2anc 644	. . . . . . . . . 10 $/\$ $/\$
110		rphalflt 10643	. . . . . . . . . . . 12
111	110	adantl 454	. . . . . . . . . . 11 $/\$ $/\$
112	59, 106, 56, 111	ltadd2dd 9234	. . . . . . . . . 10 $/\$ $/\$
113	62, 60, 107, 109, 112	lelttrd 9233	. . . . . . . . 9 $/\$ $/\$
114	62, 56, 106	ltsubadd2d 9629	. . . . . . . . 9 $/\$ $/\$
115	113, 114	mpbird 225	. . . . . . . 8 $/\$ $/\$
116	104, 115	eqbrtrd 4235	. . . . . . 7 $/\$ $/\$
117		oveq1 6091	. . . . . . . . . . 11
118	117	fveq2d 5735	. . . . . . . . . 10
119	118	breq1d 4225	. . . . . . . . 9
120		breq2 4219	. . . . . . . . 9
121	119, 120	anbi12d 693	. . . . . . . 8 $/\$ $/\$
122	121	rspcev 3054	. . . . . . 7 $/\$ $/\$ $/\$
123	103, 116, 95, 122	syl12anc 1183	. . . . . 6 $/\$ $/\$ $/\$
124		r19.29 2848	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
125		pm3.45 809	. . . . . . . . . 10 $/\$ $/\$
126	125	imp 420	. . . . . . . . 9 $/\$ $/\$ $/\$
127		simprr 735	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
128		simprl 734	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
129		simplll 736	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
130	129, 42	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
131		fveq2 5731	. . . . . . . . . . . . . . . . . . 19
132	131	eleq1d 2504	. . . . . . . . . . . . . . . . . 18
133	132	rspcv 3050	. . . . . . . . . . . . . . . . 17
134	128, 130, 133	sylc 59	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
135	129, 46	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
136	129, 13	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
137	136, 135	resubcld 9470	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
138	134, 135, 137	absdifltd 12241	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
139		ltle 9168	. . . . . . . . . . . . . . . . . . 19 $/\$
140	134, 136, 139	syl2anc 644	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
141	135	recnd 9119	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	136	recnd 9119	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
143	141, 142	pncan3d 9419	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
144	143	breq2d 4227	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
145	131	breq1d 4225	. . . . . . . . . . . . . . . . . . . . 21
146	145, 5	elrab2 3096	. . . . . . . . . . . . . . . . . . . 20 $/\$
147	146	baib 873	. . . . . . . . . . . . . . . . . . 19
148	147	ad2antrl 710	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
149	140, 144, 148	3imtr4d 261	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
150		suprub 9974	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
151	150, 4	syl6breqr 4255	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
152	151	ex 425	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
153	129, 26, 152	3syl 19	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
154	129, 11	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
155	154, 128	sseldd 3351	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
156	129, 29	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
157	155, 156	lenltd 9224	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
158	153, 157	sylibd 207	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
159	149, 158	syld 43	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
160	159	adantld 455	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
161	138, 160	sylbid 208	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
162	127, 161	mt2d 112	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
163	162	pm2.21d 101	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
164	163	expr 600	. . . . . . . . . . 11 $/\$ $/\$ $/\$
165	164	com23 75	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	165	imp3a 422	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
167	126, 166	syl5 31	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
168	167	rexlimdva 2832	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
169	124, 168	syl5 31	. . . . . 6 $/\$ $/\$ $/\$ $/\$
170	123, 169	mpan2d 657	. . . . 5 $/\$ $/\$
171	54, 170	syld 43	. . . 4 $/\$ $/\$
172	171	rexlimdva 2832	. . 3 $/\$
173	51, 172	mpd 15	. 2 $/\$
174	173	pm2.01da 431	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 178 $/\$ wa 360 $/\$ w3a 937

wceq 1653

wcel 1726

wne 2601

wral 2707

wrex 2708

crab 2711

wss 3322

c0 3630

cif 3741 class class class wbr 4215

cfv 5457 (class class class)co 6084

csup 7448

cc 8993

cr 8994

caddc 8998

cxr 9124

clt 9125

cle 9126

cmin 9296

cdiv 9682

c2 10054

crp 10617

cicc 10924

cabs 12044

ccncf 18911

This theorem is referenced by: ivthlem3 19355

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1556 ax-5 1567 ax-17 1627 ax-9 1667 ax-8 1688 ax-13 1728 ax-14 1730 ax-6 1745 ax-7 1750 ax-11 1762 ax-12 1951 ax-ext 2419 ax-sep 4333 ax-nul 4341 ax-pow 4380 ax-pr 4406 ax-un 4704 ax-cnex 9051 ax-resscn 9052 ax-1cn 9053 ax-icn 9054 ax-addcl 9055 ax-addrcl 9056 ax-mulcl 9057 ax-mulrcl 9058 ax-mulcom 9059 ax-addass 9060 ax-mulass 9061 ax-distr 9062 ax-i2m1 9063 ax-1ne0 9064 ax-1rid 9065 ax-rnegex 9066 ax-rrecex 9067 ax-cnre 9068 ax-pre-lttri 9069 ax-pre-lttrn 9070 ax-pre-ltadd 9071 ax-pre-mulgt0 9072 ax-pre-sup 9073

This theorem depends on definitions: df-bi 179 df-or 361 df-an 362 df-3or 938 df-3an 939 df-tru 1329 df-ex 1552 df-nf 1555 df-sb 1660 df-eu 2287 df-mo 2288 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2712 df-rex 2713 df-reu 2714 df-rmo 2715 df-rab 2716 df-v 2960 df-sbc 3164 df-csb 3254 df-dif 3325 df-un 3327 df-in 3329 df-ss 3336 df-pss 3338 df-nul 3631 df-if 3742 df-pw 3803 df-sn 3822 df-pr 3823 df-tp 3824 df-op 3825 df-uni 4018 df-iun 4097 df-br 4216 df-opab 4270 df-mpt 4271 df-tr 4306 df-eprel 4497 df-id 4501 df-po 4506 df-so 4507 df-fr 4544 df-we 4546 df-ord 4587 df-on 4588 df-lim 4589 df-suc 4590 df-om 4849 df-xp 4887 df-rel 4888 df-cnv 4889 df-co 4890 df-dm 4891 df-rn 4892 df-res 4893 df-ima 4894 df-iota 5421 df-fun 5459 df-fn 5460 df-f 5461 df-f1 5462 df-fo 5463 df-f1o 5464 df-fv 5465 df-ov 6087 df-oprab 6088 df-mpt2 6089 df-2nd 6353 df-riota 6552 df-recs 6636 df-rdg 6671 df-er 6908 df-map 7023 df-en 7113 df-dom 7114 df-sdom 7115 df-sup 7449 df-pnf 9127 df-mnf 9128 df-xr 9129 df-ltxr 9130 df-le 9131 df-sub 9298 df-neg 9299 df-div 9683 df-nn 10006 df-2 10063 df-3 10064 df-n0 10227 df-z 10288 df-uz 10494 df-rp 10618 df-icc 10928 df-seq 11329 df-exp 11388 df-cj 11909 df-re 11910 df-im 11911 df-sqr 12045 df-abs 12046 df-cncf 18913

W3C validator