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 31695

Description: Lemma for dvtan 31696- the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018.) Obsolete version of dvtanlem 31694 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 14157	. . . 4
2		ffun 5748	. . . 4
3		difpreima 6023	. . . 4 $\$ $\$
4	1, 2, 3	mp2b 10	. . 3 $\$ $\$
5		fimacnv 6027	. . . . 5
6	1, 5	ax-mp 5	. . . 4
7		0re 9642	. . . . . 6
8		ffn 5746	. . . . . . . . 9
9	1, 8	ax-mp 5	. . . . . . . 8
10		dffn5 5926	. . . . . . . 8
11	9, 10	mpbi 211	. . . . . . 7
12	11	mptiniseg 5349	. . . . . 6
13	7, 12	ax-mp 5	. . . . 5
14		sinhalfpip 23312	. . . . . . . 8
15	14	eqeq1d 2431	. . . . . . 7
16		halfpire 23284	. . . . . . . . . 10
17	16	recni 9654	. . . . . . . . 9
18		addcl 9620	. . . . . . . . 9 $/\$
19	17, 18	mpan 674	. . . . . . . 8
20		sineq0 23341	. . . . . . . 8
21	19, 20	syl 17	. . . . . . 7
22	15, 21	bitr3d 258	. . . . . 6
23	22	rabbiia 3076	. . . . 5
24	13, 23	eqtri 2458	. . . 4
25	6, 24	difeq12i 3587	. . 3 $\$ $\$
26	4, 25	eqtri 2458	. 2 $\$ $\$
27		eqid 2429	. . . . 5 ℂ_fld ℂ_fld
28	27	recld2 21743	. . . 4 ℂ_fld
29		nftru 1673	. . . . . . . . 9
30		nfcv 2591	. . . . . . . . 9
31		nfcv 2591	. . . . . . . . . 10
32		nfrab1 3016	. . . . . . . . . 10
33	31, 32	nfdif 3592	. . . . . . . . 9 $\$
34		eliun 4307	. . . . . . . . . . 11
35		elioore 11666	. . . . . . . . . . . . . . 15
36	35	adantl 467	. . . . . . . . . . . . . 14 $/\$
37		zre 10941	. . . . . . . . . . . . . . . . . . 19
38		pire 23278	. . . . . . . . . . . . . . . . . . . . . . . 24
39		remulcl 9623	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
40	38, 39	mpan 674	. . . . . . . . . . . . . . . . . . . . . . 23
41		resubcl 9937	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
42	40, 16, 41	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22
43	42	rexrd 9689	. . . . . . . . . . . . . . . . . . . . 21
44		peano2re 9805	. . . . . . . . . . . . . . . . . . . . . . . 24
45		remulcl 9623	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
46	38, 44, 45	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . 23
47		resubcl 9937	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
48	46, 16, 47	sylancl 666	. . . . . . . . . . . . . . . . . . . . . 22
49	48	rexrd 9689	. . . . . . . . . . . . . . . . . . . . 21
50		elioo2 11677	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
51	43, 49, 50	syl2anc 665	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
52		ltadd2 9737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
53	16, 52	mp3an3 1349	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
54	42, 53	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
55		readdcl 9621	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
56	16, 42, 55	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . 26
57		readdcl 9621	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
58	16, 57	mpan 674	. . . . . . . . . . . . . . . . . . . . . . . . . 26
59		pipos 23280	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
60	38, 59	pm3.2i 456	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
61		ltdiv1 10468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
62	60, 61	mp3an3 1349	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
63	56, 58, 62	syl2an 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
64		recn 9628	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
65		picn 23279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
66		mulcl 9622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
67	65, 66	mpan 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
68		pncan3 9882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
69	17, 67, 68	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
70	69	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
71	7, 59	gtneii 9745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
72		divcan3 10293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
73	65, 71, 72	mp3an23 1352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
74	70, 73	eqtrd 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
75	64, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
76	75	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
77	76	breq1d 4436	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
78	54, 63, 77	3bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
79	38, 45	mpan 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
80	79, 16, 47	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
81		ltadd2 9737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
82	16, 81	mp3an3 1349	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
83	80, 82	sylan2 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
84		readdcl 9621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
85	16, 80, 84	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		ltdiv1 10468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
87	60, 86	mp3an3 1349	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
88	58, 85, 87	syl2an 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
89		recn 9628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
90		mulcl 9622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
91	65, 90	mpan 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92		pncan3 9882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
93	17, 91, 92	sylancr 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
94	93	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
95		divcan3 10293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
96	65, 71, 95	mp3an23 1352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	94, 96	eqtrd 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	89, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100	99	breq2d 4438	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 11012	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
112	111	3expb 1206	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	110, 112	syldan 472	. . . . . . . . . . . . . . . 16 $/\$
114	113	olcd 394	. . . . . . . . . . . . . . 15 $/\$ $\/$
115		ianor 490	. . . . . . . . . . . . . . . 16 $/\$ $\/$
116		rabid 3012	. . . . . . . . . . . . . . . 16 $/\$
117	115, 116	xchnxbir 310	. . . . . . . . . . . . . . 15 $\/$
118	114, 117	sylibr 215	. . . . . . . . . . . . . 14 $/\$
119	36, 118	eldifd 3453	. . . . . . . . . . . . 13 $/\$ $\$
120	119	rexlimiva 2920	. . . . . . . . . . . 12 $\$
121		eldif 3452	. . . . . . . . . . . . . 14 $\$ $/\$
122		recn 9628	. . . . . . . . . . . . . . . . . 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 10325	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
129	38, 71, 128	mp3an23 1352	. . . . . . . . . . . . . . . . 17
130	58, 129	syl 17	. . . . . . . . . . . . . . . 16
131	130	flcld 12031	. . . . . . . . . . . . . . 15
132	131	adantr 466	. . . . . . . . . . . . . 14 $/\$
133		simpl 458	. . . . . . . . . . . . . . 15 $/\$
134		flle 12032	. . . . . . . . . . . . . . . . . . 19
135	130, 134	syl 17	. . . . . . . . . . . . . . . . . 18
136	135	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$
137		nelne2 2761	. . . . . . . . . . . . . . . . . . 19 $/\$
138	137	necomd 2702	. . . . . . . . . . . . . . . . . 18 $/\$
139	131, 138	sylan 473	. . . . . . . . . . . . . . . . 17 $/\$
140	131	zred 11040	. . . . . . . . . . . . . . . . . . . 20
141		pirp 23281	. . . . . . . . . . . . . . . . . . . . 21
142	141	a1i 11	. . . . . . . . . . . . . . . . . . . 20
143	140, 130, 142	ltmul2d 11380	. . . . . . . . . . . . . . . . . . 19
144	140, 130	ltlend 9779	. . . . . . . . . . . . . . . . . . 19 $/\$
145		remulcl 9623	. . . . . . . . . . . . . . . . . . . . 21 $/\$
146	38, 140, 145	sylancr 667	. . . . . . . . . . . . . . . . . . . 20
147		remulcl 9623	. . . . . . . . . . . . . . . . . . . . 21 $/\$
148	38, 130, 147	sylancr 667	. . . . . . . . . . . . . . . . . . . 20
149	16	a1i 11	. . . . . . . . . . . . . . . . . . . 20
150	146, 148, 149	ltsub1d 10221	. . . . . . . . . . . . . . . . . . 19
151	143, 144, 150	3bitr3rd 287	. . . . . . . . . . . . . . . . . 18 $/\$
152	151	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
153	136, 139, 152	mpbir2and 930	. . . . . . . . . . . . . . . 16 $/\$
154		divcan2 10277	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
155	65, 71, 154	mp3an23 1352	. . . . . . . . . . . . . . . . . . . . 21
156	19, 155	syl 17	. . . . . . . . . . . . . . . . . . . 20
157	156	oveq1d 6320	. . . . . . . . . . . . . . . . . . 19
158		pncan2 9881	. . . . . . . . . . . . . . . . . . . 20 $/\$
159	17, 158	mpan 674	. . . . . . . . . . . . . . . . . . 19
160	157, 159	eqtrd 2470	. . . . . . . . . . . . . . . . . 18
161	122, 160	syl 17	. . . . . . . . . . . . . . . . 17
162	161	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
163	153, 162	breqtrd 4450	. . . . . . . . . . . . . . 15 $/\$
164		peano2re 9805	. . . . . . . . . . . . . . . . . . . 20
165	140, 164	syl 17	. . . . . . . . . . . . . . . . . . 19
166		remulcl 9623	. . . . . . . . . . . . . . . . . . 19 $/\$
167	38, 165, 166	sylancr 667	. . . . . . . . . . . . . . . . . 18
168		flltp1 12033	. . . . . . . . . . . . . . . . . . . 20
169	130, 168	syl 17	. . . . . . . . . . . . . . . . . . 19
170	130, 165, 142, 169	ltmul2dd 11394	. . . . . . . . . . . . . . . . . 18
171	148, 167, 149, 170	ltsub1dd 10224	. . . . . . . . . . . . . . . . 17
172	161, 171	eqbrtrrd 4448	. . . . . . . . . . . . . . . 16
173	172	adantr 466	. . . . . . . . . . . . . . 15 $/\$
174		resubcl 9937	. . . . . . . . . . . . . . . . . . 19 $/\$
175	146, 16, 174	sylancl 666	. . . . . . . . . . . . . . . . . 18
176	175	rexrd 9689	. . . . . . . . . . . . . . . . 17
177		resubcl 9937	. . . . . . . . . . . . . . . . . . 19 $/\$
178	167, 16, 177	sylancl 666	. . . . . . . . . . . . . . . . . 18
179	178	rexrd 9689	. . . . . . . . . . . . . . . . 17
180		elioo2 11677	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
181	176, 179, 180	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
182	181	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
183	133, 163, 173, 182	mpbir3and 1188	. . . . . . . . . . . . . 14 $/\$
184		oveq2 6313	. . . . . . . . . . . . . . . . . 18
185	184	oveq1d 6320	. . . . . . . . . . . . . . . . 17
186		oveq1 6312	. . . . . . . . . . . . . . . . . . 19
187	186	oveq2d 6321	. . . . . . . . . . . . . . . . . 18
188	187	oveq1d 6320	. . . . . . . . . . . . . . . . 17
189	185, 188	oveq12d 6323	. . . . . . . . . . . . . . . 16
190	189	eleq2d 2499	. . . . . . . . . . . . . . 15
191	190	rspcev 3188	. . . . . . . . . . . . . 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 3488	. . . . . . . 8 $\$
198	197	trud 1446	. . . . . . 7 $\$
199		retop 21693	. . . . . . . 8
200		iooretop 21697	. . . . . . . . 9
201	200	rgenw 2793	. . . . . . . 8
202		iunopn 19859	. . . . . . . 8 $/\$
203	199, 201, 202	mp2an 676	. . . . . . 7
204	198, 203	eqeltrri 2514	. . . . . 6 $\$
205		rabss 3544	. . . . . . . 8
206		zre 10941	. . . . . . . . . . 11
207		remulcl 9623	. . . . . . . . . . 11 $/\$
208	206, 38, 207	sylancl 666	. . . . . . . . . 10
209		resubcl 9937	. . . . . . . . . 10 $/\$
210	208, 16, 209	sylancl 666	. . . . . . . . 9
211		divcan1 10278	. . . . . . . . . . . . . 14 $/\$ $/\$
212	65, 71, 211	mp3an23 1352	. . . . . . . . . . . . 13
213	19, 212	syl 17	. . . . . . . . . . . 12
214	213	oveq1d 6320	. . . . . . . . . . 11
215	214, 159	eqtrd 2470	. . . . . . . . . 10
216	215	eleq1d 2498	. . . . . . . . 9
217	210, 216	syl5ib 222	. . . . . . . 8
218	205, 217	mprgbir 2796	. . . . . . 7
219		uniretop 21694	. . . . . . . 8
220	219	iscld2 19974	. . . . . . 7 $/\$ $\$
221	199, 218, 220	mp2an 676	. . . . . 6 $\$
222	204, 221	mpbir 212	. . . . 5
223	27	tgioo2 21732	. . . . . 6 ℂ_fld ↾_t
224	223	fveq2i 5884	. . . . 5 ℂ_fld ↾_t
225	222, 224	eleqtri 2515	. . . 4 ℂ_fld ↾_t
226		restcldr 20121	. . . 4 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
227	28, 225, 226	mp2an 676	. . 3 ℂ_fld
228	27	cnfldtopon 21714	. . . . 5 ℂ_fld TopOn
229	228	toponunii 19878	. . . 4 ℂ_fld
230	229	cldopn 19977	. . 3 ℂ_fld $\$ ℂ_fld
231	227, 230	ax-mp 5	. 2 $\$ ℂ_fld
232	26, 231	eqeltri 2513	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 1870

