ovncvrrp - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ovncvrrp		Structured version Visualization version Unicode version

Theorem ovncvrrp 38504

Description: The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

**Hypotheses**
Ref	Expression
ovncvrrp.x
ovncvrrp.n0
ovncvrrp.a
ovncvrrp.e
ovncvrrp.c
ovncvrrp.l
ovncvrrp.d	Σ^{^} voln^*

**Assertion**
Ref	Expression
ovncvrrp

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem ovncvrrp Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovncvrrp.x	. . . 4
2		ovncvrrp.n0	. . . 4
3		ovncvrrp.a	. . . 4
4		ovncvrrp.e	. . . 4
5		eqid 2471	. . . 4 $/\$ Σ^{^} $/\$ Σ^{^}
6	1, 2, 3, 4, 5	ovnlerp 38502	. . 3 $/\$ Σ^{^} voln^*
7		simp1 1030	. . . . . 6 $/\$ $/\$ Σ^{^} $/\$ voln^*
8		simp3 1032	. . . . . 6 $/\$ $/\$ Σ^{^} $/\$ voln^* voln^*
9		rabid 2953	. . . . . . . . . 10 $/\$ Σ^{^} $/\$ $/\$ Σ^{^}
10	9	biimpi 199	. . . . . . . . 9 $/\$ Σ^{^} $/\$ $/\$ Σ^{^}
11	10	simprd 470	. . . . . . . 8 $/\$ Σ^{^} $/\$ Σ^{^}
12	11	adantr 472	. . . . . . 7 $/\$ Σ^{^} $/\$ voln^* $/\$ Σ^{^}
13	12	3adant1 1048	. . . . . 6 $/\$ $/\$ Σ^{^} $/\$ voln^* $/\$ Σ^{^}
14		nfv 1769	. . . . . . . 8 $/\$ voln^*
15		nfe1 1935	. . . . . . . 8 $/\$ Σ^{^} voln^*
16		simp1l 1054	. . . . . . . . . . . 12 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^}
17		simp2 1031	. . . . . . . . . . . 12 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^}
18		simp3l 1058	. . . . . . . . . . . 12 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^}
19		id 22	. . . . . . . . . . . . . . 15 $/\$ $/\$
20		fveq1 5878	. . . . . . . . . . . . . . . . . . . . 21
21	20	coeq2d 5002	. . . . . . . . . . . . . . . . . . . 20
22	21	fveq1d 5881	. . . . . . . . . . . . . . . . . . 19
23	22	ixpeq2dv 7556	. . . . . . . . . . . . . . . . . 18
24	23	iuneq2d 4296	. . . . . . . . . . . . . . . . 17
25	24	sseq2d 3446	. . . . . . . . . . . . . . . 16
26	25	elrab 3184	. . . . . . . . . . . . . . 15 $/\$
27	19, 26	sylibr 217	. . . . . . . . . . . . . 14 $/\$
28	27	3adant1 1048	. . . . . . . . . . . . 13 $/\$ $/\$
29		ovncvrrp.c	. . . . . . . . . . . . . . . . 17
30	29	a1i 11	. . . . . . . . . . . . . . . 16
31		sseq1 3439	. . . . . . . . . . . . . . . . . 18
32	31	rabbidv 3022	. . . . . . . . . . . . . . . . 17
33	32	adantl 473	. . . . . . . . . . . . . . . 16 $/\$
34		ovex 6336	. . . . . . . . . . . . . . . . . . . 20
35	34	a1i 11	. . . . . . . . . . . . . . . . . . 19
36	35, 3	ssexd 4543	. . . . . . . . . . . . . . . . . 18
37		elpwg 3950	. . . . . . . . . . . . . . . . . 18
38	36, 37	syl 17	. . . . . . . . . . . . . . . . 17
39	3, 38	mpbird 240	. . . . . . . . . . . . . . . 16
40		ovex 6336	. . . . . . . . . . . . . . . . . 18
41	40	rabex 4550	. . . . . . . . . . . . . . . . 17
42	41	a1i 11	. . . . . . . . . . . . . . . 16
43	30, 33, 39, 42	fvmptd 5969	. . . . . . . . . . . . . . 15
44	43	eqcomd 2477	. . . . . . . . . . . . . 14
45	44	3ad2ant1 1051	. . . . . . . . . . . . 13 $/\$ $/\$
46	28, 45	eleqtrd 2551	. . . . . . . . . . . 12 $/\$ $/\$
47	16, 17, 18, 46	syl3anc 1292	. . . . . . . . . . 11 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^}
48		ovncvrrp.l	. . . . . . . . . . . . . . . . . . . . 21
49	48	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
50		coeq2 4998	. . . . . . . . . . . . . . . . . . . . . . . 24
51	50	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . . . 23
52	51	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22
53	52	prodeq2ad 37769	. . . . . . . . . . . . . . . . . . . . 21
54	53	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
55		elmapi 7511	. . . . . . . . . . . . . . . . . . . . . 22
56	55	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$
57		simpr 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58	56, 57	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . 20 $/\$
59		prodex 14038	. . . . . . . . . . . . . . . . . . . . 21
60	59	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
61	49, 54, 58, 60	fvmptd 5969	. . . . . . . . . . . . . . . . . . 19 $/\$
62	61	mpteq2dva 4482	. . . . . . . . . . . . . . . . . 18
63	62	fveq2d 5883	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
64	63	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ Σ^{^} Σ^{^} Σ^{^}
65		id 22	. . . . . . . . . . . . . . . . . 18 Σ^{^} Σ^{^}
66	65	eqcomd 2477	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
67	66	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ Σ^{^} Σ^{^}
68	64, 67	eqtrd 2505	. . . . . . . . . . . . . . 15 $/\$ Σ^{^} Σ^{^}
69	68	3adant1 1048	. . . . . . . . . . . . . 14 voln^* $/\$ $/\$ Σ^{^} Σ^{^}
70		simp1 1030	. . . . . . . . . . . . . 14 voln^* $/\$ $/\$ Σ^{^} voln^*
71	69, 70	eqbrtrd 4416	. . . . . . . . . . . . 13 voln^* $/\$ $/\$ Σ^{^} Σ^{^} voln^*
72	71	3adant1l 1284	. . . . . . . . . . . 12 $/\$ voln^* $/\$ $/\$ Σ^{^} Σ^{^} voln^*
73	72	3adant3l 1288	. . . . . . . . . . 11 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^} Σ^{^} voln^*
74	47, 73	jca 541	. . . . . . . . . 10 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^} $/\$ Σ^{^} voln^*
75		19.8a 1955	. . . . . . . . . 10 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
76	74, 75	syl 17	. . . . . . . . 9 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^} $/\$ Σ^{^} voln^*
77	76	3exp 1230	. . . . . . . 8 $/\$ voln^* $/\$ Σ^{^} $/\$ Σ^{^} voln^*
78	14, 15, 77	rexlimd 2866	. . . . . . 7 $/\$ voln^* $/\$ Σ^{^} $/\$ Σ^{^} voln^*
79	78	imp 436	. . . . . 6 $/\$ voln^* $/\$ $/\$ Σ^{^} $/\$ Σ^{^} voln^*
80	7, 8, 13, 79	syl21anc 1291	. . . . 5 $/\$ $/\$ Σ^{^} $/\$ voln^* $/\$ Σ^{^} voln^*
81	80	3exp 1230	. . . 4 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
82	81	rexlimdv 2870	. . 3 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
83	6, 82	mpd 15	. 2 $/\$ Σ^{^} voln^*
84		rabid 2953	. . . . . . . 8 Σ^{^} voln^* $/\$ Σ^{^} voln^*
85	84	bicomi 207	. . . . . . 7 $/\$ Σ^{^} voln^* Σ^{^} voln^*
86	85	biimpi 199	. . . . . 6 $/\$ Σ^{^} voln^* Σ^{^} voln^*
87	86	adantl 473	. . . . 5 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
88		ovncvrrp.d	. . . . . . . . . 10 Σ^{^} voln^*
89		nfcv 2612	. . . . . . . . . . 11 Σ^{^} voln^*
90		nfcv 2612	. . . . . . . . . . . 12
91		nfv 1769	. . . . . . . . . . . . 13 Σ^{^} voln^*
92		nfmpt1 4485	. . . . . . . . . . . . . . 15
93	29, 92	nfcxfr 2610	. . . . . . . . . . . . . 14
94		nfcv 2612	. . . . . . . . . . . . . 14
95	93, 94	nffv 5886	. . . . . . . . . . . . 13
96	91, 95	nfrab 2958	. . . . . . . . . . . 12 Σ^{^} voln^*
97	90, 96	nfmpt 4484	. . . . . . . . . . 11 Σ^{^} voln^*
98		fveq2 5879	. . . . . . . . . . . . . . 15
99	98	eleq2d 2534	. . . . . . . . . . . . . 14
100		fveq2 5879	. . . . . . . . . . . . . . . 16 voln^* voln^*
101	100	oveq1d 6323	. . . . . . . . . . . . . . 15 voln^* voln^*
102	101	breq2d 4407	. . . . . . . . . . . . . 14 Σ^{^} voln^* Σ^{^} voln^*
103	99, 102	anbi12d 725	. . . . . . . . . . . . 13 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
104	103	rabbidva2 3020	. . . . . . . . . . . 12 Σ^{^} voln^* Σ^{^} voln^*
105	104	mpteq2dv 4483	. . . . . . . . . . 11 Σ^{^} voln^* Σ^{^} voln^*
106	89, 97, 105	cbvmpt 4487	. . . . . . . . . 10 Σ^{^} voln^* Σ^{^} voln^*
107	88, 106	eqtri 2493	. . . . . . . . 9 Σ^{^} voln^*
108	107	a1i 11	. . . . . . . 8 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
109		fveq2 5879	. . . . . . . . . . . . 13
110	109	eleq2d 2534	. . . . . . . . . . . 12
111		fveq2 5879	. . . . . . . . . . . . . 14 voln^* voln^*
112	111	oveq1d 6323	. . . . . . . . . . . . 13 voln^* voln^*
113	112	breq2d 4407	. . . . . . . . . . . 12 Σ^{^} voln^* Σ^{^} voln^*
114	110, 113	anbi12d 725	. . . . . . . . . . 11 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
115	114	rabbidva2 3020	. . . . . . . . . 10 Σ^{^} voln^* Σ^{^} voln^*
116	115	mpteq2dv 4483	. . . . . . . . 9 Σ^{^} voln^* Σ^{^} voln^*
117	116	adantl 473	. . . . . . . 8 $/\$ $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^* Σ^{^} voln^*
118	39	adantr 472	. . . . . . . 8 $/\$ $/\$ Σ^{^} voln^*
119		rpex 37656	. . . . . . . . . 10
120	119	mptex 6152	. . . . . . . . 9 Σ^{^} voln^*
121	120	a1i 11	. . . . . . . 8 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
122	108, 117, 118, 121	fvmptd 5969	. . . . . . 7 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
123		oveq2 6316	. . . . . . . . . 10 voln^* voln^*
124	123	breq2d 4407	. . . . . . . . 9 Σ^{^} voln^* Σ^{^} voln^*
125	124	rabbidv 3022	. . . . . . . 8 Σ^{^} voln^* Σ^{^} voln^*
126	125	adantl 473	. . . . . . 7 $/\$ $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^* Σ^{^} voln^*
127	4	adantr 472	. . . . . . 7 $/\$ $/\$ Σ^{^} voln^*
128		fvex 5889	. . . . . . . . 9
129	128	rabex 4550	. . . . . . . 8 Σ^{^} voln^*
130	129	a1i 11	. . . . . . 7 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
131	122, 126, 127, 130	fvmptd 5969	. . . . . 6 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
132	131	eqcomd 2477	. . . . 5 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
133	87, 132	eleqtrd 2551	. . . 4 $/\$ $/\$ Σ^{^} voln^*
134	133	ex 441	. . 3 $/\$ Σ^{^} voln^*
135	134	eximdv 1772	. 2 $/\$ Σ^{^} voln^*
136	83, 135	mpd 15	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wex 1671

wcel 1904

wne 2641

wrex 2757

crab 2760

cvv 3031

wss 3390

c0 3722

cpw 3942

ciun 4269 class class class wbr 4395

cmpt 4454

cxp 4837

ccom 4843

wf 5585

cfv 5589 (class class class)co 6308

cmap 7490

cixp 7540

cfn 7587

cr 9556

cxr 9692

cle 9694

cn 10631

crp 11325

cxad 11430

cico 11662

cprod 14036

cvol 22493 Σ^{^}csumge0 38318 voln^*covoln 38476

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-tpos 6991 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-rlim 13630 df-sum 13830 df-prod 14037 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-rest 15399 df-0g 15418 df-topgen 15420 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-grp 16751 df-minusg 16752 df-subg 16892 df-cmn 17510 df-abl 17511 df-mgp 17802 df-ur 17814 df-ring 17860 df-cring 17861 df-oppr 17929 df-dvdsr 17947 df-unit 17948 df-invr 17978 df-dvr 17989 df-drng 18055 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-cmp 20479 df-ovol 22494 df-vol 22496 df-sumge0 38319 df-ovoln 38477

This theorem is referenced by: ovnsubaddlem2 38511 hspmbllem3 38568

W3C validator