logtayl - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > logtayl		Structured version Unicode version

Theorem logtayl 22910

Description: The Taylor series for

. (Contributed by Mario Carneiro, 1-Apr-2015.)

**Assertion**
Ref	Expression
logtayl	$/\$

Distinct variable group:

Proof of Theorem logtayl Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0uz 11121	. . . 4
2		0zd 10879	. . . 4 $/\$
3		eqeq1 2445	. . . . . . . 8
4		oveq2 6286	. . . . . . . 8
5	3, 4	ifbieq2d 3948	. . . . . . 7
6		oveq2 6286	. . . . . . 7
7	5, 6	oveq12d 6296	. . . . . 6
8		eqid 2441	. . . . . 6
9		ovex 6306	. . . . . 6
10	7, 8, 9	fvmpt 5938	. . . . 5
11	10	adantl 466	. . . 4 $/\$ $/\$
12		0cnd 9589	. . . . . 6 $/\$ $/\$ $/\$
13		simpr 461	. . . . . . . . . . . 12 $/\$ $/\$
14		elnn0 10800	. . . . . . . . . . . 12 $\/$
15	13, 14	sylib 196	. . . . . . . . . . 11 $/\$ $/\$ $\/$
16	15	ord 377	. . . . . . . . . 10 $/\$ $/\$
17	16	con1d 124	. . . . . . . . 9 $/\$ $/\$
18	17	imp 429	. . . . . . . 8 $/\$ $/\$ $/\$
19	18	nnrecred 10584	. . . . . . 7 $/\$ $/\$ $/\$
20	19	recnd 9622	. . . . . 6 $/\$ $/\$ $/\$
21	12, 20	ifclda 3955	. . . . 5 $/\$ $/\$
22		expcl 12160	. . . . . 6 $/\$
23	22	adantlr 714	. . . . 5 $/\$ $/\$
24	21, 23	mulcld 9616	. . . 4 $/\$ $/\$
25		logtayllem 22909	. . . 4 $/\$
26	1, 2, 11, 24, 25	isumclim2 13549	. . 3 $/\$
27		simpl 457	. . . . . . . 8 $/\$
28		0cn 9588	. . . . . . . 8
29		eqid 2441	. . . . . . . . 9
30	29	cnmetdval 21148	. . . . . . . 8 $/\$
31	27, 28, 30	sylancl 662	. . . . . . 7 $/\$
32		subid1 9841	. . . . . . . . 9
33	32	adantr 465	. . . . . . . 8 $/\$
34	33	fveq2d 5857	. . . . . . 7 $/\$
35	31, 34	eqtrd 2482	. . . . . 6 $/\$
36		simpr 461	. . . . . 6 $/\$
37	35, 36	eqbrtrd 4454	. . . . 5 $/\$
38		cnxmet 21150	. . . . . . 7
39		1rp 11230	. . . . . . . 8
40		rpxr 11233	. . . . . . . 8
41	39, 40	ax-mp 5	. . . . . . 7
42		elbl3 20765	. . . . . . 7 $/\$ $/\$ $/\$
43	38, 41, 42	mpanl12 682	. . . . . 6 $/\$
44	28, 27, 43	sylancr 663	. . . . 5 $/\$
45	37, 44	mpbird 232	. . . 4 $/\$
46		tru 1385	. . . . . 6
47		eqid 2441	. . . . . . . 8
48		0cnd 9589	. . . . . . . 8
49	41	a1i 11	. . . . . . . 8
50		ax-1cn 9550	. . . . . . . . . . . . 13
51		blssm 20791	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	38, 28, 41, 51	mp3an 1323	. . . . . . . . . . . . . 14
53	52	sseli 3483	. . . . . . . . . . . . 13
54		subcl 9821	. . . . . . . . . . . . 13 $/\$
55	50, 53, 54	sylancr 663	. . . . . . . . . . . 12
56	53	abscld 13243	. . . . . . . . . . . . . . 15
57	29	cnmetdval 21148	. . . . . . . . . . . . . . . . . 18 $/\$
58	53, 28, 57	sylancl 662	. . . . . . . . . . . . . . . . 17
59	53	subid1d 9922	. . . . . . . . . . . . . . . . . 18
60	59	fveq2d 5857	. . . . . . . . . . . . . . . . 17
61	58, 60	eqtrd 2482	. . . . . . . . . . . . . . . 16
62		elbl3 20765	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
63	38, 41, 62	mpanl12 682	. . . . . . . . . . . . . . . . . 18 $/\$
64	28, 53, 63	sylancr 663	. . . . . . . . . . . . . . . . 17
65	64	ibi 241	. . . . . . . . . . . . . . . 16
66	61, 65	eqbrtrrd 4456	. . . . . . . . . . . . . . 15
67	56, 66	gtned 9720	. . . . . . . . . . . . . 14
68		abs1 13106	. . . . . . . . . . . . . . . 16
69		fveq2 5853	. . . . . . . . . . . . . . . 16
70	68, 69	syl5eqr 2496	. . . . . . . . . . . . . . 15
71	70	necon3i 2681	. . . . . . . . . . . . . 14
72	67, 71	syl 16	. . . . . . . . . . . . 13
73		subeq0 9847	. . . . . . . . . . . . . . 15 $/\$
74	73	necon3bid 2699	. . . . . . . . . . . . . 14 $/\$
75	50, 53, 74	sylancr 663	. . . . . . . . . . . . 13
76	72, 75	mpbird 232	. . . . . . . . . . . 12
77	55, 76	logcld 22827	. . . . . . . . . . 11
78	77	negcld 9920	. . . . . . . . . 10
79	78	adantl 466	. . . . . . . . 9 $/\$
80		eqid 2441	. . . . . . . . 9
81	79, 80	fmptd 6037	. . . . . . . 8
82	53	absge0d 13251	. . . . . . . . . . . 12
83	56	rexrd 9643	. . . . . . . . . . . . 13
84		peano2re 9753	. . . . . . . . . . . . . . . 16
85	56, 84	syl 16	. . . . . . . . . . . . . . 15
86	85	rehalfcld 10788	. . . . . . . . . . . . . 14
87	86	rexrd 9643	. . . . . . . . . . . . 13
88		iccssxr 11613	. . . . . . . . . . . . . . 15
89		eqeq1 2445	. . . . . . . . . . . . . . . . . . . . . 22
90		oveq2 6286	. . . . . . . . . . . . . . . . . . . . . 22
91	89, 90	ifbieq2d 3948	. . . . . . . . . . . . . . . . . . . . 21
92		eqid 2441	. . . . . . . . . . . . . . . . . . . . 21
93		c0ex 9590	. . . . . . . . . . . . . . . . . . . . . 22
94		ovex 6306	. . . . . . . . . . . . . . . . . . . . . 22
95	93, 94	ifex 3992	. . . . . . . . . . . . . . . . . . . . 21
96	91, 92, 95	fvmpt 5938	. . . . . . . . . . . . . . . . . . . 20
97	96	eqcomd 2449	. . . . . . . . . . . . . . . . . . 19
98	97	oveq1d 6293	. . . . . . . . . . . . . . . . . 18
99	98	mpteq2ia 4516	. . . . . . . . . . . . . . . . 17
100	99	mpteq2i 4517	. . . . . . . . . . . . . . . 16
101		0cnd 9589	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
102		nn0cn 10808	. . . . . . . . . . . . . . . . . . . 20
103	102	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$
104		df-ne 2638	. . . . . . . . . . . . . . . . . . . 20
105	104	biimpri 206	. . . . . . . . . . . . . . . . . . 19
106		reccl 10217	. . . . . . . . . . . . . . . . . . 19 $/\$
107	103, 105, 106	syl2an 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
108	101, 107	ifclda 3955	. . . . . . . . . . . . . . . . 17 $/\$
109	108, 92	fmptd 6037	. . . . . . . . . . . . . . . 16
110		recn 9582	. . . . . . . . . . . . . . . . . . . . . 22
111		oveq1 6285	. . . . . . . . . . . . . . . . . . . . . . . . 25
112	111	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . . . . 24
113	112	mpteq2dv 4521	. . . . . . . . . . . . . . . . . . . . . . 23
114		eqid 2441	. . . . . . . . . . . . . . . . . . . . . . 23
115		nn0ex 10804	. . . . . . . . . . . . . . . . . . . . . . . 24
116	115	mptex 6125	. . . . . . . . . . . . . . . . . . . . . . 23
117	113, 114, 116	fvmpt 5938	. . . . . . . . . . . . . . . . . . . . . 22
118	110, 117	syl 16	. . . . . . . . . . . . . . . . . . . . 21
119	118	eqcomd 2449	. . . . . . . . . . . . . . . . . . . 20
120	119	seqeq3d 12091	. . . . . . . . . . . . . . . . . . 19
121	120	eleq1d 2510	. . . . . . . . . . . . . . . . . 18
122	121	rabbiia 3082	. . . . . . . . . . . . . . . . 17
123	122	supeq1i 7906	. . . . . . . . . . . . . . . 16
124	100, 109, 123	radcnvcl 22681	. . . . . . . . . . . . . . 15
125	88, 124	sseldi 3485	. . . . . . . . . . . . . 14
126	46, 125	mp1i 12	. . . . . . . . . . . . 13
127		1re 9595	. . . . . . . . . . . . . . 15
128		avglt1 10779	. . . . . . . . . . . . . . 15 $/\$
129	56, 127, 128	sylancl 662	. . . . . . . . . . . . . 14
130	66, 129	mpbid 210	. . . . . . . . . . . . 13
131		0red 9597	. . . . . . . . . . . . . . . 16
132	131, 56, 86, 82, 130	lelttrd 9740	. . . . . . . . . . . . . . . 16
133	131, 86, 132	ltled 9733	. . . . . . . . . . . . . . 15
134	86, 133	absidd 13230	. . . . . . . . . . . . . 14
135	46, 109	mp1i 12	. . . . . . . . . . . . . . 15
136	86	recnd 9622	. . . . . . . . . . . . . . 15
137		oveq1 6285	. . . . . . . . . . . . . . . . . . . . 21
138	137	oveq2d 6294	. . . . . . . . . . . . . . . . . . . 20
139	138	mpteq2dv 4521	. . . . . . . . . . . . . . . . . . 19
140	115	mptex 6125	. . . . . . . . . . . . . . . . . . 19
141	139, 114, 140	fvmpt 5938	. . . . . . . . . . . . . . . . . 18
142	136, 141	syl 16	. . . . . . . . . . . . . . . . 17
143	142	seqeq3d 12091	. . . . . . . . . . . . . . . 16
144		avglt2 10780	. . . . . . . . . . . . . . . . . . . 20 $/\$
145	56, 127, 144	sylancl 662	. . . . . . . . . . . . . . . . . . 19
146	66, 145	mpbid 210	. . . . . . . . . . . . . . . . . 18
147	134, 146	eqbrtrd 4454	. . . . . . . . . . . . . . . . 17
148		logtayllem 22909	. . . . . . . . . . . . . . . . 17 $/\$
149	136, 147, 148	syl2anc 661	. . . . . . . . . . . . . . . 16
150	143, 149	eqeltrd 2529	. . . . . . . . . . . . . . 15
151	100, 135, 123, 136, 150	radcnvle 22684	. . . . . . . . . . . . . 14
152	134, 151	eqbrtrrd 4456	. . . . . . . . . . . . 13
153	83, 87, 126, 130, 152	xrltletrd 11370	. . . . . . . . . . . 12
154		0re 9596	. . . . . . . . . . . . 13
155		elico2 11594	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
156	154, 126, 155	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$
157	56, 82, 153, 156	mpbir3and 1178	. . . . . . . . . . 11
158		absf 13146	. . . . . . . . . . . 12
159		ffn 5718	. . . . . . . . . . . 12
160		elpreima 5989	. . . . . . . . . . . 12 $/\$
161	158, 159, 160	mp2b 10	. . . . . . . . . . 11 $/\$
162	53, 157, 161	sylanbrc 664	. . . . . . . . . 10
163		cnvimass 5344	. . . . . . . . . . . . . . . . . 18
164	158	fdmi 5723	. . . . . . . . . . . . . . . . . 18
165	163, 164	sseqtri 3519	. . . . . . . . . . . . . . . . 17
166	165	sseli 3483	. . . . . . . . . . . . . . . 16
167		oveq1 6285	. . . . . . . . . . . . . . . . . . . . . . 23
168	167	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . . 22
169	168	mpteq2dv 4521	. . . . . . . . . . . . . . . . . . . . 21
170	115	mptex 6125	. . . . . . . . . . . . . . . . . . . . 21
171	169, 114, 170	fvmpt 5938	. . . . . . . . . . . . . . . . . . . 20
172	171	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
173	172	fveq1d 5855	. . . . . . . . . . . . . . . . . 18 $/\$
174		eqeq1 2445	. . . . . . . . . . . . . . . . . . . . . 22
175		oveq2 6286	. . . . . . . . . . . . . . . . . . . . . 22
176	174, 175	ifbieq2d 3948	. . . . . . . . . . . . . . . . . . . . 21
177		oveq2 6286	. . . . . . . . . . . . . . . . . . . . 21
178	176, 177	oveq12d 6296	. . . . . . . . . . . . . . . . . . . 20
179		eqid 2441	. . . . . . . . . . . . . . . . . . . 20
180		ovex 6306	. . . . . . . . . . . . . . . . . . . 20
181	178, 179, 180	fvmpt 5938	. . . . . . . . . . . . . . . . . . 19
182	181	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
183	173, 182	eqtr2d 2483	. . . . . . . . . . . . . . . . 17 $/\$
184	183	sumeq2dv 13501	. . . . . . . . . . . . . . . 16
185	166, 184	syl 16	. . . . . . . . . . . . . . 15
186	185	mpteq2ia 4516	. . . . . . . . . . . . . 14
187		eqid 2441	. . . . . . . . . . . . . 14
188		eqid 2441	. . . . . . . . . . . . . 14
189	100, 186, 109, 123, 187, 188	psercn 22690	. . . . . . . . . . . . 13
190		cncff 21267	. . . . . . . . . . . . 13
191	189, 190	syl 16	. . . . . . . . . . . 12
192		eqid 2441	. . . . . . . . . . . . 13
193	192	fmpt 6034	. . . . . . . . . . . 12
194	191, 193	sylibr 212	. . . . . . . . . . 11
195	194	r19.21bi 2810	. . . . . . . . . 10 $/\$
196	162, 195	sylan2 474	. . . . . . . . 9 $/\$
197		eqid 2441	. . . . . . . . 9
198	196, 197	fmptd 6037	. . . . . . . 8
199		cnelprrecn 9585	. . . . . . . . . . . . 13
200	199	a1i 11	. . . . . . . . . . . 12
201	77	adantl 466	. . . . . . . . . . . 12 $/\$
202		ovex 6306	. . . . . . . . . . . . 13
203	202	a1i 11	. . . . . . . . . . . 12 $/\$
204	29	cnmetdval 21148	. . . . . . . . . . . . . . . . . 18 $/\$
205	50, 55, 204	sylancr 663	. . . . . . . . . . . . . . . . 17
206		nncan 9850	. . . . . . . . . . . . . . . . . . 19 $/\$
207	50, 53, 206	sylancr 663	. . . . . . . . . . . . . . . . . 18
208	207	fveq2d 5857	. . . . . . . . . . . . . . . . 17
209	205, 208	eqtrd 2482	. . . . . . . . . . . . . . . 16
210	209, 66	eqbrtrd 4454	. . . . . . . . . . . . . . 15
211		elbl 20761	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
212	38, 50, 41, 211	mp3an 1323	. . . . . . . . . . . . . . 15 $/\$
213	55, 210, 212	sylanbrc 664	. . . . . . . . . . . . . 14
214	213	adantl 466	. . . . . . . . . . . . 13 $/\$
215		neg1cn 10642	. . . . . . . . . . . . . 14
216	215	a1i 11	. . . . . . . . . . . . 13 $/\$
217		eqid 2441	. . . . . . . . . . . . . . . . . 18
218	217	dvlog2lem 22902	. . . . . . . . . . . . . . . . 17 $\$
219	218	sseli 3483	. . . . . . . . . . . . . . . 16 $\$
220	219	eldifad 3471	. . . . . . . . . . . . . . 15
221		eqid 2441	. . . . . . . . . . . . . . . . 17 $\$ $\$
222	221	logdmn0 22890	. . . . . . . . . . . . . . . 16 $\$
223	219, 222	syl 16	. . . . . . . . . . . . . . 15
224	220, 223	logcld 22827	. . . . . . . . . . . . . 14
225	224	adantl 466	. . . . . . . . . . . . 13 $/\$
226		ovex 6306	. . . . . . . . . . . . . 14
227	226	a1i 11	. . . . . . . . . . . . 13 $/\$
228		simpr 461	. . . . . . . . . . . . . . 15 $/\$
229	50, 228, 54	sylancr 663	. . . . . . . . . . . . . 14 $/\$
230	215	a1i 11	. . . . . . . . . . . . . 14 $/\$
231		1cnd 9612	. . . . . . . . . . . . . . . 16 $/\$
232		0cnd 9589	. . . . . . . . . . . . . . . 16 $/\$
233		1cnd 9612	. . . . . . . . . . . . . . . . 17
234	200, 233	dvmptc 22231	. . . . . . . . . . . . . . . 16
235	200	dvmptid 22230	. . . . . . . . . . . . . . . 16
236	200, 231, 232, 234, 228, 231, 235	dvmptsub 22240	. . . . . . . . . . . . . . 15
237		df-neg 9810	. . . . . . . . . . . . . . . 16
238	237	mpteq2i 4517	. . . . . . . . . . . . . . 15
239	236, 238	syl6eqr 2500	. . . . . . . . . . . . . 14
240	52	a1i 11	. . . . . . . . . . . . . 14
241		eqid 2441	. . . . . . . . . . . . . . . . 17 ℂ_fld ℂ_fld
242	241	cnfldtop 21161	. . . . . . . . . . . . . . . 16 ℂ_fld
243	241	cnfldtopon 21160	. . . . . . . . . . . . . . . . . 18 ℂ_fld TopOn
244	243	toponunii 19303	. . . . . . . . . . . . . . . . 17 ℂ_fld
245	244	restid 14705	. . . . . . . . . . . . . . . 16 ℂ_fld ℂ_fld ↾_t ℂ_fld
246	242, 245	ax-mp 5	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t ℂ_fld
247	246	eqcomi 2454	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld ↾_t
248	241	cnfldtopn 21159	. . . . . . . . . . . . . . . . 17 ℂ_fld
249	248	blopn 20873	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ℂ_fld
250	38, 28, 41, 249	mp3an 1323	. . . . . . . . . . . . . . 15 ℂ_fld
251	250	a1i 11	. . . . . . . . . . . . . 14 ℂ_fld
252	200, 229, 230, 239, 240, 247, 241, 251	dvmptres 22236	. . . . . . . . . . . . 13
253	217	dvlog2 22903	. . . . . . . . . . . . . 14
254		logf1o 22821	. . . . . . . . . . . . . . . . . . . 20 $\$
255		f1of 5803	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
256	254, 255	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$
257	221	logdmss 22892	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
258	218, 257	sstri 3496	. . . . . . . . . . . . . . . . . . 19 $\$
259		fssres 5738	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$
260	256, 258, 259	mp2an 672	. . . . . . . . . . . . . . . . . 18
261	260	a1i 11	. . . . . . . . . . . . . . . . 17
262	261	feqmptd 5908	. . . . . . . . . . . . . . . 16
263		fvres 5867	. . . . . . . . . . . . . . . . 17
264	263	mpteq2ia 4516	. . . . . . . . . . . . . . . 16
265	262, 264	syl6eq 2498	. . . . . . . . . . . . . . 15
266	265	oveq2d 6294	. . . . . . . . . . . . . 14
267	253, 266	syl5reqr 2497	. . . . . . . . . . . . 13
268		fveq2 5853	. . . . . . . . . . . . 13
269		oveq2 6286	. . . . . . . . . . . . 13
270	200, 200, 214, 216, 225, 227, 252, 267, 268, 269	dvmptco 22245	. . . . . . . . . . . 12
271	200, 201, 203, 270	dvmptneg 22239	. . . . . . . . . . 11
272	55, 76	reccld 10316	. . . . . . . . . . . . . . . 16
273		mulcom 9578	. . . . . . . . . . . . . . . 16 $/\$
274	272, 215, 273	sylancl 662	. . . . . . . . . . . . . . 15
275	272	mulm1d 10011	. . . . . . . . . . . . . . 15
276	274, 275	eqtrd 2482	. . . . . . . . . . . . . 14
277	276	negeqd 9816	. . . . . . . . . . . . 13
278	272	negnegd 9924	. . . . . . . . . . . . 13
279	277, 278	eqtrd 2482	. . . . . . . . . . . 12
280	279	mpteq2ia 4516	. . . . . . . . . . 11
281	271, 280	syl6eq 2498	. . . . . . . . . 10
282	281	dmeqd 5192	. . . . . . . . 9
283		dmmptg 5491	. . . . . . . . . 10
284		ovex 6306	. . . . . . . . . . 11
285	284	a1i 11	. . . . . . . . . 10
286	283, 285	mprg 2804	. . . . . . . . 9
287	282, 286	syl6eq 2498	. . . . . . . 8
288		sumex 13486	. . . . . . . . . . . 12
289	288	a1i 11	. . . . . . . . . . 11 $/\$
290		fveq2 5853	. . . . . . . . . . . . . . 15
291	290	cbvsumv 13494	. . . . . . . . . . . . . 14
292	185, 291	syl6eq 2498	. . . . . . . . . . . . 13
293	292	mpteq2ia 4516	. . . . . . . . . . . 12
294		eqid 2441	. . . . . . . . . . . 12
295	100, 293, 109, 123, 187, 188, 294	pserdv2 22694	. . . . . . . . . . 11
296	162	ssriv 3491	. . . . . . . . . . . 12
297	296	a1i 11	. . . . . . . . . . 11
298	200, 195, 289, 295, 297, 247, 241, 251	dvmptres 22236	. . . . . . . . . 10
299		nnnn0 10805	. . . . . . . . . . . . . . . . . . . 20
300	299	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$
301		eqeq1 2445	. . . . . . . . . . . . . . . . . . . . 21
302		oveq2 6286	. . . . . . . . . . . . . . . . . . . . 21
303	301, 302	ifbieq2d 3948	. . . . . . . . . . . . . . . . . . . 20
304		ovex 6306	. . . . . . . . . . . . . . . . . . . . 21
305	93, 304	ifex 3992	. . . . . . . . . . . . . . . . . . . 20
306	303, 92, 305	fvmpt 5938	. . . . . . . . . . . . . . . . . . 19
307	300, 306	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$
308		nnne0 10571	. . . . . . . . . . . . . . . . . . . . 21
309	308	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$
310	309	neneqd 2643	. . . . . . . . . . . . . . . . . . 19 $/\$
311	310	iffalsed 3934	. . . . . . . . . . . . . . . . . 18 $/\$
312	307, 311	eqtrd 2482	. . . . . . . . . . . . . . . . 17 $/\$
313	312	oveq2d 6294	. . . . . . . . . . . . . . . 16 $/\$
314		nncn 10547	. . . . . . . . . . . . . . . . . 18
315	314	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$
316	315, 309	recidd 10318	. . . . . . . . . . . . . . . 16 $/\$
317	313, 316	eqtrd 2482	. . . . . . . . . . . . . . 15 $/\$
318	317	oveq1d 6293	. . . . . . . . . . . . . 14 $/\$
319		nnm1nn0 10840	. . . . . . . . . . . . . . . 16
320		expcl 12160	. . . . . . . . . . . . . . . 16 $/\$
321	53, 319, 320	syl2an 477	. . . . . . . . . . . . . . 15 $/\$
322	321	mulid2d 9614	. . . . . . . . . . . . . 14 $/\$
323	318, 322	eqtrd 2482	. . . . . . . . . . . . 13 $/\$
324	323	sumeq2dv 13501	. . . . . . . . . . . 12
325		nnuz 11122	. . . . . . . . . . . . . . 15
326		1e0p1 11009	. . . . . . . . . . . . . . . 16
327	326	fveq2i 5856	. . . . . . . . . . . . . . 15
328	325, 327	eqtri 2470	. . . . . . . . . . . . . 14
329		oveq1 6285	. . . . . . . . . . . . . . 15
330	329	oveq2d 6294	. . . . . . . . . . . . . 14
331		1zzd 10898	. . . . . . . . . . . . . 14
332		0zd 10879	. . . . . . . . . . . . . 14
333	1, 328, 330, 331, 332, 321	isumshft 13627	. . . . . . . . . . . . 13
334		pncan2 9829	. . . . . . . . . . . . . . . 16 $/\$
335	50, 102, 334	sylancr 663	. . . . . . . . . . . . . . 15
336	335	oveq2d 6294	. . . . . . . . . . . . . 14
337	336	sumeq2i 13497	. . . . . . . . . . . . 13
338	333, 337	syl6eq 2498	. . . . . . . . . . . 12
339		geoisum 13662	. . . . . . . . . . . . 13 $/\$
340	53, 66, 339	syl2anc 661	. . . . . . . . . . . 12
341	324, 338, 340	3eqtrd 2486	. . . . . . . . . . 11
342	341	mpteq2ia 4516	. . . . . . . . . 10
343	298, 342	syl6eq 2498	. . . . . . . . 9
344	281, 343	eqtr4d 2485	. . . . . . . 8
345		blcntr 20786	. . . . . . . . . 10