lhop1 - Metamath Proof Explorer

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

Theorem lhop1 23015

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 467	. . . . . . . 8 $/\$
3	2	rphalfcld 11382	. . . . . . 7 $/\$
4		breq2 4420	. . . . . . . . . 10
5	4	imbi2d 322	. . . . . . . . 9 $/\$ $/\$
6	5	rexralbidv 2921	. . . . . . . 8 $/\$ $/\$
7	6	rspcv 3158	. . . . . . 7 $/\$ $/\$
8	3, 7	syl 17	. . . . . 6 $/\$ $/\$ $/\$
9		rabid 2979	. . . . . . . . . . . . . 14 $/\$
10		eliooord 11723	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
11	10	adantl 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
12	11	simprd 469	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
13	12	biantrurd 515	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
14		ioossre 11725	. . . . . . . . . . . . . . . . . . . . 21
15		simpr 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
16	14, 15	sseldi 3442	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
17		lhop1.a	. . . . . . . . . . . . . . . . . . . . 21
18	17	ad3antrrr 741	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
19		simpr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
20	19	rpred 11370	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
21	20	adantr 471	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
22	16, 18, 21	ltsubaddd 10237	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
23	16	rexrd 9716	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
24		lhop1.b	. . . . . . . . . . . . . . . . . . . . 21
25	24	ad3antrrr 741	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	17	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	20, 26	readdcld 9696	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	27	rexrd 9716	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
29	28	adantr 471	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
30		xrltmin 11506	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
31	23, 25, 29, 30	syl3anc 1276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
32	13, 22, 31	3bitr4rd 294	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
33	18	rexrd 9716	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
34	25, 29	ifcld 3936	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
35	11	simpld 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
36		elioo5 11721	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
37	36	baibd 925	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
38	33, 34, 23, 35, 37	syl31anc 1279	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
39	18, 16, 35	ltled 9809	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
40	18, 16, 39	abssubge0d 13542	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
41	40	breq1d 4426	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
42	32, 38, 41	3bitr4d 293	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
43	42	rabbi2dva 3652	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44	24	ad2antrr 737	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
45		xrmin1 11501	. . . . . . . . . . . . . . . . . . 19 $/\$
46	44, 28, 45	syl2anc 671	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
47		iooss2 11701	. . . . . . . . . . . . . . . . . 18 $/\$
48	44, 46, 47	syl2anc 671	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
49		dfss1 3649	. . . . . . . . . . . . . . . . 17
50	48, 49	sylib 201	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51	43, 50	eqtr3d 2498	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	51	eleq2d 2525	. . . . . . . . . . . . . 14 $/\$ $/\$
53	9, 52	syl5bbr 267	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
54		lbioo 11696	. . . . . . . . . . . . . . . . . . . . . 22
55		eleq1 2528	. . . . . . . . . . . . . . . . . . . . . 22
56	54, 55	mtbiri 309	. . . . . . . . . . . . . . . . . . . . 21
57	56	necon2ai 2665	. . . . . . . . . . . . . . . . . . . 20
58	57	biantrurd 515	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	bicomd 206	. . . . . . . . . . . . . . . . . 18 $/\$
60		fveq2 5888	. . . . . . . . . . . . . . . . . . . . . . 23
61		fveq2 5888	. . . . . . . . . . . . . . . . . . . . . . 23
62	60, 61	oveq12d 6333	. . . . . . . . . . . . . . . . . . . . . 22
63		eqid 2462	. . . . . . . . . . . . . . . . . . . . . 22
64		ovex 6343	. . . . . . . . . . . . . . . . . . . . . 22
65	62, 63, 64	fvmpt3i 5976	. . . . . . . . . . . . . . . . . . . . 21
66	65	oveq1d 6330	. . . . . . . . . . . . . . . . . . . 20
67	66	fveq2d 5892	. . . . . . . . . . . . . . . . . . 19
68	67	breq1d 4426	. . . . . . . . . . . . . . . . . 18
69	59, 68	imbi12d 326	. . . . . . . . . . . . . . . . 17 $/\$
70	69	ralbiia 2830	. . . . . . . . . . . . . . . 16 $/\$
71		oveq1 6322	. . . . . . . . . . . . . . . . . . 19
72	71	fveq2d 5892	. . . . . . . . . . . . . . . . . 18
73	72	breq1d 4426	. . . . . . . . . . . . . . . . 17
74	73	ralrab 3212	. . . . . . . . . . . . . . . 16
75	70, 74	bitr4i 260	. . . . . . . . . . . . . . 15 $/\$
76	51	adantrr 728	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
77	76	raleqdv 3005	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
78	17	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
79	24	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
80		lhop1.l	. . . . . . . . . . . . . . . . . . . 20
81	80	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
82		lhop1.f	. . . . . . . . . . . . . . . . . . . 20
83	82	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
84		lhop1.g	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
86		lhop1.if	. . . . . . . . . . . . . . . . . . . 20
87	86	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
88		lhop1.ig	. . . . . . . . . . . . . . . . . . . 20
89	88	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
90		lhop1.f0	. . . . . . . . . . . . . . . . . . . 20 lim
91	90	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
92		lhop1.g0	. . . . . . . . . . . . . . . . . . . 20 lim
93	92	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
94		lhop1.gn0	. . . . . . . . . . . . . . . . . . . 20
95	94	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
96		lhop1.gd0	. . . . . . . . . . . . . . . . . . . 20
97	96	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
98	1	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
99	3	adantr 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
100	78	rexrd 9716	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
101		simprll 777	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
102	101	rpred 11370	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
103	102, 78	readdcld 9696	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
104		iocssre 11743	. . . . . . . . . . . . . . . . . . . . 21 $/\$
105	100, 103, 104	syl2anc 671	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
106	79	adantr 471	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
107	102	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
108	78	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
109	107, 108	readdcld 9696	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
110	109	rexrd 9716	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
111	106, 110	ifclda 3925	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
112	78, 101	ltaddrp2d 11401	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
113	103	rexrd 9716	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
114		xrltmin 11506	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
115	100, 79, 113, 114	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
116	81, 112, 115	mpbir2and 938	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
117		xrmin2 11502	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118	79, 113, 117	syl2anc 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
119		elioc1 11707	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	100, 113, 119	syl2anc 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	111, 116, 118, 120	mpbir3and 1197	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
122	105, 121	sseldd 3445	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
123	79, 113, 45	syl2anc 671	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124		simprlr 778	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
125		simprr 771	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
126		eqid 2462	. . . . . . . . . . . . . . . . . . 19
127	78, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 98, 99, 122, 123, 124, 125, 126	lhop1lem 23014	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
128	2	rpcnd 11372	. . . . . . . . . . . . . . . . . . . 20 $/\$
129		2cnd 10710	. . . . . . . . . . . . . . . . . . . 20 $/\$
130		2ne0 10730	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	128, 129, 131	divcan2d 10413	. . . . . . . . . . . . . . . . . . 19 $/\$
133	132	adantr 471	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
134	127, 133	breqtrd 4441	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
135	134	expr 624	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136	77, 135	sylbid 223	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
137	75, 136	syl5bi 225	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
138	137	expr 624	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	53, 138	sylbid 223	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
140	139	expdimp 443	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
141		fveq2 5888	. . . . . . . . . . . . . . . . . 18
142		fveq2 5888	. . . . . . . . . . . . . . . . . 18
143	141, 142	oveq12d 6333	. . . . . . . . . . . . . . . . 17
144		eqid 2462	. . . . . . . . . . . . . . . . 17
145		ovex 6343	. . . . . . . . . . . . . . . . 17
146	143, 144, 145	fvmpt3i 5976	. . . . . . . . . . . . . . . 16
147	146	oveq1d 6330	. . . . . . . . . . . . . . 15
148	147	fveq2d 5892	. . . . . . . . . . . . . 14
149	148	breq1d 4426	. . . . . . . . . . . . 13
150	149	imbi2d 322	. . . . . . . . . . . 12 $/\$ $/\$
151	150	adantl 472	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
152	140, 151	sylibrd 242	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
153	152	adantld 473	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
154	153	com23 81	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
155	154	ralrimdva 2818	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
156	155	reximdva 2874	. . . . . 6 $/\$ $/\$ $/\$
157	8, 156	syld 45	. . . . 5 $/\$ $/\$ $/\$
158	157	ralrimdva 2818	. . . 4 $/\$ $/\$
159	158	anim2d 573	. . 3 $/\$ $/\$ $/\$ $/\$
160		dvf 22911	. . . . . . . 8
161	86	feq2d 5737	. . . . . . . 8
162	160, 161	mpbii 216	. . . . . . 7
163	162	ffvelrnda 6045	. . . . . 6 $/\$
164		dvf 22911	. . . . . . . 8
165	88	feq2d 5737	. . . . . . . 8
166	164, 165	mpbii 216	. . . . . . 7
167	166	ffvelrnda 6045	. . . . . 6 $/\$
168	96	adantr 471	. . . . . . 7 $/\$
169		ffn 5751	. . . . . . . . . . 11
170	166, 169	syl 17	. . . . . . . . . 10
171		fnfvelrn 6042	. . . . . . . . . 10 $/\$
172	170, 171	sylan 478	. . . . . . . . 9 $/\$
173		eleq1 2528	. . . . . . . . 9
174	172, 173	syl5ibcom 228	. . . . . . . 8 $/\$
175	174	necon3bd 2650	. . . . . . 7 $/\$
176	168, 175	mpd 15	. . . . . 6 $/\$
177	163, 167, 176	divcld 10411	. . . . 5 $/\$
178	177, 63	fmptd 6069	. . . 4
179		ax-resscn 9622	. . . . . 6
180	14, 179	sstri 3453	. . . . 5
181	180	a1i 11	. . . 4
182	17	recnd 9695	. . . 4
183	178, 181, 182	ellimc3 22883	. . 3 lim $/\$ $/\$
184	82	ffvelrnda 6045	. . . . . . 7 $/\$
185	184	recnd 9695	. . . . . 6 $/\$
186	84	ffvelrnda 6045	. . . . . . 7 $/\$
187	186	recnd 9695	. . . . . 6 $/\$
188	94	adantr 471	. . . . . . 7 $/\$
189		ffn 5751	. . . . . . . . . . 11
190	84, 189	syl 17	. . . . . . . . . 10
191		fnfvelrn 6042	. . . . . . . . . 10 $/\$
192	190, 191	sylan 478	. . . . . . . . 9 $/\$
193		eleq1 2528	. . . . . . . . 9
194	192, 193	syl5ibcom 228	. . . . . . . 8 $/\$
195	194	necon3bd 2650	. . . . . . 7 $/\$
196	188, 195	mpd 15	. . . . . 6 $/\$
197	185, 187, 196	divcld 10411	. . . . 5 $/\$
198	197, 144	fmptd 6069	. . . 4
199	198, 181, 182	ellimc3 22883	. . 3 lim $/\$ $/\$
200	159, 183, 199	3imtr4d 276	. 2 lim lim
201	1, 200	mpd 15	1 lim

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 375 $/\$ w3a 991