wne 2625

wral 2782

wrex 2783

crab 2786 $\$ cdif 3439

wss 3442

csn 4002

ciun 4302 class class class wbr 4426

cmpt 4484

ccnv 4853

crn 4855

cima 4857

wfun 5595

wfn 5596

wf 5597

cfv 5601 (class class class)co 6305

cc 9536

cr 9537

cc0 9538

c1 9539

caddc 9541

cmul 9543

cxr 9673

clt 9674

cle 9675

cmin 9859

cdiv 10268

c2 10659

cz 10937

crp 11302

cioo 11635

cfl 12023

csin 14094

ccos 14095

cpi 14097 ↾_t crest 15278

ctopn 15279

ctg 15295 ℂ_fldccnfld 18905

ctop 19848

ccld 19962

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-inf2 8146 ax-cnex 9594 ax-resscn 9595 ax-1cn 9596 ax-icn 9597 ax-addcl 9598 ax-addrcl 9599 ax-mulcl 9600 ax-mulrcl 9601 ax-mulcom 9602 ax-addass 9603 ax-mulass 9604 ax-distr 9605 ax-i2m1 9606 ax-1ne0 9607 ax-1rid 9608 ax-rnegex 9609 ax-rrecex 9610 ax-cnre 9611 ax-pre-lttri 9612 ax-pre-lttrn 9613 ax-pre-ltadd 9614 ax-pre-mulgt0 9615 ax-pre-sup 9616 ax-addf 9617 ax-mulf 9618

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 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-int 4259 df-iun 4304 df-iin 4305 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-se 4814 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 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 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-om 6707 df-1st 6807 df-2nd 6808 df-supp 6926 df-wrecs 7036 df-recs 7098 df-rdg 7136 df-1o 7190 df-2o 7191 df-oadd 7194 df-er 7371 df-map 7482 df-pm 7483 df-ixp 7531 df-en 7578 df-dom 7579 df-sdom 7580 df-fin 7581 df-fsupp 7890 df-fi 7931 df-sup 7962 df-inf 7963 df-oi 8025 df-card 8372 df-cda 8596 df-pnf 9676 df-mnf 9677 df-xr 9678 df-ltxr 9679 df-le 9680 df-sub 9861 df-neg 9862 df-div 10269 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ioc 11640 df-ico 11641 df-icc 11642 df-fz 11783 df-fzo 11914 df-fl 12025 df-mod 12094 df-seq 12211 df-exp 12270 df-fac 12457 df-bc 12485 df-hash 12513 df-shft 13109 df-cj 13141 df-re 13142 df-im 13143 df-sqrt 13277 df-abs 13278 df-limsup 13504 df-clim 13530 df-rlim 13531 df-sum 13731 df-ef 14099 df-sin 14101 df-cos 14102 df-pi 14104 df-struct 15086 df-ndx 15087 df-slot 15088 df-base 15089 df-sets 15090 df-ress 15091 df-plusg 15165 df-mulr 15166 df-starv 15167 df-sca 15168 df-vsca 15169 df-ip 15170 df-tset 15171 df-ple 15172 df-ds 15174 df-unif 15175 df-hom 15176 df-cco 15177 df-rest 15280 df-topn 15281 df-0g 15299 df-gsum 15300 df-topgen 15301 df-pt 15302 df-prds 15305 df-xrs 15359 df-qtop 15364 df-imas 15365 df-xps 15367 df-mre 15443 df-mrc 15444 df-acs 15446 df-mgm 16439 df-sgrp 16478 df-mnd 16488 df-submnd 16534 df-mulg 16627 df-cntz 16922 df-cmn 17367 df-psmet 18897 df-xmet 18898 df-met 18899 df-bl 18900 df-mopn 18901 df-fbas 18902 df-fg 18903 df-cnfld 18906 df-top 19852 df-bases 19853 df-topon 19854 df-topsp 19855 df-cld 19965 df-ntr 19966 df-cls 19967 df-nei 20045 df-lp 20083 df-perf 20084 df-cn 20174 df-cnp 20175 df-haus 20262 df-tx 20508 df-hmeo 20701 df-fil 20792 df-fm 20884 df-flim 20885 df-flf 20886 df-xms 21266 df-ms 21267 df-tms 21268 df-cncf 21806 df-limc 22698 df-dv 22699

This theorem is referenced by: (None)

W3C validator