dvtanlemOLD - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvtanlemOLD		Structured version Unicode version

Theorem dvtanlemOLD 31892

Description: Lemma for dvtan 31893- the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018.) Obsolete version of dvtanlem 31891 as of 3-Jul-2020. (New usage is discouraged.) (Proof modification is discouraged.)

**Assertion**
Ref	Expression
dvtanlemOLD	$\$ ℂ_fld

Proof of Theorem dvtanlemOLD Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cosf 14115	. . . 4
2		ffun 5684	. . . 4
3		difpreima 5960	. . . 4 $\$ $\$
4	1, 2, 3	mp2b 10	. . 3 $\$ $\$
5		fimacnv 5964	. . . . 5
6	1, 5	ax-mp 5	. . . 4
7		0re 9587	. . . . . 6
8		ffn 5682	. . . . . . . . 9
9	1, 8	ax-mp 5	. . . . . . . 8
10		dffn5 5863	. . . . . . . 8
11	9, 10	mpbi 211	. . . . . . 7
12	11	mptiniseg 5284	. . . . . 6
13	7, 12	ax-mp 5	. . . . 5
14		sinhalfpip 23382	. . . . . . . 8
15	14	eqeq1d 2424	. . . . . . 7
16		halfpire 23354	. . . . . . . . . 10
17	16	recni 9599	. . . . . . . . 9
18		addcl 9565	. . . . . . . . 9 $/\$
19	17, 18	mpan 674	. . . . . . . 8
20		sineq0 23411	. . . . . . . 8
21	19, 20	syl 17	. . . . . . 7
22	15, 21	bitr3d 258	. . . . . 6
23	22	rabbiia 3004	. . . . 5
24	13, 23	eqtri 2444	. . . 4
25	6, 24	difeq12i 3517	. . 3 $\$ $\$
26	4, 25	eqtri 2444	. 2 $\$ $\$
27		eqid 2422	. . . . 5 ℂ_fld ℂ_fld
28	27	recld2 21767	. . . 4 ℂ_fld
29		nftru 1671	. . . . . . . . 9
30		nfcv 2563	. . . . . . . . 9
31		nfcv 2563	. . . . . . . . . 10
32		nfrab1 2942	. . . . . . . . . 10
33	31, 32	nfdif 3522	. . . . . . . . 9 $\$
34		eliun 4240	. . . . . . . . . . 11
35		elioore 11610	. . . . . . . . . . . . . . 15
36	35	adantl 467	. . . . . . . . . . . . . 14 $/\$
37		zre 10885	. . . . . . . . . . . . . . . . . . 19
38		pire 23348	. . . . . . . . . . . . . . . . . . . . . . . 24
39		remulcl 9568	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
40	38, 39	mpan 674	. . . . . . . . . . . . . . . . . . . . . . 23
41		resubcl 9882	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
42	40, 16, 41	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22
43	42	rexrd 9634	. . . . . . . . . . . . . . . . . . . . 21
44		peano2re 9750	. . . . . . . . . . . . . . . . . . . . . . . 24
45		remulcl 9568	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
46	38, 44, 45	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . 23
47		resubcl 9882	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
48	46, 16, 47	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22
49	48	rexrd 9634	. . . . . . . . . . . . . . . . . . . . 21
50		elioo2 11621	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
51	43, 49, 50	syl2anc 665	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
52		ltadd2 9682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
53	16, 52	mp3an3 1349	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
54	42, 53	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
55		readdcl 9566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
56	16, 42, 55	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . 26
57		readdcl 9566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
58	16, 57	mpan 674	. . . . . . . . . . . . . . . . . . . . . . . . . 26
59		pipos 23350	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
60	38, 59	pm3.2i 456	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
61		ltdiv1 10413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
62	60, 61	mp3an3 1349	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
63	56, 58, 62	syl2an 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
64		recn 9573	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
65		picn 23349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
66		mulcl 9567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
67	65, 66	mpan 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
68		pncan3 9827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
69	17, 67, 68	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
70	69	oveq1d 6257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
71	7, 59	gtneii 9690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
72		divcan3 10238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
73	65, 71, 72	mp3an23 1352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
74	70, 73	eqtrd 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
75	64, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
76	75	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
77	76	breq1d 4369	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
78	54, 63, 77	3bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
79	38, 45	mpan 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
80	79, 16, 47	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
81		ltadd2 9682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
82	16, 81	mp3an3 1349	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
83	80, 82	sylan2 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
84		readdcl 9566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
85	16, 80, 84	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		ltdiv1 10413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
87	60, 86	mp3an3 1349	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
88	58, 85, 87	syl2an 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
89		recn 9573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
90		mulcl 9567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
91	65, 90	mpan 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92		pncan3 9827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
93	17, 91, 92	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
94	93	oveq1d 6257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
95		divcan3 10238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
96	65, 71, 95	mp3an23 1352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	94, 96	eqtrd 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	89, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100	99	breq2d 4371	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
101	83, 88, 100	3bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
102	44, 101	sylan2 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
103	102	ancoms 454	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
104	78, 103	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
105	104	biimpd 210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
106	105	exp4b 610	. . . . . . . . . . . . . . . . . . . . 21 $/\$
107	106	3impd 1219	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
108	51, 107	sylbid 218	. . . . . . . . . . . . . . . . . . 19 $/\$
109	37, 108	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$
110	109	imp 430	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
111		btwnnz 10956	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
112	111	3expb 1206	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	110, 112	syldan 472	. . . . . . . . . . . . . . . 16 $/\$
114	113	olcd 394	. . . . . . . . . . . . . . 15 $/\$ $\/$
115		ianor 490	. . . . . . . . . . . . . . . 16 $/\$ $\/$
116		rabid 2938	. . . . . . . . . . . . . . . 16 $/\$
117	115, 116	xchnxbir 310	. . . . . . . . . . . . . . 15 $\/$
118	114, 117	sylibr 215	. . . . . . . . . . . . . 14 $/\$
119	36, 118	eldifd 3383	. . . . . . . . . . . . 13 $/\$ $\$
120	119	rexlimiva 2846	. . . . . . . . . . . 12 $\$
121		eldif 3382	. . . . . . . . . . . . . 14 $\$ $/\$
122		recn 9573	. . . . . . . . . . . . . . . . . 18
123	122	biantrurd 510	. . . . . . . . . . . . . . . . 17 $/\$
124	123, 116	syl6bbr 266	. . . . . . . . . . . . . . . 16
125	124	notbid 295	. . . . . . . . . . . . . . 15
126	125	pm5.32i 641	. . . . . . . . . . . . . 14 $/\$ $/\$
127	121, 126	bitr4i 255	. . . . . . . . . . . . 13 $\$ $/\$
128		redivcl 10270	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
129	38, 71, 128	mp3an23 1352	. . . . . . . . . . . . . . . . 17
130	58, 129	syl 17	. . . . . . . . . . . . . . . 16
131	130	flcld 11977	. . . . . . . . . . . . . . 15
132	131	adantr 466	. . . . . . . . . . . . . 14 $/\$
133		simpl 458	. . . . . . . . . . . . . . 15 $/\$
134		flle 11978	. . . . . . . . . . . . . . . . . . 19
135	130, 134	syl 17	. . . . . . . . . . . . . . . . . 18
136	135	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$
137		nelne2 2692	. . . . . . . . . . . . . . . . . . 19 $/\$
138	137	necomd 2650	. . . . . . . . . . . . . . . . . 18 $/\$
139	131, 138	sylan 473	. . . . . . . . . . . . . . . . 17 $/\$
140	131	zred 10984	. . . . . . . . . . . . . . . . . . . 20
141		pirp 23351	. . . . . . . . . . . . . . . . . . . . 21
142	141	a1i 11	. . . . . . . . . . . . . . . . . . . 20
143	140, 130, 142	ltmul2d 11324	. . . . . . . . . . . . . . . . . . 19
144	140, 130	ltlend 9724	. . . . . . . . . . . . . . . . . . 19 $/\$
145		remulcl 9568	. . . . . . . . . . . . . . . . . . . . 21 $/\$
146	38, 140, 145	sylancr 667	. . . . . . . . . . . . . . . . . . . 20
147		remulcl 9568	. . . . . . . . . . . . . . . . . . . . 21 $/\$
148	38, 130, 147	sylancr 667	. . . . . . . . . . . . . . . . . . . 20
149	16	a1i 11	. . . . . . . . . . . . . . . . . . . 20
150	146, 148, 149	ltsub1d 10166	. . . . . . . . . . . . . . . . . . 19
151	143, 144, 150	3bitr3rd 287	. . . . . . . . . . . . . . . . . 18 $/\$
152	151	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
153	136, 139, 152	mpbir2and 930	. . . . . . . . . . . . . . . 16 $/\$
154		divcan2 10222	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
155	65, 71, 154	mp3an23 1352	. . . . . . . . . . . . . . . . . . . . 21
156	19, 155	syl 17	. . . . . . . . . . . . . . . . . . . 20
157	156	oveq1d 6257	. . . . . . . . . . . . . . . . . . 19
158		pncan2 9826	. . . . . . . . . . . . . . . . . . . 20 $/\$
159	17, 158	mpan 674	. . . . . . . . . . . . . . . . . . 19
160	157, 159	eqtrd 2456	. . . . . . . . . . . . . . . . . 18
161	122, 160	syl 17	. . . . . . . . . . . . . . . . 17
162	161	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
163	153, 162	breqtrd 4384	. . . . . . . . . . . . . . 15 $/\$
164		peano2re 9750	. . . . . . . . . . . . . . . . . . . 20
165	140, 164	syl 17	. . . . . . . . . . . . . . . . . . 19
166		remulcl 9568	. . . . . . . . . . . . . . . . . . 19 $/\$
167	38, 165, 166	sylancr 667	. . . . . . . . . . . . . . . . . 18
168		flltp1 11979	. . . . . . . . . . . . . . . . . . . 20
169	130, 168	syl 17	. . . . . . . . . . . . . . . . . . 19
170	130, 165, 142, 169	ltmul2dd 11338	. . . . . . . . . . . . . . . . . 18
171	148, 167, 149, 170	ltsub1dd 10169	. . . . . . . . . . . . . . . . 17
172	161, 171	eqbrtrrd 4382	. . . . . . . . . . . . . . . 16
173	172	adantr 466	. . . . . . . . . . . . . . 15 $/\$
174		resubcl 9882	. . . . . . . . . . . . . . . . . . 19 $/\$
175	146, 16, 174	sylancl 666	. . . . . . . . . . . . . . . . . 18
176	175	rexrd 9634	. . . . . . . . . . . . . . . . 17
177		resubcl 9882	. . . . . . . . . . . . . . . . . . 19 $/\$
178	167, 16, 177	sylancl 666	. . . . . . . . . . . . . . . . . 18
179	178	rexrd 9634	. . . . . . . . . . . . . . . . 17
180		elioo2 11621	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
181	176, 179, 180	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
182	181	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
183	133, 163, 173, 182	mpbir3and 1188	. . . . . . . . . . . . . 14 $/\$
184		oveq2 6250	. . . . . . . . . . . . . . . . . 18
185	184	oveq1d 6257	. . . . . . . . . . . . . . . . 17
186		oveq1 6249	. . . . . . . . . . . . . . . . . . 19
187	186	oveq2d 6258	. . . . . . . . . . . . . . . . . 18
188	187	oveq1d 6257	. . . . . . . . . . . . . . . . 17
189	185, 188	oveq12d 6260	. . . . . . . . . . . . . . . 16
190	189	eleq2d 2485	. . . . . . . . . . . . . . 15
191	190	rspcev 3118	. . . . . . . . . . . . . 14 $/\$
192	132, 183, 191	syl2anc 665	. . . . . . . . . . . . 13 $/\$
193	127, 192	sylbi 198	. . . . . . . . . . . 12 $\$
194	120, 193	impbii 190	. . . . . . . . . . 11 $\$
195	34, 194	bitri 252	. . . . . . . . . 10 $\$
196	195	a1i 11	. . . . . . . . 9 $\$
197	29, 30, 33, 196	eqrd 3418	. . . . . . . 8 $\$
198	197	trud 1446	. . . . . . 7 $\$
199		retop 21717	. . . . . . . 8
200		iooretop 21721	. . . . . . . . 9
201	200	rgenw 2720	. . . . . . . 8
202		iunopn 19863	. . . . . . . 8 $/\$
203	199, 201, 202	mp2an 676	. . . . . . 7
204	198, 203	eqeltrri 2497	. . . . . 6 $\$
205		rabss 3474	. . . . . . . 8
206		zre 10885	. . . . . . . . . . 11
207		remulcl 9568	. . . . . . . . . . 11 $/\$
208	206, 38, 207	sylancl 666	. . . . . . . . . 10
209		resubcl 9882	. . . . . . . . . 10 $/\$
210	208, 16, 209	sylancl 666	. . . . . . . . 9
211		divcan1 10223	. . . . . . . . . . . . . 14 $/\$ $/\$
212	65, 71, 211	mp3an23 1352	. . . . . . . . . . . . 13
213	19, 212	syl 17	. . . . . . . . . . . 12
214	213	oveq1d 6257	. . . . . . . . . . 11
215	214, 159	eqtrd 2456	. . . . . . . . . 10
216	215	eleq1d 2484	. . . . . . . . 9
217	210, 216	syl5ib 222	. . . . . . . 8
218	205, 217	mprgbir 2723	. . . . . . 7
219		uniretop 21718	. . . . . . . 8
220	219	iscld2 19978	. . . . . . 7 $/\$ $\$
221	199, 218, 220	mp2an 676	. . . . . 6 $\$
222	204, 221	mpbir 212	. . . . 5
223	27	tgioo2 21756	. . . . . 6 ℂ_fld ↾_t
224	223	fveq2i 5821	. . . . 5 ℂ_fld ↾_t
225	222, 224	eleqtri 2498	. . . 4 ℂ_fld ↾_t
226		restcldr 20125	. . . 4 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
227	28, 225, 226	mp2an 676	. . 3 ℂ_fld
228	27	cnfldtopon 21738	. . . . 5 ℂ_fld TopOn
229	228	toponunii 19882	. . . 4 ℂ_fld
230	229	cldopn 19981	. . 3 ℂ_fld $\$ ℂ_fld
231	227, 230	ax-mp 5	. 2 $\$ ℂ_fld
232	26, 231	eqeltri 2496	1 $\$ ℂ_fld

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wtru 1438

