Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . 5
|
2 | | oveq2 6658 |
. . . . . . . 8
|
3 | | 2cn 11091 |
. . . . . . . . 9
|
4 | | exp1 12866 |
. . . . . . . . 9
|
5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
|
6 | 2, 5 | syl6eq 2672 |
. . . . . . 7
|
7 | 6 | fveq2d 6195 |
. . . . . 6
|
8 | 7 | oveq2d 6666 |
. . . . 5
|
9 | 1, 8 | breq12d 4666 |
. . . 4
|
10 | 9 | imbi2d 330 |
. . 3
|
11 | | fveq2 6191 |
. . . . 5
|
12 | | oveq2 6658 |
. . . . . . 7
|
13 | 12 | fveq2d 6195 |
. . . . . 6
|
14 | 13 | oveq2d 6666 |
. . . . 5
|
15 | 11, 14 | breq12d 4666 |
. . . 4
|
16 | 15 | imbi2d 330 |
. . 3
|
17 | | fveq2 6191 |
. . . . 5
|
18 | | oveq2 6658 |
. . . . . . 7
|
19 | 18 | fveq2d 6195 |
. . . . . 6
|
20 | 19 | oveq2d 6666 |
. . . . 5
|
21 | 17, 20 | breq12d 4666 |
. . . 4
|
22 | 21 | imbi2d 330 |
. . 3
|
23 | | fveq2 6191 |
. . . . 5
|
24 | | oveq2 6658 |
. . . . . . 7
|
25 | 24 | fveq2d 6195 |
. . . . . 6
|
26 | 25 | oveq2d 6666 |
. . . . 5
|
27 | 23, 26 | breq12d 4666 |
. . . 4
|
28 | 27 | imbi2d 330 |
. . 3
|
29 | | 1nn 11031 |
. . . . . . 7
|
30 | | climcnds.2 |
. . . . . . . 8
|
31 | 30 | ralrimiva 2966 |
. . . . . . 7
|
32 | | fveq2 6191 |
. . . . . . . . 9
|
33 | 32 | breq2d 4665 |
. . . . . . . 8
|
34 | 33 | rspcv 3305 |
. . . . . . 7
|
35 | 29, 31, 34 | mpsyl 68 |
. . . . . 6
|
36 | | 2nn 11185 |
. . . . . . . 8
|
37 | | climcnds.1 |
. . . . . . . . 9
|
38 | 37 | ralrimiva 2966 |
. . . . . . . 8
|
39 | | fveq2 6191 |
. . . . . . . . . 10
|
40 | 39 | eleq1d 2686 |
. . . . . . . . 9
|
41 | 40 | rspcv 3305 |
. . . . . . . 8
|
42 | 36, 38, 41 | mpsyl 68 |
. . . . . . 7
|
43 | 32 | eleq1d 2686 |
. . . . . . . . 9
|
44 | 43 | rspcv 3305 |
. . . . . . . 8
|
45 | 29, 38, 44 | mpsyl 68 |
. . . . . . 7
|
46 | 42, 45 | addge02d 10616 |
. . . . . 6
|
47 | 35, 46 | mpbid 222 |
. . . . 5
|
48 | 45, 42 | readdcld 10069 |
. . . . . 6
|
49 | | 2re 11090 |
. . . . . . . 8
|
50 | | 2pos 11112 |
. . . . . . . 8
|
51 | 49, 50 | pm3.2i 471 |
. . . . . . 7
|
52 | 51 | a1i 11 |
. . . . . 6
|
53 | | lemul2 10876 |
. . . . . 6
|
54 | 42, 48, 52, 53 | syl3anc 1326 |
. . . . 5
|
55 | 47, 54 | mpbid 222 |
. . . 4
|
56 | | 1z 11407 |
. . . . 5
|
57 | | 1nn0 11308 |
. . . . . 6
|
58 | | climcnds.4 |
. . . . . . 7
|
59 | 58 | ralrimiva 2966 |
. . . . . 6
|
60 | | fveq2 6191 |
. . . . . . . 8
|
61 | | oveq2 6658 |
. . . . . . . . . 10
|
62 | 61, 5 | syl6eq 2672 |
. . . . . . . . 9
|
63 | 62 | fveq2d 6195 |
. . . . . . . . 9
|
64 | 62, 63 | oveq12d 6668 |
. . . . . . . 8
|
65 | 60, 64 | eqeq12d 2637 |
. . . . . . 7
|
66 | 65 | rspcv 3305 |
. . . . . 6
|
67 | 57, 59, 66 | mpsyl 68 |
. . . . 5
|
68 | 56, 67 | seq1i 12815 |
. . . 4
|
69 | | nnuz 11723 |
. . . . . 6
|
70 | | df-2 11079 |
. . . . . 6
|
71 | | eqidd 2623 |
. . . . . . 7
|
72 | 56, 71 | seq1i 12815 |
. . . . . 6
|
73 | | eqidd 2623 |
. . . . . 6
|
74 | 69, 29, 70, 72, 73 | seqp1i 12817 |
. . . . 5
|
75 | 74 | oveq2d 6666 |
. . . 4
|
76 | 55, 68, 75 | 3brtr4d 4685 |
. . 3
|
77 | | peano2nn 11032 |
. . . . . . . . . . . 12
|
78 | 77 | adantl 482 |
. . . . . . . . . . 11
|
79 | 78 | nnnn0d 11351 |
. . . . . . . . . 10
|
80 | 59 | adantr 481 |
. . . . . . . . . 10
|
81 | | fveq2 6191 |
. . . . . . . . . . . 12
|
82 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
83 | 82 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
84 | 82, 83 | oveq12d 6668 |
. . . . . . . . . . . 12
|
85 | 81, 84 | eqeq12d 2637 |
. . . . . . . . . . 11
|
86 | 85 | rspcv 3305 |
. . . . . . . . . 10
|
87 | 79, 80, 86 | sylc 65 |
. . . . . . . . 9
|
88 | | nnnn0 11299 |
. . . . . . . . . . . . 13
|
89 | 88 | adantl 482 |
. . . . . . . . . . . 12
|
90 | | expp1 12867 |
. . . . . . . . . . . 12
|
91 | 3, 89, 90 | sylancr 695 |
. . . . . . . . . . 11
|
92 | | nnexpcl 12873 |
. . . . . . . . . . . . . . 15
|
93 | 36, 88, 92 | sylancr 695 |
. . . . . . . . . . . . . 14
|
94 | 93 | adantl 482 |
. . . . . . . . . . . . 13
|
95 | 94 | nncnd 11036 |
. . . . . . . . . . . 12
|
96 | | mulcom 10022 |
. . . . . . . . . . . 12
|
97 | 95, 3, 96 | sylancl 694 |
. . . . . . . . . . 11
|
98 | 91, 97 | eqtrd 2656 |
. . . . . . . . . 10
|
99 | 98 | oveq1d 6665 |
. . . . . . . . 9
|
100 | 3 | a1i 11 |
. . . . . . . . . 10
|
101 | | nnexpcl 12873 |
. . . . . . . . . . . . 13
|
102 | 36, 79, 101 | sylancr 695 |
. . . . . . . . . . . 12
|
103 | 38 | adantr 481 |
. . . . . . . . . . . 12
|
104 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
105 | 104 | eleq1d 2686 |
. . . . . . . . . . . . 13
|
106 | 105 | rspcv 3305 |
. . . . . . . . . . . 12
|
107 | 102, 103,
106 | sylc 65 |
. . . . . . . . . . 11
|
108 | 107 | recnd 10068 |
. . . . . . . . . 10
|
109 | 100, 95, 108 | mulassd 10063 |
. . . . . . . . 9
|
110 | 87, 99, 109 | 3eqtrd 2660 |
. . . . . . . 8
|
111 | 94 | nnnn0d 11351 |
. . . . . . . . . . . . . . 15
|
112 | | hashfz1 13134 |
. . . . . . . . . . . . . . 15
|
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . 14
|
114 | 113, 95 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
115 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
|
116 | | hashcl 13147 |
. . . . . . . . . . . . . . 15
|
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . 14
|
118 | 117 | nn0cnd 11353 |
. . . . . . . . . . . . 13
|
119 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
120 | 119 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
|
121 | | uzid 11702 |
. . . . . . . . . . . . . . . . . 18
|
122 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . 18
|
123 | | 1le2 11241 |
. . . . . . . . . . . . . . . . . . 19
|
124 | | leexp2a 12916 |
. . . . . . . . . . . . . . . . . . 19
|
125 | 49, 123, 124 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . 18
|
126 | 120, 121,
122, 125 | 4syl 19 |
. . . . . . . . . . . . . . . . 17
|
127 | 94, 69 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
|
128 | 102 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
|
129 | | elfz5 12334 |
. . . . . . . . . . . . . . . . . 18
|
130 | 127, 128,
129 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
131 | 126, 130 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
132 | | fzsplit 12367 |
. . . . . . . . . . . . . . . 16
|
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . 15
|
134 | 133 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
135 | 95 | times2d 11276 |
. . . . . . . . . . . . . . . 16
|
136 | 91, 135 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
137 | 102 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
|
138 | | hashfz1 13134 |
. . . . . . . . . . . . . . . 16
|
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . . 15
|
140 | 113 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
141 | 136, 139,
140 | 3eqtr4d 2666 |
. . . . . . . . . . . . . 14
|
142 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
|
143 | 94 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
|
144 | 143 | ltp1d 10954 |
. . . . . . . . . . . . . . . 16
|
145 | | fzdisj 12368 |
. . . . . . . . . . . . . . . 16
|
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . 15
|
147 | | hashun 13171 |
. . . . . . . . . . . . . . 15
|
148 | 142, 115,
146, 147 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
149 | 134, 141,
148 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
|
150 | 114, 95, 118, 149 | addcanad 10241 |
. . . . . . . . . . . 12
|
151 | 150 | oveq1d 6665 |
. . . . . . . . . . 11
|
152 | | fsumconst 14522 |
. . . . . . . . . . . 12
|
153 | 115, 108,
152 | syl2anc 693 |
. . . . . . . . . . 11
|
154 | 151, 153 | eqtr4d 2659 |
. . . . . . . . . 10
|
155 | 107 | adantr 481 |
. . . . . . . . . . 11
|
156 | | simpl 473 |
. . . . . . . . . . . . 13
|
157 | 156 | adantr 481 |
. . . . . . . . . . . 12
|
158 | | peano2nn 11032 |
. . . . . . . . . . . . . 14
|
159 | 94, 158 | syl 17 |
. . . . . . . . . . . . 13
|
160 | | elfzuz 12338 |
. . . . . . . . . . . . 13
|
161 | | eluznn 11758 |
. . . . . . . . . . . . 13
|
162 | 159, 160,
161 | syl2an 494 |
. . . . . . . . . . . 12
|
163 | 157, 162,
37 | syl2anc 693 |
. . . . . . . . . . 11
|
164 | | elfzuz3 12339 |
. . . . . . . . . . . . . . 15
|
165 | 164 | adantl 482 |
. . . . . . . . . . . . . 14
|
166 | | simplll 798 |
. . . . . . . . . . . . . . 15
|
167 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . 17
|
168 | | eluznn 11758 |
. . . . . . . . . . . . . . . . 17
|
169 | 159, 167,
168 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
170 | | elfzuz 12338 |
. . . . . . . . . . . . . . . 16
|
171 | | eluznn 11758 |
. . . . . . . . . . . . . . . 16
|
172 | 169, 170,
171 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
173 | 166, 172,
37 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
174 | | simplll 798 |
. . . . . . . . . . . . . . 15
|
175 | | elfzuz 12338 |
. . . . . . . . . . . . . . . 16
|
176 | 169, 175,
171 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
177 | | climcnds.3 |
. . . . . . . . . . . . . . 15
|
178 | 174, 176,
177 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
179 | 165, 173,
178 | monoord2 12832 |
. . . . . . . . . . . . 13
|
180 | 179 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
181 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
182 | 181 | breq2d 4665 |
. . . . . . . . . . . . 13
|
183 | 182 | rspccva 3308 |
. . . . . . . . . . . 12
|
184 | 180, 183 | sylan 488 |
. . . . . . . . . . 11
|
185 | 115, 155,
163, 184 | fsumle 14531 |
. . . . . . . . . 10
|
186 | 154, 185 | eqbrtrd 4675 |
. . . . . . . . 9
|
187 | 143, 107 | remulcld 10070 |
. . . . . . . . . 10
|
188 | 115, 163 | fsumrecl 14465 |
. . . . . . . . . 10
|
189 | 51 | a1i 11 |
. . . . . . . . . 10
|
190 | | lemul2 10876 |
. . . . . . . . . 10
|
191 | 187, 188,
189, 190 | syl3anc 1326 |
. . . . . . . . 9
|
192 | 186, 191 | mpbid 222 |
. . . . . . . 8
|
193 | 110, 192 | eqbrtrd 4675 |
. . . . . . 7
|
194 | | 1zzd 11408 |
. . . . . . . . . 10
|
195 | | nnnn0 11299 |
. . . . . . . . . . 11
|
196 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
197 | | nnexpcl 12873 |
. . . . . . . . . . . . . . 15
|
198 | 36, 196, 197 | sylancr 695 |
. . . . . . . . . . . . . 14
|
199 | 198 | nnred 11035 |
. . . . . . . . . . . . 13
|
200 | 38 | adantr 481 |
. . . . . . . . . . . . . 14
|
201 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
202 | 201 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
|
203 | 202 | rspcv 3305 |
. . . . . . . . . . . . . 14
|
204 | 198, 200,
203 | sylc 65 |
. . . . . . . . . . . . 13
|
205 | 199, 204 | remulcld 10070 |
. . . . . . . . . . . 12
|
206 | 58, 205 | eqeltrd 2701 |
. . . . . . . . . . 11
|
207 | 195, 206 | sylan2 491 |
. . . . . . . . . 10
|
208 | 69, 194, 207 | serfre 12830 |
. . . . . . . . 9
|
209 | 208 | ffvelrnda 6359 |
. . . . . . . 8
|
210 | 207 | ralrimiva 2966 |
. . . . . . . . . 10
|
211 | 210 | adantr 481 |
. . . . . . . . 9
|
212 | 81 | eleq1d 2686 |
. . . . . . . . . 10
|
213 | 212 | rspcv 3305 |
. . . . . . . . 9
|
214 | 78, 211, 213 | sylc 65 |
. . . . . . . 8
|
215 | 69, 194, 37 | serfre 12830 |
. . . . . . . . . 10
|
216 | | ffvelrn 6357 |
. . . . . . . . . 10
|
217 | 215, 93, 216 | syl2an 494 |
. . . . . . . . 9
|
218 | | remulcl 10021 |
. . . . . . . . 9
|
219 | 49, 217, 218 | sylancr 695 |
. . . . . . . 8
|
220 | | remulcl 10021 |
. . . . . . . . 9
|
221 | 49, 188, 220 | sylancr 695 |
. . . . . . . 8
|
222 | | le2add 10510 |
. . . . . . . 8
|
223 | 209, 214,
219, 221, 222 | syl22anc 1327 |
. . . . . . 7
|
224 | 193, 223 | mpan2d 710 |
. . . . . 6
|
225 | 119, 69 | syl6eleq 2711 |
. . . . . . . 8
|
226 | | seqp1 12816 |
. . . . . . . 8
|
227 | 225, 226 | syl 17 |
. . . . . . 7
|
228 | | fzfid 12772 |
. . . . . . . . . . 11
|
229 | | elfznn 12370 |
. . . . . . . . . . . 12
|
230 | 37 | recnd 10068 |
. . . . . . . . . . . 12
|
231 | 156, 229,
230 | syl2an 494 |
. . . . . . . . . . 11
|
232 | 146, 133,
228, 231 | fsumsplit 14471 |
. . . . . . . . . 10
|
233 | | eqidd 2623 |
. . . . . . . . . . 11
|
234 | 102, 69 | syl6eleq 2711 |
. . . . . . . . . . 11
|
235 | 233, 234,
231 | fsumser 14461 |
. . . . . . . . . 10
|
236 | | eqidd 2623 |
. . . . . . . . . . . 12
|
237 | | elfznn 12370 |
. . . . . . . . . . . . 13
|
238 | 156, 237,
230 | syl2an 494 |
. . . . . . . . . . . 12
|
239 | 236, 127,
238 | fsumser 14461 |
. . . . . . . . . . 11
|
240 | 239 | oveq1d 6665 |
. . . . . . . . . 10
|
241 | 232, 235,
240 | 3eqtr3d 2664 |
. . . . . . . . 9
|
242 | 241 | oveq2d 6666 |
. . . . . . . 8
|
243 | 217 | recnd 10068 |
. . . . . . . . 9
|
244 | 188 | recnd 10068 |
. . . . . . . . 9
|
245 | 100, 243,
244 | adddid 10064 |
. . . . . . . 8
|
246 | 242, 245 | eqtrd 2656 |
. . . . . . 7
|
247 | 227, 246 | breq12d 4666 |
. . . . . 6
|
248 | 224, 247 | sylibrd 249 |
. . . . 5
|
249 | 248 | expcom 451 |
. . . 4
|
250 | 249 | a2d 29 |
. . 3
|
251 | 10, 16, 22, 28, 76, 250 | nnind 11038 |
. 2
|
252 | 251 | impcom 446 |
1
|