lhop1 - Metamath Proof Explorer

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

Theorem lhop1 22285

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 11274	. . . . . . 7 $/\$
4		breq2 4438	. . . . . . . . . 10
5	4	imbi2d 316	. . . . . . . . 9 $/\$ $/\$
6	5	rexralbidv 2960	. . . . . . . 8 $/\$ $/\$
7	6	rspcv 3190	. . . . . . 7 $/\$ $/\$
8	3, 7	syl 16	. . . . . 6 $/\$ $/\$ $/\$
9		rabid 3018	. . . . . . . . . . . . . 14 $/\$
10		eliooord 11590	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
11	10	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
12	11	simprd 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
13	12	biantrurd 508	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
14		ioossre 11592	. . . . . . . . . . . . . . . . . . . . 21
15		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
16	14, 15	sseldi 3485	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
17		lhop1.a	. . . . . . . . . . . . . . . . . . . . 21
18	17	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
19		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
20	19	rpred 11262	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
21	20	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
22	16, 18, 21	ltsubaddd 10151	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
23	16	rexrd 9643	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
24		lhop1.b	. . . . . . . . . . . . . . . . . . . . 21
25	24	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	17	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	20, 26	readdcld 9623	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	27	rexrd 9643	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
29	28	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
30		xrltmin 11389	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
31	23, 25, 29, 30	syl3anc 1227	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
32	13, 22, 31	3bitr4rd 286	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
33	18	rexrd 9643	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
34	25, 29	ifcld 3966	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
35	11	simpld 459	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
36		elioo5 11588	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
37	36	baibd 907	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
38	33, 34, 23, 35, 37	syl31anc 1230	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
39	18, 16, 35	ltled 9733	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
40	18, 16, 39	abssubge0d 13239	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
41	40	breq1d 4444	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
42	32, 38, 41	3bitr4d 285	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
43	42	rabbi2dva 3689	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44	24	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
45		xrmin1 11384	. . . . . . . . . . . . . . . . . . 19 $/\$
46	44, 28, 45	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
47		iooss2 11571	. . . . . . . . . . . . . . . . . 18 $/\$
48	44, 46, 47	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
49		dfss1 3686	. . . . . . . . . . . . . . . . 17
50	48, 49	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51	43, 50	eqtr3d 2484	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	51	eleq2d 2511	. . . . . . . . . . . . . 14 $/\$ $/\$
53	9, 52	syl5bbr 259	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
54		lbioo 11566	. . . . . . . . . . . . . . . . . . . . . 22
55		eleq1 2513	. . . . . . . . . . . . . . . . . . . . . 22
56	54, 55	mtbiri 303	. . . . . . . . . . . . . . . . . . . . 21
57	56	necon2ai 2676	. . . . . . . . . . . . . . . . . . . 20
58	57	biantrurd 508	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	bicomd 201	. . . . . . . . . . . . . . . . . 18 $/\$
60		fveq2 5853	. . . . . . . . . . . . . . . . . . . . . . 23
61		fveq2 5853	. . . . . . . . . . . . . . . . . . . . . . 23
62	60, 61	oveq12d 6296	. . . . . . . . . . . . . . . . . . . . . 22
63		eqid 2441	. . . . . . . . . . . . . . . . . . . . . 22
64		ovex 6306	. . . . . . . . . . . . . . . . . . . . . 22
65	62, 63, 64	fvmpt3i 5942	. . . . . . . . . . . . . . . . . . . . 21
66	65	oveq1d 6293	. . . . . . . . . . . . . . . . . . . 20
67	66	fveq2d 5857	. . . . . . . . . . . . . . . . . . 19
68	67	breq1d 4444	. . . . . . . . . . . . . . . . . 18
69	59, 68	imbi12d 320	. . . . . . . . . . . . . . . . 17 $/\$
70	69	ralbiia 2871	. . . . . . . . . . . . . . . 16 $/\$
71		oveq1 6285	. . . . . . . . . . . . . . . . . . 19
72	71	fveq2d 5857	. . . . . . . . . . . . . . . . . 18
73	72	breq1d 4444	. . . . . . . . . . . . . . . . 17
74	73	ralrab 3245	. . . . . . . . . . . . . . . 16
75	70, 74	bitr4i 252	. . . . . . . . . . . . . . 15 $/\$
76	51	adantrr 716	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
77	76	raleqdv 3044	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
78	17	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
79	24	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
80		lhop1.l	. . . . . . . . . . . . . . . . . . . 20
81	80	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
82		lhop1.f	. . . . . . . . . . . . . . . . . . . 20
83	82	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
84		lhop1.g	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
86		lhop1.if	. . . . . . . . . . . . . . . . . . . 20
87	86	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
88		lhop1.ig	. . . . . . . . . . . . . . . . . . . 20
89	88	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
90		lhop1.f0	. . . . . . . . . . . . . . . . . . . 20 lim
91	90	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
92		lhop1.g0	. . . . . . . . . . . . . . . . . . . 20 lim
93	92	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
94		lhop1.gn0	. . . . . . . . . . . . . . . . . . . 20
95	94	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
96		lhop1.gd0	. . . . . . . . . . . . . . . . . . . 20
97	96	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
98	1	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
99	3	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
100	78	rexrd 9643	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
101		simprll 761	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
102	101	rpred 11262	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
103	102, 78	readdcld 9623	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
104		iocssre 11610	. . . . . . . . . . . . . . . . . . . . 21 $/\$
105	100, 103, 104	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
106	79	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
107	102	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
108	78	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
109	107, 108	readdcld 9623	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
110	109	rexrd 9643	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
111	106, 110	ifclda 3955	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
112	78, 101	ltaddrp2d 11292	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
113	103	rexrd 9643	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
114		xrltmin 11389	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
115	100, 79, 113, 114	syl3anc 1227	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
116	81, 112, 115	mpbir2and 920	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
117		xrmin2 11385	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118	79, 113, 117	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
119		elioc1 11577	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	100, 113, 119	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	111, 116, 118, 120	mpbir3and 1178	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
122	105, 121	sseldd 3488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
123	79, 113, 45	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124		simprlr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
125		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
126		eqid 2441	. . . . . . . . . . . . . . . . . . 19
127	78, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 98, 99, 122, 123, 124, 125, 126	lhop1lem 22284	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
128	2	rpcnd 11264	. . . . . . . . . . . . . . . . . . . 20 $/\$
129		2cnd 10611	. . . . . . . . . . . . . . . . . . . 20 $/\$
130		2ne0 10631	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	128, 129, 131	divcan2d 10325	. . . . . . . . . . . . . . . . . . 19 $/\$
133	132	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
134	127, 133	breqtrd 4458	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
135	134	expr 615	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136	77, 135	sylbid 215	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
137	75, 136	syl5bi 217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
138	137	expr 615	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	53, 138	sylbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
140	139	expdimp 437	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
141		fveq2 5853	. . . . . . . . . . . . . . . . . 18
142		fveq2 5853	. . . . . . . . . . . . . . . . . 18
143	141, 142	oveq12d 6296	. . . . . . . . . . . . . . . . 17
144		eqid 2441	. . . . . . . . . . . . . . . . 17
145		ovex 6306	. . . . . . . . . . . . . . . . 17
146	143, 144, 145	fvmpt3i 5942	. . . . . . . . . . . . . . . 16
147	146	oveq1d 6293	. . . . . . . . . . . . . . 15
148	147	fveq2d 5857	. . . . . . . . . . . . . 14
149	148	breq1d 4444	. . . . . . . . . . . . 13
150	149	imbi2d 316	. . . . . . . . . . . 12 $/\$ $/\$
151	150	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
152	140, 151	sylibrd 234	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
153	152	adantld 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
154	153	com23 78	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
155	154	ralrimdva 2859	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
156	155	reximdva 2916	. . . . . 6 $/\$ $/\$ $/\$
157	8, 156	syld 44	. . . . 5 $/\$ $/\$ $/\$
158	157	ralrimdva 2859	. . . 4 $/\$ $/\$
159	158	anim2d 565	. . 3 $/\$ $/\$ $/\$ $/\$
160		dvf 22181	. . . . . . . 8
161	86	feq2d 5705	. . . . . . . 8
162	160, 161	mpbii 211	. . . . . . 7
163	162	ffvelrnda 6013	. . . . . 6 $/\$
164		dvf 22181	. . . . . . . 8
165	88	feq2d 5705	. . . . . . . 8
166	164, 165	mpbii 211	. . . . . . 7
167	166	ffvelrnda 6013	. . . . . 6 $/\$
168	96	adantr 465	. . . . . . 7 $/\$
169		ffn 5718	. . . . . . . . . . 11
170	166, 169	syl 16	. . . . . . . . . 10
171		fnfvelrn 6010	. . . . . . . . . 10 $/\$
172	170, 171	sylan 471	. . . . . . . . 9 $/\$
173		eleq1 2513	. . . . . . . . 9
174	172, 173	syl5ibcom 220	. . . . . . . 8 $/\$
175	174	necon3bd 2653	. . . . . . 7 $/\$
176	168, 175	mpd 15	. . . . . 6 $/\$
177	163, 167, 176	divcld 10323	. . . . 5 $/\$
178	177, 63	fmptd 6037	. . . 4
179		ax-resscn 9549	. . . . . 6
180	14, 179	sstri 3496	. . . . 5
181	180	a1i 11	. . . 4
182	17	recnd 9622	. . . 4
183	178, 181, 182	ellimc3 22153	. . 3 lim $/\$ $/\$
184	82	ffvelrnda 6013	. . . . . . 7 $/\$
185	184	recnd 9622	. . . . . 6 $/\$
186	84	ffvelrnda 6013	. . . . . . 7 $/\$
187	186	recnd 9622	. . . . . 6 $/\$
188	94	adantr 465	. . . . . . 7 $/\$
189		ffn 5718	. . . . . . . . . . 11
190	84, 189	syl 16	. . . . . . . . . 10
191		fnfvelrn 6010	. . . . . . . . . 10 $/\$
192	190, 191	sylan 471	. . . . . . . . 9 $/\$
193		eleq1 2513	. . . . . . . . 9
194	192, 193	syl5ibcom 220	. . . . . . . 8 $/\$
195	194	necon3bd 2653	. . . . . . 7 $/\$
196	188, 195	mpd 15	. . . . . 6 $/\$
197	185, 187, 196	divcld 10323	. . . . 5 $/\$
198	197, 144	fmptd 6037	. . . 4
199	198, 181, 182	ellimc3 22153	. . 3 lim $/\$ $/\$
200	159, 183, 199	3imtr4d 268	. 2 lim lim
201	1, 200	mpd 15	1 lim

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1381

