volivth - Metamath Proof Explorer

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

Theorem volivth 22565

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 760	. . . 4 $/\$ $/\$
2		mnfxr 11414	. . . . . 6
3	2	a1i 11	. . . . 5 $/\$ $/\$
4		iccssxr 11717	. . . . . . 7
5		simpr 463	. . . . . . 7 $/\$
6	4, 5	sseldi 3430	. . . . . 6 $/\$
7	6	adantr 467	. . . . 5 $/\$ $/\$
8		iccssxr 11717	. . . . . . . 8
9		volf 22483	. . . . . . . . 9
10	9	ffvelrni 6021	. . . . . . . 8
11	8, 10	sseldi 3430	. . . . . . 7
12	11	adantr 467	. . . . . 6 $/\$
13	12	adantr 467	. . . . 5 $/\$ $/\$
14		0xr 9687	. . . . . . . . . 10
15		elicc1 11680	. . . . . . . . . 10 $/\$ $/\$ $/\$
16	14, 12, 15	sylancr 669	. . . . . . . . 9 $/\$ $/\$ $/\$
17	5, 16	mpbid 214	. . . . . . . 8 $/\$ $/\$ $/\$
18	17	simp2d 1021	. . . . . . 7 $/\$
19	18	adantr 467	. . . . . 6 $/\$ $/\$
20		mnflt0 11427	. . . . . . . 8
21		xrltletr 11454	. . . . . . . 8 $/\$ $/\$ $/\$
22	20, 21	mpani 682	. . . . . . 7 $/\$ $/\$
23	2, 14, 22	mp3an12 1354	. . . . . 6
24	7, 19, 23	sylc 62	. . . . 5 $/\$ $/\$
25		simpr 463	. . . . 5 $/\$ $/\$
26		xrre2 11465	. . . . 5 $/\$ $/\$ $/\$ $/\$
27	3, 7, 13, 24, 25, 26	syl32anc 1276	. . . 4 $/\$ $/\$
28		volsup2 22563	. . . 4 $/\$ $/\$
29	1, 27, 25, 28	syl3anc 1268	. . 3 $/\$ $/\$
30		nnre 10616	. . . . . . 7
31	30	ad2antrl 734	. . . . . 6 $/\$ $/\$ $/\$ $/\$
32	31	renegcld 10046	. . . . 5 $/\$ $/\$ $/\$ $/\$
33	27	adantr 467	. . . . 5 $/\$ $/\$ $/\$ $/\$
34		0red 9644	. . . . . 6 $/\$ $/\$ $/\$ $/\$
35		nngt0 10638	. . . . . . . 8
36	35	ad2antrl 734	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
37	31	lt0neg2d 10184	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
38	36, 37	mpbid 214	. . . . . 6 $/\$ $/\$ $/\$ $/\$
39	32, 34, 31, 38, 36	lttrd 9796	. . . . 5 $/\$ $/\$ $/\$ $/\$
40		iccssre 11716	. . . . . 6 $/\$
41	32, 31, 40	syl2anc 667	. . . . 5 $/\$ $/\$ $/\$ $/\$
42		ax-resscn 9596	. . . . . . 7
43		ssid 3451	. . . . . . 7
44		cncfss 21931	. . . . . . 7 $/\$
45	42, 43, 44	mp2an 678	. . . . . 6
46	1	adantr 467	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
47		eqid 2451	. . . . . . . 8
48	47	volcn 22564	. . . . . . 7 $/\$
49	46, 32, 48	syl2anc 667	. . . . . 6 $/\$ $/\$ $/\$ $/\$
50	45, 49	sseldi 3430	. . . . 5 $/\$ $/\$ $/\$ $/\$
51	41	sselda 3432	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
52		cncff 21925	. . . . . . . 8
53	49, 52	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
54	53	ffvelrnda 6022	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	syldan 473	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
56		oveq2 6298	. . . . . . . . . . . 12
57	56	ineq2d 3634	. . . . . . . . . . 11
58	57	fveq2d 5869	. . . . . . . . . 10
59		fvex 5875	. . . . . . . . . 10
60	58, 47, 59	fvmpt 5948	. . . . . . . . 9
61	32, 60	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
62		inss2 3653	. . . . . . . . . . . 12
63	32	rexrd 9690	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64		iccid 11681	. . . . . . . . . . . . 13
65	63, 64	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
66	62, 65	syl5sseq 3480	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
67	32	snssd 4117	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
68	66, 67	sstrd 3442	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
69		ovolsn 22448	. . . . . . . . . . . 12
70	32, 69	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
71		ovolssnul 22440	. . . . . . . . . . 11 $/\$ $/\$
72	66, 67, 70, 71	syl3anc 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73		nulmbl 22489	. . . . . . . . . 10 $/\$
74	68, 72, 73	syl2anc 667	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
75		mblvol 22484	. . . . . . . . 9
76	74, 75	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
77	61, 76, 72	3eqtrd 2489	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
78	19	adantr 467	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
79	77, 78	eqbrtrd 4423	. . . . . 6 $/\$ $/\$ $/\$ $/\$
80		simprr 766	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	7	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
82		iccmbl 22519	. . . . . . . . . . . 12 $/\$
83	32, 31, 82	syl2anc 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
84		inmbl 22495	. . . . . . . . . . 11 $/\$
85	46, 83, 84	syl2anc 667	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
86	9	ffvelrni 6021	. . . . . . . . . . 11
87	8, 86	sseldi 3430	. . . . . . . . . 10
88	85, 87	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
89		xrltle 11448	. . . . . . . . 9 $/\$
90	81, 88, 89	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
91	80, 90	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
92		oveq2 6298	. . . . . . . . . . 11
93	92	ineq2d 3634	. . . . . . . . . 10
94	93	fveq2d 5869	. . . . . . . . 9
95		fvex 5875	. . . . . . . . 9
96	94, 47, 95	fvmpt 5948	. . . . . . . 8
97	31, 96	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
98	91, 97	breqtrrd 4429	. . . . . 6 $/\$ $/\$ $/\$ $/\$
99	79, 98	jca 535	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
100	32, 31, 33, 39, 41, 50, 55, 99	ivthle 22407	. . . 4 $/\$ $/\$ $/\$ $/\$
101	41	sselda 3432	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
102		oveq2 6298	. . . . . . . . . . 11
103	102	ineq2d 3634	. . . . . . . . . 10
104	103	fveq2d 5869	. . . . . . . . 9
105		fvex 5875	. . . . . . . . 9
106	104, 47, 105	fvmpt 5948	. . . . . . . 8
107	101, 106	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
108	107	eqeq1d 2453	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
109	46	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	32	adantr 467	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111	101	adantrr 723	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112		iccmbl 22519	. . . . . . . . . 10 $/\$
113	110, 111, 112	syl2anc 667	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114		inmbl 22495	. . . . . . . . 9 $/\$
115	109, 113, 114	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		inss1 3652	. . . . . . . . 9
117	116	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118		simprr 766	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119		sseq1 3453	. . . . . . . . . 10
120		fveq2 5865	. . . . . . . . . . 11
121	120	eqeq1d 2453	. . . . . . . . . 10
122	119, 121	anbi12d 717	. . . . . . . . 9 $/\$ $/\$
123	122	rspcev 3150	. . . . . . . 8 $/\$ $/\$ $/\$
124	115, 117, 118, 123	syl12anc 1266	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125	124	expr 620	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	108, 125	sylbid 219	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	126	rexlimdva 2879	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
128	100, 127	mpd 15	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
129	29, 128	rexlimddv 2883	. 2 $/\$ $/\$ $/\$
130		simpll 760	. . 3 $/\$ $/\$
131		ssid 3451	. . . 4
132	131	a1i 11	. . 3 $/\$ $/\$
133		simpr 463	. . . 4 $/\$ $/\$
134	133	eqcomd 2457	. . 3 $/\$ $/\$
135		sseq1 3453	. . . . 5
136		fveq2 5865	. . . . . 6
137	136	eqeq1d 2453	. . . . 5
138	135, 137	anbi12d 717	. . . 4 $/\$ $/\$
139	138	rspcev 3150	. . 3 $/\$ $/\$ $/\$
140	130, 132, 134, 139	syl12anc 1266	. 2 $/\$ $/\$ $/\$
141	17	simp3d 1022	. . 3 $/\$
142		xrleloe 11443	. . . 4 $/\$ $\/$
143	6, 12, 142	syl2anc 667	. . 3 $/\$ $\/$
144	141, 143	mpbid 214	. 2 $/\$ $\/$
145	129, 140, 144	mpjaodan 795	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wrex 2738

cin 3403

wss 3404

csn 3968 class class class wbr 4402

cmpt 4461

cdm 4834

wf 5578

cfv 5582 (class class class)co 6290

cc 9537

cr 9538

cc0 9539

cpnf 9672

cmnf 9673

cxr 9674

clt 9675

cle 9676

cneg 9861

cn 10609

cicc 11638

ccncf 21908

covol 22413

cvol 22415

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cc 8865 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-disj 4374 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12028 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13552 df-rlim 13553 df-sum 13753 df-rest 15321 df-topgen 15342 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-top 19921 df-bases 19922 df-topon 19923 df-cmp 20402 df-cncf 21910 df-ovol 22416 df-vol 22418

This theorem is referenced by: itg2const2 22699

W3C validator