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 38542

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 2541	. . . . . . . . 9 $/\$ Σ^{^}
3		rabid 2953	. . . . . . . . 9 $/\$ Σ^{^} $/\$ $/\$ Σ^{^}
4	2, 3	bitri 257	. . . . . . . 8 $/\$ $/\$ Σ^{^}
5	4	biimpi 199	. . . . . . 7 $/\$ $/\$ Σ^{^}
6	5	simprd 470	. . . . . 6 $/\$ Σ^{^}
7	6	adantl 473	. . . . 5 $/\$ $/\$ Σ^{^}
8		ovnhoilem2.l	. . . . . . . . . 10
9		ovnhoilem2.x	. . . . . . . . . . 11
10	9	3ad2ant1 1051	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
11		ovnhoilem2.a	. . . . . . . . . . 11
12	11	3ad2ant1 1051	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
13		ovnhoilem2.b	. . . . . . . . . . 11
14	13	3ad2ant1 1051	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
15		elmapi 7511	. . . . . . . . . . . . . . . . . . 19
16	15	ffvelrnda 6037	. . . . . . . . . . . . . . . . . 18 $/\$
17		elmapi 7511	. . . . . . . . . . . . . . . . . 18
18	16, 17	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
19	18	ffvelrnda 6037	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20		xp1st 6842	. . . . . . . . . . . . . . . 16
21	19, 20	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
22		eqid 2471	. . . . . . . . . . . . . . 15
23	21, 22	fmptd 6061	. . . . . . . . . . . . . 14 $/\$
24		reex 9648	. . . . . . . . . . . . . . . 16
25	24	a1i 11	. . . . . . . . . . . . . . 15 $/\$
26		1nn 10642	. . . . . . . . . . . . . . . . . . 19
27	26	a1i 11	. . . . . . . . . . . . . . . . . 18
28	15, 27	ffvelrnd 6038	. . . . . . . . . . . . . . . . 17
29		elmapex 7510	. . . . . . . . . . . . . . . . . 18 $/\$
30	29	simprd 470	. . . . . . . . . . . . . . . . 17
31	28, 30	syl 17	. . . . . . . . . . . . . . . 16
32	31	adantr 472	. . . . . . . . . . . . . . 15 $/\$
33		elmapg 7503	. . . . . . . . . . . . . . 15 $/\$
34	25, 32, 33	syl2anc 673	. . . . . . . . . . . . . 14 $/\$
35	23, 34	mpbird 240	. . . . . . . . . . . . 13 $/\$
36		eqid 2471	. . . . . . . . . . . . 13
37	35, 36	fmptd 6061	. . . . . . . . . . . 12
38		id 22	. . . . . . . . . . . . . 14
39		nnex 10637	. . . . . . . . . . . . . . . 16
40	39	mptex 6152	. . . . . . . . . . . . . . 15
41	40	a1i 11	. . . . . . . . . . . . . 14
42		ovnhoilem2.f	. . . . . . . . . . . . . . 15
43	42	fvmpt2 5972	. . . . . . . . . . . . . 14 $/\$
44	38, 41, 43	syl2anc 673	. . . . . . . . . . . . 13
45	44	feq1d 5724	. . . . . . . . . . . 12
46	37, 45	mpbird 240	. . . . . . . . . . 11
47	46	3ad2ant2 1052	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
48		xp2nd 6843	. . . . . . . . . . . . . . . 16
49	19, 48	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
50		eqid 2471	. . . . . . . . . . . . . . 15
51	49, 50	fmptd 6061	. . . . . . . . . . . . . 14 $/\$
52		elmapg 7503	. . . . . . . . . . . . . . 15 $/\$
53	25, 32, 52	syl2anc 673	. . . . . . . . . . . . . 14 $/\$
54	51, 53	mpbird 240	. . . . . . . . . . . . 13 $/\$
55		eqid 2471	. . . . . . . . . . . . 13
56	54, 55	fmptd 6061	. . . . . . . . . . . 12
57	39	mptex 6152	. . . . . . . . . . . . . . 15
58	57	a1i 11	. . . . . . . . . . . . . 14
59		ovnhoilem2.s	. . . . . . . . . . . . . . 15
60	59	fvmpt2 5972	. . . . . . . . . . . . . 14 $/\$
61	38, 58, 60	syl2anc 673	. . . . . . . . . . . . 13
62	61	feq1d 5724	. . . . . . . . . . . 12
63	56, 62	mpbird 240	. . . . . . . . . . 11
64	63	3ad2ant2 1052	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
65		simp3 1032	. . . . . . . . . . . 12 $/\$ $/\$
66		ovnhoilem2.i	. . . . . . . . . . . . . 14
67	66	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
68		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . 22
69	68	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . 21
70	69	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20
71	69	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20
72	70, 71	oveq12d 6326	. . . . . . . . . . . . . . . . . . 19
73	72	ixpeq2dv 7556	. . . . . . . . . . . . . . . . . 18
74	73	cbviunv 4308	. . . . . . . . . . . . . . . . 17
75	74	a1i 11	. . . . . . . . . . . . . . . 16
76	15	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . 21 $/\$
77		elmapi 7511	. . . . . . . . . . . . . . . . . . . . 21
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
79	78	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
80		simpr 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
81	79, 80	fvovco 37540	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
82	81	ixpeq2dva 7555	. . . . . . . . . . . . . . . . 17 $/\$
83	82	iuneq2dv 4291	. . . . . . . . . . . . . . . 16
84		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
85	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
86	84, 85, 43	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
87	86	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
88		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
89		mptexg 6151	. . . . . . . . . . . . . . . . . . . . . . . . . 26
90	31, 89	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	90	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
92	36	fvmpt2 5972	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
93	88, 91, 92	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
94	87, 93	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
95	94	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . 21 $/\$
96	95	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
97		eqidd 2472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
98		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
99	98	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
100	99	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
101		simpr 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
102		fvex 5889	. . . . . . . . . . . . . . . . . . . . . . 23
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
104	97, 100, 101, 103	fvmptd 5969	. . . . . . . . . . . . . . . . . . . . 21 $/\$
105	104	adantlr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
106	96, 105	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
107	61	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . . . . 24
108	107	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
109		mptexg 6151	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	31, 109	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	110	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
112	55	fvmpt2 5972	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
113	88, 111, 112	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
114	108, 113	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
115	114	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . 21 $/\$
116	115	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117		eqidd 2472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . 24
119	118	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23
120	119	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
121		fvex 5889	. . . . . . . . . . . . . . . . . . . . . . 23
122	121	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
123	117, 120, 101, 122	fvmptd 5969	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124	123	adantlr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
125	116, 124	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
126	106, 125	oveq12d 6326	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
127	126	ixpeq2dva 7555	. . . . . . . . . . . . . . . . 17 $/\$
128	127	iuneq2dv 4291	. . . . . . . . . . . . . . . 16
129	75, 83, 128	3eqtr4d 2515	. . . . . . . . . . . . . . 15
130	129	adantl 473	. . . . . . . . . . . . . 14 $/\$
131	130	3adant3 1050	. . . . . . . . . . . . 13 $/\$ $/\$
132	67, 131	sseq12d 3447	. . . . . . . . . . . 12 $/\$ $/\$
133	65, 132	mpbid 215	. . . . . . . . . . 11 $/\$ $/\$
134	133	3adant3r 1289	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
135	8, 10, 12, 14, 47, 64, 134	hoidmvle 38540	. . . . . . . . 9 $/\$ $/\$ $/\$ Σ^{^} Σ^{^}
136		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
137	136	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
138	137	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
139	138	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
140	139	mpteq2dva 4482	. . . . . . . . . . . . . . . . . . . . . 22
141	140	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . 21
142	141	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$
143		eqidd 2472	. . . . . . . . . . . . . . . . . . . . . 22
144		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . 24
145	144	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23
146	145	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
147		id 22	. . . . . . . . . . . . . . . . . . . . . 22
148		fvex 5889	. . . . . . . . . . . . . . . . . . . . . . 23
149	148	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
150	143, 146, 147, 149	fvmptd 5969	. . . . . . . . . . . . . . . . . . . . 21
151	150	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$
152	142, 151	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19 $/\$
153	138	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
154	153	mpteq2dva 4482	. . . . . . . . . . . . . . . . . . . . . 22
155	154	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . 21
156	155	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$
157		eqidd 2472	. . . . . . . . . . . . . . . . . . . . . 22
158	144	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23
159	158	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
160		fvex 5889	. . . . . . . . . . . . . . . . . . . . . . 23
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
162	157, 159, 147, 161	fvmptd 5969	. . . . . . . . . . . . . . . . . . . . 21
163	162	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$
164	156, 163	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19 $/\$
165	152, 164	oveq12d 6326	. . . . . . . . . . . . . . . . . 18 $/\$
166	165	fveq2d 5883	. . . . . . . . . . . . . . . . 17 $/\$
167	166	prodeq2dv 14054	. . . . . . . . . . . . . . . 16
168	167	cbvmptv 4488	. . . . . . . . . . . . . . 15
169	168	a1i 11	. . . . . . . . . . . . . 14
170	81	eqcomd 2477	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
171	170	fveq2d 5883	. . . . . . . . . . . . . . . 16 $/\$ $/\$
172	171	prodeq2dv 14054	. . . . . . . . . . . . . . 15 $/\$
173	172	mpteq2dva 4482	. . . . . . . . . . . . . 14
174	169, 173	eqtrd 2505	. . . . . . . . . . . . 13
175	174	fveq2d 5883	. . . . . . . . . . . 12 Σ^{^} Σ^{^}
176	175	3ad2ant2 1052	. . . . . . . . . . 11 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
177	94	adantll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
178	114	adantll 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$
179	177, 178	oveq12d 6326	. . . . . . . . . . . . . . 15 $/\$ $/\$
180	9	ad2antrr 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
181		ovnhoilem2.n	. . . . . . . . . . . . . . . . 17
182	181	ad2antrr 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
183	19	adantlll 732	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
184	183, 20	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
185	184, 22	fmptd 6061	. . . . . . . . . . . . . . . 16 $/\$ $/\$
186	183, 48	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
187	186, 50	fmptd 6061	. . . . . . . . . . . . . . . 16 $/\$ $/\$
188	8, 180, 182, 185, 187	hoidmvn0val 38524	. . . . . . . . . . . . . . 15 $/\$ $/\$
189	179, 188	eqtrd 2505	. . . . . . . . . . . . . 14 $/\$ $/\$
190	189	mpteq2dva 4482	. . . . . . . . . . . . 13 $/\$
191	190	fveq2d 5883	. . . . . . . . . . . 12 $/\$ Σ^{^} Σ^{^}
192	191	3adant3 1050	. . . . . . . . . . 11 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
193		simp3 1032	. . . . . . . . . . 11 $/\$ $/\$ Σ^{^} Σ^{^}
194	176, 192, 193	3eqtr4d 2515	. . . . . . . . . 10 $/\$ $/\$ Σ^{^} Σ^{^}
195	194	3adant3l 1288	. . . . . . . . 9 $/\$ $/\$ $/\$ Σ^{^} Σ^{^}
196	135, 195	breqtrd 4420	. . . . . . . 8 $/\$ $/\$ $/\$ Σ^{^}
197	196	3exp 1230	. . . . . . 7 $/\$ Σ^{^}
198	197	adantr 472	. . . . . 6 $/\$ $/\$ Σ^{^}
199	198	rexlimdv 2870	. . . . 5 $/\$ $/\$ Σ^{^}
200	7, 199	mpd 15	. . . 4 $/\$
201	200	ralrimiva 2809	. . 3
202		ssrab2 3500	. . . . . 6 $/\$ Σ^{^}
203	1, 202	eqsstri 3448	. . . . 5
204	203	a1i 11	. . . 4
205		icossxr 11744	. . . . 5
206	8, 9, 11, 13	hoidmvcl 38522	. . . . 5
207	205, 206	sseldi 3416	. . . 4
208		infxrgelb 11646	. . . 4 $/\$ inf
209	204, 207, 208	syl2anc 673	. . 3 inf
210	201, 209	mpbird 240	. 2 inf
211	66	a1i 11	. . . . 5
212		nfv 1769	. . . . . 6
213	11	ffvelrnda 6037	. . . . . 6 $/\$
214	13	ffvelrnda 6037	. . . . . . 7 $/\$
215	214	rexrd 9708	. . . . . 6 $/\$
216	212, 213, 215	hoissrrn2 38518	. . . . 5
217	211, 216	eqsstrd 3452	. . . 4
218	9, 181, 217, 1	ovnn0val 38491	. . 3 voln^* inf
219	218	eqcomd 2477	. 2 inf voln^*
220	210, 219	breqtrd 4420	1 voln^*

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

crab 2760

cvv 3031

wss 3390

c0 3722

cif 3872

ciun 4269 class class class wbr 4395

cmpt 4454

cxp 4837

ccom 4843

wf 5585

cfv 5589 (class class class)co 6308

cmpt2 6310

c1st 6810

c2nd 6811

cmap 7490

cixp 7540

cfn 7587 infcinf 7973

cr 9556

cc0 9557

c1 9558

cpnf 9690

cxr 9692

clt 9693

cle 9694

cn 10631

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

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-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-n0 10894 df-z 10962 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-rest 15399 df-topgen 15420 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 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: ovnhoi 38543

W3C validator