lhop1 - Metamath Proof Explorer

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

Theorem lhop1 22901

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 462	. . . . . . . 8 $/\$
3	2	rphalfcld 11297	. . . . . . 7 $/\$
4		breq2 4363	. . . . . . . . . 10
5	4	imbi2d 317	. . . . . . . . 9 $/\$ $/\$
6	5	rexralbidv 2880	. . . . . . . 8 $/\$ $/\$
7	6	rspcv 3114	. . . . . . 7 $/\$ $/\$
8	3, 7	syl 17	. . . . . 6 $/\$ $/\$ $/\$
9		rabid 2938	. . . . . . . . . . . . . 14 $/\$
10		eliooord 11638	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
11	10	adantl 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
12	11	simprd 464	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
13	12	biantrurd 510	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
14		ioossre 11640	. . . . . . . . . . . . . . . . . . . . 21
15		simpr 462	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
16	14, 15	sseldi 3398	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
17		lhop1.a	. . . . . . . . . . . . . . . . . . . . 21
18	17	ad3antrrr 734	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
19		simpr 462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
20	19	rpred 11285	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
21	20	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
22	16, 18, 21	ltsubaddd 10153	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
23	16	rexrd 9634	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
24		lhop1.b	. . . . . . . . . . . . . . . . . . . . 21
25	24	ad3antrrr 734	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	17	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	20, 26	readdcld 9614	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	27	rexrd 9634	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
29	28	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
30		xrltmin 11421	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
31	23, 25, 29, 30	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
32	13, 22, 31	3bitr4rd 289	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
33	18	rexrd 9634	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
34	25, 29	ifcld 3890	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
35	11	simpld 460	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
36		elioo5 11636	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
37	36	baibd 917	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
38	33, 34, 23, 35, 37	syl31anc 1267	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
39	18, 16, 35	ltled 9727	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
40	18, 16, 39	abssubge0d 13430	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
41	40	breq1d 4369	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
42	32, 38, 41	3bitr4d 288	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
43	42	rabbi2dva 3606	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44	24	ad2antrr 730	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
45		xrmin1 11416	. . . . . . . . . . . . . . . . . . 19 $/\$
46	44, 28, 45	syl2anc 665	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
47		iooss2 11616	. . . . . . . . . . . . . . . . . 18 $/\$
48	44, 46, 47	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
49		dfss1 3603	. . . . . . . . . . . . . . . . 17
50	48, 49	sylib 199	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51	43, 50	eqtr3d 2458	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	51	eleq2d 2485	. . . . . . . . . . . . . 14 $/\$ $/\$
53	9, 52	syl5bbr 262	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
54		lbioo 11611	. . . . . . . . . . . . . . . . . . . . . 22
55		eleq1 2488	. . . . . . . . . . . . . . . . . . . . . 22
56	54, 55	mtbiri 304	. . . . . . . . . . . . . . . . . . . . 21
57	56	necon2ai 2624	. . . . . . . . . . . . . . . . . . . 20
58	57	biantrurd 510	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	bicomd 204	. . . . . . . . . . . . . . . . . 18 $/\$
60		fveq2 5818	. . . . . . . . . . . . . . . . . . . . . . 23
61		fveq2 5818	. . . . . . . . . . . . . . . . . . . . . . 23
62	60, 61	oveq12d 6260	. . . . . . . . . . . . . . . . . . . . . 22
63		eqid 2422	. . . . . . . . . . . . . . . . . . . . . 22
64		ovex 6270	. . . . . . . . . . . . . . . . . . . . . 22
65	62, 63, 64	fvmpt3i 5906	. . . . . . . . . . . . . . . . . . . . 21
66	65	oveq1d 6257	. . . . . . . . . . . . . . . . . . . 20
67	66	fveq2d 5822	. . . . . . . . . . . . . . . . . . 19
68	67	breq1d 4369	. . . . . . . . . . . . . . . . . 18
69	59, 68	imbi12d 321	. . . . . . . . . . . . . . . . 17 $/\$
70	69	ralbiia 2789	. . . . . . . . . . . . . . . 16 $/\$
71		oveq1 6249	. . . . . . . . . . . . . . . . . . 19
72	71	fveq2d 5822	. . . . . . . . . . . . . . . . . 18
73	72	breq1d 4369	. . . . . . . . . . . . . . . . 17
74	73	ralrab 3168	. . . . . . . . . . . . . . . 16
75	70, 74	bitr4i 255	. . . . . . . . . . . . . . 15 $/\$
76	51	adantrr 721	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
77	76	raleqdv 2964	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
78	17	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
79	24	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
80		lhop1.l	. . . . . . . . . . . . . . . . . . . 20
81	80	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
82		lhop1.f	. . . . . . . . . . . . . . . . . . . 20
83	82	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
84		lhop1.g	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
86		lhop1.if	. . . . . . . . . . . . . . . . . . . 20
87	86	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
88		lhop1.ig	. . . . . . . . . . . . . . . . . . . 20
89	88	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
90		lhop1.f0	. . . . . . . . . . . . . . . . . . . 20 lim
91	90	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
92		lhop1.g0	. . . . . . . . . . . . . . . . . . . 20 lim
93	92	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
94		lhop1.gn0	. . . . . . . . . . . . . . . . . . . 20
95	94	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
96		lhop1.gd0	. . . . . . . . . . . . . . . . . . . 20
97	96	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
98	1	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
99	3	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
100	78	rexrd 9634	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
101		simprll 770	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
102	101	rpred 11285	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
103	102, 78	readdcld 9614	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
104		iocssre 11658	. . . . . . . . . . . . . . . . . . . . 21 $/\$
105	100, 103, 104	syl2anc 665	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
106	79	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
107	102	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
108	78	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
109	107, 108	readdcld 9614	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
110	109	rexrd 9634	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
111	106, 110	ifclda 3879	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
112	78, 101	ltaddrp2d 11316	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
113	103	rexrd 9634	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
114		xrltmin 11421	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
115	100, 79, 113, 114	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
116	81, 112, 115	mpbir2and 930	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
117		xrmin2 11417	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118	79, 113, 117	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
119		elioc1 11622	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	100, 113, 119	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	111, 116, 118, 120	mpbir3and 1188	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
122	105, 121	sseldd 3401	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
123	79, 113, 45	syl2anc 665	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124		simprlr 771	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
125		simprr 764	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
126		eqid 2422	. . . . . . . . . . . . . . . . . . 19
127	78, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 98, 99, 122, 123, 124, 125, 126	lhop1lem 22900	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
128	2	rpcnd 11287	. . . . . . . . . . . . . . . . . . . 20 $/\$
129		2cnd 10626	. . . . . . . . . . . . . . . . . . . 20 $/\$
130		2ne0 10646	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	128, 129, 131	divcan2d 10329	. . . . . . . . . . . . . . . . . . 19 $/\$
133	132	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
134	127, 133	breqtrd 4384	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
135	134	expr 618	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136	77, 135	sylbid 218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
137	75, 136	syl5bi 220	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
138	137	expr 618	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	53, 138	sylbid 218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
140	139	expdimp 438	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
141		fveq2 5818	. . . . . . . . . . . . . . . . . 18
142		fveq2 5818	. . . . . . . . . . . . . . . . . 18
143	141, 142	oveq12d 6260	. . . . . . . . . . . . . . . . 17
144		eqid 2422	. . . . . . . . . . . . . . . . 17
145		ovex 6270	. . . . . . . . . . . . . . . . 17
146	143, 144, 145	fvmpt3i 5906	. . . . . . . . . . . . . . . 16
147	146	oveq1d 6257	. . . . . . . . . . . . . . 15
148	147	fveq2d 5822	. . . . . . . . . . . . . 14
149	148	breq1d 4369	. . . . . . . . . . . . 13
150	149	imbi2d 317	. . . . . . . . . . . 12 $/\$ $/\$
151	150	adantl 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
152	140, 151	sylibrd 237	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
153	152	adantld 468	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
154	153	com23 81	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
155	154	ralrimdva 2777	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
156	155	reximdva 2833	. . . . . 6 $/\$ $/\$ $/\$
157	8, 156	syld 45	. . . . 5 $/\$ $/\$ $/\$
158	157	ralrimdva 2777	. . . 4 $/\$ $/\$
159	158	anim2d 567	. . 3 $/\$ $/\$ $/\$ $/\$
160		dvf 22797	. . . . . . . 8
161	86	feq2d 5669	. . . . . . . 8
162	160, 161	mpbii 214	. . . . . . 7
163	162	ffvelrnda 5974	. . . . . 6 $/\$
164		dvf 22797	. . . . . . . 8
165	88	feq2d 5669	. . . . . . . 8
166	164, 165	mpbii 214	. . . . . . 7
167	166	ffvelrnda 5974	. . . . . 6 $/\$
168	96	adantr 466	. . . . . . 7 $/\$
169		ffn 5682	. . . . . . . . . . 11
170	166, 169	syl 17	. . . . . . . . . 10
171		fnfvelrn 5971	. . . . . . . . . 10 $/\$
172	170, 171	sylan 473	. . . . . . . . 9 $/\$
173		eleq1 2488	. . . . . . . . 9
174	172, 173	syl5ibcom 223	. . . . . . . 8 $/\$
175	174	necon3bd 2609	. . . . . . 7 $/\$
176	168, 175	mpd 15	. . . . . 6 $/\$
177	163, 167, 176	divcld 10327	. . . . 5 $/\$
178	177, 63	fmptd 5998	. . . 4
179		ax-resscn 9540	. . . . . 6
180	14, 179	sstri 3409	. . . . 5
181	180	a1i 11	. . . 4
182	17	recnd 9613	. . . 4
183	178, 181, 182	ellimc3 22769	. . 3 lim $/\$ $/\$
184	82	ffvelrnda 5974	. . . . . . 7 $/\$
185	184	recnd 9613	. . . . . 6 $/\$
186	84	ffvelrnda 5974	. . . . . . 7 $/\$
187	186	recnd 9613	. . . . . 6 $/\$
188	94	adantr 466	. . . . . . 7 $/\$
189		ffn 5682	. . . . . . . . . . 11
190	84, 189	syl 17	. . . . . . . . . 10
191		fnfvelrn 5971	. . . . . . . . . 10 $/\$
192	190, 191	sylan 473	. . . . . . . . 9 $/\$
193		eleq1 2488	. . . . . . . . 9
194	192, 193	syl5ibcom 223	. . . . . . . 8 $/\$
195	194	necon3bd 2609	. . . . . . 7 $/\$
196	188, 195	mpd 15	. . . . . 6 $/\$
197	185, 187, 196	divcld 10327	. . . . 5 $/\$
198	197, 144	fmptd 5998	. . . 4
199	198, 181, 182	ellimc3 22769	. . 3 lim $/\$ $/\$
200	159, 183, 199	3imtr4d 271	. 2 lim lim
201	1, 200	mpd 15	1 lim

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1872

