lhop1 - Metamath Proof Explorer

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

Theorem lhop1 22150

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 11264	. . . . . . 7 $/\$
4		breq2 4451	. . . . . . . . . 10
5	4	imbi2d 316	. . . . . . . . 9 $/\$ $/\$
6	5	rexralbidv 2981	. . . . . . . 8 $/\$ $/\$
7	6	rspcv 3210	. . . . . . 7 $/\$ $/\$
8	3, 7	syl 16	. . . . . 6 $/\$ $/\$ $/\$
9		rabid 3038	. . . . . . . . . . . . . 14 $/\$
10		eliooord 11580	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
11	10	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
12	11	simprd 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
13	12	biantrurd 508	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
14		ioossre 11582	. . . . . . . . . . . . . . . . . . . . 21
15		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
16	14, 15	sseldi 3502	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
17		lhop1.a	. . . . . . . . . . . . . . . . . . . . 21
18	17	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
19		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
20	19	rpred 11252	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
21	20	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
22	16, 18, 21	ltsubaddd 10144	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
23	16	rexrd 9639	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
24		lhop1.b	. . . . . . . . . . . . . . . . . . . . 21
25	24	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
26	17	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	20, 26	readdcld 9619	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
28	27	rexrd 9639	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
29	28	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
30		xrltmin 11379	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
31	23, 25, 29, 30	syl3anc 1228	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
32	13, 22, 31	3bitr4rd 286	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
33	18	rexrd 9639	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
34		ifcl 3981	. . . . . . . . . . . . . . . . . . . 20 $/\$
35	25, 29, 34	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
36	11	simpld 459	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
37		elioo5 11578	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
38	37	baibd 907	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
39	33, 35, 23, 36, 38	syl31anc 1231	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
40	18, 16, 36	ltled 9728	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
41	18, 16, 40	abssubge0d 13222	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
42	41	breq1d 4457	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
43	32, 39, 42	3bitr4d 285	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
44	43	rabbi2dva 3706	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	24	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
46		xrmin1 11374	. . . . . . . . . . . . . . . . . . 19 $/\$
47	45, 28, 46	syl2anc 661	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
48		iooss2 11561	. . . . . . . . . . . . . . . . . 18 $/\$
49	45, 47, 48	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
50		dfss1 3703	. . . . . . . . . . . . . . . . 17
51	49, 50	sylib 196	. . . . . . . . . . . . . . . 16 $/\$ $/\$
52	44, 51	eqtr3d 2510	. . . . . . . . . . . . . . 15 $/\$ $/\$
53	52	eleq2d 2537	. . . . . . . . . . . . . 14 $/\$ $/\$
54	9, 53	syl5bbr 259	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
55		lbioo 11556	. . . . . . . . . . . . . . . . . . . . . 22
56		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . 22
57	55, 56	mtbiri 303	. . . . . . . . . . . . . . . . . . . . 21
58	57	necon2ai 2702	. . . . . . . . . . . . . . . . . . . 20
59	58	biantrurd 508	. . . . . . . . . . . . . . . . . . 19 $/\$
60	59	bicomd 201	. . . . . . . . . . . . . . . . . 18 $/\$
61		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . 23
62		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . 23
63	61, 62	oveq12d 6300	. . . . . . . . . . . . . . . . . . . . . 22
64		eqid 2467	. . . . . . . . . . . . . . . . . . . . . 22
65		ovex 6307	. . . . . . . . . . . . . . . . . . . . . 22
66	63, 64, 65	fvmpt3i 5952	. . . . . . . . . . . . . . . . . . . . 21
67	66	oveq1d 6297	. . . . . . . . . . . . . . . . . . . 20
68	67	fveq2d 5868	. . . . . . . . . . . . . . . . . . 19
69	68	breq1d 4457	. . . . . . . . . . . . . . . . . 18
70	60, 69	imbi12d 320	. . . . . . . . . . . . . . . . 17 $/\$
71	70	ralbiia 2894	. . . . . . . . . . . . . . . 16 $/\$
72		oveq1 6289	. . . . . . . . . . . . . . . . . . 19
73	72	fveq2d 5868	. . . . . . . . . . . . . . . . . 18
74	73	breq1d 4457	. . . . . . . . . . . . . . . . 17
75	74	ralrab 3265	. . . . . . . . . . . . . . . 16
76	71, 75	bitr4i 252	. . . . . . . . . . . . . . 15 $/\$
77	52	adantrr 716	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
78	77	raleqdv 3064	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
79	17	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
80	24	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
81		lhop1.l	. . . . . . . . . . . . . . . . . . . 20
82	81	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
83		lhop1.f	. . . . . . . . . . . . . . . . . . . 20
84	83	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
85		lhop1.g	. . . . . . . . . . . . . . . . . . . 20
86	85	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
87		lhop1.if	. . . . . . . . . . . . . . . . . . . 20
88	87	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
89		lhop1.ig	. . . . . . . . . . . . . . . . . . . 20
90	89	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
91		lhop1.f0	. . . . . . . . . . . . . . . . . . . 20 lim
92	91	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
93		lhop1.g0	. . . . . . . . . . . . . . . . . . . 20 lim
94	93	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
95		lhop1.gn0	. . . . . . . . . . . . . . . . . . . 20
96	95	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
97		lhop1.gd0	. . . . . . . . . . . . . . . . . . . 20
98	97	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
99	1	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ lim
100	3	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
101	79	rexrd 9639	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
102		simprll 761	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
103	102	rpred 11252	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
104	103, 79	readdcld 9619	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
105		iocssre 11600	. . . . . . . . . . . . . . . . . . . . 21 $/\$
106	101, 104, 105	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
107	80	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
108	103	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
109	79	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
110	108, 109	readdcld 9619	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
111	110	rexrd 9639	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
112	107, 111	ifclda 3971	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
113	79, 102	ltaddrp2d 11282	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
114	104	rexrd 9639	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
115		xrltmin 11379	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
116	101, 80, 114, 115	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
117	82, 113, 116	mpbir2and 920	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
118		xrmin2 11375	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
119	80, 114, 118	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
120		elioc1 11567	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
121	101, 114, 120	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	112, 117, 119, 121	mpbir3and 1179	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
123	106, 122	sseldd 3505	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
124	80, 114, 46	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
125		simprlr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
126		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
127		eqid 2467	. . . . . . . . . . . . . . . . . . 19
128	79, 80, 82, 84, 86, 88, 90, 92, 94, 96, 98, 99, 100, 123, 124, 125, 126, 127	lhop1lem 22149	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
129	2	rpcnd 11254	. . . . . . . . . . . . . . . . . . . 20 $/\$
130		2cnd 10604	. . . . . . . . . . . . . . . . . . . 20 $/\$
131		2ne0 10624	. . . . . . . . . . . . . . . . . . . . 21
132	131	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
133	129, 130, 132	divcan2d 10318	. . . . . . . . . . . . . . . . . . 19 $/\$
134	133	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
135	128, 134	breqtrd 4471	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
136	135	expr 615	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	78, 136	sylbid 215	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
138	76, 137	syl5bi 217	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
139	138	expr 615	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140	54, 139	sylbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
141	140	expdimp 437	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
142		fveq2 5864	. . . . . . . . . . . . . . . . . 18
143		fveq2 5864	. . . . . . . . . . . . . . . . . 18
144	142, 143	oveq12d 6300	. . . . . . . . . . . . . . . . 17
145		eqid 2467	. . . . . . . . . . . . . . . . 17
146		ovex 6307	. . . . . . . . . . . . . . . . 17
147	144, 145, 146	fvmpt3i 5952	. . . . . . . . . . . . . . . 16
148	147	oveq1d 6297	. . . . . . . . . . . . . . 15
149	148	fveq2d 5868	. . . . . . . . . . . . . 14
150	149	breq1d 4457	. . . . . . . . . . . . 13
151	150	imbi2d 316	. . . . . . . . . . . 12 $/\$ $/\$
152	151	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
153	141, 152	sylibrd 234	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
154	153	adantld 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
155	154	com23 78	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
156	155	ralrimdva 2882	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
157	156	reximdva 2938	. . . . . 6 $/\$ $/\$ $/\$
158	8, 157	syld 44	. . . . 5 $/\$ $/\$ $/\$
159	158	ralrimdva 2882	. . . 4 $/\$ $/\$
160	159	anim2d 565	. . 3 $/\$ $/\$ $/\$ $/\$
161		dvf 22046	. . . . . . . 8
162	87	feq2d 5716	. . . . . . . 8
163	161, 162	mpbii 211	. . . . . . 7
164	163	ffvelrnda 6019	. . . . . 6 $/\$
165		dvf 22046	. . . . . . . 8
166	89	feq2d 5716	. . . . . . . 8
167	165, 166	mpbii 211	. . . . . . 7
168	167	ffvelrnda 6019	. . . . . 6 $/\$
169	97	adantr 465	. . . . . . 7 $/\$
170		ffn 5729	. . . . . . . . . . 11
171	167, 170	syl 16	. . . . . . . . . 10
172		fnfvelrn 6016	. . . . . . . . . 10 $/\$
173	171, 172	sylan 471	. . . . . . . . 9 $/\$
174		eleq1 2539	. . . . . . . . 9
175	173, 174	syl5ibcom 220	. . . . . . . 8 $/\$
176	175	necon3bd 2679	. . . . . . 7 $/\$
177	169, 176	mpd 15	. . . . . 6 $/\$
178	164, 168, 177	divcld 10316	. . . . 5 $/\$
179	178, 64	fmptd 6043	. . . 4
180		ax-resscn 9545	. . . . . 6
181	14, 180	sstri 3513	. . . . 5
182	181	a1i 11	. . . 4
183	17	recnd 9618	. . . 4
184	179, 182, 183	ellimc3 22018	. . 3 lim $/\$ $/\$
185	83	ffvelrnda 6019	. . . . . . 7 $/\$
186	185	recnd 9618	. . . . . 6 $/\$
187	85	ffvelrnda 6019	. . . . . . 7 $/\$
188	187	recnd 9618	. . . . . 6 $/\$
189	95	adantr 465	. . . . . . 7 $/\$
190		ffn 5729	. . . . . . . . . . 11
191	85, 190	syl 16	. . . . . . . . . 10
192		fnfvelrn 6016	. . . . . . . . . 10 $/\$
193	191, 192	sylan 471	. . . . . . . . 9 $/\$
194		eleq1 2539	. . . . . . . . 9
195	193, 194	syl5ibcom 220	. . . . . . . 8 $/\$
196	195	necon3bd 2679	. . . . . . 7 $/\$
197	189, 196	mpd 15	. . . . . 6 $/\$
198	186, 188, 197	divcld 10316	. . . . 5 $/\$
199	198, 145	fmptd 6043	. . . 4
200	199, 182, 183	ellimc3 22018	. . 3 lim $/\$ $/\$
201	160, 184, 200	3imtr4d 268	. 2 lim lim
202	1, 201	mpd 15	1 lim

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1379

