lhop1 - Metamath Proof Explorer

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

Theorem lhop1 21461

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 11031	. . . . . . 7 $/\$
4		breq2 4291	. . . . . . . . . 10
5	4	imbi2d 316	. . . . . . . . 9 $/\$ $/\$
6	5	rexralbidv 2754	. . . . . . . 8 $/\$ $/\$
7	6	rspcv 3064	. . . . . . 7 $/\$ $/\$
8	3, 7	syl 16	. . . . . 6 $/\$ $/\$ $/\$
9		rabid 2892	. . . . . . . . . . . . . 14 $/\$
10		eliooord 11347	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
11	10	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
12	11	simprd 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
13	12	biantrurd 508	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
14		ioossre 11349	. . . . . . . . . . . . . . . . . . . . 21
15		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
16	14, 15	sseldi 3349	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
17		lhop1.a	. . . . . . . . . . . . . . . . . . . . 21
18	17	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
19		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
20	19	rpred 11019	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
21	20	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
22	16, 18, 21	ltsubaddd 9927	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
23	16	rexrd 9425	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
24		lhop1.b	. . . . . . . . . . . . . . . . . . . . 21
25	24	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	17	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	20, 26	readdcld 9405	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	27	rexrd 9425	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
29	28	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
30		xrltmin 11146	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
31	23, 25, 29, 30	syl3anc 1218	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
32	13, 22, 31	3bitr4rd 286	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
33	18	rexrd 9425	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
34		ifcl 3826	. . . . . . . . . . . . . . . . . . . 20 $/\$
35	25, 29, 34	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
36	11	simpld 459	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
37		elioo5 11345	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
38	37	baibd 900	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
39	33, 35, 23, 36, 38	syl31anc 1221	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
40	18, 16, 36	ltled 9514	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
41	18, 16, 40	abssubge0d 12910	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
42	41	breq1d 4297	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
43	32, 39, 42	3bitr4d 285	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
44	43	rabbi2dva 3553	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	24	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
46		xrmin1 11141	. . . . . . . . . . . . . . . . . . 19 $/\$
47	45, 28, 46	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
48		iooss2 11328	. . . . . . . . . . . . . . . . . 18 $/\$
49	45, 47, 48	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
50		dfss1 3550	. . . . . . . . . . . . . . . . 17
51	49, 50	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$
52	44, 51	eqtr3d 2472	. . . . . . . . . . . . . . 15 $/\$ $/\$
53	52	eleq2d 2505	. . . . . . . . . . . . . 14 $/\$ $/\$
54	9, 53	syl5bbr 259	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
55		lbioo 11323	. . . . . . . . . . . . . . . . . . . . . 22
56		eleq1 2498	. . . . . . . . . . . . . . . . . . . . . 22
57	55, 56	mtbiri 303	. . . . . . . . . . . . . . . . . . . . 21
58	57	necon2ai 2651	. . . . . . . . . . . . . . . . . . . 20
59	58	biantrurd 508	. . . . . . . . . . . . . . . . . . 19 $/\$
60	59	bicomd 201	. . . . . . . . . . . . . . . . . 18 $/\$
61		fveq2 5686	. . . . . . . . . . . . . . . . . . . . . . 23
62		fveq2 5686	. . . . . . . . . . . . . . . . . . . . . . 23
63	61, 62	oveq12d 6104	. . . . . . . . . . . . . . . . . . . . . 22
64		eqid 2438	. . . . . . . . . . . . . . . . . . . . . 22
65		ovex 6111	. . . . . . . . . . . . . . . . . . . . . 22
66	63, 64, 65	fvmpt3i 5773	. . . . . . . . . . . . . . . . . . . . 21
67	66	oveq1d 6101	. . . . . . . . . . . . . . . . . . . 20
68	67	fveq2d 5690	. . . . . . . . . . . . . . . . . . 19
69	68	breq1d 4297	. . . . . . . . . . . . . . . . . 18
70	60, 69	imbi12d 320	. . . . . . . . . . . . . . . . 17 $/\$
71	70	ralbiia 2742	. . . . . . . . . . . . . . . 16 $/\$
72		oveq1 6093	. . . . . . . . . . . . . . . . . . 19
73	72	fveq2d 5690	. . . . . . . . . . . . . . . . . 18
74	73	breq1d 4297	. . . . . . . . . . . . . . . . 17
75	74	ralrab 3116	. . . . . . . . . . . . . . . 16
76	71, 75	bitr4i 252	. . . . . . . . . . . . . . 15 $/\$
77	52	adantrr 716	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
78	77	raleqdv 2918	. . . . . . . . . . . . . . . 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 9425	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
102		simprll 761	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
103	102	rpred 11019	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
104	103, 79	readdcld 9405	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
105		iocssre 11367	. . . . . . . . . . . . . . . . . . . . 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 9405	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
111	110	rexrd 9425	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	107, 111	ifclda 3816	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
113	79, 102	ltaddrp2d 11049	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
114	104	rexrd 9425	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
115		xrltmin 11146	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
116	101, 80, 114, 115	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
117	82, 113, 116	mpbir2and 913	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
118		xrmin2 11142	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
119	80, 114, 118	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
120		elioc1 11334	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
121	101, 114, 120	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	112, 117, 119, 121	mpbir3and 1171	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
123	106, 122	sseldd 3352	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	80, 114, 46	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
125		simprlr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
126		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
127		eqid 2438	. . . . . . . . . . . . . . . . . . 19
128	79, 80, 82, 84, 86, 88, 90, 92, 94, 96, 98, 99, 100, 123, 124, 125, 126, 127	lhop1lem 21460	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
129	2	rpcnd 11021	. . . . . . . . . . . . . . . . . . . 20 $/\$
130		2cnd 10386	. . . . . . . . . . . . . . . . . . . 20 $/\$
131		2ne0 10406	. . . . . . . . . . . . . . . . . . . . 21
132	131	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
133	129, 130, 132	divcan2d 10101	. . . . . . . . . . . . . . . . . . 19 $/\$
134	133	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
135	128, 134	breqtrd 4311	. . . . . . . . . . . . . . . . 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 5686	. . . . . . . . . . . . . . . . . 18
143		fveq2 5686	. . . . . . . . . . . . . . . . . 18
144	142, 143	oveq12d 6104	. . . . . . . . . . . . . . . . 17
145		eqid 2438	. . . . . . . . . . . . . . . . 17
146		ovex 6111	. . . . . . . . . . . . . . . . 17
147	144, 145, 146	fvmpt3i 5773	. . . . . . . . . . . . . . . 16
148	147	oveq1d 6101	. . . . . . . . . . . . . . 15
149	148	fveq2d 5690	. . . . . . . . . . . . . 14
150	149	breq1d 4297	. . . . . . . . . . . . 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 2801	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
157	156	reximdva 2823	. . . . . 6 $/\$ $/\$ $/\$
158	8, 157	syld 44	. . . . 5 $/\$ $/\$ $/\$
159	158	ralrimdva 2801	. . . 4 $/\$ $/\$
160	159	anim2d 565	. . 3 $/\$ $/\$ $/\$ $/\$
161		dvf 21357	. . . . . . . 8
162	87	feq2d 5542	. . . . . . . 8
163	161, 162	mpbii 211	. . . . . . 7
164	163	ffvelrnda 5838	. . . . . 6 $/\$
165		dvf 21357	. . . . . . . 8
166	89	feq2d 5542	. . . . . . . 8
167	165, 166	mpbii 211	. . . . . . 7
168	167	ffvelrnda 5838	. . . . . 6 $/\$
169	97	adantr 465	. . . . . . 7 $/\$
170		ffn 5554	. . . . . . . . . . 11
171	167, 170	syl 16	. . . . . . . . . 10
172		fnfvelrn 5835	. . . . . . . . . 10 $/\$
173	171, 172	sylan 471	. . . . . . . . 9 $/\$
174		eleq1 2498	. . . . . . . . 9
175	173, 174	syl5ibcom 220	. . . . . . . 8 $/\$
176	175	necon3bd 2640	. . . . . . 7 $/\$
177	169, 176	mpd 15	. . . . . 6 $/\$
178	164, 168, 177	divcld 10099	. . . . 5 $/\$
179	178, 64	fmptd 5862	. . . 4
180		ax-resscn 9331	. . . . . 6
181	14, 180	sstri 3360	. . . . 5
182	181	a1i 11	. . . 4
183	17	recnd 9404	. . . 4
184	179, 182, 183	ellimc3 21329	. . 3 lim $/\$ $/\$
185	83	ffvelrnda 5838	. . . . . . 7 $/\$
186	185	recnd 9404	. . . . . 6 $/\$
187	85	ffvelrnda 5838	. . . . . . 7 $/\$
188	187	recnd 9404	. . . . . 6 $/\$
189	95	adantr 465	. . . . . . 7 $/\$
190		ffn 5554	. . . . . . . . . . 11
191	85, 190	syl 16	. . . . . . . . . 10
192		fnfvelrn 5835	. . . . . . . . . 10 $/\$
193	191, 192	sylan 471	. . . . . . . . 9 $/\$
194		eleq1 2498	. . . . . . . . 9
195	193, 194	syl5ibcom 220	. . . . . . . 8 $/\$
196	195	necon3bd 2640	. . . . . . 7 $/\$
197	189, 196	mpd 15	. . . . . 6 $/\$
198	186, 188, 197	divcld 10099	. . . . 5 $/\$
199	198, 145	fmptd 5862	. . . 4
200	199, 182, 183	ellimc3 21329	. . 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 1369

