dvnxpaek - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvnxpaek		Structured version Visualization version Unicode version

Theorem dvnxpaek 37914

Description: The

-th derivative of the polynomial (x+A)^K. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

**Hypotheses**
Ref	Expression
dvnxpaek.s
dvnxpaek.x	ℂ_fld ↾_t
dvnxpaek.a
dvnxpaek.k
dvnxpaek.f

**Assertion**
Ref	Expression
dvnxpaek	$/\$

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem dvnxpaek Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5879	. . 3
2		breq2 4399	. . . . 5
3		eqidd 2472	. . . . 5
4		oveq2 6316	. . . . . . . 8
5	4	fveq2d 5883	. . . . . . 7
6	5	oveq2d 6324	. . . . . 6
7	4	oveq2d 6324	. . . . . 6
8	6, 7	oveq12d 6326	. . . . 5
9	2, 3, 8	ifbieq12d 3899	. . . 4
10	9	mpteq2dv 4483	. . 3
11	1, 10	eqeq12d 2486	. 2
12		fveq2 5879	. . 3
13		breq2 4399	. . . . 5
14		eqidd 2472	. . . . 5
15		oveq2 6316	. . . . . . . 8
16	15	fveq2d 5883	. . . . . . 7
17	16	oveq2d 6324	. . . . . 6
18	15	oveq2d 6324	. . . . . 6
19	17, 18	oveq12d 6326	. . . . 5
20	13, 14, 19	ifbieq12d 3899	. . . 4
21	20	mpteq2dv 4483	. . 3
22	12, 21	eqeq12d 2486	. 2
23		fveq2 5879	. . 3
24		breq2 4399	. . . . 5
25		eqidd 2472	. . . . 5
26		oveq2 6316	. . . . . . . 8
27	26	fveq2d 5883	. . . . . . 7
28	27	oveq2d 6324	. . . . . 6
29	26	oveq2d 6324	. . . . . 6
30	28, 29	oveq12d 6326	. . . . 5
31	24, 25, 30	ifbieq12d 3899	. . . 4
32	31	mpteq2dv 4483	. . 3
33	23, 32	eqeq12d 2486	. 2
34		fveq2 5879	. . 3
35		breq2 4399	. . . . 5
36		eqidd 2472	. . . . 5
37		oveq2 6316	. . . . . . . 8
38	37	fveq2d 5883	. . . . . . 7
39	38	oveq2d 6324	. . . . . 6
40	37	oveq2d 6324	. . . . . 6
41	39, 40	oveq12d 6326	. . . . 5
42	35, 36, 41	ifbieq12d 3899	. . . 4
43	42	mpteq2dv 4483	. . 3
44	34, 43	eqeq12d 2486	. 2
45		dvnxpaek.s	. . . . 5
46		recnprss 22938	. . . . 5
47	45, 46	syl 17	. . . 4
48		cnex 9638	. . . . . 6
49	48	a1i 11	. . . . 5
50		dvnxpaek.x	. . . . . . . . . . . 12 ℂ_fld ↾_t
51		restsspw 15408	. . . . . . . . . . . . . 14 ℂ_fld ↾_t
52		id 22	. . . . . . . . . . . . . 14 ℂ_fld ↾_t ℂ_fld ↾_t
53	51, 52	sseldi 3416	. . . . . . . . . . . . 13 ℂ_fld ↾_t
54		elpwi 3951	. . . . . . . . . . . . 13
55	53, 54	syl 17	. . . . . . . . . . . 12 ℂ_fld ↾_t
56	50, 55	syl 17	. . . . . . . . . . 11
57	56, 47	sstrd 3428	. . . . . . . . . 10
58	57	adantr 472	. . . . . . . . 9 $/\$
59		simpr 468	. . . . . . . . 9 $/\$
60	58, 59	sseldd 3419	. . . . . . . 8 $/\$
61		dvnxpaek.a	. . . . . . . . 9
62	61	adantr 472	. . . . . . . 8 $/\$
63	60, 62	addcld 9680	. . . . . . 7 $/\$
64		dvnxpaek.k	. . . . . . . 8
65	64	adantr 472	. . . . . . 7 $/\$
66	63, 65	expcld 12454	. . . . . 6 $/\$
67		dvnxpaek.f	. . . . . 6
68	66, 67	fmptd 6061	. . . . 5
69		elpm2r 7507	. . . . 5 $/\$ $/\$ $/\$
70	49, 45, 68, 56, 69	syl22anc 1293	. . . 4
71		dvn0 22957	. . . 4 $/\$
72	47, 70, 71	syl2anc 673	. . 3
73	67	a1i 11	. . 3
74	64	nn0ge0d 10952	. . . . . . . 8
75		0red 9662	. . . . . . . . 9
76	64	nn0red 10950	. . . . . . . . 9
77	75, 76	lenltd 9798	. . . . . . . 8
78	74, 77	mpbid 215	. . . . . . 7
79	78	iffalsed 3883	. . . . . 6
80	79	adantr 472	. . . . 5 $/\$
81	64	nn0cnd 10951	. . . . . . . . . . 11
82	81	subid1d 9994	. . . . . . . . . 10
83	82	fveq2d 5883	. . . . . . . . 9
84	83	oveq2d 6324	. . . . . . . 8
85		faccl 12507	. . . . . . . . . . 11
86	64, 85	syl 17	. . . . . . . . . 10
87	86	nncnd 10647	. . . . . . . . 9
88	86	nnne0d 10676	. . . . . . . . 9
89	87, 88	dividd 10403	. . . . . . . 8
90	84, 89	eqtrd 2505	. . . . . . 7
91	82	oveq2d 6324	. . . . . . 7
92	90, 91	oveq12d 6326	. . . . . 6
93	92	adantr 472	. . . . 5 $/\$
94	66	mulid2d 9679	. . . . 5 $/\$
95	80, 93, 94	3eqtrrd 2510	. . . 4 $/\$
96	95	mpteq2dva 4482	. . 3
97	72, 73, 96	3eqtrd 2509	. 2
98	47	adantr 472	. . . . 5 $/\$
99	70	adantr 472	. . . . 5 $/\$
100		simpr 468	. . . . 5 $/\$
101		dvnp1 22958	. . . . 5 $/\$ $/\$
102	98, 99, 100, 101	syl3anc 1292	. . . 4 $/\$
103	102	adantr 472	. . 3 $/\$ $/\$
104		oveq2 6316	. . . 4
105	104	adantl 473	. . 3 $/\$ $/\$
106		iftrue 3878	. . . . . . . . 9
107	106	mpteq2dv 4483	. . . . . . . 8
108	107	oveq2d 6324	. . . . . . 7
109	108	adantl 473	. . . . . 6 $/\$ $/\$
110		0cnd 9654	. . . . . . . 8
111	45, 50, 110	dvmptconst 37882	. . . . . . 7
112	111	ad2antrr 740	. . . . . 6 $/\$ $/\$
113	76	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$
114		nn0re 10902	. . . . . . . . . . . 12
115	114	ad2antlr 741	. . . . . . . . . . 11 $/\$ $/\$
116		simpr 468	. . . . . . . . . . 11 $/\$ $/\$
117	113, 115, 116	ltled 9800	. . . . . . . . . 10 $/\$ $/\$
118	64	nn0zd 11061	. . . . . . . . . . . . 13
119	118	adantr 472	. . . . . . . . . . . 12 $/\$
120	100	nn0zd 11061	. . . . . . . . . . . 12 $/\$
121		zleltp1 11011	. . . . . . . . . . . 12 $/\$
122	119, 120, 121	syl2anc 673	. . . . . . . . . . 11 $/\$
123	122	adantr 472	. . . . . . . . . 10 $/\$ $/\$
124	117, 123	mpbid 215	. . . . . . . . 9 $/\$ $/\$
125	124	iftrued 3880	. . . . . . . 8 $/\$ $/\$
126	125	mpteq2dv 4483	. . . . . . 7 $/\$ $/\$
127	126	eqcomd 2477	. . . . . 6 $/\$ $/\$
128	109, 112, 127	3eqtrd 2509	. . . . 5 $/\$ $/\$
129		simpl 464	. . . . . 6 $/\$ $/\$ $/\$
130		simpr 468	. . . . . . 7 $/\$ $/\$
131	129, 100, 114	3syl 18	. . . . . . . 8 $/\$ $/\$
132	76	ad2antrr 740	. . . . . . . 8 $/\$ $/\$
133	131, 132	lenltd 9798	. . . . . . 7 $/\$ $/\$
134	130, 133	mpbird 240	. . . . . 6 $/\$ $/\$
135		simpr 468	. . . . . . . . . . . . . 14 $/\$ $/\$
136	114	ad2antlr 741	. . . . . . . . . . . . . . 15 $/\$ $/\$
137	76	ad2antrr 740	. . . . . . . . . . . . . . 15 $/\$ $/\$
138	136, 137	lttri3d 9792	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
139	135, 138	mpbid 215	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140		simpr 468	. . . . . . . . . . . . 13 $/\$
141	139, 140	syl 17	. . . . . . . . . . . 12 $/\$ $/\$
142	141	iffalsed 3883	. . . . . . . . . . 11 $/\$ $/\$
143	142	mpteq2dv 4483	. . . . . . . . . 10 $/\$ $/\$
144	143	oveq2d 6324	. . . . . . . . 9 $/\$ $/\$
145		oveq2 6316	. . . . . . . . . . . . . . . . . . . . 21
146	145	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20
147	146	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$
148	81	subidd 9993	. . . . . . . . . . . . . . . . . . . . . 22
149	148	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
150		fac0 12500	. . . . . . . . . . . . . . . . . . . . . 22
151	150	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
152	149, 151	eqtrd 2505	. . . . . . . . . . . . . . . . . . . 20
153	152	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
154	147, 153	eqtrd 2505	. . . . . . . . . . . . . . . . . 18 $/\$
155	154	oveq2d 6324	. . . . . . . . . . . . . . . . 17 $/\$
156	87	div1d 10397	. . . . . . . . . . . . . . . . . 18
157	156	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
158	155, 157	eqtrd 2505	. . . . . . . . . . . . . . . 16 $/\$
159	158	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
160	145	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$
161	148	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
162	160, 161	eqtrd 2505	. . . . . . . . . . . . . . . . . 18 $/\$
163	162	oveq2d 6324	. . . . . . . . . . . . . . . . 17 $/\$
164	163	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$
165	63	exp0d 12448	. . . . . . . . . . . . . . . . 17 $/\$
166	165	adantlr 729	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	164, 166	eqtrd 2505	. . . . . . . . . . . . . . 15 $/\$ $/\$
168	159, 167	oveq12d 6326	. . . . . . . . . . . . . 14 $/\$ $/\$
169	87	mulid1d 9678	. . . . . . . . . . . . . . 15
170	169	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $/\$
171	168, 170	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$
172	171	mpteq2dva 4482	. . . . . . . . . . . 12 $/\$
173	172	oveq2d 6324	. . . . . . . . . . 11 $/\$
174	45, 50, 87	dvmptconst 37882	. . . . . . . . . . . 12
175	174	adantr 472	. . . . . . . . . . 11 $/\$
176	173, 175	eqtrd 2505	. . . . . . . . . 10 $/\$
177	176	adantlr 729	. . . . . . . . 9 $/\$ $/\$
178	137	ltp1d 10559	. . . . . . . . . . . . 13 $/\$ $/\$
179		oveq1 6315	. . . . . . . . . . . . . . 15
180	179	eqcomd 2477	. . . . . . . . . . . . . 14
181	180	adantl 473	. . . . . . . . . . . . 13 $/\$ $/\$
182	178, 181	breqtrd 4420	. . . . . . . . . . . 12 $/\$ $/\$
183	182	iftrued 3880	. . . . . . . . . . 11 $/\$ $/\$
184	183	eqcomd 2477	. . . . . . . . . 10 $/\$ $/\$
185	184	mpteq2dv 4483	. . . . . . . . 9 $/\$ $/\$
186	144, 177, 185	3eqtrd 2509	. . . . . . . 8 $/\$ $/\$
187	186	adantlr 729	. . . . . . 7 $/\$ $/\$ $/\$
188		simpll 768	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
189	188, 100, 114	3syl 18	. . . . . . . . 9 $/\$ $/\$ $/\$
190	76	ad3antrrr 744	. . . . . . . . 9 $/\$ $/\$ $/\$
191		simplr 770	. . . . . . . . 9 $/\$ $/\$ $/\$
192		neqne 2651	. . . . . . . . . . 11
193	192	necomd 2698	. . . . . . . . . 10
194	193	adantl 473	. . . . . . . . 9 $/\$ $/\$ $/\$
195	189, 190, 191, 194	leneltd 9806	. . . . . . . 8 $/\$ $/\$ $/\$
196	114	ad2antlr 741	. . . . . . . . . . . . . 14 $/\$ $/\$
197	76	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $/\$
198		simpr 468	. . . . . . . . . . . . . 14 $/\$ $/\$
199	196, 197, 198	ltled 9800	. . . . . . . . . . . . 13 $/\$ $/\$
200	196, 197	lenltd 9798	. . . . . . . . . . . . 13 $/\$ $/\$
201	199, 200	mpbid 215	. . . . . . . . . . . 12 $/\$ $/\$
202	201	iffalsed 3883	. . . . . . . . . . 11 $/\$ $/\$
203	202	mpteq2dv 4483	. . . . . . . . . 10 $/\$ $/\$
204	203	oveq2d 6324	. . . . . . . . 9 $/\$ $/\$
205	45	adantr 472	. . . . . . . . . . 11 $/\$
206	205	adantr 472	. . . . . . . . . 10 $/\$ $/\$
207	87	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$
208	100	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$
209	64	ad2antrr 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
210		nn0sub 10944	. . . . . . . . . . . . . . . 16 $/\$
211	208, 209, 210	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$
212	199, 211	mpbid 215	. . . . . . . . . . . . . 14 $/\$ $/\$
213		faccl 12507	. . . . . . . . . . . . . 14
214	212, 213	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
215	214	nncnd 10647	. . . . . . . . . . . 12 $/\$ $/\$
216	214	nnne0d 10676	. . . . . . . . . . . 12 $/\$ $/\$
217	207, 215, 216	divcld 10405	. . . . . . . . . . 11 $/\$ $/\$
218	217	adantr 472	. . . . . . . . . 10 $/\$ $/\$ $/\$
219	75	ad3antrrr 744	. . . . . . . . . 10 $/\$ $/\$ $/\$
220	50	adantr 472	. . . . . . . . . . . 12 $/\$ ℂ_fld ↾_t
221	220	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ ℂ_fld ↾_t
222	206, 221, 217	dvmptconst 37882	. . . . . . . . . 10 $/\$ $/\$
223	63	adantlr 729	. . . . . . . . . . . 12 $/\$ $/\$
224	223	adantlr 729	. . . . . . . . . . 11 $/\$ $/\$ $/\$
225	212	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ $/\$
226	224, 225	expcld 12454	. . . . . . . . . 10 $/\$ $/\$ $/\$
227	225	nn0cnd 10951	. . . . . . . . . . 11 $/\$ $/\$ $/\$
228	212	nn0zd 11061	. . . . . . . . . . . . . . . 16 $/\$ $/\$
229	196, 197	posdifd 10221	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
230	198, 229	mpbid 215	. . . . . . . . . . . . . . . 16 $/\$ $/\$
231	228, 230	jca 541	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
232		elnnz 10971	. . . . . . . . . . . . . . 15 $/\$
233	231, 232	sylibr 217	. . . . . . . . . . . . . 14 $/\$ $/\$
234		nnm1nn0 10935	. . . . . . . . . . . . . 14
235	233, 234	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
236	235	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
237	224, 236	expcld 12454	. . . . . . . . . . 11 $/\$ $/\$ $/\$
238	227, 237	mulcld 9681	. . . . . . . . . 10 $/\$ $/\$ $/\$
239	61	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$
240	206, 221, 239, 233	dvxpaek 37912	. . . . . . . . . 10 $/\$ $/\$
241	206, 218, 219, 222, 226, 238, 240	dvmptmul 22994	. . . . . . . . 9 $/\$ $/\$
242	226	mul02d 9849	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
243	242	oveq1d 6323	. . . . . . . . . . 11 $/\$ $/\$ $/\$
244	238, 218	mulcld 9681	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
245	244	addid2d 9852	. . . . . . . . . . 11 $/\$ $/\$ $/\$
246	120	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
247	119	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
248		zltp1le 11010	. . . . . . . . . . . . . . . . 17 $/\$
249	246, 247, 248	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$
250	198, 249	mpbid 215	. . . . . . . . . . . . . . 15 $/\$ $/\$
251		peano2re 9824	. . . . . . . . . . . . . . . . 17
252	196, 251	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
253	252, 197	lenltd 9798	. . . . . . . . . . . . . . 15 $/\$ $/\$
254	250, 253	mpbid 215	. . . . . . . . . . . . . 14 $/\$ $/\$
255	254	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
256	255	iffalsed 3883	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
257	218, 227, 237	mulassd 9684	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
258	257	eqcomd 2477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
259	233	nncnd 10647	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
260	207, 215, 259, 216	div32d 10428	. . . . . . . . . . . . . . . 16 $/\$ $/\$
261		facnn2 12506	. . . . . . . . . . . . . . . . . . . 20
262	233, 261	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
263	262	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
264		faccl 12507	. . . . . . . . . . . . . . . . . . . . . 22
265	234, 264	syl 17	. . . . . . . . . . . . . . . . . . . . 21
266	265	nncnd 10647	. . . . . . . . . . . . . . . . . . . 20
267	233, 266	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
268	235, 264	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
269		nnne0 10664	. . . . . . . . . . . . . . . . . . . 20
270	268, 269	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
271		nnne0 10664	. . . . . . . . . . . . . . . . . . . 20
272	233, 271	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
273	267, 259, 270, 272	divcan8d 37620	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
274	263, 273	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
275	274	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$
276		eqidd 2472	. . . . . . . . . . . . . . . 16 $/\$ $/\$
277	260, 275, 276	3eqtrd 2509	. . . . . . . . . . . . . . 15 $/\$ $/\$
278	277	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
279	81	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
280	100	nn0cnd 10951	. . . . . . . . . . . . . . . . 17 $/\$
281		1cnd 9677	. . . . . . . . . . . . . . . . 17 $/\$
282	279, 280, 281	subsub4d 10036	. . . . . . . . . . . . . . . 16 $/\$
283	282	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$
284	283	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
285	278, 284	oveq12d 6326	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
286	282	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
287	286	eqcomd 2477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
288	287	fveq2d 5883	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
289	288	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$
290	207, 267, 270	divrecd 10408	. . . . . . . . . . . . . . . 16 $/\$ $/\$
291	289, 290	eqtr2d 2506	. . . . . . . . . . . . . . 15 $/\$ $/\$
292	291	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
293	292	oveq1d 6323	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
294	258, 285, 293	3eqtrrd 2510	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
295	218, 238	mulcomd 9682	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
296	256, 294, 295	3eqtrrd 2510	. . . . . . . . . . 11 $/\$ $/\$ $/\$
297	243, 245, 296	3eqtrd 2509	. . . . . . . . . 10 $/\$ $/\$ $/\$
298	297	mpteq2dva 4482	. . . . . . . . 9 $/\$ $/\$
299	204, 241, 298	3eqtrd 2509	. . . . . . . 8 $/\$ $/\$
300	188, 195, 299	syl2anc 673	. . . . . . 7 $/\$ $/\$ $/\$
301	187, 300	pm2.61dan 808	. . . . . 6 $/\$ $/\$
302	129, 134, 301	syl2anc 673	. . . . 5 $/\$ $/\$
303	128, 302	pm2.61dan 808	. . . 4 $/\$
304	303	adantr 472	. . 3 $/\$ $/\$
305	103, 105, 304	3eqtrd 2509	. 2 $/\$ $/\$
306	11, 22, 33, 44, 97, 305	nn0indd 11055	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376

wceq 1452

wcel 1904

wne 2641

cvv 3031

wss 3390

cif 3872

cpw 3942

cpr 3961 class class class wbr 4395

cmpt 4454

wf 5585

cfv 5589 (class class class)co 6308

cpm 7491

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cdiv 10291

cn 10631

cn0 10893

cz 10961

cexp 12310

cfa 12497 ↾_t crest 15397

ctopn 15398 ℂ_fldccnfld 19047

cdv 22897

cdvn 22898

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-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-icc 11667 df-fz 11811 df-fzo 11943 df-seq 12252 df-exp 12311 df-fac 12498 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 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 df-dvn 22902

This theorem is referenced by: etransclem17 38228

W3C validator