ovnhoilem2 - Mathbox for Glauco Siliprandi

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

Theorem ovnhoilem2 38434

Description: The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. Second part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)

**Hypotheses**
Ref	Expression
ovnhoilem2.x
ovnhoilem2.n
ovnhoilem2.a
ovnhoilem2.b
ovnhoilem2.i
ovnhoilem2.l
ovnhoilem2.m	$/\$ Σ^{^}
ovnhoilem2.f
ovnhoilem2.s

**Assertion**
Ref	Expression
ovnhoilem2	voln^*

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem ovnhoilem2**
Step	Hyp	Ref	Expression
1		ovnhoilem2.m	. . . . . . . . . 10 $/\$ Σ^{^}
2	1	eleq2i 2523	. . . . . . . . 9 $/\$ Σ^{^}
3		rabid 2969	. . . . . . . . 9 $/\$ Σ^{^} $/\$ $/\$ Σ^{^}
4	2, 3	bitri 253	. . . . . . . 8 $/\$ $/\$ Σ^{^}
5	4	biimpi 198	. . . . . . 7 $/\$ $/\$ Σ^{^}
6	5	simprd 465	. . . . . 6 $/\$ Σ^{^}
7	6	adantl 468	. . . . 5 $/\$ $/\$ Σ^{^}
8		ovnhoilem2.l	. . . . . . . . . 10
9		ovnhoilem2.x	. . . . . . . . . . 11
10	9	3ad2ant1 1030	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
11		ovnhoilem2.a	. . . . . . . . . . 11
12	11	3ad2ant1 1030	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
13		ovnhoilem2.b	. . . . . . . . . . 11
14	13	3ad2ant1 1030	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
15		elmapi 7498	. . . . . . . . . . . . . . . . . . 19
16	15	ffvelrnda 6027	. . . . . . . . . . . . . . . . . 18 $/\$
17		elmapi 7498	. . . . . . . . . . . . . . . . . 18
18	16, 17	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
19	18	ffvelrnda 6027	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20		xp1st 6828	. . . . . . . . . . . . . . . 16
21	19, 20	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
22		eqid 2453	. . . . . . . . . . . . . . 15
23	21, 22	fmptd 6051	. . . . . . . . . . . . . 14 $/\$
24		reex 9635	. . . . . . . . . . . . . . . 16
25	24	a1i 11	. . . . . . . . . . . . . . 15 $/\$
26		1nn 10627	. . . . . . . . . . . . . . . . . . 19
27	26	a1i 11	. . . . . . . . . . . . . . . . . 18
28	15, 27	ffvelrnd 6028	. . . . . . . . . . . . . . . . 17
29		elmapex 7497	. . . . . . . . . . . . . . . . . 18 $/\$
30	29	simprd 465	. . . . . . . . . . . . . . . . 17
31	28, 30	syl 17	. . . . . . . . . . . . . . . 16
32	31	adantr 467	. . . . . . . . . . . . . . 15 $/\$
33		elmapg 7490	. . . . . . . . . . . . . . 15 $/\$
34	25, 32, 33	syl2anc 667	. . . . . . . . . . . . . 14 $/\$
35	23, 34	mpbird 236	. . . . . . . . . . . . 13 $/\$
36		eqid 2453	. . . . . . . . . . . . 13
37	35, 36	fmptd 6051	. . . . . . . . . . . 12
38		id 22	. . . . . . . . . . . . . 14
39		nnex 10622	. . . . . . . . . . . . . . . 16
40	39	mptex 6141	. . . . . . . . . . . . . . 15
41	40	a1i 11	. . . . . . . . . . . . . 14
42		ovnhoilem2.f	. . . . . . . . . . . . . . 15
43	42	fvmpt2 5962	. . . . . . . . . . . . . 14 $/\$
44	38, 41, 43	syl2anc 667	. . . . . . . . . . . . 13
45	44	feq1d 5719	. . . . . . . . . . . 12
46	37, 45	mpbird 236	. . . . . . . . . . 11
47	46	3ad2ant2 1031	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
48		xp2nd 6829	. . . . . . . . . . . . . . . 16
49	19, 48	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
50		eqid 2453	. . . . . . . . . . . . . . 15
51	49, 50	fmptd 6051	. . . . . . . . . . . . . 14 $/\$
52		elmapg 7490	. . . . . . . . . . . . . . 15 $/\$
53	25, 32, 52	syl2anc 667	. . . . . . . . . . . . . 14 $/\$
54	51, 53	mpbird 236	. . . . . . . . . . . . 13 $/\$
55		eqid 2453	. . . . . . . . . . . . 13
56	54, 55	fmptd 6051	. . . . . . . . . . . 12
57	39	mptex 6141	. . . . . . . . . . . . . . 15
58	57	a1i 11	. . . . . . . . . . . . . 14
59		ovnhoilem2.s	. . . . . . . . . . . . . . 15
60	59	fvmpt2 5962	. . . . . . . . . . . . . 14 $/\$
61	38, 58, 60	syl2anc 667	. . . . . . . . . . . . 13
62	61	feq1d 5719	. . . . . . . . . . . 12
63	56, 62	mpbird 236	. . . . . . . . . . 11
64	63	3ad2ant2 1031	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
65		simp3 1011	. . . . . . . . . . . 12 $/\$ $/\$
66		ovnhoilem2.i	. . . . . . . . . . . . . 14
67	66	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
68		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . 22
69	68	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . 21
70	69	fveq2d 5874	. . . . . . . . . . . . . . . . . . . 20
71	69	fveq2d 5874	. . . . . . . . . . . . . . . . . . . 20
72	70, 71	oveq12d 6313	. . . . . . . . . . . . . . . . . . 19
73	72	ixpeq2dv 7543	. . . . . . . . . . . . . . . . . 18
74	73	cbviunv 4320	. . . . . . . . . . . . . . . . 17
75	74	a1i 11	. . . . . . . . . . . . . . . 16
76	15	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . 21 $/\$
77		elmapi 7498	. . . . . . . . . . . . . . . . . . . . 21
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
79	78	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
80		simpr 463	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
81	79, 80	fvovco 37479	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
82	81	ixpeq2dva 7542	. . . . . . . . . . . . . . . . 17 $/\$
83	82	iuneq2dv 4303	. . . . . . . . . . . . . . . 16
84		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
85	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
86	84, 85, 43	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
87	86	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
88		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
89		mptexg 6140	. . . . . . . . . . . . . . . . . . . . . . . . . 26
90	31, 89	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	90	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
92	36	fvmpt2 5962	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
93	88, 91, 92	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
94	87, 93	eqtrd 2487	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
95	94	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . 21 $/\$
96	95	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
97		eqidd 2454	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
98		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
99	98	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
100	99	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
102		fvex 5880	. . . . . . . . . . . . . . . . . . . . . . 23
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
104	97, 100, 101, 103	fvmptd 5959	. . . . . . . . . . . . . . . . . . . . 21 $/\$
105	104	adantlr 722	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
106	96, 105	eqtrd 2487	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
107	61	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . . . . 24
108	107	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
109		mptexg 6140	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	31, 109	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	110	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
112	55	fvmpt2 5962	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
113	88, 111, 112	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
114	108, 113	eqtrd 2487	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
115	114	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . 21 $/\$
116	115	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117		eqidd 2454	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . . . 24
119	118	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . . 23
120	119	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
121		fvex 5880	. . . . . . . . . . . . . . . . . . . . . . 23
122	121	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
123	117, 120, 101, 122	fvmptd 5959	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124	123	adantlr 722	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
125	116, 124	eqtrd 2487	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
126	106, 125	oveq12d 6313	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
127	126	ixpeq2dva 7542	. . . . . . . . . . . . . . . . 17 $/\$
128	127	iuneq2dv 4303	. . . . . . . . . . . . . . . 16
129	75, 83, 128	3eqtr4d 2497	. . . . . . . . . . . . . . 15
130	129	adantl 468	. . . . . . . . . . . . . 14 $/\$
131	130	3adant3 1029	. . . . . . . . . . . . 13 $/\$ $/\$
132	67, 131	sseq12d 3463	. . . . . . . . . . . 12 $/\$ $/\$
133	65, 132	mpbid 214	. . . . . . . . . . 11 $/\$ $/\$
134	133	3adant3r 1266	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
135	8, 10, 12, 14, 47, 64, 134	hoidmvle 38432	. . . . . . . . 9 $/\$ $/\$ $/\$ Σ^{^} Σ^{^}
136		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
137	136	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
138	137	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
139	138	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
140	139	mpteq2dva 4492	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . 21
142	141	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$
143		eqidd 2454	. . . . . . . . . . . . . . . . . . . . . 22
144		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . . . 24
145	144	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . . 23
146	145	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
147		id 22	. . . . . . . . . . . . . . . . . . . . . 22
148		fvex 5880	. . . . . . . . . . . . . . . . . . . . . . 23
149	148	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
150	143, 146, 147, 149	fvmptd 5959	. . . . . . . . . . . . . . . . . . . . 21
151	150	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
152	142, 151	eqtrd 2487	. . . . . . . . . . . . . . . . . . 19 $/\$
153	138	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
154	153	mpteq2dva 4492	. . . . . . . . . . . . . . . . . . . . . 22
155	154	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . 21
156	155	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$
157		eqidd 2454	. . . . . . . . . . . . . . . . . . . . . 22
158	144	fveq2d 5874	. . . . . . . . . . . . . . . . . . . . . . 23
159	158	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
160		fvex 5880	. . . . . . . . . . . . . . . . . . . . . . 23
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
162	157, 159, 147, 161	fvmptd 5959	. . . . . . . . . . . . . . . . . . . . 21
163	162	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
164	156, 163	eqtrd 2487	. . . . . . . . . . . . . . . . . . 19 $/\$
165	152, 164	oveq12d 6313	. . . . . . . . . . . . . . . . . 18 $/\$
166	165	fveq2d 5874	. . . . . . . . . . . . . . . . 17 $/\$
167	166	prodeq2dv 13989	. . . . . . . . . . . . . . . 16
168	167	cbvmptv 4498	. . . . . . . . . . . . . . 15
169	168	a1i 11	. . . . . . . . . . . . . 14
170	81	eqcomd 2459	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
171	170	fveq2d 5874	. . . . . . . . . . . . . . . 16 $/\$ $/\$
172	171	prodeq2dv 13989	. . . . . . . . . . . . . . 15 $/\$
173	172	mpteq2dva 4492	. . . . . . . . . . . . . 14
174	169, 173	eqtrd 2487	. . . . . . . . . . . . 13
175	174	fveq2d 5874	. . . . . . . . . . . 12 Σ^{^} Σ^{^}
176	175	3ad2ant2 1031	. . . . . . . . . . 11 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
177	94	adantll 721	. . . . . . . . . . . . . . . 16 $/\$ $/\$
178	114	adantll 721	. . . . . . . . . . . . . . . 16 $/\$ $/\$
179	177, 178	oveq12d 6313	. . . . . . . . . . . . . . 15 $/\$ $/\$
180	9	ad2antrr 733	. . . . . . . . . . . . . . . 16 $/\$ $/\$
181		ovnhoilem2.n	. . . . . . . . . . . . . . . . 17
182	181	ad2antrr 733	. . . . . . . . . . . . . . . 16 $/\$ $/\$
183	19	adantlll 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
184	183, 20	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
185	184, 22	fmptd 6051	. . . . . . . . . . . . . . . 16 $/\$ $/\$
186	183, 48	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
187	186, 50	fmptd 6051	. . . . . . . . . . . . . . . 16 $/\$ $/\$
188	8, 180, 182, 185, 187	hoidmvn0val 38416	. . . . . . . . . . . . . . 15 $/\$ $/\$
189	179, 188	eqtrd 2487	. . . . . . . . . . . . . 14 $/\$ $/\$
190	189	mpteq2dva 4492	. . . . . . . . . . . . 13 $/\$
191	190	fveq2d 5874	. . . . . . . . . . . 12 $/\$ Σ^{^} Σ^{^}
192	191	3adant3 1029	. . . . . . . . . . 11 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
193		simp3 1011	. . . . . . . . . . 11 $/\$ $/\$ Σ^{^} Σ^{^}
194	176, 192, 193	3eqtr4d 2497	. . . . . . . . . 10 $/\$ $/\$ Σ^{^} Σ^{^}
195	194	3adant3l 1265	. . . . . . . . 9 $/\$ $/\$ $/\$ Σ^{^} Σ^{^}
196	135, 195	breqtrd 4430	. . . . . . . 8 $/\$ $/\$ $/\$ Σ^{^}
197	196	3exp 1208	. . . . . . 7 $/\$ Σ^{^}
198	197	adantr 467	. . . . . 6 $/\$ $/\$ Σ^{^}
199	198	rexlimdv 2879	. . . . 5 $/\$ $/\$ Σ^{^}
200	7, 199	mpd 15	. . . 4 $/\$
201	200	ralrimiva 2804	. . 3
202		ssrab2 3516	. . . . . 6 $/\$ Σ^{^}
203	1, 202	eqsstri 3464	. . . . 5
204	203	a1i 11	. . . 4
205		icossxr 11726	. . . . 5
206	8, 9, 11, 13	hoidmvcl 38414	. . . . 5
207	205, 206	sseldi 3432	. . . 4
208		infxrgelb 11628	. . . 4 $/\$ inf
209	204, 207, 208	syl2anc 667	. . 3 inf
210	201, 209	mpbird 236	. 2 inf
211	66	a1i 11	. . . . 5
212		nfv 1763	. . . . . 6
213	11	ffvelrnda 6027	. . . . . 6 $/\$
214	13	ffvelrnda 6027	. . . . . . 7 $/\$
215	214	rexrd 9695	. . . . . 6 $/\$
216	212, 213, 215	hoissrrn2 38410	. . . . 5
217	211, 216	eqsstrd 3468	. . . 4
218	9, 181, 217, 1	ovnn0val 38383	. . 3 voln^* inf
219	218	eqcomd 2459	. 2 inf voln^*
220	210, 219	breqtrd 4430	1 voln^*

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 986