wceq 1455

wcel 1898

wne 2633

wral 2749

wrex 2750

crab 2753

cin 3415

wss 3416

cif 3893 class class class wbr 4416

cmpt 4475

cdm 4853

crn 4854

wfn 5596

wf 5597

cfv 5601 (class class class)co 6315

cc 9563

cr 9564

cc0 9565

caddc 9568

cmul 9570

cxr 9700

clt 9701

cle 9702

cmin 9886

cdiv 10297

c2 10687

crp 11331

cioo 11664

cioc 11665

cabs 13346 lim

climc 22866

cdv 22867

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4529 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-inf2 8172 ax-cnex 9621 ax-resscn 9622 ax-1cn 9623 ax-icn 9624 ax-addcl 9625 ax-addrcl 9626 ax-mulcl 9627 ax-mulrcl 9628 ax-mulcom 9629 ax-addass 9630 ax-mulass 9631 ax-distr 9632 ax-i2m1 9633 ax-1ne0 9634 ax-1rid 9635 ax-rnegex 9636 ax-rrecex 9637 ax-cnre 9638 ax-pre-lttri 9639 ax-pre-lttrn 9640 ax-pre-ltadd 9641 ax-pre-mulgt0 9642 ax-pre-sup 9643 ax-addf 9644 ax-mulf 9645

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-iin 4295 df-br 4417 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 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 6277 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-of 6558 df-om 6720 df-1st 6820 df-2nd 6821 df-supp 6942 df-wrecs 7054 df-recs 7116 df-rdg 7154 df-1o 7208 df-2o 7209 df-oadd 7212 df-er 7389 df-map 7500 df-pm 7501 df-ixp 7549 df-en 7596 df-dom 7597 df-sdom 7598 df-fin 7599 df-fsupp 7910 df-fi 7951 df-sup 7982 df-inf 7983 df-oi 8051 df-card 8399 df-cda 8624 df-pnf 9703 df-mnf 9704 df-xr 9705 df-ltxr 9706 df-le 9707 df-sub 9888 df-neg 9889 df-div 10298 df-nn 10638 df-2 10696 df-3 10697 df-4 10698 df-5 10699 df-6 10700 df-7 10701 df-8 10702 df-9 10703 df-10 10704 df-n0 10899 df-z 10967 df-dec 11081 df-uz 11189 df-q 11294 df-rp 11332 df-xneg 11438 df-xadd 11439 df-xmul 11440 df-ioo 11668 df-ioc 11669 df-ico 11670 df-icc 11671 df-fz 11814 df-fzo 11947 df-seq 12246 df-exp 12305 df-hash 12548 df-cj 13211 df-re 13212 df-im 13213 df-sqrt 13347 df-abs 13348 df-struct 15172 df-ndx 15173 df-slot 15174 df-base 15175 df-sets 15176 df-ress 15177 df-plusg 15252 df-mulr 15253 df-starv 15254 df-sca 15255 df-vsca 15256 df-ip 15257 df-tset 15258 df-ple 15259 df-ds 15261 df-unif 15262 df-hom 15263 df-cco 15264 df-rest 15370 df-topn 15371 df-0g 15389 df-gsum 15390 df-topgen 15391 df-pt 15392 df-prds 15395 df-xrs 15449 df-qtop 15455 df-imas 15456 df-xps 15459 df-mre 15541 df-mrc 15542 df-acs 15544 df-mgm 16537 df-sgrp 16576 df-mnd 16586 df-submnd 16632 df-mulg 16725 df-cntz 17020 df-cmn 17481 df-psmet 19011 df-xmet 19012 df-met 19013 df-bl 19014 df-mopn 19015 df-fbas 19016 df-fg 19017 df-cnfld 19020 df-top 19970 df-bases 19971 df-topon 19972 df-topsp 19973 df-cld 20083 df-ntr 20084 df-cls 20085 df-nei 20163 df-lp 20201 df-perf 20202 df-cn 20292 df-cnp 20293 df-haus 20380 df-cmp 20451 df-tx 20626 df-hmeo 20819 df-fil 20910 df-fm 21002 df-flim 21003 df-flf 21004 df-xms 21384 df-ms 21385 df-tms 21386 df-cncf 21959 df-limc 22870 df-dv 22871

This theorem is referenced by: lhop2 23016 lhop 23017 fourierdlem61 38069

W3C validator