volivth - Metamath Proof Explorer

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

Theorem volivth 21779

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 11323	. . . . . 6
3	2	a1i 11	. . . . 5 $/\$ $/\$
4		iccssxr 11607	. . . . . . 7
5		simpr 461	. . . . . . 7 $/\$
6	4, 5	sseldi 3502	. . . . . 6 $/\$
7	6	adantr 465	. . . . 5 $/\$ $/\$
8		iccssxr 11607	. . . . . . . 8
9		volf 21703	. . . . . . . . 9
10	9	ffvelrni 6020	. . . . . . . 8
11	8, 10	sseldi 3502	. . . . . . 7
12	11	adantr 465	. . . . . 6 $/\$
13	12	adantr 465	. . . . 5 $/\$ $/\$
14		0xr 9640	. . . . . . . . . 10
15		elicc1 11573	. . . . . . . . . 10 $/\$ $/\$ $/\$
16	14, 12, 15	sylancr 663	. . . . . . . . 9 $/\$ $/\$ $/\$
17	5, 16	mpbid 210	. . . . . . . 8 $/\$ $/\$ $/\$
18	17	simp2d 1009	. . . . . . 7 $/\$
19	18	adantr 465	. . . . . 6 $/\$ $/\$
20		mnflt0 11334	. . . . . . . 8
21		xrltletr 11360	. . . . . . . 8 $/\$ $/\$ $/\$
22	20, 21	mpani 676	. . . . . . 7 $/\$ $/\$
23	2, 14, 22	mp3an12 1314	. . . . . 6
24	7, 19, 23	sylc 60	. . . . 5 $/\$ $/\$
25		simpr 461	. . . . 5 $/\$ $/\$
26		xrre2 11371	. . . . 5 $/\$ $/\$ $/\$ $/\$
27	3, 7, 13, 24, 25, 26	syl32anc 1236	. . . 4 $/\$ $/\$
28		volsup2 21777	. . . 4 $/\$ $/\$
29	1, 27, 25, 28	syl3anc 1228	. . 3 $/\$ $/\$
30		nnre 10543	. . . . . . 7
31	30	ad2antrl 727	. . . . . 6 $/\$ $/\$ $/\$ $/\$
32	31	renegcld 9986	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	27	adantr 465	. . . . 5 $/\$ $/\$ $/\$ $/\$
34		0red 9597	. . . . . 6 $/\$ $/\$ $/\$ $/\$
35		nngt0 10565	. . . . . . . 8
36	35	ad2antrl 727	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
37	31	lt0neg2d 10123	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
38	36, 37	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$ $/\$
39	32, 34, 31, 38, 36	lttrd 9742	. . . . 5 $/\$ $/\$ $/\$ $/\$
40		iccssre 11606	. . . . . 6 $/\$
41	32, 31, 40	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $/\$
42		ax-resscn 9549	. . . . . . 7
43		ssid 3523	. . . . . . 7
44		cncfss 21166	. . . . . . 7 $/\$
45	42, 43, 44	mp2an 672	. . . . . 6
46	1	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
47		eqid 2467	. . . . . . . 8
48	47	volcn 21778	. . . . . . 7 $/\$
49	46, 32, 48	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$ $/\$
50	45, 49	sseldi 3502	. . . . 5 $/\$ $/\$ $/\$ $/\$
51	41	sselda 3504	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
52		cncff 21160	. . . . . . . 8
53	49, 52	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
54	53	ffvelrnda 6021	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	syldan 470	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
56		oveq2 6292	. . . . . . . . . . . 12
57	56	ineq2d 3700	. . . . . . . . . . 11
58	57	fveq2d 5870	. . . . . . . . . 10
59		fvex 5876	. . . . . . . . . 10
60	58, 47, 59	fvmpt 5950	. . . . . . . . 9
61	32, 60	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
62		inss2 3719	. . . . . . . . . . . 12
63	32	rexrd 9643	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64		iccid 11574	. . . . . . . . . . . . 13
65	63, 64	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
66	62, 65	syl5sseq 3552	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
67	32	snssd 4172	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
68	66, 67	sstrd 3514	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
69		ovolsn 21669	. . . . . . . . . . . 12
70	32, 69	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
71		ovolssnul 21661	. . . . . . . . . . 11 $/\$ $/\$
72	66, 67, 70, 71	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73		nulmbl 21709	. . . . . . . . . 10 $/\$
74	68, 72, 73	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
75		mblvol 21704	. . . . . . . . 9
76	74, 75	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
77	61, 76, 72	3eqtrd 2512	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
78	19	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
79	77, 78	eqbrtrd 4467	. . . . . 6 $/\$ $/\$ $/\$ $/\$
80		simprr 756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	7	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
82		iccmbl 21739	. . . . . . . . . . . 12 $/\$
83	32, 31, 82	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
84		inmbl 21715	. . . . . . . . . . 11 $/\$
85	46, 83, 84	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
86	9	ffvelrni 6020	. . . . . . . . . . 11
87	8, 86	sseldi 3502	. . . . . . . . . 10
88	85, 87	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
89		xrltle 11355	. . . . . . . . 9 $/\$
90	81, 88, 89	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
91	80, 90	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
92		oveq2 6292	. . . . . . . . . . 11
93	92	ineq2d 3700	. . . . . . . . . 10
94	93	fveq2d 5870	. . . . . . . . 9
95		fvex 5876	. . . . . . . . 9
96	94, 47, 95	fvmpt 5950	. . . . . . . 8
97	31, 96	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
98	91, 97	breqtrrd 4473	. . . . . 6 $/\$ $/\$ $/\$ $/\$
99	79, 98	jca 532	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
100	32, 31, 33, 39, 41, 50, 55, 99	ivthle 21631	. . . 4 $/\$ $/\$ $/\$ $/\$
101	41	sselda 3504	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
102		oveq2 6292	. . . . . . . . . . 11
103	102	ineq2d 3700	. . . . . . . . . 10
104	103	fveq2d 5870	. . . . . . . . 9
105		fvex 5876	. . . . . . . . 9
106	104, 47, 105	fvmpt 5950	. . . . . . . 8
107	101, 106	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
108	107	eqeq1d 2469	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
109	46	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	32	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111	101	adantrr 716	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112		iccmbl 21739	. . . . . . . . . 10 $/\$
113	110, 111, 112	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		inmbl 21715	. . . . . . . . 9 $/\$
115	109, 113, 114	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		inss1 3718	. . . . . . . . 9
117	116	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118		simprr 756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		sseq1 3525	. . . . . . . . . 10
120		fveq2 5866	. . . . . . . . . . 11
121	120	eqeq1d 2469	. . . . . . . . . 10
122	119, 121	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
123	122	rspcev 3214	. . . . . . . 8 $/\$ $/\$ $/\$
124	115, 117, 118, 123	syl12anc 1226	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	124	expr 615	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	108, 125	sylbid 215	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	126	rexlimdva 2955	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
128	100, 127	mpd 15	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
129	29, 128	rexlimddv 2959	. 2 $/\$ $/\$ $/\$
130		simpll 753	. . 3 $/\$ $/\$
131		ssid 3523	. . . 4
132	131	a1i 11	. . 3 $/\$ $/\$
133		simpr 461	. . . 4 $/\$ $/\$
134	133	eqcomd 2475	. . 3 $/\$ $/\$
135		sseq1 3525	. . . . 5
136		fveq2 5866	. . . . . 6
137	136	eqeq1d 2469	. . . . 5
138	135, 137	anbi12d 710	. . . 4 $/\$ $/\$
139	138	rspcev 3214	. . 3 $/\$ $/\$ $/\$
140	130, 132, 134, 139	syl12anc 1226	. 2 $/\$ $/\$ $/\$
141	17	simp3d 1010	. . 3 $/\$
142		xrleloe 11350	. . . 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 973

