ovncvrrp - Mathbox for Glauco Siliprandi

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

Theorem ovncvrrp 38290

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 2422	. . . 4 $/\$ Σ^{^} $/\$ Σ^{^}
6	1, 2, 3, 4, 5	ovnlerp 38288	. . 3 $/\$ Σ^{^} voln^*
7		simp1 1005	. . . . . 6 $/\$ $/\$ Σ^{^} $/\$ voln^*
8		simp3 1007	. . . . . 6 $/\$ $/\$ Σ^{^} $/\$ voln^* voln^*
9		rabid 3002	. . . . . . . . . 10 $/\$ Σ^{^} $/\$ $/\$ Σ^{^}
10	9	biimpi 197	. . . . . . . . 9 $/\$ Σ^{^} $/\$ $/\$ Σ^{^}
11	10	simprd 464	. . . . . . . 8 $/\$ Σ^{^} $/\$ Σ^{^}
12	11	adantr 466	. . . . . . 7 $/\$ Σ^{^} $/\$ voln^* $/\$ Σ^{^}
13	12	3adant1 1023	. . . . . 6 $/\$ $/\$ Σ^{^} $/\$ voln^* $/\$ Σ^{^}
14		nfv 1755	. . . . . . . 8 $/\$ voln^*
15		nfe1 1894	. . . . . . . 8 $/\$ Σ^{^} voln^*
16		simp1l 1029	. . . . . . . . . . . 12 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^}
17		simp2 1006	. . . . . . . . . . . 12 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^}
18		simp3l 1033	. . . . . . . . . . . 12 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^}
19		id 22	. . . . . . . . . . . . . . 15 $/\$ $/\$
20		fveq1 5880	. . . . . . . . . . . . . . . . . . . . 21
21	20	coeq2d 5016	. . . . . . . . . . . . . . . . . . . 20
22	21	fveq1d 5883	. . . . . . . . . . . . . . . . . . 19
23	22	ixpeq2dv 7549	. . . . . . . . . . . . . . . . . 18
24	23	iuneq2d 4326	. . . . . . . . . . . . . . . . 17
25	24	sseq2d 3492	. . . . . . . . . . . . . . . 16
26	25	elrab 3228	. . . . . . . . . . . . . . 15 $/\$
27	19, 26	sylibr 215	. . . . . . . . . . . . . 14 $/\$
28	27	3adant1 1023	. . . . . . . . . . . . 13 $/\$ $/\$
29		ovncvrrp.c	. . . . . . . . . . . . . . . . 17
30	29	a1i 11	. . . . . . . . . . . . . . . 16
31		sseq1 3485	. . . . . . . . . . . . . . . . . 18
32	31	rabbidv 3071	. . . . . . . . . . . . . . . . 17
33	32	adantl 467	. . . . . . . . . . . . . . . 16 $/\$
34		ovex 6333	. . . . . . . . . . . . . . . . . . . 20
35	34	a1i 11	. . . . . . . . . . . . . . . . . . 19
36	35, 3	ssexd 4571	. . . . . . . . . . . . . . . . . 18
37		elpwg 3989	. . . . . . . . . . . . . . . . . 18
38	36, 37	syl 17	. . . . . . . . . . . . . . . . 17
39	3, 38	mpbird 235	. . . . . . . . . . . . . . . 16
40		ovex 6333	. . . . . . . . . . . . . . . . . 18
41	40	rabex 4575	. . . . . . . . . . . . . . . . 17
42	41	a1i 11	. . . . . . . . . . . . . . . 16
43	30, 33, 39, 42	fvmptd 5970	. . . . . . . . . . . . . . 15
44	43	eqcomd 2430	. . . . . . . . . . . . . 14
45	44	3ad2ant1 1026	. . . . . . . . . . . . 13 $/\$ $/\$
46	28, 45	eleqtrd 2509	. . . . . . . . . . . 12 $/\$ $/\$
47	16, 17, 18, 46	syl3anc 1264	. . . . . . . . . . 11 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^}
48		ovncvrrp.l	. . . . . . . . . . . . . . . . . . . . 21
49	48	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
50		coeq2 5012	. . . . . . . . . . . . . . . . . . . . . . . 24
51	50	fveq1d 5883	. . . . . . . . . . . . . . . . . . . . . . 23
52	51	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . 22
53	52	prodeq2ad 37612	. . . . . . . . . . . . . . . . . . . . 21
54	53	adantl 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
55		elmapi 7504	. . . . . . . . . . . . . . . . . . . . . 22
56	55	adantr 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$
57		simpr 462	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58	56, 57	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . 20 $/\$
59		prodex 13960	. . . . . . . . . . . . . . . . . . . . 21
60	59	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
61	49, 54, 58, 60	fvmptd 5970	. . . . . . . . . . . . . . . . . . 19 $/\$
62	61	mpteq2dva 4510	. . . . . . . . . . . . . . . . . 18
63	62	fveq2d 5885	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
64	63	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ Σ^{^} Σ^{^} Σ^{^}
65		id 22	. . . . . . . . . . . . . . . . . 18 Σ^{^} Σ^{^}
66	65	eqcomd 2430	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
67	66	adantl 467	. . . . . . . . . . . . . . . 16 $/\$ Σ^{^} Σ^{^}
68	64, 67	eqtrd 2463	. . . . . . . . . . . . . . 15 $/\$ Σ^{^} Σ^{^}
69	68	3adant1 1023	. . . . . . . . . . . . . 14 voln^* $/\$ $/\$ Σ^{^} Σ^{^}
70		simp1 1005	. . . . . . . . . . . . . 14 voln^* $/\$ $/\$ Σ^{^} voln^*
71	69, 70	eqbrtrd 4444	. . . . . . . . . . . . 13 voln^* $/\$ $/\$ Σ^{^} Σ^{^} voln^*
72	71	3adant1l 1256	. . . . . . . . . . . 12 $/\$ voln^* $/\$ $/\$ Σ^{^} Σ^{^} voln^*
73	72	3adant3l 1260	. . . . . . . . . . 11 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^} Σ^{^} voln^*
74	47, 73	jca 534	. . . . . . . . . 10 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^} $/\$ Σ^{^} voln^*
75		19.8a 1912	. . . . . . . . . 10 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
76	74, 75	syl 17	. . . . . . . . 9 $/\$ voln^* $/\$ $/\$ $/\$ Σ^{^} $/\$ Σ^{^} voln^*
77	76	3exp 1204	. . . . . . . 8 $/\$ voln^* $/\$ Σ^{^} $/\$ Σ^{^} voln^*
78	14, 15, 77	rexlimd 2906	. . . . . . 7 $/\$ voln^* $/\$ Σ^{^} $/\$ Σ^{^} voln^*
79	78	imp 430	. . . . . 6 $/\$ voln^* $/\$ $/\$ Σ^{^} $/\$ Σ^{^} voln^*
80	7, 8, 13, 79	syl21anc 1263	. . . . 5 $/\$ $/\$ Σ^{^} $/\$ voln^* $/\$ Σ^{^} voln^*
81	80	3exp 1204	. . . 4 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
82	81	rexlimdv 2912	. . 3 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
83	6, 82	mpd 15	. 2 $/\$ Σ^{^} voln^*
84		rabid 3002	. . . . . . . 8 Σ^{^} voln^* $/\$ Σ^{^} voln^*
85	84	bicomi 205	. . . . . . 7 $/\$ Σ^{^} voln^* Σ^{^} voln^*
86	85	biimpi 197	. . . . . 6 $/\$ Σ^{^} voln^* Σ^{^} voln^*
87	86	adantl 467	. . . . 5 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
88		ovncvrrp.d	. . . . . . . . . 10 Σ^{^} voln^*
89		nfcv 2580	. . . . . . . . . . 11 Σ^{^} voln^*
90		nfcv 2580	. . . . . . . . . . . 12
91		nfv 1755	. . . . . . . . . . . . 13 Σ^{^} voln^*
92		nfmpt1 4513	. . . . . . . . . . . . . . 15
93	29, 92	nfcxfr 2578	. . . . . . . . . . . . . 14
94		nfcv 2580	. . . . . . . . . . . . . 14
95	93, 94	nffv 5888	. . . . . . . . . . . . 13
96	91, 95	nfrab 3007	. . . . . . . . . . . 12 Σ^{^} voln^*
97	90, 96	nfmpt 4512	. . . . . . . . . . 11 Σ^{^} voln^*
98		fveq2 5881	. . . . . . . . . . . . . . 15
99	98	eleq2d 2492	. . . . . . . . . . . . . 14
100		fveq2 5881	. . . . . . . . . . . . . . . 16 voln^* voln^*
101	100	oveq1d 6320	. . . . . . . . . . . . . . 15 voln^* voln^*
102	101	breq2d 4435	. . . . . . . . . . . . . 14 Σ^{^} voln^* Σ^{^} voln^*
103	99, 102	anbi12d 715	. . . . . . . . . . . . 13 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
104	103	rabbidva2 3069	. . . . . . . . . . . 12 Σ^{^} voln^* Σ^{^} voln^*
105	104	mpteq2dv 4511	. . . . . . . . . . 11 Σ^{^} voln^* Σ^{^} voln^*
106	89, 97, 105	cbvmpt 4515	. . . . . . . . . 10 Σ^{^} voln^* Σ^{^} voln^*
107	88, 106	eqtri 2451	. . . . . . . . 9 Σ^{^} voln^*
108	107	a1i 11	. . . . . . . 8 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
109		fveq2 5881	. . . . . . . . . . . . 13
110	109	eleq2d 2492	. . . . . . . . . . . 12
111		fveq2 5881	. . . . . . . . . . . . . 14 voln^* voln^*
112	111	oveq1d 6320	. . . . . . . . . . . . 13 voln^* voln^*
113	112	breq2d 4435	. . . . . . . . . . . 12 Σ^{^} voln^* Σ^{^} voln^*
114	110, 113	anbi12d 715	. . . . . . . . . . 11 $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^*
115	114	rabbidva2 3069	. . . . . . . . . 10 Σ^{^} voln^* Σ^{^} voln^*
116	115	mpteq2dv 4511	. . . . . . . . 9 Σ^{^} voln^* Σ^{^} voln^*
117	116	adantl 467	. . . . . . . 8 $/\$ $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^* Σ^{^} voln^*
118	39	adantr 466	. . . . . . . 8 $/\$ $/\$ Σ^{^} voln^*
119		rpex 37523	. . . . . . . . . 10
120	119	mptex 6151	. . . . . . . . 9 Σ^{^} voln^*
121	120	a1i 11	. . . . . . . 8 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
122	108, 117, 118, 121	fvmptd 5970	. . . . . . 7 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
123		oveq2 6313	. . . . . . . . . 10 voln^* voln^*
124	123	breq2d 4435	. . . . . . . . 9 Σ^{^} voln^* Σ^{^} voln^*
125	124	rabbidv 3071	. . . . . . . 8 Σ^{^} voln^* Σ^{^} voln^*
126	125	adantl 467	. . . . . . 7 $/\$ $/\$ Σ^{^} voln^* $/\$ Σ^{^} voln^* Σ^{^} voln^*
127	4	adantr 466	. . . . . . 7 $/\$ $/\$ Σ^{^} voln^*
128		fvex 5891	. . . . . . . . 9
129	128	rabex 4575	. . . . . . . 8 Σ^{^} voln^*
130	129	a1i 11	. . . . . . 7 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
131	122, 126, 127, 130	fvmptd 5970	. . . . . 6 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
132	131	eqcomd 2430	. . . . 5 $/\$ $/\$ Σ^{^} voln^* Σ^{^} voln^*
133	87, 132	eleqtrd 2509	. . . 4 $/\$ $/\$ Σ^{^} voln^*
134	133	ex 435	. . 3 $/\$ Σ^{^} voln^*
135	134	eximdv 1758	. 2 $/\$ Σ^{^} voln^*
136	83, 135	mpd 15	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wex 1657

