lhop1 - Metamath Proof Explorer

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

Theorem lhop1 22843

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 11353	. . . . . . 7 $/\$
4		breq2 4430	. . . . . . . . . 10
5	4	imbi2d 317	. . . . . . . . 9 $/\$ $/\$
6	5	rexralbidv 2954	. . . . . . . 8 $/\$ $/\$
7	6	rspcv 3184	. . . . . . 7 $/\$ $/\$
8	3, 7	syl 17	. . . . . 6 $/\$ $/\$ $/\$
9		rabid 3012	. . . . . . . . . . . . . 14 $/\$
10		eliooord 11694	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
11	10	adantl 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
12	11	simprd 464	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
13	12	biantrurd 510	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
14		ioossre 11696	. . . . . . . . . . . . . . . . . . . . 21
15		simpr 462	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
16	14, 15	sseldi 3468	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
17		lhop1.a	. . . . . . . . . . . . . . . . . . . . 21
18	17	ad3antrrr 734	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
19		simpr 462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
20	19	rpred 11341	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
21	20	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
22	16, 18, 21	ltsubaddd 10208	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
23	16	rexrd 9689	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
24		lhop1.b	. . . . . . . . . . . . . . . . . . . . 21
25	24	ad3antrrr 734	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	17	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	20, 26	readdcld 9669	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	27	rexrd 9689	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
29	28	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
30		xrltmin 11477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
31	23, 25, 29, 30	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
32	13, 22, 31	3bitr4rd 289	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
33	18	rexrd 9689	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
34	25, 29	ifcld 3958	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
35	11	simpld 460	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
36		elioo5 11692	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
37	36	baibd 917	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
38	33, 34, 23, 35, 37	syl31anc 1267	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
39	18, 16, 35	ltled 9782	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
40	18, 16, 39	abssubge0d 13472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
41	40	breq1d 4436	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
42	32, 38, 41	3bitr4d 288	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
43	42	rabbi2dva 3676	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44	24	ad2antrr 730	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
45		xrmin1 11472	. . . . . . . . . . . . . . . . . . 19 $/\$
46	44, 28, 45	syl2anc 665	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
47		iooss2 11672	. . . . . . . . . . . . . . . . . 18 $/\$
48	44, 46, 47	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
49		dfss1 3673	. . . . . . . . . . . . . . . . 17
50	48, 49	sylib 199	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51	43, 50	eqtr3d 2472	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	51	eleq2d 2499	. . . . . . . . . . . . . 14 $/\$ $/\$
53	9, 52	syl5bbr 262	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
54		lbioo 11667	. . . . . . . . . . . . . . . . . . . . . 22
55		eleq1 2501	. . . . . . . . . . . . . . . . . . . . . 22
56	54, 55	mtbiri 304	. . . . . . . . . . . . . . . . . . . . 21
57	56	necon2ai 2666	. . . . . . . . . . . . . . . . . . . 20
58	57	biantrurd 510	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	bicomd 204	. . . . . . . . . . . . . . . . . 18 $/\$
60		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . 23
61		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . 23
62	60, 61	oveq12d 6323	. . . . . . . . . . . . . . . . . . . . . 22
63		eqid 2429	. . . . . . . . . . . . . . . . . . . . . 22
64		ovex 6333	. . . . . . . . . . . . . . . . . . . . . 22
65	62, 63, 64	fvmpt3i 5969	. . . . . . . . . . . . . . . . . . . . 21
66	65	oveq1d 6320	. . . . . . . . . . . . . . . . . . . 20
67	66	fveq2d 5885	. . . . . . . . . . . . . . . . . . 19
68	67	breq1d 4436	. . . . . . . . . . . . . . . . . 18
69	59, 68	imbi12d 321	. . . . . . . . . . . . . . . . 17 $/\$
70	69	ralbiia 2862	. . . . . . . . . . . . . . . 16 $/\$
71		oveq1 6312	. . . . . . . . . . . . . . . . . . 19
72	71	fveq2d 5885	. . . . . . . . . . . . . . . . . 18
73	72	breq1d 4436	. . . . . . . . . . . . . . . . 17
74	73	ralrab 3239	. . . . . . . . . . . . . . . 16
75	70, 74	bitr4i 255	. . . . . . . . . . . . . . 15 $/\$
76	51	adantrr 721	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
77	76	raleqdv 3038	. . . . . . . . . . . . . . . 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 9689	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
101		simprll 770	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
102	101	rpred 11341	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
103	102, 78	readdcld 9669	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
104		iocssre 11714	. . . . . . . . . . . . . . . . . . . . 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 9669	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
110	109	rexrd 9689	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
111	106, 110	ifclda 3947	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
112	78, 101	ltaddrp2d 11372	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
113	103	rexrd 9689	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
114		xrltmin 11477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
115	100, 79, 113, 114	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
116	81, 112, 115	mpbir2and 930	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
117		xrmin2 11473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118	79, 113, 117	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
119		elioc1 11678	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	100, 113, 119	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	111, 116, 118, 120	mpbir3and 1188	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
122	105, 121	sseldd 3471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
123	79, 113, 45	syl2anc 665	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124		simprlr 771	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
125		simprr 764	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
126		eqid 2429	. . . . . . . . . . . . . . . . . . 19
127	78, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 98, 99, 122, 123, 124, 125, 126	lhop1lem 22842	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
128	2	rpcnd 11343	. . . . . . . . . . . . . . . . . . . 20 $/\$
129		2cnd 10682	. . . . . . . . . . . . . . . . . . . 20 $/\$
130		2ne0 10702	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	128, 129, 131	divcan2d 10384	. . . . . . . . . . . . . . . . . . 19 $/\$
133	132	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
134	127, 133	breqtrd 4450	. . . . . . . . . . . . . . . . 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 5881	. . . . . . . . . . . . . . . . . 18
142		fveq2 5881	. . . . . . . . . . . . . . . . . 18
143	141, 142	oveq12d 6323	. . . . . . . . . . . . . . . . 17
144		eqid 2429	. . . . . . . . . . . . . . . . 17
145		ovex 6333	. . . . . . . . . . . . . . . . 17
146	143, 144, 145	fvmpt3i 5969	. . . . . . . . . . . . . . . 16
147	146	oveq1d 6320	. . . . . . . . . . . . . . 15
148	147	fveq2d 5885	. . . . . . . . . . . . . 14
149	148	breq1d 4436	. . . . . . . . . . . . 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 2850	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
156	155	reximdva 2907	. . . . . 6 $/\$ $/\$ $/\$
157	8, 156	syld 45	. . . . 5 $/\$ $/\$ $/\$
158	157	ralrimdva 2850	. . . 4 $/\$ $/\$
159	158	anim2d 567	. . 3 $/\$ $/\$ $/\$ $/\$
160		dvf 22739	. . . . . . . 8
161	86	feq2d 5733	. . . . . . . 8
162	160, 161	mpbii 214	. . . . . . 7
163	162	ffvelrnda 6037	. . . . . 6 $/\$
164		dvf 22739	. . . . . . . 8
165	88	feq2d 5733	. . . . . . . 8
166	164, 165	mpbii 214	. . . . . . 7
167	166	ffvelrnda 6037	. . . . . 6 $/\$
168	96	adantr 466	. . . . . . 7 $/\$
169		ffn 5746	. . . . . . . . . . 11
170	166, 169	syl 17	. . . . . . . . . 10
171		fnfvelrn 6034	. . . . . . . . . 10 $/\$
172	170, 171	sylan 473	. . . . . . . . 9 $/\$
173		eleq1 2501	. . . . . . . . 9
174	172, 173	syl5ibcom 223	. . . . . . . 8 $/\$
175	174	necon3bd 2643	. . . . . . 7 $/\$
176	168, 175	mpd 15	. . . . . 6 $/\$
177	163, 167, 176	divcld 10382	. . . . 5 $/\$
178	177, 63	fmptd 6061	. . . 4
179		ax-resscn 9595	. . . . . 6
180	14, 179	sstri 3479	. . . . 5
181	180	a1i 11	. . . 4
182	17	recnd 9668	. . . 4
183	178, 181, 182	ellimc3 22711	. . 3 lim $/\$ $/\$
184	82	ffvelrnda 6037	. . . . . . 7 $/\$
185	184	recnd 9668	. . . . . 6 $/\$
186	84	ffvelrnda 6037	. . . . . . 7 $/\$
187	186	recnd 9668	. . . . . 6 $/\$
188	94	adantr 466	. . . . . . 7 $/\$
189		ffn 5746	. . . . . . . . . . 11
190	84, 189	syl 17	. . . . . . . . . 10
191		fnfvelrn 6034	. . . . . . . . . 10 $/\$
192	190, 191	sylan 473	. . . . . . . . 9 $/\$
193		eleq1 2501	. . . . . . . . 9
194	192, 193	syl5ibcom 223	. . . . . . . 8 $/\$
195	194	necon3bd 2643	. . . . . . 7 $/\$
196	188, 195	mpd 15	. . . . . 6 $/\$
197	185, 187, 196	divcld 10382	. . . . 5 $/\$
198	197, 144	fmptd 6061	. . . 4
199	198, 181, 182	ellimc3 22711	. . 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 1870

