lhop1 - Metamath Proof Explorer

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

Theorem lhop1 22584

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 459	. . . . . . . 8 $/\$
3	2	rphalfcld 11271	. . . . . . 7 $/\$
4		breq2 4443	. . . . . . . . . 10
5	4	imbi2d 314	. . . . . . . . 9 $/\$ $/\$
6	5	rexralbidv 2973	. . . . . . . 8 $/\$ $/\$
7	6	rspcv 3203	. . . . . . 7 $/\$ $/\$
8	3, 7	syl 16	. . . . . 6 $/\$ $/\$ $/\$
9		rabid 3031	. . . . . . . . . . . . . 14 $/\$
10		eliooord 11587	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
11	10	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
12	11	simprd 461	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
13	12	biantrurd 506	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
14		ioossre 11589	. . . . . . . . . . . . . . . . . . . . 21
15		simpr 459	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
16	14, 15	sseldi 3487	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
17		lhop1.a	. . . . . . . . . . . . . . . . . . . . 21
18	17	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
19		simpr 459	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
20	19	rpred 11259	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
21	20	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
22	16, 18, 21	ltsubaddd 10144	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
23	16	rexrd 9632	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
24		lhop1.b	. . . . . . . . . . . . . . . . . . . . 21
25	24	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	17	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	20, 26	readdcld 9612	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	27	rexrd 9632	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
29	28	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
30		xrltmin 11386	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
31	23, 25, 29, 30	syl3anc 1226	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
32	13, 22, 31	3bitr4rd 286	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
33	18	rexrd 9632	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
34	25, 29	ifcld 3972	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
35	11	simpld 457	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
36		elioo5 11585	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
37	36	baibd 907	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
38	33, 34, 23, 35, 37	syl31anc 1229	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
39	18, 16, 35	ltled 9722	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
40	18, 16, 39	abssubge0d 13348	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
41	40	breq1d 4449	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
42	32, 38, 41	3bitr4d 285	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
43	42	rabbi2dva 3692	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44	24	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
45		xrmin1 11381	. . . . . . . . . . . . . . . . . . 19 $/\$
46	44, 28, 45	syl2anc 659	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
47		iooss2 11568	. . . . . . . . . . . . . . . . . 18 $/\$
48	44, 46, 47	syl2anc 659	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
49		dfss1 3689	. . . . . . . . . . . . . . . . 17
50	48, 49	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51	43, 50	eqtr3d 2497	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	51	eleq2d 2524	. . . . . . . . . . . . . 14 $/\$ $/\$
53	9, 52	syl5bbr 259	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
54		lbioo 11563	. . . . . . . . . . . . . . . . . . . . . 22
55		eleq1 2526	. . . . . . . . . . . . . . . . . . . . . 22
56	54, 55	mtbiri 301	. . . . . . . . . . . . . . . . . . . . 21
57	56	necon2ai 2689	. . . . . . . . . . . . . . . . . . . 20
58	57	biantrurd 506	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	bicomd 201	. . . . . . . . . . . . . . . . . 18 $/\$
60		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . 23
61		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . 23
62	60, 61	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . . 22
63		eqid 2454	. . . . . . . . . . . . . . . . . . . . . 22
64		ovex 6298	. . . . . . . . . . . . . . . . . . . . . 22
65	62, 63, 64	fvmpt3i 5935	. . . . . . . . . . . . . . . . . . . . 21
66	65	oveq1d 6285	. . . . . . . . . . . . . . . . . . . 20
67	66	fveq2d 5852	. . . . . . . . . . . . . . . . . . 19
68	67	breq1d 4449	. . . . . . . . . . . . . . . . . 18
69	59, 68	imbi12d 318	. . . . . . . . . . . . . . . . 17 $/\$
70	69	ralbiia 2884	. . . . . . . . . . . . . . . 16 $/\$
71		oveq1 6277	. . . . . . . . . . . . . . . . . . 19
72	71	fveq2d 5852	. . . . . . . . . . . . . . . . . 18
73	72	breq1d 4449	. . . . . . . . . . . . . . . . 17
74	73	ralrab 3258	. . . . . . . . . . . . . . . 16
75	70, 74	bitr4i 252	. . . . . . . . . . . . . . 15 $/\$
76	51	adantrr 714	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
77	76	raleqdv 3057	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
78	17	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
79	24	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
80		lhop1.l	. . . . . . . . . . . . . . . . . . . 20
81	80	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
82		lhop1.f	. . . . . . . . . . . . . . . . . . . 20
83	82	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
84		lhop1.g	. . . . . . . . . . . . . . . . . . . 20
85	84	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
86		lhop1.if	. . . . . . . . . . . . . . . . . . . 20
87	86	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
88		lhop1.ig	. . . . . . . . . . . . . . . . . . . 20
89	88	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
90		lhop1.f0	. . . . . . . . . . . . . . . . . . . 20 lim
91	90	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
92		lhop1.g0	. . . . . . . . . . . . . . . . . . . 20 lim
93	92	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
94		lhop1.gn0	. . . . . . . . . . . . . . . . . . . 20
95	94	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
96		lhop1.gd0	. . . . . . . . . . . . . . . . . . . 20
97	96	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
98	1	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
99	3	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
100	78	rexrd 9632	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
101		simprll 761	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
102	101	rpred 11259	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
103	102, 78	readdcld 9612	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
104		iocssre 11607	. . . . . . . . . . . . . . . . . . . . 21 $/\$
105	100, 103, 104	syl2anc 659	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
106	79	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
107	102	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
108	78	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
109	107, 108	readdcld 9612	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
110	109	rexrd 9632	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
111	106, 110	ifclda 3961	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
112	78, 101	ltaddrp2d 11289	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
113	103	rexrd 9632	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
114		xrltmin 11386	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
115	100, 79, 113, 114	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
116	81, 112, 115	mpbir2and 920	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
117		xrmin2 11382	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118	79, 113, 117	syl2anc 659	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
119		elioc1 11574	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	100, 113, 119	syl2anc 659	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	111, 116, 118, 120	mpbir3and 1177	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
122	105, 121	sseldd 3490	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
123	79, 113, 45	syl2anc 659	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124		simprlr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
125		simprr 755	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
126		eqid 2454	. . . . . . . . . . . . . . . . . . 19
127	78, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 98, 99, 122, 123, 124, 125, 126	lhop1lem 22583	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
128	2	rpcnd 11261	. . . . . . . . . . . . . . . . . . . 20 $/\$
129		2cnd 10604	. . . . . . . . . . . . . . . . . . . 20 $/\$
130		2ne0 10624	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	128, 129, 131	divcan2d 10318	. . . . . . . . . . . . . . . . . . 19 $/\$
133	132	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
134	127, 133	breqtrd 4463	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
135	134	expr 613	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
136	77, 135	sylbid 215	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
137	75, 136	syl5bi 217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
138	137	expr 613	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139	53, 138	sylbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
140	139	expdimp 435	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
141		fveq2 5848	. . . . . . . . . . . . . . . . . 18
142		fveq2 5848	. . . . . . . . . . . . . . . . . 18
143	141, 142	oveq12d 6288	. . . . . . . . . . . . . . . . 17
144		eqid 2454	. . . . . . . . . . . . . . . . 17
145		ovex 6298	. . . . . . . . . . . . . . . . 17
146	143, 144, 145	fvmpt3i 5935	. . . . . . . . . . . . . . . 16
147	146	oveq1d 6285	. . . . . . . . . . . . . . 15
148	147	fveq2d 5852	. . . . . . . . . . . . . 14
149	148	breq1d 4449	. . . . . . . . . . . . 13
150	149	imbi2d 314	. . . . . . . . . . . 12 $/\$ $/\$
151	150	adantl 464	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
152	140, 151	sylibrd 234	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
153	152	adantld 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
154	153	com23 78	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
155	154	ralrimdva 2872	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
156	155	reximdva 2929	. . . . . 6 $/\$ $/\$ $/\$
157	8, 156	syld 44	. . . . 5 $/\$ $/\$ $/\$
158	157	ralrimdva 2872	. . . 4 $/\$ $/\$
159	158	anim2d 563	. . 3 $/\$ $/\$ $/\$ $/\$
160		dvf 22480	. . . . . . . 8
161	86	feq2d 5700	. . . . . . . 8
162	160, 161	mpbii 211	. . . . . . 7
163	162	ffvelrnda 6007	. . . . . 6 $/\$
164		dvf 22480	. . . . . . . 8
165	88	feq2d 5700	. . . . . . . 8
166	164, 165	mpbii 211	. . . . . . 7
167	166	ffvelrnda 6007	. . . . . 6 $/\$
168	96	adantr 463	. . . . . . 7 $/\$
169		ffn 5713	. . . . . . . . . . 11
170	166, 169	syl 16	. . . . . . . . . 10
171		fnfvelrn 6004	. . . . . . . . . 10 $/\$
172	170, 171	sylan 469	. . . . . . . . 9 $/\$
173		eleq1 2526	. . . . . . . . 9
174	172, 173	syl5ibcom 220	. . . . . . . 8 $/\$
175	174	necon3bd 2666	. . . . . . 7 $/\$
176	168, 175	mpd 15	. . . . . 6 $/\$
177	163, 167, 176	divcld 10316	. . . . 5 $/\$
178	177, 63	fmptd 6031	. . . 4
179		ax-resscn 9538	. . . . . 6
180	14, 179	sstri 3498	. . . . 5
181	180	a1i 11	. . . 4
182	17	recnd 9611	. . . 4
183	178, 181, 182	ellimc3 22452	. . 3 lim $/\$ $/\$
184	82	ffvelrnda 6007	. . . . . . 7 $/\$
185	184	recnd 9611	. . . . . 6 $/\$
186	84	ffvelrnda 6007	. . . . . . 7 $/\$
187	186	recnd 9611	. . . . . 6 $/\$
188	94	adantr 463	. . . . . . 7 $/\$
189		ffn 5713	. . . . . . . . . . 11
190	84, 189	syl 16	. . . . . . . . . 10
191		fnfvelrn 6004	. . . . . . . . . 10 $/\$
192	190, 191	sylan 469	. . . . . . . . 9 $/\$
193		eleq1 2526	. . . . . . . . 9
194	192, 193	syl5ibcom 220	. . . . . . . 8 $/\$
195	194	necon3bd 2666	. . . . . . 7 $/\$
196	188, 195	mpd 15	. . . . . 6 $/\$
197	185, 187, 196	divcld 10316	. . . . 5 $/\$
198	197, 144	fmptd 6031	. . . 4
199	198, 181, 182	ellimc3 22452	. . 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 367 $/\$ w3a 971