wceq 1446

wcel 1889

wne 2624

wral 2739

wrex 2740

crab 2743

cvv 3047

wss 3406

c0 3733

cif 3883

ciun 4281 class class class wbr 4405

cmpt 4464

cxp 4835

ccom 4841

wf 5581

cfv 5585 (class class class)co 6295

cmpt2 6297

c1st 6796

c2nd 6797

cmap 7477

cixp 7527

cfn 7574 infcinf 7960

cr 9543

cc0 9544

c1 9545

cpnf 9677

cxr 9679

clt 9680

cle 9681

cn 10616

cico 11644

cprod 13971

cvol 22427 Σ^{^}csumge0 38214 voln^*covoln 38367

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-inf2 8151 ax-cnex 9600 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 ax-pre-mulgt0 9621 ax-pre-sup 9622

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-fal 1452 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-int 4238 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-se 4797 df-we 4798 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-isom 5594 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-of 6536 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-2o 7188 df-oadd 7191 df-er 7368 df-map 7479 df-pm 7480 df-ixp 7528 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-fi 7930 df-sup 7961 df-inf 7962 df-oi 8030 df-card 8378 df-cda 8603 df-pnf 9682 df-mnf 9683 df-xr 9684 df-ltxr 9685 df-le 9686 df-sub 9867 df-neg 9868 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-n0 10877 df-z 10945 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 12035 df-seq 12221 df-exp 12280 df-hash 12523 df-cj 13174 df-re 13175 df-im 13176 df-sqrt 13310 df-abs 13311 df-clim 13564 df-rlim 13565 df-sum 13765 df-prod 13972 df-rest 15333 df-topgen 15354 df-psmet 18974 df-xmet 18975 df-met 18976 df-bl 18977 df-mopn 18978 df-top 19933 df-bases 19934 df-topon 19935 df-cmp 20414 df-ovol 22428 df-vol 22430 df-sumge0 38215 df-ovoln 38368

This theorem is referenced by: ovnhoi 38435

W3C validator