wne 2593

wral 2708

wrex 2709

crab 2712

cin 3371

wss 3372

cif 3847 class class class wbr 4359

cmpt 4418

cdm 4789

crn 4790

wfn 5532

wf 5533

cfv 5537 (class class class)co 6242

cc 9481

cr 9482

cc0 9483

caddc 9486

cmul 9488

cxr 9618

clt 9619

cle 9620

cmin 9804

cdiv 10213

c2 10603

crp 11246

cioo 11579

cioc 11580

cabs 13234 lim

climc 22752

cdv 22753

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 2058 ax-ext 2402 ax-rep 4472 ax-sep 4482 ax-nul 4491 ax-pow 4538 ax-pr 4596 ax-un 6534 ax-inf2 8092 ax-cnex 9539 ax-resscn 9540 ax-1cn 9541 ax-icn 9542 ax-addcl 9543 ax-addrcl 9544 ax-mulcl 9545 ax-mulrcl 9546 ax-mulcom 9547 ax-addass 9548 ax-mulass 9549 ax-distr 9550 ax-i2m1 9551 ax-1ne0 9552 ax-1rid 9553 ax-rnegex 9554 ax-rrecex 9555 ax-cnre 9556 ax-pre-lttri 9557 ax-pre-lttrn 9558 ax-pre-ltadd 9559 ax-pre-mulgt0 9560 ax-pre-sup 9561 ax-addf 9562 ax-mulf 9563

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2274 df-mo 2275 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2552 df-ne 2595 df-nel 2596 df-ral 2713 df-rex 2714 df-reu 2715 df-rmo 2716 df-rab 2717 df-v 3018 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-pss 3388 df-nul 3698 df-if 3848 df-pw 3919 df-sn 3935 df-pr 3937 df-tp 3939 df-op 3941 df-uni 4156 df-int 4192 df-iun 4237 df-iin 4238 df-br 4360 df-opab 4419 df-mpt 4420 df-tr 4455 df-eprel 4700 df-id 4704 df-po 4710 df-so 4711 df-fr 4748 df-se 4749 df-we 4750 df-xp 4795 df-rel 4796 df-cnv 4797 df-co 4798 df-dm 4799 df-rn 4800 df-res 4801 df-ima 4802 df-pred 5335 df-ord 5381 df-on 5382 df-lim 5383 df-suc 5384 df-iota 5501 df-fun 5539 df-fn 5540 df-f 5541 df-f1 5542 df-fo 5543 df-f1o 5544 df-fv 5545 df-isom 5546 df-riota 6204 df-ov 6245 df-oprab 6246 df-mpt2 6247 df-of 6482 df-om 6644 df-1st 6744 df-2nd 6745 df-supp 6863 df-wrecs 6976 df-recs 7038 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-ixp 7471 df-en 7518 df-dom 7519 df-sdom 7520 df-fin 7521 df-fsupp 7830 df-fi 7871 df-sup 7902 df-inf 7903 df-oi 7971 df-card 8318 df-cda 8542 df-pnf 9621 df-mnf 9622 df-xr 9623 df-ltxr 9624 df-le 9625 df-sub 9806 df-neg 9807 df-div 10214 df-nn 10554 df-2 10612 df-3 10613 df-4 10614 df-5 10615 df-6 10616 df-7 10617 df-8 10618 df-9 10619 df-10 10620 df-n0 10814 df-z 10882 df-dec 10996 df-uz 11104 df-q 11209 df-rp 11247 df-xneg 11353 df-xadd 11354 df-xmul 11355 df-ioo 11583 df-ioc 11584 df-ico 11585 df-icc 11586 df-fz 11729 df-fzo 11860 df-seq 12157 df-exp 12216 df-hash 12459 df-cj 13099 df-re 13100 df-im 13101 df-sqrt 13235 df-abs 13236 df-struct 15059 df-ndx 15060 df-slot 15061 df-base 15062 df-sets 15063 df-ress 15064 df-plusg 15139 df-mulr 15140 df-starv 15141 df-sca 15142 df-vsca 15143 df-ip 15144 df-tset 15145 df-ple 15146 df-ds 15148 df-unif 15149 df-hom 15150 df-cco 15151 df-rest 15257 df-topn 15258 df-0g 15276 df-gsum 15277 df-topgen 15278 df-pt 15279 df-prds 15282 df-xrs 15336 df-qtop 15342 df-imas 15343 df-xps 15346 df-mre 15428 df-mrc 15429 df-acs 15431 df-mgm 16424 df-sgrp 16463 df-mnd 16473 df-submnd 16519 df-mulg 16612 df-cntz 16907 df-cmn 17368 df-psmet 18898 df-xmet 18899 df-met 18900 df-bl 18901 df-mopn 18902 df-fbas 18903 df-fg 18904 df-cnfld 18907 df-top 19856 df-bases 19857 df-topon 19858 df-topsp 19859 df-cld 19969 df-ntr 19970 df-cls 19971 df-nei 20049 df-lp 20087 df-perf 20088 df-cn 20178 df-cnp 20179 df-haus 20266 df-cmp 20337 df-tx 20512 df-hmeo 20705 df-fil 20796 df-fm 20888 df-flim 20889 df-flf 20890 df-xms 21270 df-ms 21271 df-tms 21272 df-cncf 21845 df-limc 22756 df-dv 22757

This theorem is referenced by: lhop2 22902 lhop 22903 fourierdlem61 37908

W3C validator