volivth - Metamath Proof Explorer

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

Theorem volivth 22142

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 11348	. . . . . 6
3	2	a1i 11	. . . . 5 $/\$ $/\$
4		iccssxr 11632	. . . . . . 7
5		simpr 461	. . . . . . 7 $/\$
6	4, 5	sseldi 3497	. . . . . 6 $/\$
7	6	adantr 465	. . . . 5 $/\$ $/\$
8		iccssxr 11632	. . . . . . . 8
9		volf 22066	. . . . . . . . 9
10	9	ffvelrni 6031	. . . . . . . 8
11	8, 10	sseldi 3497	. . . . . . 7
12	11	adantr 465	. . . . . 6 $/\$
13	12	adantr 465	. . . . 5 $/\$ $/\$
14		0xr 9657	. . . . . . . . . 10
15		elicc1 11598	. . . . . . . . . 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 11359	. . . . . . . 8
21		xrltletr 11385	. . . . . . . 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 11396	. . . . 5 $/\$ $/\$ $/\$ $/\$
27	3, 7, 13, 24, 25, 26	syl32anc 1236	. . . 4 $/\$ $/\$
28		volsup2 22140	. . . 4 $/\$ $/\$
29	1, 27, 25, 28	syl3anc 1228	. . 3 $/\$ $/\$
30		nnre 10563	. . . . . . 7
31	30	ad2antrl 727	. . . . . 6 $/\$ $/\$ $/\$ $/\$
32	31	renegcld 10007	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	27	adantr 465	. . . . 5 $/\$ $/\$ $/\$ $/\$
34		0red 9614	. . . . . 6 $/\$ $/\$ $/\$ $/\$
35		nngt0 10585	. . . . . . . 8
36	35	ad2antrl 727	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
37	31	lt0neg2d 10144	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
38	36, 37	mpbid 210	. . . . . 6 $/\$ $/\$ $/\$ $/\$
39	32, 34, 31, 38, 36	lttrd 9760	. . . . 5 $/\$ $/\$ $/\$ $/\$
40		iccssre 11631	. . . . . 6 $/\$
41	32, 31, 40	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $/\$
42		ax-resscn 9566	. . . . . . 7
43		ssid 3518	. . . . . . 7
44		cncfss 21529	. . . . . . 7 $/\$
45	42, 43, 44	mp2an 672	. . . . . 6
46	1	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
47		eqid 2457	. . . . . . . 8
48	47	volcn 22141	. . . . . . 7 $/\$
49	46, 32, 48	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$ $/\$
50	45, 49	sseldi 3497	. . . . 5 $/\$ $/\$ $/\$ $/\$
51	41	sselda 3499	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
52		cncff 21523	. . . . . . . 8
53	49, 52	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
54	53	ffvelrnda 6032	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	syldan 470	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
56		oveq2 6304	. . . . . . . . . . . 12
57	56	ineq2d 3696	. . . . . . . . . . 11
58	57	fveq2d 5876	. . . . . . . . . 10
59		fvex 5882	. . . . . . . . . 10
60	58, 47, 59	fvmpt 5956	. . . . . . . . 9
61	32, 60	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
62		inss2 3715	. . . . . . . . . . . 12
63	32	rexrd 9660	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64		iccid 11599	. . . . . . . . . . . . 13
65	63, 64	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
66	62, 65	syl5sseq 3547	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
67	32	snssd 4177	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
68	66, 67	sstrd 3509	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
69		ovolsn 22032	. . . . . . . . . . . 12
70	32, 69	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
71		ovolssnul 22024	. . . . . . . . . . 11 $/\$ $/\$
72	66, 67, 70, 71	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73		nulmbl 22072	. . . . . . . . . 10 $/\$
74	68, 72, 73	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
75		mblvol 22067	. . . . . . . . 9
76	74, 75	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
77	61, 76, 72	3eqtrd 2502	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
78	19	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
79	77, 78	eqbrtrd 4476	. . . . . 6 $/\$ $/\$ $/\$ $/\$
80		simprr 757	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	7	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
82		iccmbl 22102	. . . . . . . . . . . 12 $/\$
83	32, 31, 82	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
84		inmbl 22078	. . . . . . . . . . 11 $/\$
85	46, 83, 84	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
86	9	ffvelrni 6031	. . . . . . . . . . 11
87	8, 86	sseldi 3497	. . . . . . . . . 10
88	85, 87	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
89		xrltle 11380	. . . . . . . . 9 $/\$
90	81, 88, 89	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
91	80, 90	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
92		oveq2 6304	. . . . . . . . . . 11
93	92	ineq2d 3696	. . . . . . . . . 10
94	93	fveq2d 5876	. . . . . . . . 9
95		fvex 5882	. . . . . . . . 9
96	94, 47, 95	fvmpt 5956	. . . . . . . 8
97	31, 96	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
98	91, 97	breqtrrd 4482	. . . . . 6 $/\$ $/\$ $/\$ $/\$
99	79, 98	jca 532	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
100	32, 31, 33, 39, 41, 50, 55, 99	ivthle 21994	. . . 4 $/\$ $/\$ $/\$ $/\$
101	41	sselda 3499	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
102		oveq2 6304	. . . . . . . . . . 11
103	102	ineq2d 3696	. . . . . . . . . 10
104	103	fveq2d 5876	. . . . . . . . 9
105		fvex 5882	. . . . . . . . 9
106	104, 47, 105	fvmpt 5956	. . . . . . . 8
107	101, 106	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
108	107	eqeq1d 2459	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
109	46	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	32	adantr 465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111	101	adantrr 716	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112		iccmbl 22102	. . . . . . . . . 10 $/\$
113	110, 111, 112	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		inmbl 22078	. . . . . . . . 9 $/\$
115	109, 113, 114	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		inss1 3714	. . . . . . . . 9
117	116	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118		simprr 757	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		sseq1 3520	. . . . . . . . . 10
120		fveq2 5872	. . . . . . . . . . 11
121	120	eqeq1d 2459	. . . . . . . . . 10
122	119, 121	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
123	122	rspcev 3210	. . . . . . . 8 $/\$ $/\$ $/\$
124	115, 117, 118, 123	syl12anc 1226	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	124	expr 615	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	108, 125	sylbid 215	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	126	rexlimdva 2949	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
128	100, 127	mpd 15	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
129	29, 128	rexlimddv 2953	. 2 $/\$ $/\$ $/\$
130		simpll 753	. . 3 $/\$ $/\$
131		ssid 3518	. . . 4
132	131	a1i 11	. . 3 $/\$ $/\$
133		simpr 461	. . . 4 $/\$ $/\$
134	133	eqcomd 2465	. . 3 $/\$ $/\$
135		sseq1 3520	. . . . 5
136		fveq2 5872	. . . . . 6
137	136	eqeq1d 2459	. . . . 5
138	135, 137	anbi12d 710	. . . 4 $/\$ $/\$
139	138	rspcev 3210	. . 3 $/\$ $/\$ $/\$
140	130, 132, 134, 139	syl12anc 1226	. 2 $/\$ $/\$ $/\$
141	17	simp3d 1010	. . 3 $/\$
142		xrleloe 11375	. . . 4 $/\$ $\/$
143	6, 12, 142	syl2anc 661	. . 3 $/\$ $\/$
144	141, 143	mpbid 210	. 2 $/\$ $\/$
145	129, 140, 144	mpjaodan 786	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1395

wcel 1819

wrex 2808

cin 3470

wss 3471

csn 4032 class class class wbr 4456

cmpt 4515

cdm 5008

wf 5590

cfv 5594 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

cpnf 9642

cmnf 9643

cxr 9644

clt 9645

cle 9646

cneg 9825

cn 10556

cicc 11557

ccncf 21506

covol 22000

cvol 22001

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cc 8832 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fi 7889 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-ioo 11558 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11822 df-fl 11932 df-seq 12111 df-exp 12170 df-hash 12409 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-clim 13323 df-rlim 13324 df-sum 13521 df-rest 14840 df-topgen 14861 df-psmet 18538 df-xmet 18539 df-met 18540 df-bl 18541 df-mopn 18542 df-top 19526 df-bases 19528 df-topon 19529 df-cmp 20014 df-cncf 21508 df-ovol 22002 df-vol 22003

This theorem is referenced by: itg2const2 22274

W3C validator