lhop1 - Metamath Proof Explorer

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

Theorem lhop1 21612

Description: L'Hôpital's Rule for limits from the right. If

and

are differentiable real functions on

, and

and

both approach 0 at

, and

and

are not zero on

, and the limit of

, then the limit

also exists and equals

. (Contributed by Mario Carneiro, 29-Dec-2016.)

**Hypotheses**
Ref	Expression
lhop1.a
lhop1.b
lhop1.l
lhop1.f
lhop1.g
lhop1.if
lhop1.ig
lhop1.f0	lim
lhop1.g0	lim
lhop1.gn0
lhop1.gd0
lhop1.c	lim

**Assertion**
Ref	Expression
lhop1	lim

Distinct variable groups:

Proof of Theorem lhop1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lhop1.c	. 2 lim
2		simpr 461	. . . . . . . 8 $/\$
3	2	rphalfcld 11143	. . . . . . 7 $/\$
4		breq2 4397	. . . . . . . . . 10
5	4	imbi2d 316	. . . . . . . . 9 $/\$ $/\$
6	5	rexralbidv 2873	. . . . . . . 8 $/\$ $/\$
7	6	rspcv 3168	. . . . . . 7 $/\$ $/\$
8	3, 7	syl 16	. . . . . 6 $/\$ $/\$ $/\$
9		rabid 2996	. . . . . . . . . . . . . 14 $/\$
10		eliooord 11459	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
11	10	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
12	11	simprd 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
13	12	biantrurd 508	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
14		ioossre 11461	. . . . . . . . . . . . . . . . . . . . 21
15		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
16	14, 15	sseldi 3455	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
17		lhop1.a	. . . . . . . . . . . . . . . . . . . . 21
18	17	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
19		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
20	19	rpred 11131	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
21	20	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
22	16, 18, 21	ltsubaddd 10039	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
23	16	rexrd 9537	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
24		lhop1.b	. . . . . . . . . . . . . . . . . . . . 21
25	24	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	17	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	20, 26	readdcld 9517	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	27	rexrd 9537	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
29	28	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
30		xrltmin 11258	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
31	23, 25, 29, 30	syl3anc 1219	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
32	13, 22, 31	3bitr4rd 286	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
33	18	rexrd 9537	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
34		ifcl 3932	. . . . . . . . . . . . . . . . . . . 20 $/\$
35	25, 29, 34	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
36	11	simpld 459	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
37		elioo5 11457	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
38	37	baibd 900	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
39	33, 35, 23, 36, 38	syl31anc 1222	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
40	18, 16, 36	ltled 9626	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
41	18, 16, 40	abssubge0d 13029	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
42	41	breq1d 4403	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
43	32, 39, 42	3bitr4d 285	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
44	43	rabbi2dva 3659	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	24	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
46		xrmin1 11253	. . . . . . . . . . . . . . . . . . 19 $/\$
47	45, 28, 46	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
48		iooss2 11440	. . . . . . . . . . . . . . . . . 18 $/\$
49	45, 47, 48	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
50		dfss1 3656	. . . . . . . . . . . . . . . . 17
51	49, 50	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$
52	44, 51	eqtr3d 2494	. . . . . . . . . . . . . . 15 $/\$ $/\$
53	52	eleq2d 2521	. . . . . . . . . . . . . 14 $/\$ $/\$
54	9, 53	syl5bbr 259	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
55		lbioo 11435	. . . . . . . . . . . . . . . . . . . . . 22
56		eleq1 2523	. . . . . . . . . . . . . . . . . . . . . 22
57	55, 56	mtbiri 303	. . . . . . . . . . . . . . . . . . . . 21
58	57	necon2ai 2683	. . . . . . . . . . . . . . . . . . . 20
59	58	biantrurd 508	. . . . . . . . . . . . . . . . . . 19 $/\$
60	59	bicomd 201	. . . . . . . . . . . . . . . . . 18 $/\$
61		fveq2 5792	. . . . . . . . . . . . . . . . . . . . . . 23
62		fveq2 5792	. . . . . . . . . . . . . . . . . . . . . . 23
63	61, 62	oveq12d 6211	. . . . . . . . . . . . . . . . . . . . . 22
64		eqid 2451	. . . . . . . . . . . . . . . . . . . . . 22
65		ovex 6218	. . . . . . . . . . . . . . . . . . . . . 22
66	63, 64, 65	fvmpt3i 5880	. . . . . . . . . . . . . . . . . . . . 21
67	66	oveq1d 6208	. . . . . . . . . . . . . . . . . . . 20
68	67	fveq2d 5796	. . . . . . . . . . . . . . . . . . 19
69	68	breq1d 4403	. . . . . . . . . . . . . . . . . 18
70	60, 69	imbi12d 320	. . . . . . . . . . . . . . . . 17 $/\$
71	70	ralbiia 2833	. . . . . . . . . . . . . . . 16 $/\$
72		oveq1 6200	. . . . . . . . . . . . . . . . . . 19
73	72	fveq2d 5796	. . . . . . . . . . . . . . . . . 18
74	73	breq1d 4403	. . . . . . . . . . . . . . . . 17
75	74	ralrab 3221	. . . . . . . . . . . . . . . 16
76	71, 75	bitr4i 252	. . . . . . . . . . . . . . 15 $/\$
77	52	adantrr 716	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
78	77	raleqdv 3022	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
79	17	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
80	24	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
81		lhop1.l	. . . . . . . . . . . . . . . . . . . 20
82	81	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
83		lhop1.f	. . . . . . . . . . . . . . . . . . . 20
84	83	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
85		lhop1.g	. . . . . . . . . . . . . . . . . . . 20
86	85	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
87		lhop1.if	. . . . . . . . . . . . . . . . . . . 20
88	87	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
89		lhop1.ig	. . . . . . . . . . . . . . . . . . . 20
90	89	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
91		lhop1.f0	. . . . . . . . . . . . . . . . . . . 20 lim
92	91	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
93		lhop1.g0	. . . . . . . . . . . . . . . . . . . 20 lim
94	93	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
95		lhop1.gn0	. . . . . . . . . . . . . . . . . . . 20
96	95	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
97		lhop1.gd0	. . . . . . . . . . . . . . . . . . . 20
98	97	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
99	1	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
100	3	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
101	79	rexrd 9537	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
102		simprll 761	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
103	102	rpred 11131	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
104	103, 79	readdcld 9517	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
105		iocssre 11479	. . . . . . . . . . . . . . . . . . . . 21 $/\$
106	101, 104, 105	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
107	80	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
108	103	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
109	79	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
110	108, 109	readdcld 9517	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
111	110	rexrd 9537	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	107, 111	ifclda 3922	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
113	79, 102	ltaddrp2d 11161	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
114	104	rexrd 9537	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
115		xrltmin 11258	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
116	101, 80, 114, 115	syl3anc 1219	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
117	82, 113, 116	mpbir2and 913	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
118		xrmin2 11254	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
119	80, 114, 118	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
120		elioc1 11446	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
121	101, 114, 120	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	112, 117, 119, 121	mpbir3and 1171	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
123	106, 122	sseldd 3458	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	80, 114, 46	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
125		simprlr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
126		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
127		eqid 2451	. . . . . . . . . . . . . . . . . . 19
128	79, 80, 82, 84, 86, 88, 90, 92, 94, 96, 98, 99, 100, 123, 124, 125, 126, 127	lhop1lem 21611	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
129	2	rpcnd 11133	. . . . . . . . . . . . . . . . . . . 20 $/\$
130		2cnd 10498	. . . . . . . . . . . . . . . . . . . 20 $/\$
131		2ne0 10518	. . . . . . . . . . . . . . . . . . . . 21
132	131	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
133	129, 130, 132	divcan2d 10213	. . . . . . . . . . . . . . . . . . 19 $/\$
134	133	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
135	128, 134	breqtrd 4417	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
136	135	expr 615	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	78, 136	sylbid 215	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
138	76, 137	syl5bi 217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
139	138	expr 615	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140	54, 139	sylbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
141	140	expdimp 437	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
142		fveq2 5792	. . . . . . . . . . . . . . . . . 18
143		fveq2 5792	. . . . . . . . . . . . . . . . . 18
144	142, 143	oveq12d 6211	. . . . . . . . . . . . . . . . 17
145		eqid 2451	. . . . . . . . . . . . . . . . 17
146		ovex 6218	. . . . . . . . . . . . . . . . 17
147	144, 145, 146	fvmpt3i 5880	. . . . . . . . . . . . . . . 16
148	147	oveq1d 6208	. . . . . . . . . . . . . . 15
149	148	fveq2d 5796	. . . . . . . . . . . . . 14
150	149	breq1d 4403	. . . . . . . . . . . . 13
151	150	imbi2d 316	. . . . . . . . . . . 12 $/\$ $/\$
152	151	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
153	141, 152	sylibrd 234	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
154	153	adantld 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
155	154	com23 78	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
156	155	ralrimdva 2905	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
157	156	reximdva 2927	. . . . . 6 $/\$ $/\$ $/\$
158	8, 157	syld 44	. . . . 5 $/\$ $/\$ $/\$
159	158	ralrimdva 2905	. . . 4 $/\$ $/\$
160	159	anim2d 565	. . 3 $/\$ $/\$ $/\$ $/\$
161		dvf 21508	. . . . . . . 8
162	87	feq2d 5648	. . . . . . . 8
163	161, 162	mpbii 211	. . . . . . 7
164	163	ffvelrnda 5945	. . . . . 6 $/\$
165		dvf 21508	. . . . . . . 8
166	89	feq2d 5648	. . . . . . . 8
167	165, 166	mpbii 211	. . . . . . 7
168	167	ffvelrnda 5945	. . . . . 6 $/\$
169	97	adantr 465	. . . . . . 7 $/\$
170		ffn 5660	. . . . . . . . . . 11
171	167, 170	syl 16	. . . . . . . . . 10
172		fnfvelrn 5942	. . . . . . . . . 10 $/\$
173	171, 172	sylan 471	. . . . . . . . 9 $/\$
174		eleq1 2523	. . . . . . . . 9
175	173, 174	syl5ibcom 220	. . . . . . . 8 $/\$
176	175	necon3bd 2660	. . . . . . 7 $/\$
177	169, 176	mpd 15	. . . . . 6 $/\$
178	164, 168, 177	divcld 10211	. . . . 5 $/\$
179	178, 64	fmptd 5969	. . . 4
180		ax-resscn 9443	. . . . . 6
181	14, 180	sstri 3466	. . . . 5
182	181	a1i 11	. . . 4
183	17	recnd 9516	. . . 4
184	179, 182, 183	ellimc3 21480	. . 3 lim $/\$ $/\$
185	83	ffvelrnda 5945	. . . . . . 7 $/\$
186	185	recnd 9516	. . . . . 6 $/\$
187	85	ffvelrnda 5945	. . . . . . 7 $/\$
188	187	recnd 9516	. . . . . 6 $/\$
189	95	adantr 465	. . . . . . 7 $/\$
190		ffn 5660	. . . . . . . . . . 11
191	85, 190	syl 16	. . . . . . . . . 10
192		fnfvelrn 5942	. . . . . . . . . 10 $/\$
193	191, 192	sylan 471	. . . . . . . . 9 $/\$
194		eleq1 2523	. . . . . . . . 9
195	193, 194	syl5ibcom 220	. . . . . . . 8 $/\$
196	195	necon3bd 2660	. . . . . . 7 $/\$
197	189, 196	mpd 15	. . . . . 6 $/\$
198	186, 188, 197	divcld 10211	. . . . 5 $/\$
199	198, 145	fmptd 5969	. . . 4
200	199, 182, 183	ellimc3 21480	. . 3 lim $/\$ $/\$
201	160, 184, 200	3imtr4d 268	. 2 lim lim
202	1, 201	mpd 15	1 lim

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758

