logtayl - Metamath Proof Explorer

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

Theorem logtayl 22769

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 11112	. . . 4
2		0zd 10872	. . . 4 $/\$
3		eqeq1 2471	. . . . . . . 8
4		oveq2 6290	. . . . . . . 8
5	3, 4	ifbieq2d 3964	. . . . . . 7
6		oveq2 6290	. . . . . . 7
7	5, 6	oveq12d 6300	. . . . . 6
8		eqid 2467	. . . . . 6
9		ovex 6307	. . . . . 6
10	7, 8, 9	fvmpt 5948	. . . . 5
11	10	adantl 466	. . . 4 $/\$ $/\$
12		0cnd 9585	. . . . . 6 $/\$ $/\$ $/\$
13		simpr 461	. . . . . . . . . . . 12 $/\$ $/\$
14		elnn0 10793	. . . . . . . . . . . 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 10577	. . . . . . 7 $/\$ $/\$ $/\$
20	19	recnd 9618	. . . . . 6 $/\$ $/\$ $/\$
21	12, 20	ifclda 3971	. . . . 5 $/\$ $/\$
22		expcl 12148	. . . . . 6 $/\$
23	22	adantlr 714	. . . . 5 $/\$ $/\$
24	21, 23	mulcld 9612	. . . 4 $/\$ $/\$
25		logtayllem 22768	. . . 4 $/\$
26	1, 2, 11, 24, 25	isumclim2 13532	. . 3 $/\$
27		simpl 457	. . . . . . . 8 $/\$
28		0cn 9584	. . . . . . . 8
29		eqid 2467	. . . . . . . . 9
30	29	cnmetdval 21013	. . . . . . . 8 $/\$
31	27, 28, 30	sylancl 662	. . . . . . 7 $/\$
32		subid1 9835	. . . . . . . . 9
33	32	adantr 465	. . . . . . . 8 $/\$
34	33	fveq2d 5868	. . . . . . 7 $/\$
35	31, 34	eqtrd 2508	. . . . . 6 $/\$
36		simpr 461	. . . . . 6 $/\$
37	35, 36	eqbrtrd 4467	. . . . 5 $/\$
38		cnxmet 21015	. . . . . . 7
39		1rp 11220	. . . . . . . 8
40		rpxr 11223	. . . . . . . 8
41	39, 40	ax-mp 5	. . . . . . 7
42		elbl3 20630	. . . . . . 7 $/\$ $/\$ $/\$
43	38, 41, 42	mpanl12 682	. . . . . 6 $/\$
44	28, 27, 43	sylancr 663	. . . . 5 $/\$
45	37, 44	mpbird 232	. . . 4 $/\$
46		tru 1383	. . . . . 6
47		eqid 2467	. . . . . . . 8
48		0cnd 9585	. . . . . . . 8
49	41	a1i 11	. . . . . . . 8
50		ax-1cn 9546	. . . . . . . . . . . . 13
51		blssm 20656	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	38, 28, 41, 51	mp3an 1324	. . . . . . . . . . . . . 14
53	52	sseli 3500	. . . . . . . . . . . . 13
54		subcl 9815	. . . . . . . . . . . . 13 $/\$
55	50, 53, 54	sylancr 663	. . . . . . . . . . . 12
56	53	abscld 13226	. . . . . . . . . . . . . . 15
57	29	cnmetdval 21013	. . . . . . . . . . . . . . . . . 18 $/\$
58	53, 28, 57	sylancl 662	. . . . . . . . . . . . . . . . 17
59	53	subid1d 9915	. . . . . . . . . . . . . . . . . 18
60	59	fveq2d 5868	. . . . . . . . . . . . . . . . 17
61	58, 60	eqtrd 2508	. . . . . . . . . . . . . . . 16
62		elbl3 20630	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
63	38, 41, 62	mpanl12 682	. . . . . . . . . . . . . . . . . 18 $/\$
64	28, 53, 63	sylancr 663	. . . . . . . . . . . . . . . . 17
65	64	ibi 241	. . . . . . . . . . . . . . . 16
66	61, 65	eqbrtrrd 4469	. . . . . . . . . . . . . . 15
67	56, 66	gtned 9715	. . . . . . . . . . . . . 14
68		abs1 13089	. . . . . . . . . . . . . . . 16
69		fveq2 5864	. . . . . . . . . . . . . . . 16
70	68, 69	syl5eqr 2522	. . . . . . . . . . . . . . 15
71	70	necon3i 2707	. . . . . . . . . . . . . 14
72	67, 71	syl 16	. . . . . . . . . . . . 13
73		subeq0 9841	. . . . . . . . . . . . . . 15 $/\$
74	73	necon3bid 2725	. . . . . . . . . . . . . 14 $/\$
75	50, 53, 74	sylancr 663	. . . . . . . . . . . . 13
76	72, 75	mpbird 232	. . . . . . . . . . . 12
77	55, 76	logcld 22686	. . . . . . . . . . 11
78	77	negcld 9913	. . . . . . . . . 10
79	78	adantl 466	. . . . . . . . 9 $/\$
80		eqid 2467	. . . . . . . . 9
81	79, 80	fmptd 6043	. . . . . . . 8
82	53	absge0d 13234	. . . . . . . . . . . 12
83	56	rexrd 9639	. . . . . . . . . . . . 13
84		peano2re 9748	. . . . . . . . . . . . . . . 16
85	56, 84	syl 16	. . . . . . . . . . . . . . 15
86	85	rehalfcld 10781	. . . . . . . . . . . . . 14
87	86	rexrd 9639	. . . . . . . . . . . . 13
88		iccssxr 11603	. . . . . . . . . . . . . . 15
89		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . 22
90		oveq2 6290	. . . . . . . . . . . . . . . . . . . . . 22
91	89, 90	ifbieq2d 3964	. . . . . . . . . . . . . . . . . . . . 21
92		eqid 2467	. . . . . . . . . . . . . . . . . . . . 21
93		c0ex 9586	. . . . . . . . . . . . . . . . . . . . . 22
94		ovex 6307	. . . . . . . . . . . . . . . . . . . . . 22
95	93, 94	ifex 4008	. . . . . . . . . . . . . . . . . . . . 21
96	91, 92, 95	fvmpt 5948	. . . . . . . . . . . . . . . . . . . 20
97	96	eqcomd 2475	. . . . . . . . . . . . . . . . . . 19
98	97	oveq1d 6297	. . . . . . . . . . . . . . . . . 18
99	98	mpteq2ia 4529	. . . . . . . . . . . . . . . . 17
100	99	mpteq2i 4530	. . . . . . . . . . . . . . . 16
101		0cnd 9585	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
102		nn0cn 10801	. . . . . . . . . . . . . . . . . . . 20
103	102	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$
104		df-ne 2664	. . . . . . . . . . . . . . . . . . . 20
105	104	biimpri 206	. . . . . . . . . . . . . . . . . . 19
106		reccl 10210	. . . . . . . . . . . . . . . . . . 19 $/\$
107	103, 105, 106	syl2an 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
108	101, 107	ifclda 3971	. . . . . . . . . . . . . . . . 17 $/\$
109	108, 92	fmptd 6043	. . . . . . . . . . . . . . . 16
110		recn 9578	. . . . . . . . . . . . . . . . . . . . . 22
111		oveq1 6289	. . . . . . . . . . . . . . . . . . . . . . . . 25
112	111	oveq2d 6298	. . . . . . . . . . . . . . . . . . . . . . . 24
113	112	mpteq2dv 4534	. . . . . . . . . . . . . . . . . . . . . . 23
114		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . 23
115		nn0ex 10797	. . . . . . . . . . . . . . . . . . . . . . . 24
116	115	mptex 6129	. . . . . . . . . . . . . . . . . . . . . . 23
117	113, 114, 116	fvmpt 5948	. . . . . . . . . . . . . . . . . . . . . 22
118	110, 117	syl 16	. . . . . . . . . . . . . . . . . . . . 21
119	118	eqcomd 2475	. . . . . . . . . . . . . . . . . . . 20
120	119	seqeq3d 12079	. . . . . . . . . . . . . . . . . . 19
121	120	eleq1d 2536	. . . . . . . . . . . . . . . . . 18
122	121	rabbiia 3102	. . . . . . . . . . . . . . . . 17
123	122	supeq1i 7903	. . . . . . . . . . . . . . . 16
124	100, 109, 123	radcnvcl 22546	. . . . . . . . . . . . . . 15
125	88, 124	sseldi 3502	. . . . . . . . . . . . . 14
126	46, 125	mp1i 12	. . . . . . . . . . . . 13
127		1re 9591	. . . . . . . . . . . . . . 15
128		avglt1 10772	. . . . . . . . . . . . . . 15 $/\$
129	56, 127, 128	sylancl 662	. . . . . . . . . . . . . 14
130	66, 129	mpbid 210	. . . . . . . . . . . . 13
131		0red 9593	. . . . . . . . . . . . . . . 16
132	131, 56, 86, 82, 130	lelttrd 9735	. . . . . . . . . . . . . . . 16
133	131, 86, 132	ltled 9728	. . . . . . . . . . . . . . 15
134	86, 133	absidd 13213	. . . . . . . . . . . . . 14
135	46, 109	mp1i 12	. . . . . . . . . . . . . . 15
136	86	recnd 9618	. . . . . . . . . . . . . . 15
137		oveq1 6289	. . . . . . . . . . . . . . . . . . . . 21
138	137	oveq2d 6298	. . . . . . . . . . . . . . . . . . . 20
139	138	mpteq2dv 4534	. . . . . . . . . . . . . . . . . . 19
140	115	mptex 6129	. . . . . . . . . . . . . . . . . . 19
141	139, 114, 140	fvmpt 5948	. . . . . . . . . . . . . . . . . 18
142	136, 141	syl 16	. . . . . . . . . . . . . . . . 17
143	142	seqeq3d 12079	. . . . . . . . . . . . . . . 16
144		avglt2 10773	. . . . . . . . . . . . . . . . . . . 20 $/\$
145	56, 127, 144	sylancl 662	. . . . . . . . . . . . . . . . . . 19
146	66, 145	mpbid 210	. . . . . . . . . . . . . . . . . 18
147	134, 146	eqbrtrd 4467	. . . . . . . . . . . . . . . . 17
148		logtayllem 22768	. . . . . . . . . . . . . . . . 17 $/\$
149	136, 147, 148	syl2anc 661	. . . . . . . . . . . . . . . 16
150	143, 149	eqeltrd 2555	. . . . . . . . . . . . . . 15
151	100, 135, 123, 136, 150	radcnvle 22549	. . . . . . . . . . . . . 14
152	134, 151	eqbrtrrd 4469	. . . . . . . . . . . . 13
153	83, 87, 126, 130, 152	xrltletrd 11360	. . . . . . . . . . . 12
154		0re 9592	. . . . . . . . . . . . 13
155		elico2 11584	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
156	154, 126, 155	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$
157	56, 82, 153, 156	mpbir3and 1179	. . . . . . . . . . 11
158		absf 13129	. . . . . . . . . . . 12
159		ffn 5729	. . . . . . . . . . . 12
160		elpreima 5999	. . . . . . . . . . . 12 $/\$
161	158, 159, 160	mp2b 10	. . . . . . . . . . 11 $/\$
162	53, 157, 161	sylanbrc 664	. . . . . . . . . 10
163		cnvimass 5355	. . . . . . . . . . . . . . . . . 18
164	158	fdmi 5734	. . . . . . . . . . . . . . . . . 18
165	163, 164	sseqtri 3536	. . . . . . . . . . . . . . . . 17
166	165	sseli 3500	. . . . . . . . . . . . . . . 16
167		oveq1 6289	. . . . . . . . . . . . . . . . . . . . . . 23
168	167	oveq2d 6298	. . . . . . . . . . . . . . . . . . . . . 22
169	168	mpteq2dv 4534	. . . . . . . . . . . . . . . . . . . . 21
170	115	mptex 6129	. . . . . . . . . . . . . . . . . . . . 21
171	169, 114, 170	fvmpt 5948	. . . . . . . . . . . . . . . . . . . 20
172	171	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
173	172	fveq1d 5866	. . . . . . . . . . . . . . . . . 18 $/\$
174		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . 22
175		oveq2 6290	. . . . . . . . . . . . . . . . . . . . . 22
176	174, 175	ifbieq2d 3964	. . . . . . . . . . . . . . . . . . . . 21
177		oveq2 6290	. . . . . . . . . . . . . . . . . . . . 21
178	176, 177	oveq12d 6300	. . . . . . . . . . . . . . . . . . . 20
179		eqid 2467	. . . . . . . . . . . . . . . . . . . 20
180		ovex 6307	. . . . . . . . . . . . . . . . . . . 20
181	178, 179, 180	fvmpt 5948	. . . . . . . . . . . . . . . . . . 19
182	181	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
183	173, 182	eqtr2d 2509	. . . . . . . . . . . . . . . . 17 $/\$
184	183	sumeq2dv 13484	. . . . . . . . . . . . . . . 16
185	166, 184	syl 16	. . . . . . . . . . . . . . 15
186	185	mpteq2ia 4529	. . . . . . . . . . . . . 14
187		eqid 2467	. . . . . . . . . . . . . 14
188		eqid 2467	. . . . . . . . . . . . . 14
189	100, 186, 109, 123, 187, 188	psercn 22555	. . . . . . . . . . . . 13
190		cncff 21132	. . . . . . . . . . . . 13
191	189, 190	syl 16	. . . . . . . . . . . 12
192		eqid 2467	. . . . . . . . . . . . 13
193	192	fmpt 6040	. . . . . . . . . . . 12
194	191, 193	sylibr 212	. . . . . . . . . . 11
195	194	r19.21bi 2833	. . . . . . . . . 10 $/\$
196	162, 195	sylan2 474	. . . . . . . . 9 $/\$
197		eqid 2467	. . . . . . . . 9
198	196, 197	fmptd 6043	. . . . . . . 8
199		cnelprrecn 9581	. . . . . . . . . . . . 13
200	199	a1i 11	. . . . . . . . . . . 12
201	77	adantl 466	. . . . . . . . . . . 12 $/\$
202		ovex 6307	. . . . . . . . . . . . 13
203	202	a1i 11	. . . . . . . . . . . 12 $/\$
204	29	cnmetdval 21013	. . . . . . . . . . . . . . . . . 18 $/\$
205	50, 55, 204	sylancr 663	. . . . . . . . . . . . . . . . 17
206		nncan 9844	. . . . . . . . . . . . . . . . . . 19 $/\$
207	50, 53, 206	sylancr 663	. . . . . . . . . . . . . . . . . 18
208	207	fveq2d 5868	. . . . . . . . . . . . . . . . 17
209	205, 208	eqtrd 2508	. . . . . . . . . . . . . . . 16
210	209, 66	eqbrtrd 4467	. . . . . . . . . . . . . . 15
211		elbl 20626	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
212	38, 50, 41, 211	mp3an 1324	. . . . . . . . . . . . . . 15 $/\$
213	55, 210, 212	sylanbrc 664	. . . . . . . . . . . . . 14
214	213	adantl 466	. . . . . . . . . . . . 13 $/\$
215		neg1cn 10635	. . . . . . . . . . . . . 14
216	215	a1i 11	. . . . . . . . . . . . 13 $/\$
217		eqid 2467	. . . . . . . . . . . . . . . . . 18
218	217	dvlog2lem 22761	. . . . . . . . . . . . . . . . 17 $\$
219	218	sseli 3500	. . . . . . . . . . . . . . . 16 $\$
220	219	eldifad 3488	. . . . . . . . . . . . . . 15
221		eqid 2467	. . . . . . . . . . . . . . . . 17 $\$ $\$
222	221	logdmn0 22749	. . . . . . . . . . . . . . . 16 $\$
223	219, 222	syl 16	. . . . . . . . . . . . . . 15
224	220, 223	logcld 22686	. . . . . . . . . . . . . 14
225	224	adantl 466	. . . . . . . . . . . . 13 $/\$
226		ovex 6307	. . . . . . . . . . . . . 14
227	226	a1i 11	. . . . . . . . . . . . 13 $/\$
228		simpr 461	. . . . . . . . . . . . . . 15 $/\$
229	50, 228, 54	sylancr 663	. . . . . . . . . . . . . 14 $/\$
230	215	a1i 11	. . . . . . . . . . . . . 14 $/\$
231		1cnd 9608	. . . . . . . . . . . . . . . 16 $/\$
232		0cnd 9585	. . . . . . . . . . . . . . . 16 $/\$
233		1cnd 9608	. . . . . . . . . . . . . . . . 17
234	200, 233	dvmptc 22096	. . . . . . . . . . . . . . . 16
235	200	dvmptid 22095	. . . . . . . . . . . . . . . 16
236	200, 231, 232, 234, 228, 231, 235	dvmptsub 22105	. . . . . . . . . . . . . . 15
237		df-neg 9804	. . . . . . . . . . . . . . . 16
238	237	mpteq2i 4530	. . . . . . . . . . . . . . 15
239	236, 238	syl6eqr 2526	. . . . . . . . . . . . . 14
240	52	a1i 11	. . . . . . . . . . . . . 14
241		eqid 2467	. . . . . . . . . . . . . . . . 17 ℂ_fld ℂ_fld
242	241	cnfldtop 21026	. . . . . . . . . . . . . . . 16 ℂ_fld
243	241	cnfldtopon 21025	. . . . . . . . . . . . . . . . . 18 ℂ_fld TopOn
244	243	toponunii 19200	. . . . . . . . . . . . . . . . 17 ℂ_fld
245	244	restid 14685	. . . . . . . . . . . . . . . 16 ℂ_fld ℂ_fld ↾_t ℂ_fld
246	242, 245	ax-mp 5	. . . . . . . . . . . . . . 15 ℂ_fld ↾_t ℂ_fld
247	246	eqcomi 2480	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld ↾_t
248	241	cnfldtopn 21024	. . . . . . . . . . . . . . . . 17 ℂ_fld
249	248	blopn 20738	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ℂ_fld
250	38, 28, 41, 249	mp3an 1324	. . . . . . . . . . . . . . 15 ℂ_fld
251	250	a1i 11	. . . . . . . . . . . . . 14 ℂ_fld
252	200, 229, 230, 239, 240, 247, 241, 251	dvmptres 22101	. . . . . . . . . . . . 13
253	217	dvlog2 22762	. . . . . . . . . . . . . 14
254		logf1o 22680	. . . . . . . . . . . . . . . . . . . 20 $\$
255		f1of 5814	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
256	254, 255	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$
257	221	logdmss 22751	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
258	218, 257	sstri 3513	. . . . . . . . . . . . . . . . . . 19 $\$
259		fssres 5749	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$
260	256, 258, 259	mp2an 672	. . . . . . . . . . . . . . . . . 18
261	260	a1i 11	. . . . . . . . . . . . . . . . 17
262	261	feqmptd 5918	. . . . . . . . . . . . . . . 16
263		fvres 5878	. . . . . . . . . . . . . . . . 17
264	263	mpteq2ia 4529	. . . . . . . . . . . . . . . 16
265	262, 264	syl6eq 2524	. . . . . . . . . . . . . . 15
266	265	oveq2d 6298	. . . . . . . . . . . . . 14
267	253, 266	syl5reqr 2523	. . . . . . . . . . . . 13
268		fveq2 5864	. . . . . . . . . . . . 13
269		oveq2 6290	. . . . . . . . . . . . 13
270	200, 200, 214, 216, 225, 227, 252, 267, 268, 269	dvmptco 22110	. . . . . . . . . . . 12
271	200, 201, 203, 270	dvmptneg 22104	. . . . . . . . . . 11
272	55, 76	reccld 10309	. . . . . . . . . . . . . . . 16
273		mulcom 9574	. . . . . . . . . . . . . . . 16 $/\$
274	272, 215, 273	sylancl 662	. . . . . . . . . . . . . . 15
275	272	mulm1d 10004	. . . . . . . . . . . . . . 15
276	274, 275	eqtrd 2508	. . . . . . . . . . . . . 14
277	276	negeqd 9810	. . . . . . . . . . . . 13
278	272	negnegd 9917	. . . . . . . . . . . . 13
279	277, 278	eqtrd 2508	. . . . . . . . . . . 12
280	279	mpteq2ia 4529	. . . . . . . . . . 11
281	271, 280	syl6eq 2524	. . . . . . . . . 10
282	281	dmeqd 5203	. . . . . . . . 9
283		dmmptg 5502	. . . . . . . . . 10
284		ovex 6307	. . . . . . . . . . 11
285	284	a1i 11	. . . . . . . . . 10
286	283, 285	mprg 2827	. . . . . . . . 9
287	282, 286	syl6eq 2524	. . . . . . . 8
288		sumex 13469	. . . . . . . . . . . 12
289	288	a1i 11	. . . . . . . . . . 11 $/\$
290		fveq2 5864	. . . . . . . . . . . . . . 15
291	290	cbvsumv 13477	. . . . . . . . . . . . . 14
292	185, 291	syl6eq 2524	. . . . . . . . . . . . 13
293	292	mpteq2ia 4529	. . . . . . . . . . . 12
294		eqid 2467	. . . . . . . . . . . 12
295	100, 293, 109, 123, 187, 188, 294	pserdv2 22559	. . . . . . . . . . 11
296	162	ssriv 3508	. . . . . . . . . . . 12
297	296	a1i 11	. . . . . . . . . . 11
298	200, 195, 289, 295, 297, 247, 241, 251	dvmptres 22101	. . . . . . . . . 10
299		nnnn0 10798	. . . . . . . . . . . . . . . . . . . 20
300	299	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$
301		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . 21
302		oveq2 6290	. . . . . . . . . . . . . . . . . . . . 21
303	301, 302	ifbieq2d 3964	. . . . . . . . . . . . . . . . . . . 20
304		ovex 6307	. . . . . . . . . . . . . . . . . . . . 21
305	93, 304	ifex 4008	. . . . . . . . . . . . . . . . . . . 20
306	303, 92, 305	fvmpt 5948	. . . . . . . . . . . . . . . . . . 19
307	300, 306	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$
308		nnne0 10564	. . . . . . . . . . . . . . . . . . . . 21
309	308	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$
310	309	neneqd 2669	. . . . . . . . . . . . . . . . . . 19 $/\$
311		iffalse 3948	. . . . . . . . . . . . . . . . . . 19
312	310, 311	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$
313	307, 312	eqtrd 2508	. . . . . . . . . . . . . . . . 17 $/\$
314	313	oveq2d 6298	. . . . . . . . . . . . . . . 16 $/\$
315		nncn 10540	. . . . . . . . . . . . . . . . . 18
316	315	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$
317	316, 309	recidd 10311	. . . . . . . . . . . . . . . 16 $/\$
318	314, 317	eqtrd 2508	. . . . . . . . . . . . . . 15 $/\$
319	318	oveq1d 6297	. . . . . . . . . . . . . 14 $/\$
320		nnm1nn0 10833	. . . . . . . . . . . . . . . 16
321		expcl 12148	. . . . . . . . . . . . . . . 16 $/\$
322	53, 320, 321	syl2an 477	. . . . . . . . . . . . . . 15 $/\$
323	322	mulid2d 9610	. . . . . . . . . . . . . 14 $/\$
324	319, 323	eqtrd 2508	. . . . . . . . . . . . 13 $/\$
325	324	sumeq2dv 13484	. . . . . . . . . . . 12
326		nnuz 11113	. . . . . . . . . . . . . . 15
327		1e0p1 11000	. . . . . . . . . . . . . . . 16
328	327	fveq2i 5867	. . . . . . . . . . . . . . 15
329	326, 328	eqtri 2496	. . . . . . . . . . . . . 14
330		oveq1 6289	. . . . . . . . . . . . . . 15
331	330	oveq2d 6298	. . . . . . . . . . . . . 14
332		1zzd 10891	. . . . . . . . . . . . . 14
333		0zd 10872	. . . . . . . . . . . . . 14
334	1, 329, 331, 332, 333, 322	isumshft 13610	. . . . . . . . . . . . 13
335		pncan2 9823	. . . . . . . . . . . . . . . 16 $/\$
336	50, 102, 335	sylancr 663	. . . . . . . . . . . . . . 15
337	336	oveq2d 6298	. . . . . . . . . . . . . 14
338	337	sumeq2i 13480	. . . . . . . . . . . . 13
339	334, 338	syl6eq 2524	. . . . . . . . . . . 12
340		geoisum 13645	. . . . . . . . . . . . 13 $/\$
341	53, 66, 340	syl2anc 661	. . . . . . . . . . . 12
342	325, 339, 341	3eqtrd 2512	. . . . . . . . . . 11
343	342	mpteq2ia 4529	. . . . . . . . . 10
344	298, 343	syl6eq 2524	. . . . . . . . 9
345	281, 344	eqtr4d 2511	. . . . . . . 8