logexprlim - Metamath Proof Explorer

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

Theorem logexprlim 24201

Description: The sum

has the asymptotic expansion

. (More precisely, the omitted term has order

.) (Contributed by Mario Carneiro, 22-May-2016.)

**Assertion**
Ref	Expression
logexprlim

Distinct variable group:

Proof of Theorem logexprlim Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 12217	. . . . . 6 $/\$
2		simpr 467	. . . . . . . . 9 $/\$
3		elfznn 11856	. . . . . . . . . 10
4	3	nnrpd 11367	. . . . . . . . 9
5		rpdivcl 11353	. . . . . . . . 9 $/\$
6	2, 4, 5	syl2an 484	. . . . . . . 8 $/\$ $/\$
7	6	relogcld 23620	. . . . . . 7 $/\$ $/\$
8		simpll 765	. . . . . . 7 $/\$ $/\$
9	7, 8	reexpcld 12464	. . . . . 6 $/\$ $/\$
10	1, 9	fsumrecl 13848	. . . . 5 $/\$
11		relogcl 23573	. . . . . . 7
12		id 22	. . . . . . 7
13		reexpcl 12320	. . . . . . 7 $/\$
14	11, 12, 13	syl2anr 485	. . . . . 6 $/\$
15		faccl 12500	. . . . . . . . 9
16	15	adantr 471	. . . . . . . 8 $/\$
17	16	nnred 10651	. . . . . . 7 $/\$
18		fzfid 12217	. . . . . . . 8 $/\$
19	11	adantl 472	. . . . . . . . . 10 $/\$
20		elfznn0 11915	. . . . . . . . . 10
21		reexpcl 12320	. . . . . . . . . 10 $/\$
22	19, 20, 21	syl2an 484	. . . . . . . . 9 $/\$ $/\$
23	20	adantl 472	. . . . . . . . . 10 $/\$ $/\$
24		faccl 12500	. . . . . . . . . 10
25	23, 24	syl 17	. . . . . . . . 9 $/\$ $/\$
26	22, 25	nndivred 10685	. . . . . . . 8 $/\$ $/\$
27	18, 26	fsumrecl 13848	. . . . . . 7 $/\$
28	17, 27	remulcld 9696	. . . . . 6 $/\$
29	14, 28	resubcld 10074	. . . . 5 $/\$
30	10, 29	resubcld 10074	. . . 4 $/\$
31	30, 2	rerpdivcld 11397	. . 3 $/\$
32		rerpdivcl 11358	. . . 4 $/\$
33	29, 32	sylancom 678	. . 3 $/\$
34		1red 9683	. . . 4
35	15	nncnd 10652	. . . 4
36		simpl 463	. . . . . . . . 9 $/\$
37	36	oveq2d 6330	. . . . . . . 8 $/\$
38	37	oveq1d 6329	. . . . . . 7 $/\$
39	38	mpteq2dva 4502	. . . . . 6
40	39	breq1d 4425	. . . . 5
41	11	recnd 9694	. . . . . . . . 9
42		id 22	. . . . . . . . 9
43		cxpexp 23661	. . . . . . . . 9 $/\$
44	41, 42, 43	syl2anr 485	. . . . . . . 8 $/\$
45		rpcn 11338	. . . . . . . . . 10
46	45	adantl 472	. . . . . . . . 9 $/\$
47	46	cxp1d 23699	. . . . . . . 8 $/\$
48	44, 47	oveq12d 6332	. . . . . . 7 $/\$
49	48	mpteq2dva 4502	. . . . . 6
50		nn0cn 10907	. . . . . . 7
51		1rp 11334	. . . . . . 7
52		cxploglim2 23952	. . . . . . 7 $/\$
53	50, 51, 52	sylancl 673	. . . . . 6
54	49, 53	eqbrtrrd 4438	. . . . 5
55	40, 54	vtoclga 3124	. . . 4
56		rerpdivcl 11358	. . . . . 6 $/\$
57	14, 56	sylancom 678	. . . . 5 $/\$
58	57	recnd 9694	. . . 4 $/\$
59	10	recnd 9694	. . . . . 6 $/\$
60	14	recnd 9694	. . . . . . 7 $/\$
61	35	adantr 471	. . . . . . . 8 $/\$
62	27	recnd 9694	. . . . . . . 8 $/\$
63	61, 62	mulcld 9688	. . . . . . 7 $/\$
64	60, 63	subcld 10011	. . . . . 6 $/\$
65	59, 64	subcld 10011	. . . . 5 $/\$
66		rpcnne0 11347	. . . . . . 7 $/\$
67	66	adantl 472	. . . . . 6 $/\$ $/\$
68	67	simpld 465	. . . . 5 $/\$
69	67	simprd 469	. . . . 5 $/\$
70	65, 68, 69	divcld 10410	. . . 4 $/\$
71	70	adantrr 728	. . . . . . . 8 $/\$ $/\$
72	15	adantr 471	. . . . . . . . 9 $/\$ $/\$
73	72	nncnd 10652	. . . . . . . 8 $/\$ $/\$
74	71, 73	subcld 10011	. . . . . . 7 $/\$ $/\$
75	74	abscld 13546	. . . . . 6 $/\$ $/\$
76	57	adantrr 728	. . . . . 6 $/\$ $/\$
77	76	recnd 9694	. . . . . . 7 $/\$ $/\$
78	77	abscld 13546	. . . . . 6 $/\$ $/\$
79		ioorp 11740	. . . . . . . . . 10
80	79	eqcomi 2470	. . . . . . . . 9
81		nnuz 11222	. . . . . . . . 9
82		1z 10995	. . . . . . . . . 10
83	82	a1i 11	. . . . . . . . 9 $/\$ $/\$
84		1red 9683	. . . . . . . . 9 $/\$ $/\$
85		1re 9667	. . . . . . . . . . 11
86		1nn0 10913	. . . . . . . . . . 11
87	85, 86	nn0addge1i 10946	. . . . . . . . . 10
88	87	a1i 11	. . . . . . . . 9 $/\$ $/\$
89		0red 9669	. . . . . . . . 9 $/\$ $/\$
90	72	adantr 471	. . . . . . . . . . 11 $/\$ $/\$ $/\$
91	90	nnred 10651	. . . . . . . . . 10 $/\$ $/\$ $/\$
92		rpre 11336	. . . . . . . . . . . 12
93	92	adantl 472	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94		fzfid 12217	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
95		simprl 769	. . . . . . . . . . . . . . . 16 $/\$ $/\$
96		rpdivcl 11353	. . . . . . . . . . . . . . . 16 $/\$
97	95, 96	sylan 478	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
98	97	relogcld 23620	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
99		reexpcl 12320	. . . . . . . . . . . . . 14 $/\$
100	98, 20, 99	syl2an 484	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101	20	adantl 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
102	101, 24	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
103	100, 102	nndivred 10685	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
104	94, 103	fsumrecl 13848	. . . . . . . . . . 11 $/\$ $/\$ $/\$
105	93, 104	remulcld 9696	. . . . . . . . . 10 $/\$ $/\$ $/\$
106	91, 105	remulcld 9696	. . . . . . . . 9 $/\$ $/\$ $/\$
107		simpll 765	. . . . . . . . . 10 $/\$ $/\$ $/\$
108	98, 107	reexpcld 12464	. . . . . . . . 9 $/\$ $/\$ $/\$
109		nnrp 11339	. . . . . . . . . 10
110	109, 108	sylan2 481	. . . . . . . . 9 $/\$ $/\$ $/\$
111		reelprrecn 9656	. . . . . . . . . . . 12
112	111	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
113	105	recnd 9694	. . . . . . . . . . 11 $/\$ $/\$ $/\$
114	108, 90	nndivred 10685	. . . . . . . . . . 11 $/\$ $/\$ $/\$
115		simpl 463	. . . . . . . . . . . 12 $/\$ $/\$
116		advlogexp 23648	. . . . . . . . . . . 12 $/\$
117	95, 115, 116	syl2anc 671	. . . . . . . . . . 11 $/\$ $/\$
118	112, 113, 114, 117, 73	dvmptcmul 22966	. . . . . . . . . 10 $/\$ $/\$
119	108	recnd 9694	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
120	73	adantr 471	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	72	nnne0d 10681	. . . . . . . . . . . . 13 $/\$ $/\$
122	121	adantr 471	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
123	119, 120, 122	divcan2d 10412	. . . . . . . . . . 11 $/\$ $/\$ $/\$
124	123	mpteq2dva 4502	. . . . . . . . . 10 $/\$ $/\$
125	118, 124	eqtrd 2495	. . . . . . . . 9 $/\$ $/\$
126		oveq2 6322	. . . . . . . . . . 11
127	126	fveq2d 5891	. . . . . . . . . 10
128	127	oveq1d 6329	. . . . . . . . 9
129	95	rpxrd 11370	. . . . . . . . 9 $/\$ $/\$
130		simp1rl 1079	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131		simp2r 1041	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	130, 131	rpdivcld 11386	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133	132	relogcld 23620	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
134		simp2l 1040	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	130, 134	rpdivcld 11386	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136	135	relogcld 23620	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
137		simp1l 1038	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
138		log1 23583	. . . . . . . . . . 11
139	131	rpcnd 11371	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140	139	mulid2d 9686	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
141		simp33 1052	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
142	140, 141	eqbrtrd 4436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
143		1red 9683	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
144	130	rpred 11369	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
145	143, 144, 131	lemuldivd 11415	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	142, 145	mpbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147		logleb 23600	. . . . . . . . . . . . 13 $/\$
148	51, 132, 147	sylancr 674	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149	146, 148	mpbid 215	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	138, 149	syl5eqbrr 4450	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151		simp32 1051	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
152	134, 131, 130	lediv2d 11393	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153	151, 152	mpbid 215	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
154	132, 135	logled 23624	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
155	153, 154	mpbid 215	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156		leexp1a 12362	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
157	133, 136, 137, 150, 155, 156	syl32anc 1284	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158		eqid 2461	. . . . . . . . 9
159	97	3ad2antr1 1179	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
160	159	relogcld 23620	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
161		simpll 765	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
162		rpcn 11338	. . . . . . . . . . . . . . . . 17
163	162	adantl 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
164	163	3ad2antr1 1179	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
165	164	mulid2d 9686	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
166		simpr3 1022	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
167	165, 166	eqbrtrd 4436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
168		1red 9683	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
169	95	rpred 11369	. . . . . . . . . . . . . . 15 $/\$ $/\$
170	169	adantr 471	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
171		simpr1 1020	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
172	168, 170, 171	lemuldivd 11415	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
173	167, 172	mpbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
174		logleb 23600	. . . . . . . . . . . . 13 $/\$
175	51, 159, 174	sylancr 674	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
176	173, 175	mpbid 215	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
177	138, 176	syl5eqbrr 4450	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
178	160, 161, 177	expge0d 12465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
179	51	a1i 11	. . . . . . . . 9 $/\$ $/\$
180		1le1 10267	. . . . . . . . . 10
181	180	a1i 11	. . . . . . . . 9 $/\$ $/\$
182		simprr 771	. . . . . . . . 9 $/\$ $/\$
183	169	leidd 10207	. . . . . . . . 9 $/\$ $/\$
184	80, 81, 83, 84, 88, 89, 106, 108, 110, 125, 128, 129, 157, 158, 178, 179, 95, 181, 182, 183	dvfsumlem4 23029	. . . . . . . 8 $/\$ $/\$
185		fzfid 12217	. . . . . . . . . . . . . 14 $/\$ $/\$
186	95, 4, 5	syl2an 484	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
187	186	relogcld 23620	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188		simpll 765	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
189	187, 188	reexpcld 12464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
190	185, 189	fsumrecl 13848	. . . . . . . . . . . . 13 $/\$ $/\$
191	190	recnd 9694	. . . . . . . . . . . 12 $/\$ $/\$
192	95	rpcnd 11371	. . . . . . . . . . . . 13 $/\$ $/\$
193	73, 192	mulcld 9688	. . . . . . . . . . . 12 $/\$ $/\$
194	11	ad2antrl 739	. . . . . . . . . . . . . . 15 $/\$ $/\$
195	194	recnd 9694	. . . . . . . . . . . . . 14 $/\$ $/\$
196	195, 115	expcld 12447	. . . . . . . . . . . . 13 $/\$ $/\$
197		fzfid 12217	. . . . . . . . . . . . . . 15 $/\$ $/\$
198	194, 20, 21	syl2an 484	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
199	20	adantl 472	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
200	199, 24	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
201	198, 200	nndivred 10685	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
202	201	recnd 9694	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
203	197, 202	fsumcl 13847	. . . . . . . . . . . . . 14 $/\$ $/\$
204	73, 203	mulcld 9688	. . . . . . . . . . . . 13 $/\$ $/\$
205	196, 204	subcld 10011	. . . . . . . . . . . 12 $/\$ $/\$
206	191, 193, 205	sub32d 10043	. . . . . . . . . . 11 $/\$ $/\$
207		eqidd 2462	. . . . . . . . . . . . 13 $/\$ $/\$
208		simpr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
209	208	fveq2d 5891	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
210	209	oveq2d 6330	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
211	210	sumeq1d 13815	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
212		oveq2 6322	. . . . . . . . . . . . . . . . . . . . . . . . . 26
213	66	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
214		divid 10324	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
216	212, 215	sylan9eqr 2517	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
217	216	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
218	217	fveq2d 5891	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
219	218, 138	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
220	219	oveq1d 6329	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
221	220	oveq1d 6329	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
222	221	sumeq2dv 13817	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
223		nn0uz 11221	. . . . . . . . . . . . . . . . . . . . . . . 24
224	115, 223	syl6eleq 2549	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
225		eluzfz1 11834	. . . . . . . . . . . . . . . . . . . . . . 23
226	224, 225	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
227	226	adantr 471	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
228	227	snssd 4129	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
229		elsni 4004	. . . . . . . . . . . . . . . . . . . . . . 23
230	229	adantl 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
231		oveq2 6322	. . . . . . . . . . . . . . . . . . . . . . . . 25
232		0exp0e1 12308	. . . . . . . . . . . . . . . . . . . . . . . . 25
233	231, 232	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . 24
234		fveq2 5887	. . . . . . . . . . . . . . . . . . . . . . . . 25
235		fac0 12493	. . . . . . . . . . . . . . . . . . . . . . . . 25
236	234, 235	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . 24
237	233, 236	oveq12d 6332	. . . . . . . . . . . . . . . . . . . . . . 23
238		1div1e1 10327	. . . . . . . . . . . . . . . . . . . . . . 23
239	237, 238	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . 22
240	230, 239	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
241		ax-1cn 9622	. . . . . . . . . . . . . . . . . . . . 21
242	240, 241	syl6eqel 2547	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
243		eldifi 3566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
244	243	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $\$
245	244, 20	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $\$
246		eldifsni 4110	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
247	246	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $\$
248		eldifsn 4109	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
249	245, 247, 248	sylanbrc 675	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $\$ $\$
250		dfn2 10910	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
251	249, 250	syl6eleqr 2550	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $\$
252	251	0expd 12463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$
253	252	oveq1d 6329	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $\$
254	245, 24	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $\$
255	254	nncnd 10652	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$
256	254	nnne0d 10681	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$
257	255, 256	div0d 10409	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $\$
258	253, 257	eqtrd 2495	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
259		fzfid 12217	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
260	228, 242, 258, 259	fsumss 13839	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
261	222, 260	eqtr4d 2498	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
262		0cn 9660	. . . . . . . . . . . . . . . . . . 19
263	239	sumsn 13855	. . . . . . . . . . . . . . . . . . 19 $/\$
264	262, 241, 263	mp2an 683	. . . . . . . . . . . . . . . . . 18
265	261, 264	syl6eq 2511	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
266	208, 265	oveq12d 6332	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
267	192	mulid1d 9685	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
268	267	adantr 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
269	266, 268	eqtrd 2495	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
270	269	oveq2d 6330	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
271	211, 270	oveq12d 6332	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
272		ovex 6342	. . . . . . . . . . . . . 14
273	272	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
274	207, 271, 95, 273	fvmptd 5976	. . . . . . . . . . . 12 $/\$ $/\$
275		simpr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
276	275	fveq2d 5891	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
277		flid 12075	. . . . . . . . . . . . . . . . . . 19
278	82, 277	ax-mp 5	. . . . . . . . . . . . . . . . . 18
279	276, 278	syl6eq 2511	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
280	279	oveq2d 6330	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
281	280	sumeq1d 13815	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
282	192	div1d 10402	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
283	282	adantr 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
284	283	fveq2d 5891	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
285	284	oveq1d 6329	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
286	196	adantr 471	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
287	285, 286	eqeltrd 2539	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
288		oveq2 6322	. . . . . . . . . . . . . . . . . . 19
289	288	fveq2d 5891	. . . . . . . . . . . . . . . . . 18
290	289	oveq1d 6329	. . . . . . . . . . . . . . . . 17
291	290	fsum1 13856	. . . . . . . . . . . . . . . 16 $/\$
292	82, 287, 291	sylancr 674	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
293	281, 292, 285	3eqtrd 2499	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
294	275	oveq2d 6330	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
295	294, 283	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
296	295	fveq2d 5891	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
297	296	adantr 471	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
298	297	oveq1d 6329	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
299	298	oveq1d 6329	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
300	299	sumeq2dv 13817	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
301	275, 300	oveq12d 6332	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
302	203	adantr 471	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
303	302	mulid2d 9686	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
304	301, 303	eqtrd 2495	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
305	304	oveq2d 6330	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
306	293, 305	oveq12d 6332	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
307		ovex 6342	. . . . . . . . . . . . . 14
308	307	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
309	207, 306, 179, 308	fvmptd 5976	. . . . . . . . . . . 12 $/\$ $/\$
310	274, 309	oveq12d 6332	. . . . . . . . . . 11 $/\$ $/\$
311	71, 73, 192	subdird 10102	. . . . . . . . . . . 12 $/\$ $/\$
312	65	adantrr 728	. . . . . . . . . . . . . 14 $/\$ $/\$
313	213	simprd 469	. . . . . . . . . . . . . 14 $/\$ $/\$
314	312, 192, 313	divcan1d 10411	. . . . . . . . . . . . 13 $/\$ $/\$
315	314	oveq1d 6329	. . . . . . . . . . . 12 $/\$ $/\$
316	311, 315	eqtrd 2495	. . . . . . . . . . 11 $/\$ $/\$
317	206, 310, 316	3eqtr4d 2505	. . . . . . . . . 10 $/\$ $/\$
318	317	fveq2d 5891	. . . . . . . . 9 $/\$ $/\$
319	74, 192	absmuld 13564	. . . . . . . . 9 $/\$ $/\$
320		rprege0 11344	. . . . . . . . . . . 12 $/\$
321	320	ad2antrl 739	. . . . . . . . . . 11 $/\$ $/\$ $/\$
322		absid 13407	. . . . . . . . . . 11 $/\$
323	321, 322	syl 17	. . . . . . . . . 10 $/\$ $/\$
324	323	oveq2d 6330	. . . . . . . . 9 $/\$ $/\$
325	318, 319, 324	3eqtrd 2499	. . . . . . . 8 $/\$ $/\$
326		1cnd 9684	. . . . . . . . 9 $/\$ $/\$
327	296	oveq1d 6329	. . . . . . . . 9 $/\$ $/\$ $/\$
328	326, 327	csbied 3401	. . . . . . . 8 $/\$ $/\$
329	184, 325, 328	3brtr3d 4445	. . . . . . 7 $/\$ $/\$
330	14	adantrr 728	. . . . . . . 8 $/\$ $/\$
331	75, 330, 95	lemuldivd 11415	. . . . . . 7 $/\$ $/\$