wceq 1379

wcel 1767

wrex 2815

cin 3475

wss 3476

csn 4027 class class class wbr 4447

cmpt 4505

cdm 4999

wf 5584

cfv 5588 (class class class)co 6284

cc 9490

cr 9491

cc0 9492

cpnf 9625

cmnf 9626

cxr 9627

clt 9628

cle 9629

cneg 9806

cn 10536

cicc 11532

ccncf 21143

covol 21637

cvol 21638

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-cc 8815 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-of 6524 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-fi 7871 df-sup 7901 df-oi 7935 df-card 8320 df-cda 8548 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-n0 10796 df-z 10865 df-uz 11083 df-q 11183 df-rp 11221 df-xneg 11318 df-xadd 11319 df-xmul 11320 df-ioo 11533 df-ico 11535 df-icc 11536 df-fz 11673 df-fzo 11793 df-fl 11897 df-seq 12076 df-exp 12135 df-hash 12374 df-cj 12895 df-re 12896 df-im 12897 df-sqrt 13031 df-abs 13032 df-clim 13274 df-rlim 13275 df-sum 13472 df-rest 14678 df-topgen 14699 df-psmet 18210 df-xmet 18211 df-met 18212 df-bl 18213 df-mopn 18214 df-top 19194 df-bases 19196 df-topon 19197 df-cmp 19681 df-cncf 21145 df-ovol 21639 df-vol 21640

This theorem is referenced by: itg2const2 21911

W3C validator