wne 2625

wral 2782

wrex 2783

crab 2786

cin 3441

wss 3442

cif 3915 class class class wbr 4426

cmpt 4484

cdm 4854

crn 4855

wfn 5596

wf 5597

cfv 5601 (class class class)co 6305

cc 9536

cr 9537

cc0 9538

caddc 9541

cmul 9543

cxr 9673

clt 9674

cle 9675

cmin 9859

cdiv 10268

c2 10659

crp 11302

cioo 11635

cioc 11636

cabs 13276 lim

climc 22694

cdv 22695

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-inf2 8146 ax-cnex 9594 ax-resscn 9595 ax-1cn 9596 ax-icn 9597 ax-addcl 9598 ax-addrcl 9599 ax-mulcl 9600 ax-mulrcl 9601 ax-mulcom 9602 ax-addass 9603 ax-mulass 9604 ax-distr 9605 ax-i2m1 9606 ax-1ne0 9607 ax-1rid 9608 ax-rnegex 9609 ax-rrecex 9610 ax-cnre 9611 ax-pre-lttri 9612 ax-pre-lttrn 9613 ax-pre-ltadd 9614 ax-pre-mulgt0 9615 ax-pre-sup 9616 ax-addf 9617 ax-mulf 9618

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 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-int 4259 df-iun 4304 df-iin 4305 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-se 4814 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-om 6707 df-1st 6807 df-2nd 6808 df-supp 6926 df-wrecs 7036 df-recs 7098 df-rdg 7136 df-1o 7190 df-2o 7191 df-oadd 7194 df-er 7371 df-map 7482 df-pm 7483 df-ixp 7531 df-en 7578 df-dom 7579 df-sdom 7580 df-fin 7581 df-fsupp 7890 df-fi 7931 df-sup 7962 df-oi 8025 df-card 8372 df-cda 8596 df-pnf 9676 df-mnf 9677 df-xr 9678 df-ltxr 9679 df-le 9680 df-sub 9861 df-neg 9862 df-div 10269 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ioc 11640 df-ico 11641 df-icc 11642 df-fz 11783 df-fzo 11914 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13141 df-re 13142 df-im 13143 df-sqrt 13277 df-abs 13278 df-struct 15086 df-ndx 15087 df-slot 15088 df-base 15089 df-sets 15090 df-ress 15091 df-plusg 15165 df-mulr 15166 df-starv 15167 df-sca 15168 df-vsca 15169 df-ip 15170 df-tset 15171 df-ple 15172 df-ds 15174 df-unif 15175 df-hom 15176 df-cco 15177 df-rest 15280 df-topn 15281 df-0g 15299 df-gsum 15300 df-topgen 15301 df-pt 15302 df-prds 15305 df-xrs 15359 df-qtop 15364 df-imas 15365 df-xps 15367 df-mre 15443 df-mrc 15444 df-acs 15446 df-mgm 16439 df-sgrp 16478 df-mnd 16488 df-submnd 16534 df-mulg 16627 df-cntz 16922 df-cmn 17367 df-psmet 18897 df-xmet 18898 df-met 18899 df-bl 18900 df-mopn 18901 df-fbas 18902 df-fg 18903 df-cnfld 18906 df-top 19852 df-bases 19853 df-topon 19854 df-topsp 19855 df-cld 19965 df-ntr 19966 df-cls 19967 df-nei 20045 df-lp 20083 df-perf 20084 df-cn 20174 df-cnp 20175 df-haus 20262 df-cmp 20333 df-tx 20508 df-hmeo 20701 df-fil 20792 df-fm 20884 df-flim 20885 df-flf 20886 df-xms 21266 df-ms 21267 df-tms 21268 df-cncf 21806 df-limc 22698 df-dv 22699

This theorem is referenced by: lhop2 22844 lhop 22845 fourierdlem61 37599

W3C validator