binomcxplemnotnn0 - Mathbox for Steve Rodriguez

	Mathbox for Steve Rodriguez		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > binomcxplemnotnn0		Structured version Visualization version Unicode version

Theorem binomcxplemnotnn0 38555

Description: Lemma for binomcxp 38556. When

is not a nonnegative integer, the generalized sum in binomcxplemnn0 38548 —which we will call

—is a convergent power series: its base

is always of smaller absolute value than the radius of convergence.

pserdv2 24184 gives the derivative of , which by dvradcnv 24175 also converges in that radius. When is fixed at one, times that derivative equals and fraction is always defined with derivative zero, so the fraction is a constant—specifically one, because . Thus .

Finally, let be , and multiply both the binomial and the sum by to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020.)

**Hypotheses**
Ref	Expression
binomcxp.a
binomcxp.b
binomcxp.lt
binomcxp.c
binomcxplem.f	C_𝑐
binomcxplem.s
binomcxplem.r
binomcxplem.e
binomcxplem.d
binomcxplem.p

**Assertion**
Ref	Expression
binomcxplemnotnn0	$/\$ C_𝑐

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem binomcxplemnotnn0 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		binomcxplem.p	. . . . . . 7
2		binomcxplem.d	. . . . . . . . 9
3		nfcv 2764	. . . . . . . . . 10
4		nfcv 2764	. . . . . . . . . . 11
5		nfcv 2764	. . . . . . . . . . 11
6		binomcxplem.r	. . . . . . . . . . . 12
7		nfcv 2764	. . . . . . . . . . . . . . . 16
8		binomcxplem.s	. . . . . . . . . . . . . . . . . 18
9		nfmpt1 4747	. . . . . . . . . . . . . . . . . 18
10	8, 9	nfcxfr 2762	. . . . . . . . . . . . . . . . 17
11		nfcv 2764	. . . . . . . . . . . . . . . . 17
12	10, 11	nffv 6198	. . . . . . . . . . . . . . . 16
13	4, 7, 12	nfseq 12811	. . . . . . . . . . . . . . 15
14	13	nfel1 2779	. . . . . . . . . . . . . 14
15		nfcv 2764	. . . . . . . . . . . . . 14
16	14, 15	nfrab 3123	. . . . . . . . . . . . 13
17		nfcv 2764	. . . . . . . . . . . . 13
18		nfcv 2764	. . . . . . . . . . . . 13
19	16, 17, 18	nfsup 8357	. . . . . . . . . . . 12
20	6, 19	nfcxfr 2762	. . . . . . . . . . 11
21	4, 5, 20	nfov 6676	. . . . . . . . . 10
22	3, 21	nfima 5474	. . . . . . . . 9
23	2, 22	nfcxfr 2762	. . . . . . . 8
24		nfcv 2764	. . . . . . . 8
25		nfcv 2764	. . . . . . . 8
26		nfcv 2764	. . . . . . . . 9
27		nfcv 2764	. . . . . . . . . . 11
28	10, 27	nffv 6198	. . . . . . . . . 10
29		nfcv 2764	. . . . . . . . . 10
30	28, 29	nffv 6198	. . . . . . . . 9
31	26, 30	nfsum 14421	. . . . . . . 8
32		simpl 473	. . . . . . . . . . 11 $/\$
33	32	fveq2d 6195	. . . . . . . . . 10 $/\$
34	33	fveq1d 6193	. . . . . . . . 9 $/\$
35	34	sumeq2dv 14433	. . . . . . . 8
36	23, 24, 25, 31, 35	cbvmptf 4748	. . . . . . 7
37	1, 36	eqtri 2644	. . . . . 6
38	37	a1i 11	. . . . 5 $/\$
39		simplr 792	. . . . . . . 8 $/\$ $/\$ $/\$
40	39	fveq2d 6195	. . . . . . 7 $/\$ $/\$ $/\$
41	40	fveq1d 6193	. . . . . 6 $/\$ $/\$ $/\$
42	41	sumeq2dv 14433	. . . . 5 $/\$ $/\$
43		binomcxp.b	. . . . . . . . 9
44	43	recnd 10068	. . . . . . . 8
45	44	adantr 481	. . . . . . 7 $/\$
46		binomcxp.a	. . . . . . . . 9
47	46	rpcnd 11874	. . . . . . . 8
48	47	adantr 481	. . . . . . 7 $/\$
49		0red 10041	. . . . . . . . . 10 $/\$
50	45	abscld 14175	. . . . . . . . . 10 $/\$
51	48	abscld 14175	. . . . . . . . . 10 $/\$
52	45	absge0d 14183	. . . . . . . . . 10 $/\$
53		binomcxp.lt	. . . . . . . . . . 11
54	53	adantr 481	. . . . . . . . . 10 $/\$
55	49, 50, 51, 52, 54	lelttrd 10195	. . . . . . . . 9 $/\$
56	55	gt0ne0d 10592	. . . . . . . 8 $/\$
57	48	abs00ad 14030	. . . . . . . . 9 $/\$
58	57	necon3bid 2838	. . . . . . . 8 $/\$
59	56, 58	mpbid 222	. . . . . . 7 $/\$
60	45, 48, 59	divcld 10801	. . . . . 6 $/\$
61	60	abscld 14175	. . . . . . 7 $/\$
62	60	absge0d 14183	. . . . . . 7 $/\$
63	51	recnd 10068	. . . . . . . . . . 11 $/\$
64	63	mulid1d 10057	. . . . . . . . . 10 $/\$
65	54, 64	breqtrrd 4681	. . . . . . . . 9 $/\$
66		1red 10055	. . . . . . . . . 10 $/\$
67	51, 55	elrpd 11869	. . . . . . . . . 10 $/\$
68	50, 66, 67	ltdivmuld 11923	. . . . . . . . 9 $/\$
69	65, 68	mpbird 247	. . . . . . . 8 $/\$
70	45, 48, 59	absdivd 14194	. . . . . . . 8 $/\$
71		binomcxp.c	. . . . . . . . 9
72		binomcxplem.f	. . . . . . . . 9 C_𝑐
73	46, 43, 53, 71, 72, 8, 6	binomcxplemradcnv 38551	. . . . . . . 8 $/\$
74	69, 70, 73	3brtr4d 4685	. . . . . . 7 $/\$
75		0re 10040	. . . . . . . 8
76		ssrab2 3687	. . . . . . . . . . 11
77		ressxr 10083	. . . . . . . . . . 11
78	76, 77	sstri 3612	. . . . . . . . . 10
79		supxrcl 12145	. . . . . . . . . 10
80	78, 79	ax-mp 5	. . . . . . . . 9
81	6, 80	eqeltri 2697	. . . . . . . 8
82		elico2 12237	. . . . . . . 8 $/\$ $/\$ $/\$
83	75, 81, 82	mp2an 708	. . . . . . 7 $/\$ $/\$
84	61, 62, 74, 83	syl3anbrc 1246	. . . . . 6 $/\$
85	2	eleq2i 2693	. . . . . . 7
86		absf 14077	. . . . . . . 8
87		ffn 6045	. . . . . . . 8
88		elpreima 6337	. . . . . . . 8 $/\$
89	86, 87, 88	mp2b 10	. . . . . . 7 $/\$
90	85, 89	bitri 264	. . . . . 6 $/\$
91	60, 84, 90	sylanbrc 698	. . . . 5 $/\$
92		sumex 14418	. . . . . 6
93	92	a1i 11	. . . . 5 $/\$
94	38, 42, 91, 93	fvmptd 6288	. . . 4 $/\$
95		eqid 2622	. . . . . . . . . . . . 13
96	95	cnbl0 22577	. . . . . . . . . . . 12
97	81, 96	ax-mp 5	. . . . . . . . . . 11
98	2, 97	eqtri 2644	. . . . . . . . . 10
99		0cnd 10033	. . . . . . . . . 10 $/\$
100	81	a1i 11	. . . . . . . . . 10 $/\$
101		mulcl 10020	. . . . . . . . . . . 12 $/\$
102	101	adantl 482	. . . . . . . . . . 11 $/\$ $/\$ $/\$
103		nfv 1843	. . . . . . . . . . . . . . 15 $/\$
104	23	nfcri 2758	. . . . . . . . . . . . . . 15
105	103, 104	nfan 1828	. . . . . . . . . . . . . 14 $/\$ $/\$
106	31	nfel1 2779	. . . . . . . . . . . . . 14
107	105, 106	nfim 1825	. . . . . . . . . . . . 13 $/\$ $/\$
108		eleq1 2689	. . . . . . . . . . . . . . 15
109	108	anbi2d 740	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
110	35	eleq1d 2686	. . . . . . . . . . . . . 14
111	109, 110	imbi12d 334	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112		nn0uz 11722	. . . . . . . . . . . . . 14
113		0zd 11389	. . . . . . . . . . . . . 14 $/\$ $/\$
114		eqidd 2623	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115		cnvimass 5485	. . . . . . . . . . . . . . . . . . . 20
116	2, 115	eqsstri 3635	. . . . . . . . . . . . . . . . . . 19
117	86	fdmi 6052	. . . . . . . . . . . . . . . . . . 19
118	116, 117	sseqtri 3637	. . . . . . . . . . . . . . . . . 18
119	118	sseli 3599	. . . . . . . . . . . . . . . . 17
120	8	a1i 11	. . . . . . . . . . . . . . . . . . . 20
121		nn0ex 11298	. . . . . . . . . . . . . . . . . . . . . 22
122	121	mptex 6486	. . . . . . . . . . . . . . . . . . . . 21
123	122	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
124	120, 123	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . 19 $/\$
125		ovexd 6680	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
126	124, 125	fvmpt2d 6293	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
127	72	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ C_𝑐
128		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
129	128	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ C_𝑐 C_𝑐
130		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
131		ovexd 6680	. . . . . . . . . . . . . . . . . . . . 21 $/\$ C_𝑐
132	127, 129, 130, 131	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 20 $/\$ C_𝑐
133	132	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 $/\$ C_𝑐
134	133	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ C_𝑐
135	126, 134	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ C_𝑐
136	119, 135	sylanl2 683	. . . . . . . . . . . . . . . 16 $/\$ $/\$ C_𝑐
137	71	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
138		simpr 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
139	137, 138	bcccl 38538	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ C_𝑐
140	119	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141	140, 138	expcld 13008	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
142	139, 141	mulcld 10060	. . . . . . . . . . . . . . . 16 $/\$ $/\$ C_𝑐
143	136, 142	eqeltrd 2701	. . . . . . . . . . . . . . 15 $/\$ $/\$
144	143	adantllr 755	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
145		eleq1 2689	. . . . . . . . . . . . . . . . . . 19
146	145	anbi2d 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
147		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
148	147	seqeq3d 12809	. . . . . . . . . . . . . . . . . . . 20
149	148	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19
150		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
151	150	seqeq3d 12809	. . . . . . . . . . . . . . . . . . . 20
152	151	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19
153	149, 152	anbi12d 747	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
154	146, 153	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
155		binomcxplem.e	. . . . . . . . . . . . . . . . . 18
156	46, 43, 53, 71, 72, 8, 6, 155, 2	binomcxplemcvg 38553	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
157	154, 156	chvarv 2263	. . . . . . . . . . . . . . . 16 $/\$ $/\$
158	157	simpld 475	. . . . . . . . . . . . . . 15 $/\$
159	158	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$
160	112, 113, 114, 144, 159	isumcl 14492	. . . . . . . . . . . . 13 $/\$ $/\$
161	107, 111, 160	chvar 2262	. . . . . . . . . . . 12 $/\$ $/\$
162	161, 37	fmptd 6385	. . . . . . . . . . 11 $/\$
163		1cnd 10056	. . . . . . . . . . . . . 14 $/\$ $/\$
164	118	sseli 3599	. . . . . . . . . . . . . . 15
165	164	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
166	163, 165	addcld 10059	. . . . . . . . . . . . 13 $/\$ $/\$
167	71	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$
168	167	negcld 10379	. . . . . . . . . . . . 13 $/\$ $/\$
169	166, 168	cxpcld 24454	. . . . . . . . . . . 12 $/\$ $/\$
170		nfcv 2764	. . . . . . . . . . . . 13
171		nfcv 2764	. . . . . . . . . . . . 13
172		oveq2 6658	. . . . . . . . . . . . . 14
173	172	oveq1d 6665	. . . . . . . . . . . . 13
174	23, 24, 170, 171, 173	cbvmptf 4748	. . . . . . . . . . . 12
175	169, 174	fmptd 6385	. . . . . . . . . . 11 $/\$
176		cnex 10017	. . . . . . . . . . . . . . . 16
177		fex 6490	. . . . . . . . . . . . . . . 16 $/\$
178	86, 176, 177	mp2an 708	. . . . . . . . . . . . . . 15
179	178	cnvex 7113	. . . . . . . . . . . . . 14
180		imaexg 7103	. . . . . . . . . . . . . 14
181	179, 180	ax-mp 5	. . . . . . . . . . . . 13
182	2, 181	eqeltri 2697	. . . . . . . . . . . 12
183	182	a1i 11	. . . . . . . . . . 11 $/\$
184		inidm 3822	. . . . . . . . . . 11
185	102, 162, 175, 183, 183, 184	off 6912	. . . . . . . . . 10 $/\$
186		1ex 10035	. . . . . . . . . . . . . 14
187	186	fconst 6091	. . . . . . . . . . . . 13
188		fconstmpt 5163	. . . . . . . . . . . . . . 15
189		nfcv 2764	. . . . . . . . . . . . . . . 16
190		nfcv 2764	. . . . . . . . . . . . . . . 16
191		eqidd 2623	. . . . . . . . . . . . . . . 16
192	24, 23, 189, 190, 191	cbvmptf 4748	. . . . . . . . . . . . . . 15
193	188, 192	eqtri 2644	. . . . . . . . . . . . . 14
194	193	feq1i 6036	. . . . . . . . . . . . 13
195	187, 194	mpbi 220	. . . . . . . . . . . 12
196		ax-1cn 9994	. . . . . . . . . . . . 13
197		snssi 4339	. . . . . . . . . . . . 13
198	196, 197	ax-mp 5	. . . . . . . . . . . 12
199		fss 6056	. . . . . . . . . . . 12 $/\$
200	195, 198, 199	mp2an 708	. . . . . . . . . . 11
201	200	a1i 11	. . . . . . . . . 10 $/\$
202		cnelprrecn 10029	. . . . . . . . . . . . . . . . 17
203	202	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
204	46, 43, 53, 71, 72, 8, 6, 155, 2, 1	binomcxplemdvsum 38554	. . . . . . . . . . . . . . . . . . . 20
205	204	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
206		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
207		nfcv 2764	. . . . . . . . . . . . . . . . . . . . 21
208		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . . . 24
209	155, 208	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . . . 23
210	209, 27	nffv 6198	. . . . . . . . . . . . . . . . . . . . . 22
211	210, 29	nffv 6198	. . . . . . . . . . . . . . . . . . . . 21
212	207, 211	nfsum 14421	. . . . . . . . . . . . . . . . . . . 20
213		simpl 473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
214	213	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
215	214	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21 $/\$
216	215	sumeq2dv 14433	. . . . . . . . . . . . . . . . . . . 20
217	23, 24, 206, 212, 216	cbvmptf 4748	. . . . . . . . . . . . . . . . . . 19
218	205, 217	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 $/\$
219		sumex 14418	. . . . . . . . . . . . . . . . . . 19
220	219	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
221	218, 220	fmpt3d 6386	. . . . . . . . . . . . . . . . 17 $/\$
222		fdm 6051	. . . . . . . . . . . . . . . . 17
223	221, 222	syl 17	. . . . . . . . . . . . . . . 16 $/\$
224	46, 43, 53, 71, 72, 8, 6, 155, 2	binomcxplemdvbinom 38552	. . . . . . . . . . . . . . . . . . 19 $/\$
225		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
226		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
227	172	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21
228	227	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20
229	23, 24, 225, 226, 228	cbvmptf 4748	. . . . . . . . . . . . . . . . . . 19
230	224, 229	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 $/\$
231	168, 163	subcld 10392	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
232	166, 231	cxpcld 24454	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
233	168, 232	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
234	230, 233	fmpt3d 6386	. . . . . . . . . . . . . . . . 17 $/\$
235		fdm 6051	. . . . . . . . . . . . . . . . 17
236	234, 235	syl 17	. . . . . . . . . . . . . . . 16 $/\$
237	203, 162, 175, 223, 236	dvmulf 23706	. . . . . . . . . . . . . . 15 $/\$
238	71	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
239	238	mulid1d 10057	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
240	239	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ C_𝑐 C_𝑐
241		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
242		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . . . . 25
243		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
244		nnnn0 11299	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
245	244, 136	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ C_𝑐
246	245	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ C_𝑐
247	71	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
248		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
249	247, 248	bcccl 38538	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ C_𝑐
250	244, 249	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ C_𝑐
251	119	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
252	251	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
253	252, 248	expcld 13008	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
254	244, 253	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
255	250, 254	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ C_𝑐
256		1nn0 11308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
257	256	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
258	112, 257, 143	iserex 14387	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
259	158, 258	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
260	259	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
261	242, 243, 246, 255, 260	isumcl 14492	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ C_𝑐
262	238, 241, 261	adddid 10064	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ C_𝑐 C_𝑐
263	155	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
264		nnex 11026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
265	264	mptex 6486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
266	265	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
267	263, 266	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
268	119, 267	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
269	268	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
270		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
271	269, 270	fmpt3d 6386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
272	271	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
273		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
274	267, 273	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
275	244, 132	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ C_𝑐
276	275	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ C_𝑐
277	276	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ C_𝑐
278	277	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ C_𝑐
279	274, 278	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ C_𝑐
280	71	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
281		nnm1nn0 11334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
282	281	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
283	280, 282	bccp1k 38540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ C_𝑐 C_𝑐
284	244	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
285	284	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
286		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
287	285, 286	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
288	287	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ C_𝑐 C_𝑐
289	287	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
290	289	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ C_𝑐 C_𝑐
291	283, 288, 290	3eqtr3d 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ C_𝑐 C_𝑐
292	291	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ C_𝑐 C_𝑐
293	280, 282	bcccl 38538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ C_𝑐
294	285, 286	subcld 10392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
295	280, 294	subcld 10392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
296		nnne0 11053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
297	296	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
298	293, 295, 285, 297	divassd 10836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ C_𝑐 C_𝑐
299	298	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ C_𝑐 C_𝑐
300	293, 295	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ C_𝑐
301	300, 285, 297	divcan2d 10803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ C_𝑐 C_𝑐
302	292, 299, 301	3eqtr2d 2662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ C_𝑐 C_𝑐
303	302	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ C_𝑐 C_𝑐
304	303	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ C_𝑐 C_𝑐
305	293	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ C_𝑐
306	295	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
307	305, 306	mulcomd 10061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ C_𝑐 C_𝑐
308	307	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ C_𝑐 C_𝑐
309	279, 304, 308	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ C_𝑐
310	119, 309	sylanl2 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ C_𝑐
311	310	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ C_𝑐
312	311	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ C_𝑐
313	272, 312	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ C_𝑐
314	313	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ C_𝑐
315		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C_𝑐 C_𝑐
316		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C_𝑐
317		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
318	317	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
319	317	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 C_𝑐 C_𝑐
320	318, 319	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 C_𝑐 C_𝑐
321	317	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
322	320, 321	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C_𝑐 C_𝑐
323		1pneg1e0 11129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
324	323	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
325	112, 324	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
326	243	znegcld 11484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
327	315, 316, 322, 242, 325, 243, 326	uzmptshftfval 38545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ C_𝑐 C_𝑐
328		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
329	328	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
330	329	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
331	329	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 C_𝑐 C_𝑐
332	330, 331	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 C_𝑐 C_𝑐
333	329	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
334	332, 333	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 C_𝑐 C_𝑐
335	334	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C_𝑐 C_𝑐
336	335	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ C_𝑐 C_𝑐
337	314, 327, 336	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ C_𝑐
338		nn0cn 11302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
339		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
340	338, 339	subnegd 10399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
341	340	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
342	338, 339	pncand 10393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
343	341, 342	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
344	343	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
345	344	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
346	344	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
347	345, 346	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
348	344	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
349	347, 348	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
350	349	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ C_𝑐 C_𝑐
351	337, 350	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ C_𝑐
352		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ C_𝑐
353	351, 352	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ C_𝑐
354	244, 353	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ C_𝑐
355	338	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
356	247, 355	subcld 10392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
357	356, 249	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ C_𝑐
358	357, 253	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ C_𝑐
359	244, 358	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ C_𝑐
360		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
361	360	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
362	361	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
363	311	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ C_𝑐
364	251	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
365	71	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
366		nncn 11028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
367	366	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
368		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
369	367, 368	subcld 10392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
370	365, 369	subcld 10392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
371	281	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
372	365, 371	bcccl 38538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ C_𝑐
373	370, 372	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ C_𝑐
374	364, 371	expcld 13008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
375	364, 373, 374	mul12d 10245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
376	364, 374	mulcomd 10061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
377	364, 371	expp1d 13009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
378	287	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
379	378	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
380	379	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
381	376, 377, 380	3eqtr2d 2662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
382	381	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
383	375, 382	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
384	363, 383	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ C_𝑐
385	384	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ C_𝑐
386	362, 385	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐
387		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ C_𝑐
388	386, 387	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ C_𝑐
389	373, 254	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ C_𝑐
390		climrel 14223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
391	157	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
392	391	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
393		climdm 14285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
394	392, 393	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
395		0z 11388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
396		neg1z 11413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
397		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
398	397	seqshft 13825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
399	395, 396, 398	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
400		0cn 10032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
401	400, 196	subnegi 10360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
402		0p1e1 11132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
403	401, 402	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
404		seqeq1 12804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
405	403, 404	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
406	405	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
407	399, 406	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
408	407	breq1i 4660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
409		seqex 12803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
410		climshft 14307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
411	396, 409, 410	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
412	408, 411	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
413	394, 412	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
414		releldm 5358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
415	390, 413, 414	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
416	256	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
417	353, 358	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
418	112, 416, 417	iserex 14387	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
419	415, 418	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
420	373, 374	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ C_𝑐
421	311, 420	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
422	388, 384	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
423	242, 243, 251, 394, 421, 422	isermulc2 14388	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
424		releldm 5358	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
425	390, 423, 424	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
426	242, 243, 354, 359, 388, 389, 419, 425	isumadd 14498	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐 C_𝑐
427	426	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐 C_𝑐
428	365, 367	subcld 10392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
429	428, 250	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ C_𝑐
430	429, 373, 254	adddird 10065	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐 C_𝑐
431	430	sumeq2dv 14433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐 C_𝑐
432	431	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐 C_𝑐
433	309	sumeq2dv 14433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ C_𝑐
434	433	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ C_𝑐
435	119, 434	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ C_𝑐
436	435	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ C_𝑐
437	242, 243, 311, 420, 392	isumcl 14492	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐
438	241, 251, 437	adddird 10065	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐
439	437	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐 C_𝑐
440	242, 243, 311, 420, 392, 251	isummulc2 14493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ C_𝑐 C_𝑐
441	383	sumeq2dv 14433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ C_𝑐 C_𝑐
442	440, 441	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐 C_𝑐
443	439, 442	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐 C_𝑐
444	436, 438, 443	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ C_𝑐 C_𝑐
445	402	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
446	242, 445	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
447		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
448	447	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
449	447	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C_𝑐 C_𝑐
450	448, 449	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 C_𝑐 C_𝑐
451	447	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
452	450, 451	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C_𝑐 C_𝑐
453	112, 446, 452, 243, 113, 420	isumshft 14571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ C_𝑐 C_𝑐
454		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
455	454	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
456	455	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
457	455	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 C_𝑐 C_𝑐
458	456, 457	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C_𝑐 C_𝑐
459	455	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
460	458, 459	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 C_𝑐 C_𝑐
461	460	cbvsumv 14426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C_𝑐 C_𝑐
462	461	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ C_𝑐 C_𝑐
463		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
464	463, 355	pncan2d 10394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
465	464	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
466	464	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
467	465, 466	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
468	464	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
469	467, 468	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
470	469	sumeq2dv 14433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ C_𝑐 C_𝑐
471	453, 462, 470	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐 C_𝑐
472	112, 113, 353, 358, 415	isum1p 14573	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐 C_𝑐
473		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
474	473	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
475	473	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
476	474, 475	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
477	473	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
478	476, 477	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
479		0nn0 11307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
480	479	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
481		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ C_𝑐
482	351, 478, 480, 481	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ C_𝑐
483	238	subid1d 10381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
484	238	bccn0 38542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ C_𝑐
485	483, 484	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ C_𝑐
486	485, 239	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ C_𝑐
487	251	exp0d 13002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
488	486, 487	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ C_𝑐
489	482, 488, 239	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
490	446	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
491	490	sumeq1i 14428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C_𝑐 C_𝑐
492	491	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ C_𝑐 C_𝑐
493	489, 492	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐 C_𝑐
494	471, 472, 493	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ C_𝑐 C_𝑐
495	494	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐 C_𝑐
496	242, 243, 354, 359, 419	isumcl 14492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ C_𝑐
497	251, 437	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐
498	442, 497	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ C_𝑐
499	238, 496, 498	addassd 10062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐 C_𝑐
500	444, 495, 499	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ C_𝑐 C_𝑐
501	427, 432, 500	3eqtr4rd 2667	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ C_𝑐 C_𝑐
502		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
503	280, 502	binomcxplemwb 38547	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ C_𝑐 C_𝑐 C_𝑐
504	503	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ C_𝑐 C_𝑐 C_𝑐
505	504	sumeq2dv 14433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 C_𝑐 C_𝑐 C_𝑐
506	505	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 C_𝑐 C_𝑐 C_𝑐
507	506	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ C_𝑐 C_𝑐 C_𝑐
508	365, 250, 254	mulassd 10063	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ C_𝑐 C_𝑐
509	508	sumeq2dv 14433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ C_𝑐 C_𝑐
510	242, 243, 246, 255, 260, 238	isummulc2 14493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ C_𝑐 C_𝑐
511	509, 510	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ C_𝑐 C_𝑐
512	511	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ C_𝑐 C_𝑐
513	501, 507, 512	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ C_𝑐
514	240, 262, 513	3eqtr4rd 2667	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ C_𝑐
515	8	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
516	122	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
517	515, 516	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
518	119, 517	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
519		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
520	518, 519	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
521	520	sumeq2dv 14433	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
522	71	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
523	522, 130	bcccl 38538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ C_𝑐
524	132, 523	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
525	524	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
526	525	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
527	526, 253	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
528	112, 113, 520, 527, 159	isum1p 14573	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
529	473	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
530	529, 477	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
531		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
532	518, 530, 480, 531	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
533	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C_𝑐
534		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
535	534	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ C_𝑐 C_𝑐
536	479	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
537		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C_𝑐
538	533, 535, 536, 537	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 C_𝑐
539	538	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐
540	539, 484	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
541	540, 487	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
542	241	mulid1d 10057	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
543	532, 541, 542	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
544	490	sumeq1i 14428	. . . . . . . . . . . . . . . . . . . . . . . . . 26
545	133	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ C_𝑐
546	244, 545	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ C_𝑐
547	546	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ C_𝑐
548	547	sumeq2dv 14433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ C_𝑐
549	544, 548	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ C_𝑐
550	543, 549	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ C_𝑐
551	521, 528, 550	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ C_𝑐
552	551	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ C_𝑐
553	514, 552	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
554	238, 160	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
555	241, 251	addcld 10059	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
556		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
557	242, 243, 556, 421, 392	isumcl 14492	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
558	241, 251	subnegd 10399	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
559	251	negcld 10379	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
560		elpreima 6337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
561	86, 87, 560	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
562	561	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
563	562, 2	eleq2s 2719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
564		elico2 12237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
565	75, 81, 564	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
566	565	simp3bi 1078	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
567	563, 566	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
568	567	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
569	251	absnegd 14188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
570	569	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
571	73	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
572	568, 570, 571	3brtr3d 4684	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
573		1re 10039	. . . . . . . . . . . . . . . . . . . . . . . . 25
574		abssubne0 14056	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
575	573, 574	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
576	559, 572, 575	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
577	558, 576	eqnetrrd 2862	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
578	554, 555, 557, 577	divmuld 10823	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
579	553, 578	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
580	238, 160, 555, 577	div23d 10838	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
581	579, 580	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
582	581	mpteq2dva 4744	. . . . . . . . . . . . . . . . . 18 $/\$
583		ovexd 6680	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
584		sumex 14418	. . . . . . . . . . . . . . . . . . . 20
585	584	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
586		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 $/\$
587	1	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
588	103, 23, 183, 583, 585, 586, 587	offval2f 6909	. . . . . . . . . . . . . . . . . 18 $/\$
589	582, 205, 588	3eqtr4d 2666	. . . . . . . . . . . . . . . . 17 $/\$
590	589	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$
591	224	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$
592	590, 591	oveq12d 6668	. . . . . . . . . . . . . . 15 $/\$
593		ovexd 6680	. . . . . . . . . . . . . . . 16 $/\$ $/\$
594		ovexd 6680	. . . . . . . . . . . . . . . 16 $/\$ $/\$
595		ovexd 6680	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
596		ovexd 6680	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
597		eqidd 2623	. . . . . . . . . . . . . . . . 17 $/\$
598	103, 23, 183, 595, 596, 588, 597	offval2f 6909	. . . . . . . . . . . . . . . 16 $/\$
599		ovexd 6680	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
600		eqidd 2623	. . . . . . . . . . . . . . . . 17 $/\$
601	103, 23, 183, 599, 585, 600, 587	offval2f 6909	. . . . . . . . . . . . . . . 16 $/\$
602	103, 23, 183, 593, 594, 598, 601	offval2f 6909	. . . . . . . . . . . . . . 15 $/\$
603	237, 592, 602	3eqtrd 2660	. . . . . . . . . . . . . 14 $/\$
604	238, 555, 577	divcld 10801	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
605	238	negcld 10379	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
606	555, 605	cxpcld 24454	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
607	604, 160, 606	mul32d 10246	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
608	238, 555, 606, 577	div32d 10824	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
609	555, 577, 605, 241	cxpsubd 24464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
610	555	cxp1d 24452	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
611	610	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
612	609, 611	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
613	612	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
614	608, 613	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
615	614	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
616	607, 615	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
617	605, 241	subcld 10392	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
618	555, 617	cxpcld 24454	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
619	238, 618	mulneg1d 10483	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
620	619	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
621	238, 618	mulcld 10060	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
622	621, 160	mulneg1d 10483	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
623	620, 622	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
624	616, 623	oveq12d 6668	. . . . . . . . . . . . . . . 16 $/\$ $/\$
625	621, 160	mulcld 10060	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
626	625	negidd 10382	. . . . . . . . . . . . . . . 16 $/\$ $/\$
627	624, 626	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ $/\$
628	627	mpteq2dva 4744	. . . . . . . . . . . . . 14 $/\$
629	603, 628	eqtrd 2656	. . . . . . . . . . . . 13 $/\$
630		nfcv 2764	. . . . . . . . . . . . . 14
631		eqidd 2623	. . . . . . . . . . . . . 14
632	24, 23, 4, 630, 631	cbvmptf 4748	. . . . . . . . . . . . 13
633	629, 632	syl6eqr 2674	. . . . . . . . . . . 12 $/\$
634		c0ex 10034	. . . . . . . . . . . . . 14
635	634	snid 4208	. . . . . . . . . . . . 13
636	635	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
637	633, 636	fmpt3d 6386	. . . . . . . . . . 11 $/\$
638		fdm 6051	. . . . . . . . . . 11
639	637, 638	syl 17	. . . . . . . . . 10 $/\$
640		1cnd 10056	. . . . . . . . . . . . 13 $/\$ $/\$
641		0cnd 10033	. . . . . . . . . . . . 13 $/\$ $/\$
642		dvconst 23680	. . . . . . . . . . . . . . . 16
643	196, 642	ax-mp 5	. . . . . . . . . . . . . . 15
644		fconstmpt 5163	. . . . . . . . . . . . . . . 16
645	644	oveq2i 6661	. . . . . . . . . . . . . . 15
646		fconstmpt 5163	. . . . . . . . . . . . . . 15
647	643, 645, 646	3eqtr3i 2652	. . . . . . . . . . . . . 14
648	647	a1i 11	. . . . . . . . . . . . 13 $/\$
649	118	a1i 11	. . . . . . . . . . . . 13 $/\$
650		fvex 6201	. . . . . . . . . . . . . . 15 ℂ_fld
651		cnfldtps 22581	. . . . . . . . . . . . . . . . 17 ℂ_fld
652		cnfldbas 19750	. . . . . . . . . . . . . . . . . 18 ℂ_fld
653		eqid 2622	. . . . . . . . . . . . . . . . . 18 ℂ_fld ℂ_fld
654	652, 653	tpsuni 20740	. . . . . . . . . . . . . . . . 17 ℂ_fld ℂ_fld
655	651, 654	ax-mp 5	. . . . . . . . . . . . . . . 16 ℂ_fld
656	655	restid 16094	. . . . . . . . . . . . . . 15 ℂ_fld ℂ_fld ↾_t ℂ_fld
657	650, 656	ax-mp 5	. . . . . . . . . . . . . 14 ℂ_fld ↾_t ℂ_fld
658	657	eqcomi 2631	. . . . . . . . . . . . 13 ℂ_fld ℂ_fld ↾_t
659	653	cnfldtop 22587	. . . . . . . . . . . . . . 15 ℂ_fld
660		cnxmet 22576	. . . . . . . . . . . . . . . . 17
661	653	cnfldtopn 22585	. . . . . . . . . . . . . . . . . 18 ℂ_fld
662	661	blopn 22305	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ℂ_fld
663	660, 400, 81, 662	mp3an 1424	. . . . . . . . . . . . . . . 16 ℂ_fld
664	98, 663	eqeltri 2697	. . . . . . . . . . . . . . 15 ℂ_fld
665		isopn3i 20886	. . . . . . . . . . . . . . 15 ℂ_fld $/\$ ℂ_fld ℂ_fld
666	659, 664, 665	mp2an 708	. . . . . . . . . . . . . 14 ℂ_fld
667	666	a1i 11	. . . . . . . . . . . . 13 $/\$ ℂ_fld
668	203, 640, 641, 648, 649, 658, 653, 667	dvmptres2 23725	. . . . . . . . . . . 12 $/\$
669	192	oveq2i 6661	. . . . . . . . . . . 12
670	668, 669, 632	3eqtr3g 2679	. . . . . . . . . . 11 $/\$
671	628, 603, 670	3eqtr4d 2666	. . . . . . . . . 10 $/\$
672		1rp 11836	. . . . . . . . . . . . 13
673	73, 672	syl6eqel 2709	. . . . . . . . . . . 12 $/\$
674		blcntr 22218	. . . . . . . . . . . . 13 $/\$ $/\$
675	660, 400, 674	mp3an12 1414	. . . . . . . . . . . 12
676	673, 675	syl 17	. . . . . . . . . . 11 $/\$
677	676, 98	syl6eleqr 2712	. . . . . . . . . 10 $/\$
678		0zd 11389	. . . . . . . . . . . . . . 15 $/\$
679		eqidd 2623	. . . . . . . . . . . . . . 15 $/\$ $/\$
680		nfv 1843	. . . . . . . . . . . . . . . . . . . 20
681	23	nfel2 2781	. . . . . . . . . . . . . . . . . . . 20
682	680, 681	nfan 1828	. . . . . . . . . . . . . . . . . . 19 $/\$
683		nfv 1843	. . . . . . . . . . . . . . . . . . 19
684	682, 683	nfan 1828	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
685	10, 4	nffv 6198	. . . . . . . . . . . . . . . . . . . 20
686	685, 29	nffv 6198	. . . . . . . . . . . . . . . . . . 19
687	686	nfel1 2779	. . . . . . . . . . . . . . . . . 18
688	684, 687	nfim 1825	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
689		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20
690	689	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
691	690	anbi1d 741	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
692		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
693	692	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
694	693	eleq1d 2686	. . . . . . . . . . . . . . . . . 18
695	691, 694	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
696	688, 634, 695, 143	vtoclf 3258	. . . . . . . . . . . . . . . 16 $/\$ $/\$
697	677, 696	syldanl 735	. . . . . . . . . . . . . . 15 $/\$ $/\$
698	4, 7, 685	nfseq 12811	. . . . . . . . . . . . . . . . . . 19
699	698	nfel1 2779	. . . . . . . . . . . . . . . . . 18
700	682, 699	nfim 1825	. . . . . . . . . . . . . . . . 17 $/\$
701	692	seqeq3d 12809	. . . . . . . . . . . . . . . . . . 19
702	701	eleq1d 2686	. . . . . . . . . . . . . . . . . 18
703	690, 702	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
704	700, 634, 703, 158	vtoclf 3258	. . . . . . . . . . . . . . . 16 $/\$
705	677, 704	syldan 487	. . . . . . . . . . . . . . 15 $/\$
706	112, 678, 679, 697, 705	isum1p 14573	. . . . . . . . . . . . . 14 $/\$
707	132	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ C_𝑐
708	707	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ C_𝑐
709		simplr 792	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
710	709	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
711	708, 710	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ C_𝑐
712	711	mpteq2dva 4744	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ C_𝑐
713	121	mptex 6486	. . . . . . . . . . . . . . . . . . 19 C_𝑐
714	713	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ C_𝑐
715	515, 712, 99, 714	fvmptd 6288	. . . . . . . . . . . . . . . . 17 $/\$ C_𝑐
716		simpr 477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
717	716	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ C_𝑐 C_𝑐
718	716	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
719	717, 718	oveq12d 6668	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ C_𝑐 C_𝑐
720	479	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
721		ovexd 6680	. . . . . . . . . . . . . . . . 17 $/\$ C_𝑐
722	715, 719, 720, 721	fvmptd 6288	. . . . . . . . . . . . . . . 16 $/\$ C_𝑐
723	71	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
724	723	bccn0 38542	. . . . . . . . . . . . . . . . 17 $/\$ C_𝑐
725	99	exp0d 13002	. . . . . . . . . . . . . . . . 17 $/\$
726	724, 725	oveq12d 6668	. . . . . . . . . . . . . . . 16 $/\$ C_𝑐
727		1t1e1 11175	. . . . . . . . . . . . . . . . 17
728	727	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
729	722, 726, 728	3eqtrd 2660	. . . . . . . . . . . . . . 15 $/\$
730		ovexd 6680	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ C_𝑐
731	715, 730	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ C_𝑐
732	244, 731	sylan2 491	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ C_𝑐
733		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
734	733	0expd 13024	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
735	734	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ C_𝑐 C_𝑐
736	523	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ C_𝑐
737	244, 736	sylan2 491	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ C_𝑐
738	737	mul01d 10235	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ C_𝑐
739	732, 735, 738	3eqtrd 2660	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
740	739	sumeq2dv 14433	. . . . . . . . . . . . . . . 16 $/\$
741	446	sumeq1i 14428	. . . . . . . . . . . . . . . 16
742	242	eqimssi 3659	. . . . . . . . . . . . . . . . . 18
743	742	orci 405	. . . . . . . . . . . . . . . . 17 $\/$
744		sumz 14453	. . . . . . . . . . . . . . . . 17 $\/$
745	743, 744	ax-mp 5	. . . . . . . . . . . . . . . 16
746	740, 741, 745	3eqtr3g 2679	. . . . . . . . . . . . . . 15 $/\$
747	729, 746	oveq12d 6668	. . . . . . . . . . . . . 14 $/\$
748	706, 747	eqtrd 2656	. . . . . . . . . . . . 13 $/\$
749		1p0e1 11133	. . . . . . . . . . . . . . 15
750	749	oveq1i 6660	. . . . . . . . . . . . . 14
751	723	negcld 10379	. . . . . . . . . . . . . . 15 $/\$
752	751	1cxpd 24453	. . . . . . . . . . . . . 14 $/\$
753	750, 752	syl5eq 2668	. . . . . . . . . . . . 13 $/\$
754	748, 753	oveq12d 6668	. . . . . . . . . . . 12 $/\$
755	749	oveq1i 6660	. . . . . . . . . . . . 13
756	755, 727	eqtri 2644	. . . . . . . . . . . 12
757	754, 756	syl6eq 2672	. . . . . . . . . . 11 $/\$
758		ffn 6045	. . . . . . . . . . . . . 14
759	162, 758	syl 17	. . . . . . . . . . . . 13 $/\$
760		ffn 6045	. . . . . . . . . . . . . 14
761	175, 760	syl 17	. . . . . . . . . . . . 13 $/\$
762	37	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
763		simplr 792	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
764	763	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
765	764	fveq1d 6193	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
766	765	sumeq2dv 14433	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
767		simpr 477	. . . . . . . . . . . . . 14 $/\$ $/\$
768		sumex 14418	. . . . . . . . . . . . . . 15
769	768	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
770	762, 766, 767, 769	fvmptd 6288	. . . . . . . . . . . . 13 $/\$ $/\$
771	174	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
772		simpr 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
773	772	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
774	773	oveq1d 6665	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
775		ovexd 6680	. . . . . . . . . . . . . 14 $/\$ $/\$
776	771, 774, 767, 775	fvmptd 6288	. . . . . . . . . . . . 13 $/\$ $/\$
777	759, 761, 183, 183, 184, 770, 776	ofval 6906	. . . . . . . . . . . 12 $/\$ $/\$
778	677, 777	mpdan 702	. . . . . . . . . . 11 $/\$
779	193	fveq1i 6192	. . . . . . . . . . . 12
780	186	fvconst2 6469	. . . . . . . . . . . . 13
781	677, 780	syl 17	. . . . . . . . . . . 12 $/\$
782	779, 781	syl5eqr 2670	. . . . . . . . . . 11 $/\$
783	757, 778, 782	3eqtr4d 2666	. . . . . . . . . 10 $/\$
784	98, 99, 100, 185, 201, 639, 671, 677, 783	dv11cn 23764	. . . . . . . . 9 $/\$
785	784	oveq1d 6665	. . . . . . . 8 $/\$
786		nfv 1843	. . . . . . . . . . . . . 14
787	105, 786	nfim 1825	. . . . . . . . . . . . 13 $/\$ $/\$
788	172	neeq1d 2853	. . . . . . . . . . . . . 14
789	109, 788	imbi12d 334	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
790	787, 789, 577	chvar 2262	. . . . . . . . . . . 12 $/\$ $/\$
791	166, 790, 168	cxpne0d 24459	. . . . . . . . . . 11 $/\$ $/\$
792		eldifsn 4317	. . . . . . . . . . 11 $\$ $/\$
793	169, 791, 792	sylanbrc 698	. . . . . . . . . 10 $/\$ $/\$ $\$
794	793, 174	fmptd 6385	. . . . . . . . 9 $/\$ $\$
795		ofdivcan4 38526	. . . . . . . . 9 $/\$ $/\$ $\$
796	183, 162, 794, 795	syl3anc 1326	. . . . . . . 8 $/\$
797		eqidd 2623	. . . . . . . . 9 $/\$
798	103, 23, 183, 241, 606, 797, 597	offval2f 6909	. . . . . . . 8 $/\$
799	785, 796, 798	3eqtr3d 2664	. . . . . . 7 $/\$
800	555, 577, 605	cxpnegd 24461	. . . . . . . . 9 $/\$ $/\$
801	238	negnegd 10383	. . . . . . . . . 10 $/\$ $/\$
802	801	oveq2d 6666	. . . . . . . . 9 $/\$ $/\$
803	800, 802	eqtr3d 2658	. . . . . . . 8 $/\$ $/\$
804	803	mpteq2dva 4744	. . . . . . 7 $/\$
805	799, 804	eqtrd 2656	. . . . . 6 $/\$
806		nfcv 2764	. . . . . . 7
807		nfcv 2764	. . . . . . 7
808	172	oveq1d 6665	. . . . . . 7
809	23, 24, 806, 807, 808	cbvmptf 4748	. . . . . 6
810	805, 809	syl6eq 2672	. . . . 5 $/\$
811		simpr 477	. . . . . . 7 $/\$ $/\$
812	811	oveq2d 6666	. . . . . 6 $/\$ $/\$
813	812	oveq1d 6665	. . . . 5 $/\$ $/\$
814		1cnd 10056	. . . . . . 7 $/\$
815	814, 60	addcld 10059	. . . . . 6 $/\$
816	815, 723	cxpcld 24454	. . . . 5 $/\$
817	810, 813, 91, 816	fvmptd 6288	. . . 4 $/\$
818	707	adantlr 751	. . . . . . . . 9 $/\$ $/\$ $/\$ C_𝑐
819		simplr 792	. . . . . . . . . 10 $/\$ $/\$ $/\$
820	819	oveq1d 6665	. . . . . . . . 9 $/\$ $/\$ $/\$
821	818, 820	oveq12d 6668	. . . . . . . 8 $/\$ $/\$ $/\$ C_𝑐
822	821	mpteq2dva 4744	. . . . . . 7 $/\$ $/\$ C_𝑐
823	121	mptex 6486	. . . . . . . 8 C_𝑐
824	823	a1i 11	. . . . . . 7 $/\$ C_𝑐
825	515, 822, 60, 824	fvmptd 6288	. . . . . 6 $/\$ C_𝑐
826		ovexd 6680	. . . . . 6 $/\$ $/\$ C_𝑐
827	825, 826	fvmpt2d 6293	. . . . 5 $/\$ $/\$ C_𝑐
828	827	sumeq2dv 14433	. . . 4 $/\$ C_𝑐
829	94, 817, 828	3eqtr3d 2664	. . 3 $/\$ C_𝑐
830	829	oveq1d 6665	. 2 $/\$ C_𝑐
831	43, 46	rerpdivcld 11903	. . . . . 6
832	831	adantr 481	. . . . 5 $/\$
833	66, 832	readdcld 10069	. . . 4 $/\$
834		df-neg 10269	. . . . . . 7
835	831	recnd 10068	. . . . . . . . . . . 12
836	835	negcld 10379	. . . . . . . . . . 11
837	836	abscld 14175	. . . . . . . . . 10
838		1red 10055	. . . . . . . . . 10
839	835	absnegd 14188	. . . . . . . . . . . 12
840	46	rpne0d 11877	. . . . . . . . . . . . 13
841	44, 47, 840	absdivd 14194	. . . . . . . . . . . 12
842	839, 841	eqtrd 2656	. . . . . . . . . . 11
843	44	abscld 14175	. . . . . . . . . . . 12
844	672	a1i 11	. . . . . . . . . . . 12
845	47, 840	absrpcld 14187	. . . . . . . . . . . 12
846	843	recnd 10068	. . . . . . . . . . . . . 14
847	846	div1d 10793	. . . . . . . . . . . . 13
848	847, 53	eqbrtrd 4675	. . . . . . . . . . . 12
849	843, 844, 845, 848	ltdiv23d 11937	. . . . . . . . . . 11
850	842, 849	eqbrtrd 4675	. . . . . . . . . 10
851	837, 838, 850	ltled 10185	. . . . . . . . 9
852	831	renegcld 10457	. . . . . . . . . 10
853	852, 838	absled 14169	. . . . . . . . 9 $/\$
854	851, 853	mpbid 222	. . . . . . . 8 $/\$
855	854	simprd 479	. . . . . . 7
856	834, 855	syl5eqbrr 4689	. . . . . 6
857		0red 10041	. . . . . . 7
858	857, 831, 838	lesubaddd 10624	. . . . . 6
859	856, 858	mpbid 222	. . . . 5
860	859	adantr 481	. . . 4 $/\$
861	46	adantr 481	. . . . 5 $/\$
862	861	rpred 11872	. . . 4 $/\$
863	861	rpge0d 11876	. . . 4 $/\$
864	833, 860, 862, 863, 723	mulcxpd 24474	. . 3 $/\$
865	814, 60, 48	adddird 10065	. . . . 5 $/\$
866	48	mulid2d 10058	. . . . . 6 $/\$
867	45, 48, 59	divcan1d 10802	. . . . . 6 $/\$
868	866, 867	oveq12d 6668	. . . . 5 $/\$
869	865, 868	eqtrd 2656	. . . 4 $/\$
870	869	oveq1d 6665	. . 3 $/\$
871	864, 870	eqtr3d 2658	. 2 $/\$
872	60	adantr 481	. . . . . 6 $/\$ $/\$
873		simpr 477	. . . . . 6 $/\$ $/\$
874	872, 873	expcld 13008	. . . . 5 $/\$ $/\$
875	736, 874	mulcld 10060	. . . 4 $/\$ $/\$ C_𝑐
876	46, 43, 53, 71, 72, 8, 6, 155, 2	binomcxplemcvg 38553	. . . . . 6 $/\$ $/\$
877	876	simpld 475	. . . . 5 $/\$
878	91, 877	syldan 487	. . . 4 $/\$
879	48, 723	cxpcld 24454	. . . 4 $/\$
880	112, 678, 827, 875, 878, 879	isummulc1 14494	. . 3 $/\$ C_𝑐 C_𝑐
881	44	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$
882	47	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$
883	840	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$
884	881, 882, 883	divrecd 10804	. . . . . . . . . . . 12 $/\$ $/\$
885	884	oveq1d 6665	. . . . . . . . . . 11 $/\$ $/\$
886	882, 883	reccld 10794	. . . . . . . . . . . 12 $/\$ $/\$
887	881, 886, 873	mulexpd 13023	. . . . . . . . . . 11 $/\$ $/\$
888	885, 887	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$
889	888	oveq2d 6666	. . . . . . . . 9 $/\$ $/\$ C_𝑐 C_𝑐
890	881, 873	expcld 13008	. . . . . . . . . 10 $/\$ $/\$
891	886, 873	expcld 13008	. . . . . . . . . 10 $/\$ $/\$
892	736, 890, 891	mulassd 10063	. . . . . . . . 9 $/\$ $/\$ C_𝑐 C_𝑐
893	889, 892	eqtr4d 2659	. . . . . . . 8 $/\$ $/\$ C_𝑐 C_𝑐
894	893	oveq1d 6665	. . . . . . 7 $/\$ $/\$ C_𝑐 C_𝑐
895	736, 890	mulcld 10060	. . . . . . . 8 $/\$ $/\$ C_𝑐
896	879	adantr 481	. . . . . . . 8 $/\$ $/\$
897	895, 891, 896	mul32d 10246	. . . . . . 7 $/\$ $/\$ C_𝑐 C_𝑐
898	895, 896, 891	mulassd 10063	. . . . . . 7 $/\$ $/\$ C_𝑐 C_𝑐
899	894, 897, 898	3eqtrd 2660	. . . . . 6 $/\$ $/\$ C_𝑐 C_𝑐
900	873	nn0cnd 11353	. . . . . . . . . 10 $/\$ $/\$
901	882, 900	cxpcld 24454	. . . . . . . . 9 $/\$ $/\$
902	882, 883, 900	cxpne0d 24459	. . . . . . . . 9 $/\$ $/\$
903	896, 901, 902	divrecd 10804	. . . . . . . 8 $/\$ $/\$
904	71	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$
905	882, 883, 904, 900	cxpsubd 24464	. . . . . . . 8 $/\$ $/\$
906	873	nn0zd 11480	. . . . . . . . . . 11 $/\$ $/\$
907	882, 883, 906	exprecd 13016	. . . . . . . . . 10 $/\$ $/\$
908		cxpexp 24414	. . . . . . . . . . . 12 $/\$
909	882, 873, 908	syl2anc 693	. . . . . . . . . . 11 $/\$ $/\$
910	909	oveq2d 6666	. . . . . . . . . 10 $/\$ $/\$
911	907, 910	eqtr4d 2659	. . . . . . . . 9 $/\$ $/\$
912	911	oveq2d 6666	. . . . . . . 8 $/\$ $/\$
913	903, 905, 912	3eqtr4rd 2667	. . . . . . 7 $/\$ $/\$
914	913	oveq2d 6666	. . . . . 6 $/\$ $/\$ C_𝑐 C_𝑐
915	904, 900	subcld 10392	. . . . . . . 8 $/\$ $/\$
916	882, 915	cxpcld 24454	. . . . . . 7 $/\$ $/\$
917	736, 890, 916	mul32d 10246	. . . . . 6 $/\$ $/\$ C_𝑐 C_𝑐
918	899, 914, 917	3eqtrd 2660	. . . . 5 $/\$ $/\$ C_𝑐 C_𝑐
919	736, 916, 890	mulassd 10063	. . . . 5 $/\$ $/\$ C_𝑐 C_𝑐
920	918, 919	eqtrd 2656	. . . 4 $/\$ $/\$ C_𝑐 C_𝑐
921	920	sumeq2dv 14433	. . 3 $/\$ C_𝑐 C_𝑐
922	880, 921	eqtrd 2656	. 2 $/\$ C_𝑐 C_𝑐
923	830, 871, 922	3eqtr3d 2664	1 $/\$ C_𝑐

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

crab 2916

cvv 3200 $\$ cdif 3571

wss 3574

csn 4177

cpr 4179

cuni 4436 class class class wbr 4653

cmpt 4729

cxp 5112

ccnv 5113

cdm 5114

cima 5117

ccom 5118

wrel 5119

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cof 6895

cfn 7955

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

cn 11020

cn0 11292

cz 11377

cuz 11687

crp 11832

cico 12177

cseq 12801

cexp 12860

cshi 13806

cabs 13974

cli 14215

csu 14416 ↾_t crest 16081

ctopn 16082

cxmt 19731

cbl 19733 ℂ_fldccnfld 19746

ctop 20698

ctps 20736

cnt 20821

cdv 23627

ccxp 24302 C_𝑐cbcc 38535

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-prod 14636 df-risefac 14737 df-fallfac 14738 df-ef 14798 df-sin 14800 df-cos 14801 df-tan 14802 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-ulm 24131 df-log 24303 df-cxp 24304 df-bcc 38536

This theorem is referenced by: binomcxp 38556

W3C validator