dvtanlemOLD - Mathbox for Brendan Leahy

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

Theorem dvtanlemOLD 32055

Description: Lemma for dvtan 32056- the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018.) Obsolete version of dvtanlem 32054 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 14256	. . . 4
2		ffun 5742	. . . 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 9661	. . . . . 6
8		ffn 5739	. . . . . . . . 9
9	1, 8	ax-mp 5	. . . . . . . 8
10		dffn5 5924	. . . . . . . 8
11	9, 10	mpbi 213	. . . . . . 7
12	11	mptiniseg 5336	. . . . . 6
13	7, 12	ax-mp 5	. . . . 5
14		sinhalfpip 23526	. . . . . . . 8
15	14	eqeq1d 2473	. . . . . . 7
16		halfpire 23498	. . . . . . . . . 10
17	16	recni 9673	. . . . . . . . 9
18		addcl 9639	. . . . . . . . 9 $/\$
19	17, 18	mpan 684	. . . . . . . 8
20		sineq0 23555	. . . . . . . 8
21	19, 20	syl 17	. . . . . . 7
22	15, 21	bitr3d 263	. . . . . 6
23	22	rabbiia 3019	. . . . 5
24	13, 23	eqtri 2493	. . . 4
25	6, 24	difeq12i 3538	. . 3 $\$ $\$
26	4, 25	eqtri 2493	. 2 $\$ $\$
27		eqid 2471	. . . . 5 ℂ_fld ℂ_fld
28	27	recld2 21910	. . . 4 ℂ_fld
29		nftru 1685	. . . . . . . . 9
30		nfcv 2612	. . . . . . . . 9
31		nfcv 2612	. . . . . . . . . 10
32		nfrab1 2957	. . . . . . . . . 10
33	31, 32	nfdif 3543	. . . . . . . . 9 $\$
34		eliun 4274	. . . . . . . . . . 11
35		elioore 11691	. . . . . . . . . . . . . . 15
36	35	adantl 473	. . . . . . . . . . . . . 14 $/\$
37		zre 10965	. . . . . . . . . . . . . . . . . . 19
38		pire 23492	. . . . . . . . . . . . . . . . . . . . . . . 24
39		remulcl 9642	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
40	38, 39	mpan 684	. . . . . . . . . . . . . . . . . . . . . . 23
41		resubcl 9958	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
42	40, 16, 41	sylancl 675	. . . . . . . . . . . . . . . . . . . . . 22
43	42	rexrd 9708	. . . . . . . . . . . . . . . . . . . . 21
44		peano2re 9824	. . . . . . . . . . . . . . . . . . . . . . . 24
45		remulcl 9642	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
46	38, 44, 45	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . 23
47		resubcl 9958	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
48	46, 16, 47	sylancl 675	. . . . . . . . . . . . . . . . . . . . . 22
49	48	rexrd 9708	. . . . . . . . . . . . . . . . . . . . 21
50		elioo2 11702	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
51	43, 49, 50	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
52		ltadd2 9756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
53	16, 52	mp3an3 1379	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
54	42, 53	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
55		readdcl 9640	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
56	16, 42, 55	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . 26
57		readdcl 9640	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
58	16, 57	mpan 684	. . . . . . . . . . . . . . . . . . . . . . . . . 26
59		pipos 23494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
60	38, 59	pm3.2i 462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
61		ltdiv1 10491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
62	60, 61	mp3an3 1379	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
63	56, 58, 62	syl2an 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
64		recn 9647	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
65		picn 23493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
66		mulcl 9641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
67	65, 66	mpan 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
68		pncan3 9903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
69	17, 67, 68	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
70	69	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
71	7, 59	gtneii 9764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
72		divcan3 10316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
73	65, 71, 72	mp3an23 1382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
74	70, 73	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
75	64, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
76	75	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
77	76	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
78	54, 63, 77	3bitrd 287	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
79	38, 45	mpan 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
80	79, 16, 47	sylancl 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
81		ltadd2 9756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
82	16, 81	mp3an3 1379	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
83	80, 82	sylan2 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
84		readdcl 9640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
85	16, 80, 84	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
86		ltdiv1 10491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
87	60, 86	mp3an3 1379	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
88	58, 85, 87	syl2an 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
89		recn 9647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
90		mulcl 9641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
91	65, 90	mpan 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92		pncan3 9903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
93	17, 91, 92	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
94	93	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
95		divcan3 10316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
96	65, 71, 95	mp3an23 1382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	94, 96	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	89, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100	99	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
101	83, 88, 100	3bitrd 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
102	44, 101	sylan2 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
103	102	ancoms 460	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
104	78, 103	anbi12d 725	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
105	104	biimpd 212	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
106	105	exp4b 618	. . . . . . . . . . . . . . . . . . . . 21 $/\$
107	106	3impd 1247	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
108	51, 107	sylbid 223	. . . . . . . . . . . . . . . . . . 19 $/\$
109	37, 108	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$
110	109	imp 436	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
111		btwnnz 11035	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
112	111	3expb 1232	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	110, 112	syldan 478	. . . . . . . . . . . . . . . 16 $/\$
114	113	olcd 400	. . . . . . . . . . . . . . 15 $/\$ $\/$
115		ianor 496	. . . . . . . . . . . . . . . 16 $/\$ $\/$
116		rabid 2953	. . . . . . . . . . . . . . . 16 $/\$
117	115, 116	xchnxbir 316	. . . . . . . . . . . . . . 15 $\/$
118	114, 117	sylibr 217	. . . . . . . . . . . . . 14 $/\$
119	36, 118	eldifd 3401	. . . . . . . . . . . . 13 $/\$ $\$
120	119	rexlimiva 2868	. . . . . . . . . . . 12 $\$
121		eldif 3400	. . . . . . . . . . . . . 14 $\$ $/\$
122		recn 9647	. . . . . . . . . . . . . . . . . 18
123	122	biantrurd 516	. . . . . . . . . . . . . . . . 17 $/\$
124	123, 116	syl6bbr 271	. . . . . . . . . . . . . . . 16
125	124	notbid 301	. . . . . . . . . . . . . . 15
126	125	pm5.32i 649	. . . . . . . . . . . . . 14 $/\$ $/\$
127	121, 126	bitr4i 260	. . . . . . . . . . . . 13 $\$ $/\$
128		redivcl 10348	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
129	38, 71, 128	mp3an23 1382	. . . . . . . . . . . . . . . . 17
130	58, 129	syl 17	. . . . . . . . . . . . . . . 16
131	130	flcld 12067	. . . . . . . . . . . . . . 15
132	131	adantr 472	. . . . . . . . . . . . . 14 $/\$
133		simpl 464	. . . . . . . . . . . . . . 15 $/\$
134		flle 12068	. . . . . . . . . . . . . . . . . . 19
135	130, 134	syl 17	. . . . . . . . . . . . . . . . . 18
136	135	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
137		nelne2 2740	. . . . . . . . . . . . . . . . . . 19 $/\$
138	137	necomd 2698	. . . . . . . . . . . . . . . . . 18 $/\$
139	131, 138	sylan 479	. . . . . . . . . . . . . . . . 17 $/\$
140	131	zred 11063	. . . . . . . . . . . . . . . . . . . 20
141		pirp 23495	. . . . . . . . . . . . . . . . . . . . 21
142	141	a1i 11	. . . . . . . . . . . . . . . . . . . 20
143	140, 130, 142	ltmul2d 11403	. . . . . . . . . . . . . . . . . . 19
144	140, 130	ltlend 9797	. . . . . . . . . . . . . . . . . . 19 $/\$
145		remulcl 9642	. . . . . . . . . . . . . . . . . . . . 21 $/\$
146	38, 140, 145	sylancr 676	. . . . . . . . . . . . . . . . . . . 20
147		remulcl 9642	. . . . . . . . . . . . . . . . . . . . 21 $/\$
148	38, 130, 147	sylancr 676	. . . . . . . . . . . . . . . . . . . 20
149	16	a1i 11	. . . . . . . . . . . . . . . . . . . 20
150	146, 148, 149	ltsub1d 10243	. . . . . . . . . . . . . . . . . . 19
151	143, 144, 150	3bitr3rd 292	. . . . . . . . . . . . . . . . . 18 $/\$
152	151	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
153	136, 139, 152	mpbir2and 936	. . . . . . . . . . . . . . . 16 $/\$
154		divcan2 10300	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
155	65, 71, 154	mp3an23 1382	. . . . . . . . . . . . . . . . . . . . 21
156	19, 155	syl 17	. . . . . . . . . . . . . . . . . . . 20
157	156	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19
158		pncan2 9902	. . . . . . . . . . . . . . . . . . . 20 $/\$
159	17, 158	mpan 684	. . . . . . . . . . . . . . . . . . 19
160	157, 159	eqtrd 2505	. . . . . . . . . . . . . . . . . 18
161	122, 160	syl 17	. . . . . . . . . . . . . . . . 17
162	161	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
163	153, 162	breqtrd 4420	. . . . . . . . . . . . . . 15 $/\$
164		peano2re 9824	. . . . . . . . . . . . . . . . . . . 20
165	140, 164	syl 17	. . . . . . . . . . . . . . . . . . 19
166		remulcl 9642	. . . . . . . . . . . . . . . . . . 19 $/\$
167	38, 165, 166	sylancr 676	. . . . . . . . . . . . . . . . . 18
168		flltp1 12069	. . . . . . . . . . . . . . . . . . . 20
169	130, 168	syl 17	. . . . . . . . . . . . . . . . . . 19
170	130, 165, 142, 169	ltmul2dd 11417	. . . . . . . . . . . . . . . . . 18
171	148, 167, 149, 170	ltsub1dd 10246	. . . . . . . . . . . . . . . . 17
172	161, 171	eqbrtrrd 4418	. . . . . . . . . . . . . . . 16
173	172	adantr 472	. . . . . . . . . . . . . . 15 $/\$
174		resubcl 9958	. . . . . . . . . . . . . . . . . . 19 $/\$
175	146, 16, 174	sylancl 675	. . . . . . . . . . . . . . . . . 18
176	175	rexrd 9708	. . . . . . . . . . . . . . . . 17
177		resubcl 9958	. . . . . . . . . . . . . . . . . . 19 $/\$
178	167, 16, 177	sylancl 675	. . . . . . . . . . . . . . . . . 18
179	178	rexrd 9708	. . . . . . . . . . . . . . . . 17
180		elioo2 11702	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
181	176, 179, 180	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$
182	181	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
183	133, 163, 173, 182	mpbir3and 1213	. . . . . . . . . . . . . 14 $/\$
184		oveq2 6316	. . . . . . . . . . . . . . . . . 18
185	184	oveq1d 6323	. . . . . . . . . . . . . . . . 17
186		oveq1 6315	. . . . . . . . . . . . . . . . . . 19
187	186	oveq2d 6324	. . . . . . . . . . . . . . . . . 18
188	187	oveq1d 6323	. . . . . . . . . . . . . . . . 17
189	185, 188	oveq12d 6326	. . . . . . . . . . . . . . . 16
190	189	eleq2d 2534	. . . . . . . . . . . . . . 15
191	190	rspcev 3136	. . . . . . . . . . . . . 14 $/\$
192	132, 183, 191	syl2anc 673	. . . . . . . . . . . . 13 $/\$
193	127, 192	sylbi 200	. . . . . . . . . . . 12 $\$
194	120, 193	impbii 192	. . . . . . . . . . 11 $\$
195	34, 194	bitri 257	. . . . . . . . . 10 $\$
196	195	a1i 11	. . . . . . . . 9 $\$
197	29, 30, 33, 196	eqrd 3436	. . . . . . . 8 $\$
198	197	trud 1461	. . . . . . 7 $\$
199		retop 21860	. . . . . . . 8
200		iooretop 21864	. . . . . . . . 9
201	200	rgenw 2768	. . . . . . . 8
202		iunopn 20005	. . . . . . . 8 $/\$
203	199, 201, 202	mp2an 686	. . . . . . 7
204	198, 203	eqeltrri 2546	. . . . . 6 $\$
205		rabss 3492	. . . . . . . 8
206		zre 10965	. . . . . . . . . . 11
207		remulcl 9642	. . . . . . . . . . 11 $/\$
208	206, 38, 207	sylancl 675	. . . . . . . . . 10
209		resubcl 9958	. . . . . . . . . 10 $/\$
210	208, 16, 209	sylancl 675	. . . . . . . . 9
211		divcan1 10301	. . . . . . . . . . . . . 14 $/\$ $/\$
212	65, 71, 211	mp3an23 1382	. . . . . . . . . . . . 13
213	19, 212	syl 17	. . . . . . . . . . . 12
214	213	oveq1d 6323	. . . . . . . . . . 11
215	214, 159	eqtrd 2505	. . . . . . . . . 10
216	215	eleq1d 2533	. . . . . . . . 9
217	210, 216	syl5ib 227	. . . . . . . 8
218	205, 217	mprgbir 2771	. . . . . . 7
219		uniretop 21861	. . . . . . . 8
220	219	iscld2 20120	. . . . . . 7 $/\$ $\$
221	199, 218, 220	mp2an 686	. . . . . 6 $\$
222	204, 221	mpbir 214	. . . . 5
223	27	tgioo2 21899	. . . . . 6 ℂ_fld ↾_t
224	223	fveq2i 5882	. . . . 5 ℂ_fld ↾_t
225	222, 224	eleqtri 2547	. . . 4 ℂ_fld ↾_t
226		restcldr 20267	. . . 4 ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
227	28, 225, 226	mp2an 686	. . 3 ℂ_fld
228	27	cnfldtopon 21881	. . . . 5 ℂ_fld TopOn
229	228	toponunii 20024	. . . 4 ℂ_fld
230	229	cldopn 20123	. . 3 ℂ_fld $\$ ℂ_fld
231	227, 230	ax-mp 5	. 2 $\$ ℂ_fld
232	26, 231	eqeltri 2545	1 $\$ ℂ_fld

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wtru 1453

wcel 1904

wne 2641

wral 2756

wrex 2757

crab 2760 $\$ cdif 3387

wss 3390

csn 3959

ciun 4269 class class class wbr 4395

cmpt 4454

ccnv 4838

crn 4840

cima 4842

wfun 5583

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

cxr 9692

clt 9693

cle 9694

cmin 9880

cdiv 10291

c2 10681

cz 10961

crp 11325

cioo 11660

cfl 12059

csin 14193

ccos 14194

cpi 14196 ↾_t crest 15397

ctopn 15398

ctg 15414 ℂ_fldccnfld 19047

ctop 19994

ccld 20108

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-pi 14203 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901

This theorem is referenced by: (None)

W3C validator