wcel 1802

wne 2636

wral 2791

wrex 2792

crab 2795

cin 3458

wss 3459

cif 3923 class class class wbr 4434

cmpt 4492

cdm 4986

crn 4987

wfn 5570

wf 5571

cfv 5575 (class class class)co 6278

cc 9490

cr 9491

cc0 9492

caddc 9495

cmul 9497

cxr 9627

clt 9628

cle 9629

cmin 9807

cdiv 10209

c2 10588

crp 11226

cioo 11535

cioc 11536

cabs 13043 lim

climc 22136

cdv 22137

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4545 ax-sep 4555 ax-nul 4563 ax-pow 4612 ax-pr 4673 ax-un 6574 ax-inf2 8058 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570 ax-addf 9571 ax-mulf 9572

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3419 df-dif 3462 df-un 3464 df-in 3466 df-ss 3473 df-pss 3475 df-nul 3769 df-if 3924 df-pw 3996 df-sn 4012 df-pr 4014 df-tp 4016 df-op 4018 df-uni 4232 df-int 4269 df-iun 4314 df-iin 4315 df-br 4435 df-opab 4493 df-mpt 4494 df-tr 4528 df-eprel 4778 df-id 4782 df-po 4787 df-so 4788 df-fr 4825 df-se 4826 df-we 4827 df-ord 4868 df-on 4869 df-lim 4870 df-suc 4871 df-xp 4992 df-rel 4993 df-cnv 4994 df-co 4995 df-dm 4996 df-rn 4997 df-res 4998 df-ima 4999 df-iota 5538 df-fun 5577 df-fn 5578 df-f 5579 df-f1 5580 df-fo 5581 df-f1o 5582 df-fv 5583 df-isom 5584 df-riota 6239 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-of 6522 df-om 6683 df-1st 6782 df-2nd 6783 df-supp 6901 df-recs 7041 df-rdg 7075 df-1o 7129 df-2o 7130 df-oadd 7133 df-er 7310 df-map 7421 df-pm 7422 df-ixp 7469 df-en 7516 df-dom 7517 df-sdom 7518 df-fin 7519 df-fsupp 7829 df-fi 7870 df-sup 7900 df-oi 7935 df-card 8320 df-cda 8548 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9809 df-neg 9810 df-div 10210 df-nn 10540 df-2 10597 df-3 10598 df-4 10599 df-5 10600 df-6 10601 df-7 10602 df-8 10603 df-9 10604 df-10 10605 df-n0 10799 df-z 10868 df-dec 10982 df-uz 11088 df-q 11189 df-rp 11227 df-xneg 11324 df-xadd 11325 df-xmul 11326 df-ioo 11539 df-ioc 11540 df-ico 11541 df-icc 11542 df-fz 11679 df-fzo 11801 df-seq 12084 df-exp 12143 df-hash 12382 df-cj 12908 df-re 12909 df-im 12910 df-sqrt 13044 df-abs 13045 df-struct 14508 df-ndx 14509 df-slot 14510 df-base 14511 df-sets 14512 df-ress 14513 df-plusg 14584 df-mulr 14585 df-starv 14586 df-sca 14587 df-vsca 14588 df-ip 14589 df-tset 14590 df-ple 14591 df-ds 14593 df-unif 14594 df-hom 14595 df-cco 14596 df-rest 14694 df-topn 14695 df-0g 14713 df-gsum 14714 df-topgen 14715 df-pt 14716 df-prds 14719 df-xrs 14773 df-qtop 14778 df-imas 14779 df-xps 14781 df-mre 14857 df-mrc 14858 df-acs 14860 df-mgm 15743 df-sgrp 15782 df-mnd 15792 df-submnd 15838 df-mulg 15931 df-cntz 16226 df-cmn 16671 df-psmet 18282 df-xmet 18283 df-met 18284 df-bl 18285 df-mopn 18286 df-fbas 18287 df-fg 18288 df-cnfld 18292 df-top 19269 df-bases 19271 df-topon 19272 df-topsp 19273 df-cld 19390 df-ntr 19391 df-cls 19392 df-nei 19469 df-lp 19507 df-perf 19508 df-cn 19598 df-cnp 19599 df-haus 19686 df-cmp 19757 df-tx 19933 df-hmeo 20126 df-fil 20217 df-fm 20309 df-flim 20310 df-flf 20311 df-xms 20693 df-ms 20694 df-tms 20695 df-cncf 21252 df-limc 22140 df-dv 22141

This theorem is referenced by: lhop2 22286 lhop 22287 fourierdlem61 31839

W3C validator