wceq 1398

wcel 1823

wne 2649

wral 2804

wrex 2805

crab 2808

cin 3460

wss 3461

cif 3929 class class class wbr 4439

cmpt 4497

cdm 4988

crn 4989

wfn 5565

wf 5566

cfv 5570 (class class class)co 6270

cc 9479

cr 9480

cc0 9481

caddc 9484

cmul 9486

cxr 9616

clt 9617

cle 9618

cmin 9796

cdiv 10202

c2 10581

crp 11221

cioo 11532

cioc 11533

cabs 13152 lim

climc 22435

cdv 22436

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-inf2 8049 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559 ax-addf 9560 ax-mulf 9561

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-iin 4318 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-se 4828 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-isom 5579 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-of 6513 df-om 6674 df-1st 6773 df-2nd 6774 df-supp 6892 df-recs 7034 df-rdg 7068 df-1o 7122 df-2o 7123 df-oadd 7126 df-er 7303 df-map 7414 df-pm 7415 df-ixp 7463 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-fsupp 7822 df-fi 7863 df-sup 7893 df-oi 7927 df-card 8311 df-cda 8539 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-div 10203 df-nn 10532 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10977 df-uz 11083 df-q 11184 df-rp 11222 df-xneg 11321 df-xadd 11322 df-xmul 11323 df-ioo 11536 df-ioc 11537 df-ico 11538 df-icc 11539 df-fz 11676 df-fzo 11800 df-seq 12093 df-exp 12152 df-hash 12391 df-cj 13017 df-re 13018 df-im 13019 df-sqrt 13153 df-abs 13154 df-struct 14721 df-ndx 14722 df-slot 14723 df-base 14724 df-sets 14725 df-ress 14726 df-plusg 14800 df-mulr 14801 df-starv 14802 df-sca 14803 df-vsca 14804 df-ip 14805 df-tset 14806 df-ple 14807 df-ds 14809 df-unif 14810 df-hom 14811 df-cco 14812 df-rest 14915 df-topn 14916 df-0g 14934 df-gsum 14935 df-topgen 14936 df-pt 14937 df-prds 14940 df-xrs 14994 df-qtop 14999 df-imas 15000 df-xps 15002 df-mre 15078 df-mrc 15079 df-acs 15081 df-mgm 16074 df-sgrp 16113 df-mnd 16123 df-submnd 16169 df-mulg 16262 df-cntz 16557 df-cmn 17002 df-psmet 18609 df-xmet 18610 df-met 18611 df-bl 18612 df-mopn 18613 df-fbas 18614 df-fg 18615 df-cnfld 18619 df-top 19569 df-bases 19571 df-topon 19572 df-topsp 19573 df-cld 19690 df-ntr 19691 df-cls 19692 df-nei 19769 df-lp 19807 df-perf 19808 df-cn 19898 df-cnp 19899 df-haus 19986 df-cmp 20057 df-tx 20232 df-hmeo 20425 df-fil 20516 df-fm 20608 df-flim 20609 df-flf 20610 df-xms 20992 df-ms 20993 df-tms 20994 df-cncf 21551 df-limc 22439 df-dv 22440

This theorem is referenced by: lhop2 22585 lhop 22586 fourierdlem61 32192

W3C validator