volivth - Metamath Proof Explorer

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

Theorem volivth 21109

Description: The Intermediate Value Theorem for the Lebesgue volume function. For any positive

, there is a measurable subset of

whose volume is

. (Contributed by Mario Carneiro, 30-Aug-2014.)

**Assertion**
Ref	Expression
volivth	$/\$ $/\$

Distinct variable groups:

Proof of Theorem volivth Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 753	. . . 4 $/\$ $/\$
2		mnfxr 11115	. . . . . 6
3	2	a1i 11	. . . . 5 $/\$ $/\$
4		iccssxr 11399	. . . . . . 7
5		simpr 461	. . . . . . 7 $/\$
6	4, 5	sseldi 3375	. . . . . 6 $/\$
7	6	adantr 465	. . . . 5 $/\$ $/\$
8		iccssxr 11399	. . . . . . . 8
9		volf 21034	. . . . . . . . 9
10	9	ffvelrni 5863	. . . . . . . 8
11	8, 10	sseldi 3375	. . . . . . 7
12	11	adantr 465	. . . . . 6 $/\$
13	12	adantr 465	. . . . 5 $/\$ $/\$
14		0xr 9451	. . . . . . . . . 10
15		elicc1 11365	. . . . . . . . . 10 $/\$ $/\$ $/\$
16	14, 12, 15	sylancr 663	. . . . . . . . 9 $/\$ $/\$ $/\$
17	5, 16	mpbid 210	. . . . . . . 8 $/\$ $/\$ $/\$
18	17	simp2d 1001	. . . . . . 7 $/\$
19	18	adantr 465	. . . . . 6 $/\$ $/\$
20		mnflt0 11126	. . . . . . . 8
21		xrltletr 11152	. . . . . . . 8 $/\$ $/\$ $/\$
22	20, 21	mpani 676	. . . . . . 7 $/\$ $/\$
23	2, 14, 22	mp3an12 1304	. . . . . 6
24	7, 19, 23	sylc 60	. . . . 5 $/\$ $/\$
25		simpr 461	. . . . 5 $/\$ $/\$
26		xrre2 11163	. . . . 5 $/\$ $/\$ $/\$ $/\$
27	3, 7, 13, 24, 25, 26	syl32anc 1226	. . . 4 $/\$ $/\$
28		volsup2 21107	. . . 4 $/\$ $/\$
29	1, 27, 25, 28	syl3anc 1218	. . 3 $/\$ $/\$
30		nnre 10350	. . . . . . 7
31	30	ad2antrl 727	. . . . . 6 $/\$ $/\$ $/\$ $/\$
32	31	renegcld 9796	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	27	adantr 465	. . . . 5 $/\$ $/\$ $/\$ $/\$
34		0red 9408	. . . . . 6 $/\$ $/\$ $/\$ $/\$
35		nngt0 10372	. . . . . . . 8
36	35	ad2antrl 727	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
37	31	lt0neg2d 9931	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
38	36, 37	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$ $/\$
39	32, 34, 31, 38, 36	lttrd 9553	. . . . 5 $/\$ $/\$ $/\$ $/\$
40		iccssre 11398	. . . . . 6 $/\$
41	32, 31, 40	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $/\$
42		ax-resscn 9360	. . . . . . 7
43		ssid 3396	. . . . . . 7
44		cncfss 20497	. . . . . . 7 $/\$
45	42, 43, 44	mp2an 672	. . . . . 6
46	1	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
47		eqid 2443	. . . . . . . 8
48	47	volcn 21108	. . . . . . 7 $/\$
49	46, 32, 48	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$ $/\$
50	45, 49	sseldi 3375	. . . . 5 $/\$ $/\$ $/\$ $/\$
51	41	sselda 3377	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
52		cncff 20491	. . . . . . . 8
53	49, 52	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
54	53	ffvelrnda 5864	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	syldan 470	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
56		oveq2 6120	. . . . . . . . . . . 12
57	56	ineq2d 3573	. . . . . . . . . . 11
58	57	fveq2d 5716	. . . . . . . . . 10
59		fvex 5722	. . . . . . . . . 10
60	58, 47, 59	fvmpt 5795	. . . . . . . . 9
61	32, 60	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
62		inss2 3592	. . . . . . . . . . . 12
63	32	rexrd 9454	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64		iccid 11366	. . . . . . . . . . . . 13
65	63, 64	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
66	62, 65	syl5sseq 3425	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
67	32	snssd 4039	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
68	66, 67	sstrd 3387	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
69		ovolsn 21000	. . . . . . . . . . . 12
70	32, 69	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
71		ovolssnul 20992	. . . . . . . . . . 11 $/\$ $/\$
72	66, 67, 70, 71	syl3anc 1218	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73		nulmbl 21039	. . . . . . . . . 10 $/\$
74	68, 72, 73	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
75		mblvol 21035	. . . . . . . . 9
76	74, 75	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
77	61, 76, 72	3eqtrd 2479	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
78	19	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
79	77, 78	eqbrtrd 4333	. . . . . 6 $/\$ $/\$ $/\$ $/\$
80		simprr 756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	7	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
82		iccmbl 21069	. . . . . . . . . . . 12 $/\$
83	32, 31, 82	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
84		inmbl 21045	. . . . . . . . . . 11 $/\$
85	46, 83, 84	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
86	9	ffvelrni 5863	. . . . . . . . . . 11
87	8, 86	sseldi 3375	. . . . . . . . . 10
88	85, 87	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
89		xrltle 11147	. . . . . . . . 9 $/\$
90	81, 88, 89	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
91	80, 90	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
92		oveq2 6120	. . . . . . . . . . 11
93	92	ineq2d 3573	. . . . . . . . . 10
94	93	fveq2d 5716	. . . . . . . . 9
95		fvex 5722	. . . . . . . . 9
96	94, 47, 95	fvmpt 5795	. . . . . . . 8
97	31, 96	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
98	91, 97	breqtrrd 4339	. . . . . 6 $/\$ $/\$ $/\$ $/\$
99	79, 98	jca 532	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
100	32, 31, 33, 39, 41, 50, 55, 99	ivthle 20962	. . . 4 $/\$ $/\$ $/\$ $/\$
101	41	sselda 3377	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
102		oveq2 6120	. . . . . . . . . . 11
103	102	ineq2d 3573	. . . . . . . . . 10
104	103	fveq2d 5716	. . . . . . . . 9
105		fvex 5722	. . . . . . . . 9
106	104, 47, 105	fvmpt 5795	. . . . . . . 8
107	101, 106	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
108	107	eqeq1d 2451	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
109	46	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	32	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111	101	adantrr 716	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112		iccmbl 21069	. . . . . . . . . 10 $/\$
113	110, 111, 112	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		inmbl 21045	. . . . . . . . 9 $/\$
115	109, 113, 114	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		inss1 3591	. . . . . . . . 9
117	116	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118		simprr 756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		sseq1 3398	. . . . . . . . . 10
120		fveq2 5712	. . . . . . . . . . 11
121	120	eqeq1d 2451	. . . . . . . . . 10
122	119, 121	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
123	122	rspcev 3094	. . . . . . . 8 $/\$ $/\$ $/\$
124	115, 117, 118, 123	syl12anc 1216	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	124	expr 615	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	108, 125	sylbid 215	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	126	rexlimdva 2862	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
128	100, 127	mpd 15	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
129	29, 128	rexlimddv 2866	. 2 $/\$ $/\$ $/\$
130		simpll 753	. . 3 $/\$ $/\$
131		ssid 3396	. . . 4
132	131	a1i 11	. . 3 $/\$ $/\$
133		simpr 461	. . . 4 $/\$ $/\$
134	133	eqcomd 2448	. . 3 $/\$ $/\$
135		sseq1 3398	. . . . 5
136		fveq2 5712	. . . . . 6
137	136	eqeq1d 2451	. . . . 5
138	135, 137	anbi12d 710	. . . 4 $/\$ $/\$
139	138	rspcev 3094	. . 3 $/\$ $/\$ $/\$
140	130, 132, 134, 139	syl12anc 1216	. 2 $/\$ $/\$ $/\$
141	17	simp3d 1002	. . 3 $/\$
142		xrleloe 11142	. . . 4 $/\$ $\/$
143	6, 12, 142	syl2anc 661	. . 3 $/\$ $\/$
144	141, 143	mpbid 210	. 2 $/\$ $\/$
145	129, 140, 144	mpjaodan 784	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

