logtayl - Metamath Proof Explorer

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

Theorem logtayl 23684

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 11217	. . . 4
2		0zd 10973	. . . 4 $/\$
3		eqeq1 2475	. . . . . . . 8
4		oveq2 6316	. . . . . . . 8
5	3, 4	ifbieq2d 3897	. . . . . . 7
6		oveq2 6316	. . . . . . 7
7	5, 6	oveq12d 6326	. . . . . 6
8		eqid 2471	. . . . . 6
9		ovex 6336	. . . . . 6
10	7, 8, 9	fvmpt 5963	. . . . 5
11	10	adantl 473	. . . 4 $/\$ $/\$
12		0cnd 9654	. . . . . 6 $/\$ $/\$ $/\$
13		simpr 468	. . . . . . . . . . . 12 $/\$ $/\$
14		elnn0 10895	. . . . . . . . . . . 12 $\/$
15	13, 14	sylib 201	. . . . . . . . . . 11 $/\$ $/\$ $\/$
16	15	ord 384	. . . . . . . . . 10 $/\$ $/\$
17	16	con1d 129	. . . . . . . . 9 $/\$ $/\$
18	17	imp 436	. . . . . . . 8 $/\$ $/\$ $/\$
19	18	nnrecred 10677	. . . . . . 7 $/\$ $/\$ $/\$
20	19	recnd 9687	. . . . . 6 $/\$ $/\$ $/\$
21	12, 20	ifclda 3904	. . . . 5 $/\$ $/\$
22		expcl 12328	. . . . . 6 $/\$
23	22	adantlr 729	. . . . 5 $/\$ $/\$
24	21, 23	mulcld 9681	. . . 4 $/\$ $/\$
25		logtayllem 23683	. . . 4 $/\$
26	1, 2, 11, 24, 25	isumclim2 13896	. . 3 $/\$
27		simpl 464	. . . . . . . 8 $/\$
28		0cn 9653	. . . . . . . 8
29		eqid 2471	. . . . . . . . 9
30	29	cnmetdval 21869	. . . . . . . 8 $/\$
31	27, 28, 30	sylancl 675	. . . . . . 7 $/\$
32		subid1 9914	. . . . . . . . 9
33	32	adantr 472	. . . . . . . 8 $/\$
34	33	fveq2d 5883	. . . . . . 7 $/\$
35	31, 34	eqtrd 2505	. . . . . 6 $/\$
36		simpr 468	. . . . . 6 $/\$
37	35, 36	eqbrtrd 4416	. . . . 5 $/\$
38		cnxmet 21871	. . . . . . 7
39		1rp 11329	. . . . . . . 8
40		rpxr 11332	. . . . . . . 8
41	39, 40	ax-mp 5	. . . . . . 7
42		elbl3 21485	. . . . . . 7 $/\$ $/\$ $/\$
43	38, 41, 42	mpanl12 696	. . . . . 6 $/\$
44	28, 27, 43	sylancr 676	. . . . 5 $/\$
45	37, 44	mpbird 240	. . . 4 $/\$
46		tru 1456	. . . . . 6
47		eqid 2471	. . . . . . . 8
48		0cnd 9654	. . . . . . . 8
49	41	a1i 11	. . . . . . . 8
50		ax-1cn 9615	. . . . . . . . . . . . 13
51		blssm 21511	. . . . . . . . . . . . . . 15 $/\$ $/\$
52	38, 28, 41, 51	mp3an 1390	. . . . . . . . . . . . . 14
53	52	sseli 3414	. . . . . . . . . . . . 13
54		subcl 9894	. . . . . . . . . . . . 13 $/\$
55	50, 53, 54	sylancr 676	. . . . . . . . . . . 12
56	53	abscld 13575	. . . . . . . . . . . . . . 15
57	29	cnmetdval 21869	. . . . . . . . . . . . . . . . . 18 $/\$
58	53, 28, 57	sylancl 675	. . . . . . . . . . . . . . . . 17
59	53	subid1d 9994	. . . . . . . . . . . . . . . . . 18
60	59	fveq2d 5883	. . . . . . . . . . . . . . . . 17
61	58, 60	eqtrd 2505	. . . . . . . . . . . . . . . 16
62		elbl3 21485	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
63	38, 41, 62	mpanl12 696	. . . . . . . . . . . . . . . . . 18 $/\$
64	28, 53, 63	sylancr 676	. . . . . . . . . . . . . . . . 17
65	64	ibi 249	. . . . . . . . . . . . . . . 16
66	61, 65	eqbrtrrd 4418	. . . . . . . . . . . . . . 15
67	56, 66	gtned 9787	. . . . . . . . . . . . . 14
68		abs1 13437	. . . . . . . . . . . . . . . 16
69		fveq2 5879	. . . . . . . . . . . . . . . 16
70	68, 69	syl5eqr 2519	. . . . . . . . . . . . . . 15
71	70	necon3i 2675	. . . . . . . . . . . . . 14
72	67, 71	syl 17	. . . . . . . . . . . . 13
73		subeq0 9920	. . . . . . . . . . . . . . 15 $/\$
74	73	necon3bid 2687	. . . . . . . . . . . . . 14 $/\$
75	50, 53, 74	sylancr 676	. . . . . . . . . . . . 13
76	72, 75	mpbird 240	. . . . . . . . . . . 12
77	55, 76	logcld 23599	. . . . . . . . . . 11
78	77	negcld 9992	. . . . . . . . . 10
79	78	adantl 473	. . . . . . . . 9 $/\$
80		eqid 2471	. . . . . . . . 9
81	79, 80	fmptd 6061	. . . . . . . 8
82	53	absge0d 13583	. . . . . . . . . . . 12
83	56	rexrd 9708	. . . . . . . . . . . . 13
84		peano2re 9824	. . . . . . . . . . . . . . . 16
85	56, 84	syl 17	. . . . . . . . . . . . . . 15
86	85	rehalfcld 10882	. . . . . . . . . . . . . 14
87	86	rexrd 9708	. . . . . . . . . . . . 13
88		iccssxr 11742	. . . . . . . . . . . . . . 15
89		eqeq1 2475	. . . . . . . . . . . . . . . . . . . . . 22
90		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . 22
91	89, 90	ifbieq2d 3897	. . . . . . . . . . . . . . . . . . . . 21
92		eqid 2471	. . . . . . . . . . . . . . . . . . . . 21
93		c0ex 9655	. . . . . . . . . . . . . . . . . . . . . 22
94		ovex 6336	. . . . . . . . . . . . . . . . . . . . . 22
95	93, 94	ifex 3940	. . . . . . . . . . . . . . . . . . . . 21
96	91, 92, 95	fvmpt 5963	. . . . . . . . . . . . . . . . . . . 20
97	96	eqcomd 2477	. . . . . . . . . . . . . . . . . . 19
98	97	oveq1d 6323	. . . . . . . . . . . . . . . . . 18
99	98	mpteq2ia 4478	. . . . . . . . . . . . . . . . 17
100	99	mpteq2i 4479	. . . . . . . . . . . . . . . 16
101		0cnd 9654	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
102		nn0cn 10903	. . . . . . . . . . . . . . . . . . . 20
103	102	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$
104		df-ne 2643	. . . . . . . . . . . . . . . . . . . 20
105	104	biimpri 211	. . . . . . . . . . . . . . . . . . 19
106		reccl 10299	. . . . . . . . . . . . . . . . . . 19 $/\$
107	103, 105, 106	syl2an 485	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
108	101, 107	ifclda 3904	. . . . . . . . . . . . . . . . 17 $/\$
109	108, 92	fmptd 6061	. . . . . . . . . . . . . . . 16
110		recn 9647	. . . . . . . . . . . . . . . . . . . . . 22
111		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . . . 25
112	111	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . . 24
113	112	mpteq2dv 4483	. . . . . . . . . . . . . . . . . . . . . . 23
114		eqid 2471	. . . . . . . . . . . . . . . . . . . . . . 23
115		nn0ex 10899	. . . . . . . . . . . . . . . . . . . . . . . 24
116	115	mptex 6152	. . . . . . . . . . . . . . . . . . . . . . 23
117	113, 114, 116	fvmpt 5963	. . . . . . . . . . . . . . . . . . . . . 22
118	110, 117	syl 17	. . . . . . . . . . . . . . . . . . . . 21
119	118	eqcomd 2477	. . . . . . . . . . . . . . . . . . . 20
120	119	seqeq3d 12259	. . . . . . . . . . . . . . . . . . 19
121	120	eleq1d 2533	. . . . . . . . . . . . . . . . . 18
122	121	rabbiia 3019	. . . . . . . . . . . . . . . . 17
123	122	supeq1i 7979	. . . . . . . . . . . . . . . 16
124	100, 109, 123	radcnvcl 23451	. . . . . . . . . . . . . . 15
125	88, 124	sseldi 3416	. . . . . . . . . . . . . 14
126	46, 125	mp1i 13	. . . . . . . . . . . . 13
127		1re 9660	. . . . . . . . . . . . . . 15
128		avglt1 10873	. . . . . . . . . . . . . . 15 $/\$
129	56, 127, 128	sylancl 675	. . . . . . . . . . . . . 14
130	66, 129	mpbid 215	. . . . . . . . . . . . 13
131		0red 9662	. . . . . . . . . . . . . . . 16
132	131, 56, 86, 82, 130	lelttrd 9810	. . . . . . . . . . . . . . . 16
133	131, 86, 132	ltled 9800	. . . . . . . . . . . . . . 15
134	86, 133	absidd 13561	. . . . . . . . . . . . . 14
135	46, 109	mp1i 13	. . . . . . . . . . . . . . 15
136	86	recnd 9687	. . . . . . . . . . . . . . 15
137		oveq1 6315	. . . . . . . . . . . . . . . . . . . . 21
138	137	oveq2d 6324	. . . . . . . . . . . . . . . . . . . 20
139	138	mpteq2dv 4483	. . . . . . . . . . . . . . . . . . 19
140	115	mptex 6152	. . . . . . . . . . . . . . . . . . 19
141	139, 114, 140	fvmpt 5963	. . . . . . . . . . . . . . . . . 18
142	136, 141	syl 17	. . . . . . . . . . . . . . . . 17
143	142	seqeq3d 12259	. . . . . . . . . . . . . . . 16
144		avglt2 10874	. . . . . . . . . . . . . . . . . . . 20 $/\$
145	56, 127, 144	sylancl 675	. . . . . . . . . . . . . . . . . . 19
146	66, 145	mpbid 215	. . . . . . . . . . . . . . . . . 18
147	134, 146	eqbrtrd 4416	. . . . . . . . . . . . . . . . 17
148		logtayllem 23683	. . . . . . . . . . . . . . . . 17 $/\$
149	136, 147, 148	syl2anc 673	. . . . . . . . . . . . . . . 16
150	143, 149	eqeltrd 2549	. . . . . . . . . . . . . . 15
151	100, 135, 123, 136, 150	radcnvle 23454	. . . . . . . . . . . . . 14
152	134, 151	eqbrtrrd 4418	. . . . . . . . . . . . 13
153	83, 87, 126, 130, 152	xrltletrd 11481	. . . . . . . . . . . 12
154		0re 9661	. . . . . . . . . . . . 13
155		elico2 11723	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
156	154, 126, 155	sylancr 676	. . . . . . . . . . . 12 $/\$ $/\$
157	56, 82, 153, 156	mpbir3and 1213	. . . . . . . . . . 11
158		absf 13477	. . . . . . . . . . . 12
159		ffn 5739	. . . . . . . . . . . 12
160		elpreima 6017	. . . . . . . . . . . 12 $/\$
161	158, 159, 160	mp2b 10	. . . . . . . . . . 11 $/\$
162	53, 157, 161	sylanbrc 677	. . . . . . . . . 10
163		cnvimass 5194	. . . . . . . . . . . . . . . . . 18
164	158	fdmi 5746	. . . . . . . . . . . . . . . . . 18
165	163, 164	sseqtri 3450	. . . . . . . . . . . . . . . . 17
166	165	sseli 3414	. . . . . . . . . . . . . . . 16
167		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . 23
168	167	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . 22
169	168	mpteq2dv 4483	. . . . . . . . . . . . . . . . . . . . 21
170	115	mptex 6152	. . . . . . . . . . . . . . . . . . . . 21
171	169, 114, 170	fvmpt 5963	. . . . . . . . . . . . . . . . . . . 20
172	171	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
173	172	fveq1d 5881	. . . . . . . . . . . . . . . . . 18 $/\$
174		eqeq1 2475	. . . . . . . . . . . . . . . . . . . . . 22
175		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . 22
176	174, 175	ifbieq2d 3897	. . . . . . . . . . . . . . . . . . . . 21
177		oveq2 6316	. . . . . . . . . . . . . . . . . . . . 21
178	176, 177	oveq12d 6326	. . . . . . . . . . . . . . . . . . . 20
179		eqid 2471	. . . . . . . . . . . . . . . . . . . 20
180		ovex 6336	. . . . . . . . . . . . . . . . . . . 20
181	178, 179, 180	fvmpt 5963	. . . . . . . . . . . . . . . . . . 19
182	181	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$
183	173, 182	eqtr2d 2506	. . . . . . . . . . . . . . . . 17 $/\$
184	183	sumeq2dv 13846	. . . . . . . . . . . . . . . 16
185	166, 184	syl 17	. . . . . . . . . . . . . . 15
186	185	mpteq2ia 4478	. . . . . . . . . . . . . 14
187		eqid 2471	. . . . . . . . . . . . . 14
188		eqid 2471	. . . . . . . . . . . . . 14
189	100, 186, 109, 123, 187, 188	psercn 23460	. . . . . . . . . . . . 13
190		cncff 22003	. . . . . . . . . . . . 13
191	189, 190	syl 17	. . . . . . . . . . . 12
192		eqid 2471	. . . . . . . . . . . . 13
193	192	fmpt 6058	. . . . . . . . . . . 12
194	191, 193	sylibr 217	. . . . . . . . . . 11
195	194	r19.21bi 2776	. . . . . . . . . 10 $/\$
196	162, 195	sylan2 482	. . . . . . . . 9 $/\$
197		eqid 2471	. . . . . . . . 9
198	196, 197	fmptd 6061	. . . . . . . 8
199		cnelprrecn 9650	. . . . . . . . . . . . 13
200	199	a1i 11	. . . . . . . . . . . 12
201	77	adantl 473	. . . . . . . . . . . 12 $/\$
202		ovex 6336	. . . . . . . . . . . . 13
203	202	a1i 11	. . . . . . . . . . . 12 $/\$
204	29	cnmetdval 21869	. . . . . . . . . . . . . . . . . 18 $/\$
205	50, 55, 204	sylancr 676	. . . . . . . . . . . . . . . . 17
206		nncan 9923	. . . . . . . . . . . . . . . . . . 19 $/\$
207	50, 53, 206	sylancr 676	. . . . . . . . . . . . . . . . . 18
208	207	fveq2d 5883	. . . . . . . . . . . . . . . . 17
209	205, 208	eqtrd 2505	. . . . . . . . . . . . . . . 16
210	209, 66	eqbrtrd 4416	. . . . . . . . . . . . . . 15
211		elbl 21481	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
212	38, 50, 41, 211	mp3an 1390	. . . . . . . . . . . . . . 15 $/\$
213	55, 210, 212	sylanbrc 677	. . . . . . . . . . . . . 14
214	213	adantl 473	. . . . . . . . . . . . 13 $/\$
215		neg1cn 10735	. . . . . . . . . . . . . 14
216	215	a1i 11	. . . . . . . . . . . . 13 $/\$
217		eqid 2471	. . . . . . . . . . . . . . . . . 18
218	217	dvlog2lem 23676	. . . . . . . . . . . . . . . . 17 $\$
219	218	sseli 3414	. . . . . . . . . . . . . . . 16 $\$
220	219	eldifad 3402	. . . . . . . . . . . . . . 15
221		eqid 2471	. . . . . . . . . . . . . . . . 17 $\$ $\$
222	221	logdmn0 23664	. . . . . . . . . . . . . . . 16 $\$
223	219, 222	syl 17	. . . . . . . . . . . . . . 15
224	220, 223	logcld 23599	. . . . . . . . . . . . . 14
225	224	adantl 473	. . . . . . . . . . . . 13 $/\$
226		ovex 6336	. . . . . . . . . . . . . 14
227	226	a1i 11	. . . . . . . . . . . . 13 $/\$
228		simpr 468	. . . . . . . . . . . . . . 15 $/\$
229	50, 228, 54	sylancr 676	. . . . . . . . . . . . . 14 $/\$
230	215	a1i 11	. . . . . . . . . . . . . 14 $/\$
231		1cnd 9677	. . . . . . . . . . . . . . . 16 $/\$
232		0cnd 9654	. . . . . . . . . . . . . . . 16 $/\$
233		1cnd 9677	. . . . . . . . . . . . . . . . 17
234	200, 233	dvmptc 22991	. . . . . . . . . . . . . . . 16
235	200	dvmptid 22990	. . . . . . . . . . . . . . . 16
236	200, 231, 232, 234, 228, 231, 235	dvmptsub 23000	. . . . . . . . . . . . . . 15
237		df-neg 9883	. . . . . . . . . . . . . . . 16
238	237	mpteq2i 4479	. . . . . . . . . . . . . . 15
239	236, 238	syl6eqr 2523	. . . . . . . . . . . . . 14
240	52	a1i 11	. . . . . . . . . . . . . 14
241		eqid 2471	. . . . . . . . . . . . . . . . 17 ℂ_fld ℂ_fld
242	241	cnfldtop 21882	. . . . . . . . . . . . . . . 16 ℂ_fld
243	241	cnfldtopon 21881	. . . . . . . . . . . . . . . . . 18 ℂ_fld TopOn
244	243	toponunii 20024	. . . . . . . . . . . . . . . . 17 ℂ_fld
245	244	restid 15410	. . . . . . . . . . . . . . . 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 21880	. . . . . . . . . . . . . . . . 17 ℂ_fld
249	248	blopn 21593	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ℂ_fld
250	38, 28, 41, 249	mp3an 1390	. . . . . . . . . . . . . . 15 ℂ_fld
251	250	a1i 11	. . . . . . . . . . . . . 14 ℂ_fld
252	200, 229, 230, 239, 240, 247, 241, 251	dvmptres 22996	. . . . . . . . . . . . 13
253	217	dvlog2 23677	. . . . . . . . . . . . . 14
254		logf1o 23593	. . . . . . . . . . . . . . . . . . . 20 $\$
255		f1of 5828	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
256	254, 255	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$
257	221	logdmss 23666	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
258	218, 257	sstri 3427	. . . . . . . . . . . . . . . . . . 19 $\$
259		fssres 5761	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$
260	256, 258, 259	mp2an 686	. . . . . . . . . . . . . . . . . 18
261	260	a1i 11	. . . . . . . . . . . . . . . . 17
262	261	feqmptd 5932	. . . . . . . . . . . . . . . 16
263		fvres 5893	. . . . . . . . . . . . . . . . 17
264	263	mpteq2ia 4478	. . . . . . . . . . . . . . . 16
265	262, 264	syl6eq 2521	. . . . . . . . . . . . . . 15
266	265	oveq2d 6324	. . . . . . . . . . . . . 14
267	253, 266	syl5reqr 2520	. . . . . . . . . . . . 13
268		fveq2 5879	. . . . . . . . . . . . 13
269		oveq2 6316	. . . . . . . . . . . . 13
270	200, 200, 214, 216, 225, 227, 252, 267, 268, 269	dvmptco 23005	. . . . . . . . . . . 12
271	200, 201, 203, 270	dvmptneg 22999	. . . . . . . . . . 11
272	55, 76	reccld 10398	. . . . . . . . . . . . . . . 16
273		mulcom 9643	. . . . . . . . . . . . . . . 16 $/\$
274	272, 215, 273	sylancl 675	. . . . . . . . . . . . . . 15
275	272	mulm1d 10091	. . . . . . . . . . . . . . 15
276	274, 275	eqtrd 2505	. . . . . . . . . . . . . 14
277	276	negeqd 9889	. . . . . . . . . . . . 13
278	272	negnegd 9996	. . . . . . . . . . . . 13
279	277, 278	eqtrd 2505	. . . . . . . . . . . 12
280	279	mpteq2ia 4478	. . . . . . . . . . 11
281	271, 280	syl6eq 2521	. . . . . . . . . 10
282	281	dmeqd 5042	. . . . . . . . 9
283		dmmptg 5339	. . . . . . . . . 10
284		ovex 6336	. . . . . . . . . . 11
285	284	a1i 11	. . . . . . . . . 10
286	283, 285	mprg 2770	. . . . . . . . 9
287	282, 286	syl6eq 2521	. . . . . . . 8
288		sumex 13831	. . . . . . . . . . . 12
289	288	a1i 11	. . . . . . . . . . 11 $/\$
290		fveq2 5879	. . . . . . . . . . . . . . 15
291	290	cbvsumv 13839	. . . . . . . . . . . . . 14
292	185, 291	syl6eq 2521	. . . . . . . . . . . . 13
293	292	mpteq2ia 4478	. . . . . . . . . . . 12
294		eqid 2471	. . . . . . . . . . . 12
295	100, 293, 109, 123, 187, 188, 294	pserdv2 23464	. . . . . . . . . . 11
296	162	ssriv 3422	. . . . . . . . . . . 12
297	296	a1i 11	. . . . . . . . . . 11
298	200, 195, 289, 295, 297, 247, 241, 251	dvmptres 22996	. . . . . . . . . 10
299		nnnn0 10900	. . . . . . . . . . . . . . . . . . . 20
300	299	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$
301		eqeq1 2475	. . . . . . . . . . . . . . . . . . . . 21
302		oveq2 6316	. . . . . . . . . . . . . . . . . . . . 21
303	301, 302	ifbieq2d 3897	. . . . . . . . . . . . . . . . . . . 20
304		ovex 6336	. . . . . . . . . . . . . . . . . . . . 21
305	93, 304	ifex 3940	. . . . . . . . . . . . . . . . . . . 20
306	303, 92, 305	fvmpt 5963	. . . . . . . . . . . . . . . . . . 19
307	300, 306	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$
308		nnne0 10664	. . . . . . . . . . . . . . . . . . . . 21
309	308	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$
310	309	neneqd 2648	. . . . . . . . . . . . . . . . . . 19 $/\$
311	310	iffalsed 3883	. . . . . . . . . . . . . . . . . 18 $/\$
312	307, 311	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$
313	312	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$
314		nncn 10639	. . . . . . . . . . . . . . . . . 18
315	314	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$
316	315, 309	recidd 10400	. . . . . . . . . . . . . . . 16 $/\$
317	313, 316	eqtrd 2505	. . . . . . . . . . . . . . 15 $/\$
318	317	oveq1d 6323	. . . . . . . . . . . . . 14 $/\$
319		nnm1nn0 10935	. . . . . . . . . . . . . . . 16
320		expcl 12328	. . . . . . . . . . . . . . . 16 $/\$
321	53, 319, 320	syl2an 485	. . . . . . . . . . . . . . 15 $/\$
322	321	mulid2d 9679	. . . . . . . . . . . . . 14 $/\$
323	318, 322	eqtrd 2505	. . . . . . . . . . . . 13 $/\$
324	323	sumeq2dv 13846	. . . . . . . . . . . 12
325		nnuz 11218	. . . . . . . . . . . . . . 15
326		1e0p1 11102	. . . . . . . . . . . . . . . 16
327	326	fveq2i 5882	. . . . . . . . . . . . . . 15
328	325, 327	eqtri 2493	. . . . . . . . . . . . . 14
329		oveq1 6315	. . . . . . . . . . . . . . 15
330	329	oveq2d 6324	. . . . . . . . . . . . . 14
331		1zzd 10992	. . . . . . . . . . . . . 14
332		0zd 10973	. . . . . . . . . . . . . 14
333	1, 328, 330, 331, 332, 321	isumshft 13974	. . . . . . . . . . . . 13
334		pncan2 9902	. . . . . . . . . . . . . . . 16 $/\$
335	50, 102, 334	sylancr 676	. . . . . . . . . . . . . . 15
336	335	oveq2d 6324	. . . . . . . . . . . . . 14
337	336	sumeq2i 13842	. . . . . . . . . . . . 13
338	333, 337	syl6eq 2521	. . . . . . . . . . . 12
339		geoisum 14010	. . . . . . . . . . . . 13 $/\$
340	53, 66, 339	syl2anc 673	. . . . . . . . . . . 12
341	324, 338, 340	3eqtrd 2509	. . . . . . . . . . 11
342	341	mpteq2ia 4478	. . . . . . . . . 10
343	298, 342	syl6eq 2521	. . . . . . . . 9
344	281, 343	eqtr4d 2508	. . . . . . . 8
345		blcntr 21506	. . . . . . . . . 10