wcel 1872

wne 2614

wrex 2772

crab 2775

cvv 3080

wss 3436

c0 3761

cpw 3981

ciun 4299 class class class wbr 4423

cmpt 4482

cxp 4851

ccom 4857

wf 5597

cfv 5601 (class class class)co 6305

cmap 7483

cixp 7533

cfn 7580

cr 9545

cxr 9681

cle 9683

cn 10616

crp 11309

cxad 11414

cico 11644

cprod 13958

cvol 22413 Σ^{^}csumge0 38112 voln^*covoln 38261

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597 ax-inf2 8155 ax-cnex 9602 ax-resscn 9603 ax-1cn 9604 ax-icn 9605 ax-addcl 9606 ax-addrcl 9607 ax-mulcl 9608 ax-mulrcl 9609 ax-mulcom 9610 ax-addass 9611 ax-mulass 9612 ax-distr 9613 ax-i2m1 9614 ax-1ne0 9615 ax-1rid 9616 ax-rnegex 9617 ax-rrecex 9618 ax-cnre 9619 ax-pre-lttri 9620 ax-pre-lttrn 9621 ax-pre-ltadd 9622 ax-pre-mulgt0 9623 ax-pre-sup 9624 ax-addf 9625 ax-mulf 9626

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-om 6707 df-1st 6807 df-2nd 6808 df-tpos 6984 df-wrecs 7039 df-recs 7101 df-rdg 7139 df-1o 7193 df-2o 7194 df-oadd 7197 df-er 7374 df-map 7485 df-pm 7486 df-ixp 7534 df-en 7581 df-dom 7582 df-sdom 7583 df-fin 7584 df-fi 7934 df-sup 7965 df-inf 7966 df-oi 8034 df-card 8381 df-cda 8605 df-pnf 9684 df-mnf 9685 df-xr 9686 df-ltxr 9687 df-le 9688 df-sub 9869 df-neg 9870 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-4 10677 df-5 10678 df-6 10679 df-7 10680 df-8 10681 df-9 10682 df-10 10683 df-n0 10877 df-z 10945 df-dec 11059 df-uz 11167 df-q 11272 df-rp 11310 df-xneg 11416 df-xadd 11417 df-xmul 11418 df-ioo 11646 df-ico 11648 df-icc 11649 df-fz 11792 df-fzo 11923 df-fl 12034 df-seq 12220 df-exp 12279 df-hash 12522 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13551 df-rlim 13552 df-sum 13752 df-prod 13959 df-struct 15122 df-ndx 15123 df-slot 15124 df-base 15125 df-sets 15126 df-ress 15127 df-plusg 15202 df-mulr 15203 df-starv 15204 df-tset 15208 df-ple 15209 df-ds 15211 df-unif 15212 df-rest 15320 df-0g 15339 df-topgen 15341 df-mgm 16487 df-sgrp 16526 df-mnd 16536 df-grp 16672 df-minusg 16673 df-subg 16813 df-cmn 17431 df-abl 17432 df-mgp 17723 df-ur 17735 df-ring 17781 df-cring 17782 df-oppr 17850 df-dvdsr 17868 df-unit 17869 df-invr 17899 df-dvr 17910 df-drng 17976 df-psmet 18961 df-xmet 18962 df-met 18963 df-bl 18964 df-mopn 18965 df-cnfld 18970 df-top 19919 df-bases 19920 df-topon 19921 df-cmp 20400 df-ovol 22414 df-vol 22416 df-sumge0 38113 df-ovoln 38262

This theorem is referenced by: ovnsubaddlem2 38297

W3C validator