wrex 2737

cin 3348

wss 3349

csn 3898 class class class wbr 4313

cmpt 4371

cdm 4861

wf 5435

cfv 5439 (class class class)co 6112

cc 9301

cr 9302

cc0 9303

cpnf 9436

cmnf 9437

cxr 9438

clt 9439

cle 9440

cneg 9617

cn 10343

cicc 11324

ccncf 20474

covol 20968

cvol 20969

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4424 ax-sep 4434 ax-nul 4442 ax-pow 4491 ax-pr 4552 ax-un 6393 ax-inf2 7868 ax-cc 8625 ax-cnex 9359 ax-resscn 9360 ax-1cn 9361 ax-icn 9362 ax-addcl 9363 ax-addrcl 9364 ax-mulcl 9365 ax-mulrcl 9366 ax-mulcom 9367 ax-addass 9368 ax-mulass 9369 ax-distr 9370 ax-i2m1 9371 ax-1ne0 9372 ax-1rid 9373 ax-rnegex 9374 ax-rrecex 9375 ax-cnre 9376 ax-pre-lttri 9377 ax-pre-lttrn 9378 ax-pre-ltadd 9379 ax-pre-mulgt0 9380 ax-pre-sup 9381

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 2995 df-sbc 3208 df-csb 3310 df-dif 3352 df-un 3354 df-in 3356 df-ss 3363 df-pss 3365 df-nul 3659 df-if 3813 df-pw 3883 df-sn 3899 df-pr 3901 df-tp 3903 df-op 3905 df-uni 4113 df-int 4150 df-iun 4194 df-disj 4284 df-br 4314 df-opab 4372 df-mpt 4373 df-tr 4407 df-eprel 4653 df-id 4657 df-po 4662 df-so 4663 df-fr 4700 df-se 4701 df-we 4702 df-ord 4743 df-on 4744 df-lim 4745 df-suc 4746 df-xp 4867 df-rel 4868 df-cnv 4869 df-co 4870 df-dm 4871 df-rn 4872 df-res 4873 df-ima 4874 df-iota 5402 df-fun 5441 df-fn 5442 df-f 5443 df-f1 5444 df-fo 5445 df-f1o 5446 df-fv 5447 df-isom 5448 df-riota 6073 df-ov 6115 df-oprab 6116 df-mpt2 6117 df-of 6341 df-om 6498 df-1st 6598 df-2nd 6599 df-recs 6853 df-rdg 6887 df-1o 6941 df-2o 6942 df-oadd 6945 df-er 7122 df-map 7237 df-pm 7238 df-en 7332 df-dom 7333 df-sdom 7334 df-fin 7335 df-fi 7682 df-sup 7712 df-oi 7745 df-card 8130 df-cda 8358 df-pnf 9441 df-mnf 9442 df-xr 9443 df-ltxr 9444 df-le 9445 df-sub 9618 df-neg 9619 df-div 10015 df-nn 10344 df-2 10401 df-3 10402 df-n0 10601 df-z 10668 df-uz 10883 df-q 10975 df-rp 11013 df-xneg 11110 df-xadd 11111 df-xmul 11112 df-ioo 11325 df-ico 11327 df-icc 11328 df-fz 11459 df-fzo 11570 df-fl 11663 df-seq 11828 df-exp 11887 df-hash 12125 df-cj 12609 df-re 12610 df-im 12611 df-sqr 12745 df-abs 12746 df-clim 12987 df-rlim 12988 df-sum 13185 df-rest 14382 df-topgen 14403 df-psmet 17831 df-xmet 17832 df-met 17833 df-bl 17834 df-mopn 17835 df-top 18525 df-bases 18527 df-topon 18528 df-cmp 19012 df-cncf 20476 df-ovol 20970 df-vol 20971

This theorem is referenced by: itg2const2 21241

W3C validator