Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . . 6
|
2 | | simpr 477 |
. . . . . . . . 9
|
3 | | elfznn 12370 |
. . . . . . . . . 10
|
4 | 3 | nnrpd 11870 |
. . . . . . . . 9
|
5 | | rpdivcl 11856 |
. . . . . . . . 9
|
6 | 2, 4, 5 | syl2an 494 |
. . . . . . . 8
|
7 | 6 | relogcld 24369 |
. . . . . . 7
|
8 | | simpll 790 |
. . . . . . 7
|
9 | 7, 8 | reexpcld 13025 |
. . . . . 6
|
10 | 1, 9 | fsumrecl 14465 |
. . . . 5
|
11 | | relogcl 24322 |
. . . . . . 7
|
12 | | id 22 |
. . . . . . 7
|
13 | | reexpcl 12877 |
. . . . . . 7
|
14 | 11, 12, 13 | syl2anr 495 |
. . . . . 6
|
15 | | faccl 13070 |
. . . . . . . . 9
|
16 | 15 | adantr 481 |
. . . . . . . 8
|
17 | 16 | nnred 11035 |
. . . . . . 7
|
18 | | fzfid 12772 |
. . . . . . . 8
|
19 | 11 | adantl 482 |
. . . . . . . . . 10
|
20 | | elfznn0 12433 |
. . . . . . . . . 10
|
21 | | reexpcl 12877 |
. . . . . . . . . 10
|
22 | 19, 20, 21 | syl2an 494 |
. . . . . . . . 9
|
23 | 20 | adantl 482 |
. . . . . . . . . 10
|
24 | | faccl 13070 |
. . . . . . . . . 10
|
25 | 23, 24 | syl 17 |
. . . . . . . . 9
|
26 | 22, 25 | nndivred 11069 |
. . . . . . . 8
|
27 | 18, 26 | fsumrecl 14465 |
. . . . . . 7
|
28 | 17, 27 | remulcld 10070 |
. . . . . 6
|
29 | 14, 28 | resubcld 10458 |
. . . . 5
|
30 | 10, 29 | resubcld 10458 |
. . . 4
|
31 | 30, 2 | rerpdivcld 11903 |
. . 3
|
32 | | rerpdivcl 11861 |
. . . 4
|
33 | 29, 32 | sylancom 701 |
. . 3
|
34 | | 1red 10055 |
. . . 4
|
35 | 15 | nncnd 11036 |
. . . 4
|
36 | | simpl 473 |
. . . . . . . . 9
|
37 | 36 | oveq2d 6666 |
. . . . . . . 8
|
38 | 37 | oveq1d 6665 |
. . . . . . 7
|
39 | 38 | mpteq2dva 4744 |
. . . . . 6
|
40 | 39 | breq1d 4663 |
. . . . 5
|
41 | 11 | recnd 10068 |
. . . . . . . . 9
|
42 | | id 22 |
. . . . . . . . 9
|
43 | | cxpexp 24414 |
. . . . . . . . 9
|
44 | 41, 42, 43 | syl2anr 495 |
. . . . . . . 8
|
45 | | rpcn 11841 |
. . . . . . . . . 10
|
46 | 45 | adantl 482 |
. . . . . . . . 9
|
47 | 46 | cxp1d 24452 |
. . . . . . . 8
|
48 | 44, 47 | oveq12d 6668 |
. . . . . . 7
|
49 | 48 | mpteq2dva 4744 |
. . . . . 6
|
50 | | nn0cn 11302 |
. . . . . . 7
|
51 | | 1rp 11836 |
. . . . . . 7
|
52 | | cxploglim2 24705 |
. . . . . . 7
|
53 | 50, 51, 52 | sylancl 694 |
. . . . . 6
|
54 | 49, 53 | eqbrtrrd 4677 |
. . . . 5
|
55 | 40, 54 | vtoclga 3272 |
. . . 4
|
56 | | rerpdivcl 11861 |
. . . . . 6
|
57 | 14, 56 | sylancom 701 |
. . . . 5
|
58 | 57 | recnd 10068 |
. . . 4
|
59 | 10 | recnd 10068 |
. . . . . 6
|
60 | 14 | recnd 10068 |
. . . . . . 7
|
61 | 35 | adantr 481 |
. . . . . . . 8
|
62 | 27 | recnd 10068 |
. . . . . . . 8
|
63 | 61, 62 | mulcld 10060 |
. . . . . . 7
|
64 | 60, 63 | subcld 10392 |
. . . . . 6
|
65 | 59, 64 | subcld 10392 |
. . . . 5
|
66 | | rpcnne0 11850 |
. . . . . . 7
|
67 | 66 | adantl 482 |
. . . . . 6
|
68 | 67 | simpld 475 |
. . . . 5
|
69 | 67 | simprd 479 |
. . . . 5
|
70 | 65, 68, 69 | divcld 10801 |
. . . 4
|
71 | 70 | adantrr 753 |
. . . . . . . 8
|
72 | 15 | adantr 481 |
. . . . . . . . 9
|
73 | 72 | nncnd 11036 |
. . . . . . . 8
|
74 | 71, 73 | subcld 10392 |
. . . . . . 7
|
75 | 74 | abscld 14175 |
. . . . . 6
|
76 | 57 | adantrr 753 |
. . . . . 6
|
77 | 76 | recnd 10068 |
. . . . . . 7
|
78 | 77 | abscld 14175 |
. . . . . 6
|
79 | | ioorp 12251 |
. . . . . . . . . 10
|
80 | 79 | eqcomi 2631 |
. . . . . . . . 9
|
81 | | nnuz 11723 |
. . . . . . . . 9
|
82 | | 1z 11407 |
. . . . . . . . . 10
|
83 | 82 | a1i 11 |
. . . . . . . . 9
|
84 | | 1red 10055 |
. . . . . . . . 9
|
85 | | 1re 10039 |
. . . . . . . . . . 11
|
86 | | 1nn0 11308 |
. . . . . . . . . . 11
|
87 | 85, 86 | nn0addge1i 11341 |
. . . . . . . . . 10
|
88 | 87 | a1i 11 |
. . . . . . . . 9
|
89 | | 0red 10041 |
. . . . . . . . 9
|
90 | 72 | adantr 481 |
. . . . . . . . . . 11
|
91 | 90 | nnred 11035 |
. . . . . . . . . 10
|
92 | | rpre 11839 |
. . . . . . . . . . . 12
|
93 | 92 | adantl 482 |
. . . . . . . . . . 11
|
94 | | fzfid 12772 |
. . . . . . . . . . . 12
|
95 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
96 | | rpdivcl 11856 |
. . . . . . . . . . . . . . . 16
|
97 | 95, 96 | sylan 488 |
. . . . . . . . . . . . . . 15
|
98 | 97 | relogcld 24369 |
. . . . . . . . . . . . . 14
|
99 | | reexpcl 12877 |
. . . . . . . . . . . . . 14
|
100 | 98, 20, 99 | syl2an 494 |
. . . . . . . . . . . . 13
|
101 | 20 | adantl 482 |
. . . . . . . . . . . . . 14
|
102 | 101, 24 | syl 17 |
. . . . . . . . . . . . 13
|
103 | 100, 102 | nndivred 11069 |
. . . . . . . . . . . 12
|
104 | 94, 103 | fsumrecl 14465 |
. . . . . . . . . . 11
|
105 | 93, 104 | remulcld 10070 |
. . . . . . . . . 10
|
106 | 91, 105 | remulcld 10070 |
. . . . . . . . 9
|
107 | | simpll 790 |
. . . . . . . . . 10
|
108 | 98, 107 | reexpcld 13025 |
. . . . . . . . 9
|
109 | | nnrp 11842 |
. . . . . . . . . 10
|
110 | 109, 108 | sylan2 491 |
. . . . . . . . 9
|
111 | | reelprrecn 10028 |
. . . . . . . . . . . 12
|
112 | 111 | a1i 11 |
. . . . . . . . . . 11
|
113 | 105 | recnd 10068 |
. . . . . . . . . . 11
|
114 | 108, 90 | nndivred 11069 |
. . . . . . . . . . 11
|
115 | | simpl 473 |
. . . . . . . . . . . 12
|
116 | | advlogexp 24401 |
. . . . . . . . . . . 12
|
117 | 95, 115, 116 | syl2anc 693 |
. . . . . . . . . . 11
|
118 | 112, 113,
114, 117, 73 | dvmptcmul 23727 |
. . . . . . . . . 10
|
119 | 108 | recnd 10068 |
. . . . . . . . . . . 12
|
120 | 73 | adantr 481 |
. . . . . . . . . . . 12
|
121 | 72 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
122 | 121 | adantr 481 |
. . . . . . . . . . . 12
|
123 | 119, 120,
122 | divcan2d 10803 |
. . . . . . . . . . 11
|
124 | 123 | mpteq2dva 4744 |
. . . . . . . . . 10
|
125 | 118, 124 | eqtrd 2656 |
. . . . . . . . 9
|
126 | | oveq2 6658 |
. . . . . . . . . . 11
|
127 | 126 | fveq2d 6195 |
. . . . . . . . . 10
|
128 | 127 | oveq1d 6665 |
. . . . . . . . 9
|
129 | 95 | rpxrd 11873 |
. . . . . . . . 9
|
130 | | simp1rl 1126 |
. . . . . . . . . . . 12
|
131 | | simp2r 1088 |
. . . . . . . . . . . 12
|
132 | 130, 131 | rpdivcld 11889 |
. . . . . . . . . . 11
|
133 | 132 | relogcld 24369 |
. . . . . . . . . 10
|
134 | | simp2l 1087 |
. . . . . . . . . . . 12
|
135 | 130, 134 | rpdivcld 11889 |
. . . . . . . . . . 11
|
136 | 135 | relogcld 24369 |
. . . . . . . . . 10
|
137 | | simp1l 1085 |
. . . . . . . . . 10
|
138 | | log1 24332 |
. . . . . . . . . . 11
|
139 | 131 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
|
140 | 139 | mulid2d 10058 |
. . . . . . . . . . . . . 14
|
141 | | simp33 1099 |
. . . . . . . . . . . . . 14
|
142 | 140, 141 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
143 | | 1red 10055 |
. . . . . . . . . . . . . 14
|
144 | 130 | rpred 11872 |
. . . . . . . . . . . . . 14
|
145 | 143, 144,
131 | lemuldivd 11921 |
. . . . . . . . . . . . 13
|
146 | 142, 145 | mpbid 222 |
. . . . . . . . . . . 12
|
147 | | logleb 24349 |
. . . . . . . . . . . . 13
|
148 | 51, 132, 147 | sylancr 695 |
. . . . . . . . . . . 12
|
149 | 146, 148 | mpbid 222 |
. . . . . . . . . . 11
|
150 | 138, 149 | syl5eqbrr 4689 |
. . . . . . . . . 10
|
151 | | simp32 1098 |
. . . . . . . . . . . 12
|
152 | 134, 131,
130 | lediv2d 11896 |
. . . . . . . . . . . 12
|
153 | 151, 152 | mpbid 222 |
. . . . . . . . . . 11
|
154 | 132, 135 | logled 24373 |
. . . . . . . . . . 11
|
155 | 153, 154 | mpbid 222 |
. . . . . . . . . 10
|
156 | | leexp1a 12919 |
. . . . . . . . . 10
|
157 | 133, 136,
137, 150, 155, 156 | syl32anc 1334 |
. . . . . . . . 9
|
158 | | eqid 2622 |
. . . . . . . . 9
|
159 | 97 | 3ad2antr1 1226 |
. . . . . . . . . . 11
|
160 | 159 | relogcld 24369 |
. . . . . . . . . 10
|
161 | | simpll 790 |
. . . . . . . . . 10
|
162 | | rpcn 11841 |
. . . . . . . . . . . . . . . . 17
|
163 | 162 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
164 | 163 | 3ad2antr1 1226 |
. . . . . . . . . . . . . . 15
|
165 | 164 | mulid2d 10058 |
. . . . . . . . . . . . . 14
|
166 | | simpr3 1069 |
. . . . . . . . . . . . . 14
|
167 | 165, 166 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
168 | | 1red 10055 |
. . . . . . . . . . . . . 14
|
169 | 95 | rpred 11872 |
. . . . . . . . . . . . . . 15
|
170 | 169 | adantr 481 |
. . . . . . . . . . . . . 14
|
171 | | simpr1 1067 |
. . . . . . . . . . . . . 14
|
172 | 168, 170,
171 | lemuldivd 11921 |
. . . . . . . . . . . . 13
|
173 | 167, 172 | mpbid 222 |
. . . . . . . . . . . 12
|
174 | | logleb 24349 |
. . . . . . . . . . . . 13
|
175 | 51, 159, 174 | sylancr 695 |
. . . . . . . . . . . 12
|
176 | 173, 175 | mpbid 222 |
. . . . . . . . . . 11
|
177 | 138, 176 | syl5eqbrr 4689 |
. . . . . . . . . 10
|
178 | 160, 161,
177 | expge0d 13026 |
. . . . . . . . 9
|
179 | 51 | a1i 11 |
. . . . . . . . 9
|
180 | | 1le1 10655 |
. . . . . . . . . 10
|
181 | 180 | a1i 11 |
. . . . . . . . 9
|
182 | | simprr 796 |
. . . . . . . . 9
|
183 | 169 | leidd 10594 |
. . . . . . . . 9
|
184 | 80, 81, 83, 84, 88, 89, 106, 108, 110, 125, 128, 129, 157, 158, 178, 179, 95, 181, 182, 183 | dvfsumlem4 23792 |
. . . . . . . 8
|
185 | | fzfid 12772 |
. . . . . . . . . . . . . 14
|
186 | 95, 4, 5 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
187 | 186 | relogcld 24369 |
. . . . . . . . . . . . . . 15
|
188 | | simpll 790 |
. . . . . . . . . . . . . . 15
|
189 | 187, 188 | reexpcld 13025 |
. . . . . . . . . . . . . 14
|
190 | 185, 189 | fsumrecl 14465 |
. . . . . . . . . . . . 13
|
191 | 190 | recnd 10068 |
. . . . . . . . . . . 12
|
192 | 95 | rpcnd 11874 |
. . . . . . . . . . . . 13
|
193 | 73, 192 | mulcld 10060 |
. . . . . . . . . . . 12
|
194 | 11 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
|
195 | 194 | recnd 10068 |
. . . . . . . . . . . . . 14
|
196 | 195, 115 | expcld 13008 |
. . . . . . . . . . . . 13
|
197 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
|
198 | 194, 20, 21 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
|
199 | 20 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
200 | 199, 24 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
201 | 198, 200 | nndivred 11069 |
. . . . . . . . . . . . . . . 16
|
202 | 201 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
203 | 197, 202 | fsumcl 14464 |
. . . . . . . . . . . . . 14
|
204 | 73, 203 | mulcld 10060 |
. . . . . . . . . . . . 13
|
205 | 196, 204 | subcld 10392 |
. . . . . . . . . . . 12
|
206 | 191, 193,
205 | sub32d 10424 |
. . . . . . . . . . 11
|
207 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
208 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
209 | 208 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
210 | 209 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
211 | 210 | sumeq1d 14431 |
. . . . . . . . . . . . . 14
|
212 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
213 | 66 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
214 | | divid 10714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
216 | 212, 215 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
217 | 216 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
218 | 217 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
219 | 218, 138 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
|
220 | 219 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
|
221 | 220 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
|
222 | 221 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . . . . 19
|
223 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
224 | 115, 223 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
225 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
227 | 226 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
228 | 227 | snssd 4340 |
. . . . . . . . . . . . . . . . . . . 20
|
229 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
230 | 229 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
231 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
232 | | 0exp0e1 12865 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
233 | 231, 232 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
234 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
235 | | fac0 13063 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
236 | 234, 235 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
237 | 233, 236 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
238 | | 1div1e1 10717 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
239 | 237, 238 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
|
240 | 230, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
241 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . 21
|
242 | 240, 241 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . . 20
|
243 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
244 | 243 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
245 | 244, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
246 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
247 | 246 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
248 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
249 | 245, 247,
248 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
250 | | dfn2 11305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
251 | 249, 250 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
252 | 251 | 0expd 13024 |
. . . . . . . . . . . . . . . . . . . . . 22
|
253 | 252 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
|
254 | 245, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
255 | 254 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . 22
|
256 | 254 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . . . 22
|
257 | 255, 256 | div0d 10800 |
. . . . . . . . . . . . . . . . . . . . 21
|
258 | 253, 257 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
|
259 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . . . 20
|
260 | 228, 242,
258, 259 | fsumss 14456 |
. . . . . . . . . . . . . . . . . . 19
|
261 | 222, 260 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
|
262 | | 0cn 10032 |
. . . . . . . . . . . . . . . . . . 19
|
263 | 239 | sumsn 14475 |
. . . . . . . . . . . . . . . . . . 19
|
264 | 262, 241,
263 | mp2an 708 |
. . . . . . . . . . . . . . . . . 18
|
265 | 261, 264 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
|
266 | 208, 265 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
267 | 192 | mulid1d 10057 |
. . . . . . . . . . . . . . . . 17
|
268 | 267 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
269 | 266, 268 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
270 | 269 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
271 | 211, 270 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
272 | | ovexd 6680 |
. . . . . . . . . . . . 13
|
273 | 207, 271,
95, 272 | fvmptd 6288 |
. . . . . . . . . . . 12
|
274 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
275 | 274 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
276 | | flid 12609 |
. . . . . . . . . . . . . . . . . . 19
|
277 | 82, 276 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
278 | 275, 277 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
|
279 | 278 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
280 | 279 | sumeq1d 14431 |
. . . . . . . . . . . . . . 15
|
281 | 192 | div1d 10793 |
. . . . . . . . . . . . . . . . . . . 20
|
282 | 281 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
283 | 282 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
284 | 283 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
285 | 196 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
286 | 284, 285 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
|
287 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
288 | 287 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
289 | 288 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
290 | 289 | fsum1 14476 |
. . . . . . . . . . . . . . . 16
|
291 | 82, 286, 290 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
292 | 280, 291,
284 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
293 | 274 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
294 | 293, 282 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
295 | 294 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
296 | 295 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
297 | 296 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
298 | 297 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
299 | 298 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . . 17
|
300 | 274, 299 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
301 | 203 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
302 | 301 | mulid2d 10058 |
. . . . . . . . . . . . . . . 16
|
303 | 300, 302 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
304 | 303 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
305 | 292, 304 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
306 | | ovexd 6680 |
. . . . . . . . . . . . 13
|
307 | 207, 305,
179, 306 | fvmptd 6288 |
. . . . . . . . . . . 12
|
308 | 273, 307 | oveq12d 6668 |
. . . . . . . . . . 11
|
309 | 71, 73, 192 | subdird 10487 |
. . . . . . . . . . . 12
|
310 | 65 | adantrr 753 |
. . . . . . . . . . . . . 14
|
311 | 213 | simprd 479 |
. . . . . . . . . . . . . 14
|
312 | 310, 192,
311 | divcan1d 10802 |
. . . . . . . . . . . . 13
|
313 | 312 | oveq1d 6665 |
. . . . . . . . . . . 12
|
314 | 309, 313 | eqtrd 2656 |
. . . . . . . . . . 11
|
315 | 206, 308,
314 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
316 | 315 | fveq2d 6195 |
. . . . . . . . 9
|
317 | 74, 192 | absmuld 14193 |
. . . . . . . . 9
|
318 | | rprege0 11847 |
. . . . . . . . . . . 12
|
319 | 318 | ad2antrl 764 |
. . . . . . . . . . 11
|
320 | | absid 14036 |
. . . . . . . . . . 11
|
321 | 319, 320 | syl 17 |
. . . . . . . . . 10
|
322 | 321 | oveq2d 6666 |
. . . . . . . . 9
|
323 | 316, 317,
322 | 3eqtrd 2660 |
. . . . . . . 8
|
324 | | 1cnd 10056 |
. . . . . . . . 9
|
325 | 295 | oveq1d 6665 |
. . . . . . . . 9
|
326 | 324, 325 | csbied 3560 |
. . . . . . . 8
|
327 | 184, 323,
326 | 3brtr3d 4684 |
. . . . . . 7
|
328 | 14 | adantrr 753 |
. . . . . . . 8
|
329 | 75, 328, 95 | lemuldivd 11921 |
. . . . . . 7
|
330 | 327, 329 | mpbid 222 |
. . . . . 6
|
331 | 76 | leabsd 14153 |
. . . . . 6
|
332 | 75, 76, 78, 330, 331 | letrd 10194 |
. . . . 5
|
333 | 58 | adantrr 753 |
. . . . . . 7
|
334 | 333 | subid1d 10381 |
. . . . . 6
|
335 | 334 | fveq2d 6195 |
. . . . 5
|
336 | 332, 335 | breqtrrd 4681 |
. . . 4
|
337 | 34, 35, 55, 58, 70, 336 | rlimsqzlem 14379 |
. . 3
|
338 | | divsubdir 10721 |
. . . . . 6
|
339 | 60, 63, 67, 338 | syl3anc 1326 |
. . . . 5
|
340 | 339 | mpteq2dva 4744 |
. . . 4
|
341 | | rerpdivcl 11861 |
. . . . . . 7
|
342 | 28, 341 | sylancom 701 |
. . . . . 6
|
343 | | divass 10703 |
. . . . . . . . . 10
|
344 | 61, 62, 67, 343 | syl3anc 1326 |
. . . . . . . . 9
|
345 | 26 | recnd 10068 |
. . . . . . . . . . . 12
|
346 | 18, 68, 345, 69 | fsumdivc 14518 |
. . . . . . . . . . 11
|
347 | 22 | recnd 10068 |
. . . . . . . . . . . . 13
|
348 | 25 | nnrpd 11870 |
. . . . . . . . . . . . . 14
|
349 | 348 | rpcnne0d 11881 |
. . . . . . . . . . . . 13
|
350 | 67 | adantr 481 |
. . . . . . . . . . . . 13
|
351 | | divdiv32 10733 |
. . . . . . . . . . . . 13
|
352 | 347, 349,
350, 351 | syl3anc 1326 |
. . . . . . . . . . . 12
|
353 | 352 | sumeq2dv 14433 |
. . . . . . . . . . 11
|
354 | 346, 353 | eqtrd 2656 |
. . . . . . . . . 10
|
355 | 354 | oveq2d 6666 |
. . . . . . . . 9
|
356 | 344, 355 | eqtrd 2656 |
. . . . . . . 8
|
357 | 356 | mpteq2dva 4744 |
. . . . . . 7
|
358 | 2 | adantr 481 |
. . . . . . . . . . . 12
|
359 | 22, 358 | rerpdivcld 11903 |
. . . . . . . . . . 11
|
360 | 359, 25 | nndivred 11069 |
. . . . . . . . . 10
|
361 | 18, 360 | fsumrecl 14465 |
. . . . . . . . 9
|
362 | | rpssre 11843 |
. . . . . . . . . 10
|
363 | | rlimconst 14275 |
. . . . . . . . . 10
|
364 | 362, 35, 363 | sylancr 695 |
. . . . . . . . 9
|
365 | 362 | a1i 11 |
. . . . . . . . . . 11
|
366 | | fzfid 12772 |
. . . . . . . . . . 11
|
367 | 360 | anasss 679 |
. . . . . . . . . . 11
|
368 | 359 | an32s 846 |
. . . . . . . . . . . . 13
|
369 | 20 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
370 | 369, 24 | syl 17 |
. . . . . . . . . . . . . . 15
|
371 | 370 | nnred 11035 |
. . . . . . . . . . . . . 14
|
372 | 371 | adantr 481 |
. . . . . . . . . . . . 13
|
373 | 369, 54 | syl 17 |
. . . . . . . . . . . . 13
|
374 | 370 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
375 | | rlimconst 14275 |
. . . . . . . . . . . . . 14
|
376 | 362, 374,
375 | sylancr 695 |
. . . . . . . . . . . . 13
|
377 | 370 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
378 | 377 | adantr 481 |
. . . . . . . . . . . . 13
|
379 | 368, 372,
373, 376, 377, 378 | rlimdiv 14376 |
. . . . . . . . . . . 12
|
380 | 374, 377 | div0d 10800 |
. . . . . . . . . . . 12
|
381 | 379, 380 | breqtrd 4679 |
. . . . . . . . . . 11
|
382 | 365, 366,
367, 381 | fsumrlim 14543 |
. . . . . . . . . 10
|
383 | | fzfi 12771 |
. . . . . . . . . . . 12
|
384 | 383 | olci 406 |
. . . . . . . . . . 11
|
385 | | sumz 14453 |
. . . . . . . . . . 11
|
386 | 384, 385 | ax-mp 5 |
. . . . . . . . . 10
|
387 | 382, 386 | syl6breq 4694 |
. . . . . . . . 9
|
388 | 17, 361, 364, 387 | rlimmul 14375 |
. . . . . . . 8
|
389 | 35 | mul01d 10235 |
. . . . . . . 8
|
390 | 388, 389 | breqtrd 4679 |
. . . . . . 7
|
391 | 357, 390 | eqbrtrd 4675 |
. . . . . 6
|
392 | 57, 342, 55, 391 | rlimsub 14374 |
. . . . 5
|
393 | | 0m0e0 11130 |
. . . . 5
|
394 | 392, 393 | syl6breq 4694 |
. . . 4
|
395 | 340, 394 | eqbrtrd 4675 |
. . 3
|
396 | 31, 33, 337, 395 | rlimadd 14373 |
. 2
|
397 | | divsubdir 10721 |
. . . . . 6
|
398 | 59, 64, 67, 397 | syl3anc 1326 |
. . . . 5
|
399 | 398 | oveq1d 6665 |
. . . 4
|
400 | 10, 2 | rerpdivcld 11903 |
. . . . . 6
|
401 | 400 | recnd 10068 |
. . . . 5
|
402 | 33 | recnd 10068 |
. . . . 5
|
403 | 401, 402 | npcand 10396 |
. . . 4
|
404 | 399, 403 | eqtrd 2656 |
. . 3
|
405 | 404 | mpteq2dva 4744 |
. 2
|
406 | 35 | addid1d 10236 |
. 2
|
407 | 396, 405,
406 | 3brtr3d 4684 |
1
|