wcel 1756

wne 2601

wral 2710

wrex 2711

crab 2714

cin 3322

wss 3323

cif 3786 class class class wbr 4287

cmpt 4345

cdm 4835

crn 4836

wfn 5408

wf 5409

cfv 5413 (class class class)co 6086

cc 9272

cr 9273

cc0 9274

caddc 9277

cmul 9279

cxr 9409

clt 9410

cle 9411

cmin 9587

cdiv 9985

c2 10363

crp 10983

cioo 11292

cioc 11293

cabs 12715 lim

climc 21312

cdv 21313

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353 ax-mulf 9354

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-iin 4169 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-om 6472 df-1st 6572 df-2nd 6573 df-supp 6686 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-er 7093 df-map 7208 df-pm 7209 df-ixp 7256 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-fsupp 7613 df-fi 7653 df-sup 7683 df-oi 7716 df-card 8101 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-4 10374 df-5 10375 df-6 10376 df-7 10377 df-8 10378 df-9 10379 df-10 10380 df-n0 10572 df-z 10639 df-dec 10748 df-uz 10854 df-q 10946 df-rp 10984 df-xneg 11081 df-xadd 11082 df-xmul 11083 df-ioo 11296 df-ioc 11297 df-ico 11298 df-icc 11299 df-fz 11430 df-fzo 11541 df-seq 11799 df-exp 11858 df-hash 12096 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-struct 14168 df-ndx 14169 df-slot 14170 df-base 14171 df-sets 14172 df-ress 14173 df-plusg 14243 df-mulr 14244 df-starv 14245 df-sca 14246 df-vsca 14247 df-ip 14248 df-tset 14249 df-ple 14250 df-ds 14252 df-unif 14253 df-hom 14254 df-cco 14255 df-rest 14353 df-topn 14354 df-0g 14372 df-gsum 14373 df-topgen 14374 df-pt 14375 df-prds 14378 df-xrs 14432 df-qtop 14437 df-imas 14438 df-xps 14440 df-mre 14516 df-mrc 14517 df-acs 14519 df-mnd 15407 df-submnd 15457 df-mulg 15539 df-cntz 15826 df-cmn 16270 df-psmet 17784 df-xmet 17785 df-met 17786 df-bl 17787 df-mopn 17788 df-fbas 17789 df-fg 17790 df-cnfld 17794 df-top 18478 df-bases 18480 df-topon 18481 df-topsp 18482 df-cld 18598 df-ntr 18599 df-cls 18600 df-nei 18677 df-lp 18715 df-perf 18716 df-cn 18806 df-cnp 18807 df-haus 18894 df-cmp 18965 df-tx 19110 df-hmeo 19303 df-fil 19394 df-fm 19486 df-flim 19487 df-flf 19488 df-xms 19870 df-ms 19871 df-tms 19872 df-cncf 20429 df-limc 21316 df-dv 21317

This theorem is referenced by: lhop2 21462 lhop 21463

W3C validator