wcel 1767

wne 2662

wral 2814

wrex 2815

crab 2818

cin 3475

wss 3476

cif 3939 class class class wbr 4447

cmpt 4505

cdm 4999

crn 5000

wfn 5581

wf 5582

cfv 5586 (class class class)co 6282

cc 9486

cr 9487

cc0 9488

caddc 9491

cmul 9493

cxr 9623

clt 9624

cle 9625

cmin 9801

cdiv 10202

c2 10581

crp 11216

cioo 11525

cioc 11526

cabs 13026 lim

climc 22001

cdv 22002

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-om 6679 df-1st 6781 df-2nd 6782 df-supp 6899 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-ixp 7467 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fsupp 7826 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 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 10973 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ioc 11530 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-seq 12072 df-exp 12131 df-hash 12370 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-struct 14488 df-ndx 14489 df-slot 14490 df-base 14491 df-sets 14492 df-ress 14493 df-plusg 14564 df-mulr 14565 df-starv 14566 df-sca 14567 df-vsca 14568 df-ip 14569 df-tset 14570 df-ple 14571 df-ds 14573 df-unif 14574 df-hom 14575 df-cco 14576 df-rest 14674 df-topn 14675 df-0g 14693 df-gsum 14694 df-topgen 14695 df-pt 14696 df-prds 14699 df-xrs 14753 df-qtop 14758 df-imas 14759 df-xps 14761 df-mre 14837 df-mrc 14838 df-acs 14840 df-mnd 15728 df-submnd 15778 df-mulg 15861 df-cntz 16150 df-cmn 16596 df-psmet 18182 df-xmet 18183 df-met 18184 df-bl 18185 df-mopn 18186 df-fbas 18187 df-fg 18188 df-cnfld 18192 df-top 19166 df-bases 19168 df-topon 19169 df-topsp 19170 df-cld 19286 df-ntr 19287 df-cls 19288 df-nei 19365 df-lp 19403 df-perf 19404 df-cn 19494 df-cnp 19495 df-haus 19582 df-cmp 19653 df-tx 19798 df-hmeo 19991 df-fil 20082 df-fm 20174 df-flim 20175 df-flf 20176 df-xms 20558 df-ms 20559 df-tms 20560 df-cncf 21117 df-limc 22005 df-dv 22006

This theorem is referenced by: lhop2 22151 lhop 22152 fourierdlem61 31468

W3C validator