wcel 1872

wne 2593

wral 2708

wrex 2709

crab 2712 $\$ cdif 3369

wss 3372

csn 3934

ciun 4235 class class class wbr 4359

cmpt 4418

ccnv 4788

crn 4790

cima 4792

wfun 5531

wfn 5532

wf 5533

cfv 5537 (class class class)co 6242

cc 9481

cr 9482

cc0 9483

c1 9484

caddc 9486

cmul 9488

cxr 9618

clt 9619

cle 9620

cmin 9804

cdiv 10213

c2 10603

cz 10881

crp 11246

cioo 11579

cfl 11969

csin 14052

ccos 14053

cpi 14055 ↾_t crest 15255

ctopn 15256

ctg 15272 ℂ_fldccnfld 18906

ctop 19852

ccld 19966

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2058 ax-ext 2402 ax-rep 4472 ax-sep 4482 ax-nul 4491 ax-pow 4538 ax-pr 4596 ax-un 6534 ax-inf2 8092 ax-cnex 9539 ax-resscn 9540 ax-1cn 9541 ax-icn 9542 ax-addcl 9543 ax-addrcl 9544 ax-mulcl 9545 ax-mulrcl 9546 ax-mulcom 9547 ax-addass 9548 ax-mulass 9549 ax-distr 9550 ax-i2m1 9551 ax-1ne0 9552 ax-1rid 9553 ax-rnegex 9554 ax-rrecex 9555 ax-cnre 9556 ax-pre-lttri 9557 ax-pre-lttrn 9558 ax-pre-ltadd 9559 ax-pre-mulgt0 9560 ax-pre-sup 9561 ax-addf 9562 ax-mulf 9563

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2274 df-mo 2275 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2552 df-ne 2595 df-nel 2596 df-ral 2713 df-rex 2714 df-reu 2715 df-rmo 2716 df-rab 2717 df-v 3018 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-pss 3388 df-nul 3698 df-if 3848 df-pw 3919 df-sn 3935 df-pr 3937 df-tp 3939 df-op 3941 df-uni 4156 df-int 4192 df-iun 4237 df-iin 4238 df-br 4360 df-opab 4419 df-mpt 4420 df-tr 4455 df-eprel 4700 df-id 4704 df-po 4710 df-so 4711 df-fr 4748 df-se 4749 df-we 4750 df-xp 4795 df-rel 4796 df-cnv 4797 df-co 4798 df-dm 4799 df-rn 4800 df-res 4801 df-ima 4802 df-pred 5335 df-ord 5381 df-on 5382 df-lim 5383 df-suc 5384 df-iota 5501 df-fun 5539 df-fn 5540 df-f 5541 df-f1 5542 df-fo 5543 df-f1o 5544 df-fv 5545 df-isom 5546 df-riota 6204 df-ov 6245 df-oprab 6246 df-mpt2 6247 df-of 6482 df-om 6644 df-1st 6744 df-2nd 6745 df-supp 6863 df-wrecs 6976 df-recs 7038 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-ixp 7471 df-en 7518 df-dom 7519 df-sdom 7520 df-fin 7521 df-fsupp 7830 df-fi 7871 df-sup 7902 df-inf 7903 df-oi 7971 df-card 8318 df-cda 8542 df-pnf 9621 df-mnf 9622 df-xr 9623 df-ltxr 9624 df-le 9625 df-sub 9806 df-neg 9807 df-div 10214 df-nn 10554 df-2 10612 df-3 10613 df-4 10614 df-5 10615 df-6 10616 df-7 10617 df-8 10618 df-9 10619 df-10 10620 df-n0 10814 df-z 10882 df-dec 10996 df-uz 11104 df-q 11209 df-rp 11247 df-xneg 11353 df-xadd 11354 df-xmul 11355 df-ioo 11583 df-ioc 11584 df-ico 11585 df-icc 11586 df-fz 11729 df-fzo 11860 df-fl 11971 df-mod 12040 df-seq 12157 df-exp 12216 df-fac 12403 df-bc 12431 df-hash 12459 df-shft 13067 df-cj 13099 df-re 13100 df-im 13101 df-sqrt 13235 df-abs 13236 df-limsup 13462 df-clim 13488 df-rlim 13489 df-sum 13689 df-ef 14057 df-sin 14059 df-cos 14060 df-pi 14062 df-struct 15059 df-ndx 15060 df-slot 15061 df-base 15062 df-sets 15063 df-ress 15064 df-plusg 15139 df-mulr 15140 df-starv 15141 df-sca 15142 df-vsca 15143 df-ip 15144 df-tset 15145 df-ple 15146 df-ds 15148 df-unif 15149 df-hom 15150 df-cco 15151 df-rest 15257 df-topn 15258 df-0g 15276 df-gsum 15277 df-topgen 15278 df-pt 15279 df-prds 15282 df-xrs 15336 df-qtop 15342 df-imas 15343 df-xps 15346 df-mre 15428 df-mrc 15429 df-acs 15431 df-mgm 16424 df-sgrp 16463 df-mnd 16473 df-submnd 16519 df-mulg 16612 df-cntz 16907 df-cmn 17368 df-psmet 18898 df-xmet 18899 df-met 18900 df-bl 18901 df-mopn 18902 df-fbas 18903 df-fg 18904 df-cnfld 18907 df-top 19856 df-bases 19857 df-topon 19858 df-topsp 19859 df-cld 19969 df-ntr 19970 df-cls 19971 df-nei 20049 df-lp 20087 df-perf 20088 df-cn 20178 df-cnp 20179 df-haus 20266 df-tx 20512 df-hmeo 20705 df-fil 20796 df-fm 20888 df-flim 20889 df-flf 20890 df-xms 21270 df-ms 21271 df-tms 21272 df-cncf 21845 df-limc 22756 df-dv 22757

This theorem is referenced by: (None)

W3C validator