wne 2644

wral 2795

wrex 2796

crab 2799

cin 3428

wss 3429

cif 3892 class class class wbr 4393

cmpt 4451

cdm 4941

crn 4942

wfn 5514

wf 5515

cfv 5519 (class class class)co 6193

cc 9384

cr 9385

cc0 9386

caddc 9389

cmul 9391

cxr 9521

clt 9522

cle 9523

cmin 9699

cdiv 10097

c2 10475

crp 11095

cioo 11404

cioc 11405

cabs 12834 lim

climc 21463

cdv 21464

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4504 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475 ax-inf2 7951 ax-cnex 9442 ax-resscn 9443 ax-1cn 9444 ax-icn 9445 ax-addcl 9446 ax-addrcl 9447 ax-mulcl 9448 ax-mulrcl 9449 ax-mulcom 9450 ax-addass 9451 ax-mulass 9452 ax-distr 9453 ax-i2m1 9454 ax-1ne0 9455 ax-1rid 9456 ax-rnegex 9457 ax-rrecex 9458 ax-cnre 9459 ax-pre-lttri 9460 ax-pre-lttrn 9461 ax-pre-ltadd 9462 ax-pre-mulgt0 9463 ax-pre-sup 9464 ax-addf 9465 ax-mulf 9466

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3073 df-sbc 3288 df-csb 3390 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-pss 3445 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-tp 3983 df-op 3985 df-uni 4193 df-int 4230 df-iun 4274 df-iin 4275 df-br 4394 df-opab 4452 df-mpt 4453 df-tr 4487 df-eprel 4733 df-id 4737 df-po 4742 df-so 4743 df-fr 4780 df-se 4781 df-we 4782 df-ord 4823 df-on 4824 df-lim 4825 df-suc 4826 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-iota 5482 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-fv 5527 df-isom 5528 df-riota 6154 df-ov 6196 df-oprab 6197 df-mpt2 6198 df-of 6423 df-om 6580 df-1st 6680 df-2nd 6681 df-supp 6794 df-recs 6935 df-rdg 6969 df-1o 7023 df-2o 7024 df-oadd 7027 df-er 7204 df-map 7319 df-pm 7320 df-ixp 7367 df-en 7414 df-dom 7415 df-sdom 7416 df-fin 7417 df-fsupp 7725 df-fi 7765 df-sup 7795 df-oi 7828 df-card 8213 df-cda 8441 df-pnf 9524 df-mnf 9525 df-xr 9526 df-ltxr 9527 df-le 9528 df-sub 9701 df-neg 9702 df-div 10098 df-nn 10427 df-2 10484 df-3 10485 df-4 10486 df-5 10487 df-6 10488 df-7 10489 df-8 10490 df-9 10491 df-10 10492 df-n0 10684 df-z 10751 df-dec 10860 df-uz 10966 df-q 11058 df-rp 11096 df-xneg 11193 df-xadd 11194 df-xmul 11195 df-ioo 11408 df-ioc 11409 df-ico 11410 df-icc 11411 df-fz 11548 df-fzo 11659 df-seq 11917 df-exp 11976 df-hash 12214 df-cj 12699 df-re 12700 df-im 12701 df-sqr 12835 df-abs 12836 df-struct 14287 df-ndx 14288 df-slot 14289 df-base 14290 df-sets 14291 df-ress 14292 df-plusg 14362 df-mulr 14363 df-starv 14364 df-sca 14365 df-vsca 14366 df-ip 14367 df-tset 14368 df-ple 14369 df-ds 14371 df-unif 14372 df-hom 14373 df-cco 14374 df-rest 14472 df-topn 14473 df-0g 14491 df-gsum 14492 df-topgen 14493 df-pt 14494 df-prds 14497 df-xrs 14551 df-qtop 14556 df-imas 14557 df-xps 14559 df-mre 14635 df-mrc 14636 df-acs 14638 df-mnd 15526 df-submnd 15576 df-mulg 15659 df-cntz 15946 df-cmn 16392 df-psmet 17927 df-xmet 17928 df-met 17929 df-bl 17930 df-mopn 17931 df-fbas 17932 df-fg 17933 df-cnfld 17937 df-top 18628 df-bases 18630 df-topon 18631 df-topsp 18632 df-cld 18748 df-ntr 18749 df-cls 18750 df-nei 18827 df-lp 18865 df-perf 18866 df-cn 18956 df-cnp 18957 df-haus 19044 df-cmp 19115 df-tx 19260 df-hmeo 19453 df-fil 19544 df-fm 19636 df-flim 19637 df-flf 19638 df-xms 20020 df-ms 20021 df-tms 20022 df-cncf 20579 df-limc 21467 df-dv 21468

This theorem is referenced by: lhop2 21613 lhop 21614

W3C validator