Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . . 6
|
2 | | rpcn 11841 |
. . . . . . 7
|
3 | 2 | adantl 482 |
. . . . . 6
|
4 | | rpdivcl 11856 |
. . . . . . . . . . 11
|
5 | 4 | adantlr 751 |
. . . . . . . . . 10
|
6 | 5 | relogcld 24369 |
. . . . . . . . 9
|
7 | | elfznn0 12433 |
. . . . . . . . 9
|
8 | | reexpcl 12877 |
. . . . . . . . 9
|
9 | 6, 7, 8 | syl2an 494 |
. . . . . . . 8
|
10 | 7 | adantl 482 |
. . . . . . . . 9
|
11 | | faccl 13070 |
. . . . . . . . 9
|
12 | 10, 11 | syl 17 |
. . . . . . . 8
|
13 | 9, 12 | nndivred 11069 |
. . . . . . 7
|
14 | 13 | recnd 10068 |
. . . . . 6
|
15 | 1, 3, 14 | fsummulc2 14516 |
. . . . 5
|
16 | | simplr 792 |
. . . . . . 7
|
17 | | nn0uz 11722 |
. . . . . . 7
|
18 | 16, 17 | syl6eleq 2711 |
. . . . . 6
|
19 | 3 | adantr 481 |
. . . . . . 7
|
20 | 19, 14 | mulcld 10060 |
. . . . . 6
|
21 | | oveq2 6658 |
. . . . . . . 8
|
22 | | fveq2 6191 |
. . . . . . . . 9
|
23 | | fac0 13063 |
. . . . . . . . 9
|
24 | 22, 23 | syl6eq 2672 |
. . . . . . . 8
|
25 | 21, 24 | oveq12d 6668 |
. . . . . . 7
|
26 | 25 | oveq2d 6666 |
. . . . . 6
|
27 | 18, 20, 26 | fsum1p 14482 |
. . . . 5
|
28 | 6 | recnd 10068 |
. . . . . . . . . . 11
|
29 | 28 | exp0d 13002 |
. . . . . . . . . 10
|
30 | 29 | oveq1d 6665 |
. . . . . . . . 9
|
31 | | 1div1e1 10717 |
. . . . . . . . 9
|
32 | 30, 31 | syl6eq 2672 |
. . . . . . . 8
|
33 | 32 | oveq2d 6666 |
. . . . . . 7
|
34 | 3 | mulid1d 10057 |
. . . . . . 7
|
35 | 33, 34 | eqtrd 2656 |
. . . . . 6
|
36 | | 1zzd 11408 |
. . . . . . . 8
|
37 | | nn0z 11400 |
. . . . . . . . 9
|
38 | 37 | ad2antlr 763 |
. . . . . . . 8
|
39 | | 0p1e1 11132 |
. . . . . . . . . . . 12
|
40 | 39 | oveq1i 6660 |
. . . . . . . . . . 11
|
41 | | 0z 11388 |
. . . . . . . . . . . 12
|
42 | | fzp1ss 12392 |
. . . . . . . . . . . 12
|
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . 11
|
44 | 40, 43 | eqsstr3i 3636 |
. . . . . . . . . 10
|
45 | 44 | sseli 3599 |
. . . . . . . . 9
|
46 | 45, 20 | sylan2 491 |
. . . . . . . 8
|
47 | | oveq2 6658 |
. . . . . . . . . 10
|
48 | | fveq2 6191 |
. . . . . . . . . 10
|
49 | 47, 48 | oveq12d 6668 |
. . . . . . . . 9
|
50 | 49 | oveq2d 6666 |
. . . . . . . 8
|
51 | 36, 36, 38, 46, 50 | fsumshftm 14513 |
. . . . . . 7
|
52 | 40 | sumeq1i 14428 |
. . . . . . . 8
|
53 | 52 | a1i 11 |
. . . . . . 7
|
54 | | 1m1e0 11089 |
. . . . . . . . . 10
|
55 | 54 | oveq1i 6660 |
. . . . . . . . 9
..^ ..^ |
56 | | fzoval 12471 |
. . . . . . . . . 10
..^
|
57 | 38, 56 | syl 17 |
. . . . . . . . 9
..^ |
58 | 55, 57 | syl5eqr 2670 |
. . . . . . . 8
..^ |
59 | 58 | sumeq1d 14431 |
. . . . . . 7
..^ |
60 | 51, 53, 59 | 3eqtr4d 2666 |
. . . . . 6
..^ |
61 | 35, 60 | oveq12d 6668 |
. . . . 5
..^ |
62 | 15, 27, 61 | 3eqtrd 2660 |
. . . 4
..^ |
63 | 62 | mpteq2dva 4744 |
. . 3
..^ |
64 | 63 | oveq2d 6666 |
. 2
..^ |
65 | | reelprrecn 10028 |
. . . 4
|
66 | 65 | a1i 11 |
. . 3
|
67 | | 1cnd 10056 |
. . 3
|
68 | | recn 10026 |
. . . . 5
|
69 | 68 | adantl 482 |
. . . 4
|
70 | | 1cnd 10056 |
. . . 4
|
71 | 66 | dvmptid 23720 |
. . . 4
|
72 | | rpssre 11843 |
. . . . 5
|
73 | 72 | a1i 11 |
. . . 4
|
74 | | eqid 2622 |
. . . . 5
ℂfld ℂfld |
75 | 74 | tgioo2 22606 |
. . . 4
ℂfld
↾t |
76 | | ioorp 12251 |
. . . . . 6
|
77 | | iooretop 22569 |
. . . . . 6
|
78 | 76, 77 | eqeltrri 2698 |
. . . . 5
|
79 | 78 | a1i 11 |
. . . 4
|
80 | 66, 69, 70, 71, 73, 75, 74, 79 | dvmptres 23726 |
. . 3
|
81 | | fzofi 12773 |
. . . . 5
..^ |
82 | 81 | a1i 11 |
. . . 4
..^ |
83 | 3 | adantr 481 |
. . . . 5
..^ |
84 | | elfzonn0 12512 |
. . . . . . . . 9
..^
|
85 | | peano2nn0 11333 |
. . . . . . . . 9
|
86 | 84, 85 | syl 17 |
. . . . . . . 8
..^
|
87 | | reexpcl 12877 |
. . . . . . . 8
|
88 | 6, 86, 87 | syl2an 494 |
. . . . . . 7
..^ |
89 | 86 | adantl 482 |
. . . . . . . 8
..^ |
90 | | faccl 13070 |
. . . . . . . 8
|
91 | 89, 90 | syl 17 |
. . . . . . 7
..^ |
92 | 88, 91 | nndivred 11069 |
. . . . . 6
..^ |
93 | 92 | recnd 10068 |
. . . . 5
..^ |
94 | 83, 93 | mulcld 10060 |
. . . 4
..^ |
95 | 82, 94 | fsumcl 14464 |
. . 3
..^ |
96 | 6, 16 | reexpcld 13025 |
. . . . . 6
|
97 | | faccl 13070 |
. . . . . . 7
|
98 | 97 | ad2antlr 763 |
. . . . . 6
|
99 | 96, 98 | nndivred 11069 |
. . . . 5
|
100 | 99 | recnd 10068 |
. . . 4
|
101 | | ax-1cn 9994 |
. . . 4
|
102 | | subcl 10280 |
. . . 4
|
103 | 100, 101,
102 | sylancl 694 |
. . 3
|
104 | 81 | a1i 11 |
. . . . 5
..^ |
105 | 94 | an32s 846 |
. . . . . 6
..^ |
106 | 105 | 3impa 1259 |
. . . . 5
..^
|
107 | | reexpcl 12877 |
. . . . . . . . . . 11
|
108 | 6, 84, 107 | syl2an 494 |
. . . . . . . . . 10
..^ |
109 | 84 | adantl 482 |
. . . . . . . . . . 11
..^ |
110 | | faccl 13070 |
. . . . . . . . . . 11
|
111 | 109, 110 | syl 17 |
. . . . . . . . . 10
..^ |
112 | 108, 111 | nndivred 11069 |
. . . . . . . . 9
..^ |
113 | 112 | recnd 10068 |
. . . . . . . 8
..^ |
114 | 93, 113 | subcld 10392 |
. . . . . . 7
..^ |
115 | 114 | an32s 846 |
. . . . . 6
..^ |
116 | 115 | 3impa 1259 |
. . . . 5
..^
|
117 | 65 | a1i 11 |
. . . . . . 7
..^
|
118 | 2 | adantl 482 |
. . . . . . 7
..^ |
119 | | 1cnd 10056 |
. . . . . . 7
..^ |
120 | 80 | adantr 481 |
. . . . . . 7
..^
|
121 | 93 | an32s 846 |
. . . . . . 7
..^ |
122 | | negex 10279 |
. . . . . . . 8
|
123 | 122 | a1i 11 |
. . . . . . 7
..^ |
124 | | cnelprrecn 10029 |
. . . . . . . . . 10
|
125 | 124 | a1i 11 |
. . . . . . . . 9
..^
|
126 | 28 | adantlr 751 |
. . . . . . . . 9
..^ |
127 | | negex 10279 |
. . . . . . . . . 10
|
128 | 127 | a1i 11 |
. . . . . . . . 9
..^ |
129 | | id 22 |
. . . . . . . . . . 11
|
130 | 84 | adantl 482 |
. . . . . . . . . . . 12
..^ |
131 | 130, 85 | syl 17 |
. . . . . . . . . . 11
..^ |
132 | | expcl 12878 |
. . . . . . . . . . 11
|
133 | 129, 131,
132 | syl2anr 495 |
. . . . . . . . . 10
..^ |
134 | 131, 90 | syl 17 |
. . . . . . . . . . . 12
..^ |
135 | 134 | nncnd 11036 |
. . . . . . . . . . 11
..^ |
136 | 135 | adantr 481 |
. . . . . . . . . 10
..^ |
137 | 134 | nnne0d 11065 |
. . . . . . . . . . 11
..^ |
138 | 137 | adantr 481 |
. . . . . . . . . 10
..^ |
139 | 133, 136,
138 | divcld 10801 |
. . . . . . . . 9
..^ |
140 | | expcl 12878 |
. . . . . . . . . . 11
|
141 | 129, 130,
140 | syl2anr 495 |
. . . . . . . . . 10
..^ |
142 | 130, 110 | syl 17 |
. . . . . . . . . . . 12
..^ |
143 | 142 | nncnd 11036 |
. . . . . . . . . . 11
..^ |
144 | 143 | adantr 481 |
. . . . . . . . . 10
..^ |
145 | 130 | adantr 481 |
. . . . . . . . . . . 12
..^ |
146 | 145, 110 | syl 17 |
. . . . . . . . . . 11
..^ |
147 | 146 | nnne0d 11065 |
. . . . . . . . . 10
..^ |
148 | 141, 144,
147 | divcld 10801 |
. . . . . . . . 9
..^ |
149 | | simplll 798 |
. . . . . . . . . . . . . 14
..^ |
150 | | simpr 477 |
. . . . . . . . . . . . . 14
..^ |
151 | 149, 150 | relogdivd 24372 |
. . . . . . . . . . . . 13
..^ |
152 | 151 | mpteq2dva 4744 |
. . . . . . . . . . . 12
..^
|
153 | 152 | oveq2d 6666 |
. . . . . . . . . . 11
..^
|
154 | | relogcl 24322 |
. . . . . . . . . . . . . . 15
|
155 | 154 | ad2antrr 762 |
. . . . . . . . . . . . . 14
..^ |
156 | 155 | recnd 10068 |
. . . . . . . . . . . . 13
..^ |
157 | 156 | adantr 481 |
. . . . . . . . . . . 12
..^ |
158 | | 0cnd 10033 |
. . . . . . . . . . . 12
..^ |
159 | 156 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
160 | | 0cnd 10033 |
. . . . . . . . . . . . 13
..^ |
161 | 117, 156 | dvmptc 23721 |
. . . . . . . . . . . . 13
..^
|
162 | 72 | a1i 11 |
. . . . . . . . . . . . 13
..^
|
163 | 78 | a1i 11 |
. . . . . . . . . . . . 13
..^ |
164 | 117, 159,
160, 161, 162, 75, 74, 163 | dvmptres 23726 |
. . . . . . . . . . . 12
..^
|
165 | 150 | relogcld 24369 |
. . . . . . . . . . . . 13
..^ |
166 | 165 | recnd 10068 |
. . . . . . . . . . . 12
..^ |
167 | 150 | rpreccld 11882 |
. . . . . . . . . . . 12
..^ |
168 | | dvrelog 24383 |
. . . . . . . . . . . . 13
|
169 | | relogf1o 24313 |
. . . . . . . . . . . . . . . . 17
|
170 | | f1of 6137 |
. . . . . . . . . . . . . . . . 17
|
171 | 169, 170 | mp1i 13 |
. . . . . . . . . . . . . . . 16
..^ |
172 | 171 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
..^ |
173 | | fvres 6207 |
. . . . . . . . . . . . . . . 16
|
174 | 173 | mpteq2ia 4740 |
. . . . . . . . . . . . . . 15
|
175 | 172, 174 | syl6eq 2672 |
. . . . . . . . . . . . . 14
..^ |
176 | 175 | oveq2d 6666 |
. . . . . . . . . . . . 13
..^
|
177 | 168, 176 | syl5reqr 2671 |
. . . . . . . . . . . 12
..^
|
178 | 117, 157,
158, 164, 166, 167, 177 | dvmptsub 23730 |
. . . . . . . . . . 11
..^
|
179 | 153, 178 | eqtrd 2656 |
. . . . . . . . . 10
..^
|
180 | | df-neg 10269 |
. . . . . . . . . . 11
|
181 | 180 | mpteq2i 4741 |
. . . . . . . . . 10
|
182 | 179, 181 | syl6eqr 2674 |
. . . . . . . . 9
..^
|
183 | | ovexd 6680 |
. . . . . . . . . . 11
..^ |
184 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
|
185 | 130, 184 | syl 17 |
. . . . . . . . . . . 12
..^ |
186 | | dvexp 23716 |
. . . . . . . . . . . 12
|
187 | 185, 186 | syl 17 |
. . . . . . . . . . 11
..^ |
188 | 125, 133,
183, 187, 135, 137 | dvmptdivc 23728 |
. . . . . . . . . 10
..^ |
189 | 130 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
..^ |
190 | 189 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^ |
191 | | pncan 10287 |
. . . . . . . . . . . . . . . 16
|
192 | 190, 101,
191 | sylancl 694 |
. . . . . . . . . . . . . . 15
..^ |
193 | 192 | oveq2d 6666 |
. . . . . . . . . . . . . 14
..^ |
194 | 193 | oveq2d 6666 |
. . . . . . . . . . . . 13
..^ |
195 | | facp1 13065 |
. . . . . . . . . . . . . . 15
|
196 | 145, 195 | syl 17 |
. . . . . . . . . . . . . 14
..^ |
197 | | peano2cn 10208 |
. . . . . . . . . . . . . . . 16
|
198 | 190, 197 | syl 17 |
. . . . . . . . . . . . . . 15
..^ |
199 | 144, 198 | mulcomd 10061 |
. . . . . . . . . . . . . 14
..^ |
200 | 196, 199 | eqtrd 2656 |
. . . . . . . . . . . . 13
..^ |
201 | 194, 200 | oveq12d 6668 |
. . . . . . . . . . . 12
..^ |
202 | 185 | nnne0d 11065 |
. . . . . . . . . . . . . 14
..^ |
203 | 202 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
204 | 141, 144,
198, 147, 203 | divcan5d 10827 |
. . . . . . . . . . . 12
..^ |
205 | 201, 204 | eqtrd 2656 |
. . . . . . . . . . 11
..^ |
206 | 205 | mpteq2dva 4744 |
. . . . . . . . . 10
..^ |
207 | 188, 206 | eqtrd 2656 |
. . . . . . . . 9
..^ |
208 | | oveq1 6657 |
. . . . . . . . . 10
|
209 | 208 | oveq1d 6665 |
. . . . . . . . 9
|
210 | | oveq1 6657 |
. . . . . . . . . 10
|
211 | 210 | oveq1d 6665 |
. . . . . . . . 9
|
212 | 117, 125,
126, 128, 139, 148, 182, 207, 209, 211 | dvmptco 23735 |
. . . . . . . 8
..^
|
213 | 113 | an32s 846 |
. . . . . . . . . . 11
..^ |
214 | 167 | rpcnd 11874 |
. . . . . . . . . . 11
..^ |
215 | 213, 214 | mulneg2d 10484 |
. . . . . . . . . 10
..^ |
216 | | rpne0 11848 |
. . . . . . . . . . . . 13
|
217 | 216 | adantl 482 |
. . . . . . . . . . . 12
..^ |
218 | 213, 118,
217 | divrecd 10804 |
. . . . . . . . . . 11
..^ |
219 | 218 | negeqd 10275 |
. . . . . . . . . 10
..^ |
220 | 215, 219 | eqtr4d 2659 |
. . . . . . . . 9
..^ |
221 | 220 | mpteq2dva 4744 |
. . . . . . . 8
..^ |
222 | 212, 221 | eqtrd 2656 |
. . . . . . 7
..^
|
223 | 117, 118,
119, 120, 121, 123, 222 | dvmptmul 23724 |
. . . . . 6
..^
|
224 | 93 | mulid2d 10058 |
. . . . . . . . . 10
..^ |
225 | | simplr 792 |
. . . . . . . . . . . . . 14
..^ |
226 | 112, 225 | rerpdivcld 11903 |
. . . . . . . . . . . . 13
..^ |
227 | 226 | recnd 10068 |
. . . . . . . . . . . 12
..^ |
228 | 227, 83 | mulneg1d 10483 |
. . . . . . . . . . 11
..^ |
229 | 217 | an32s 846 |
. . . . . . . . . . . . 13
..^ |
230 | 113, 83, 229 | divcan1d 10802 |
. . . . . . . . . . . 12
..^ |
231 | 230 | negeqd 10275 |
. . . . . . . . . . 11
..^ |
232 | 228, 231 | eqtrd 2656 |
. . . . . . . . . 10
..^ |
233 | 224, 232 | oveq12d 6668 |
. . . . . . . . 9
..^ |
234 | 93, 113 | negsubd 10398 |
. . . . . . . . 9
..^ |
235 | 233, 234 | eqtrd 2656 |
. . . . . . . 8
..^ |
236 | 235 | an32s 846 |
. . . . . . 7
..^ |
237 | 236 | mpteq2dva 4744 |
. . . . . 6
..^ |
238 | 223, 237 | eqtrd 2656 |
. . . . 5
..^
|
239 | 75, 74, 66, 79, 104, 106, 116, 238 | dvmptfsum 23738 |
. . . 4
..^
..^ |
240 | | oveq2 6658 |
. . . . . . . 8
|
241 | | fveq2 6191 |
. . . . . . . 8
|
242 | 240, 241 | oveq12d 6668 |
. . . . . . 7
|
243 | | oveq2 6658 |
. . . . . . . 8
|
244 | | fveq2 6191 |
. . . . . . . 8
|
245 | 243, 244 | oveq12d 6668 |
. . . . . . 7
|
246 | 242, 49, 25, 245, 18, 14 | telfsumo2 14535 |
. . . . . 6
..^ |
247 | 32 | oveq2d 6666 |
. . . . . 6
|
248 | 246, 247 | eqtrd 2656 |
. . . . 5
..^ |
249 | 248 | mpteq2dva 4744 |
. . . 4
..^ |
250 | 239, 249 | eqtrd 2656 |
. . 3
..^
|
251 | 66, 3, 67, 80, 95, 103, 250 | dvmptadd 23723 |
. 2
..^ |
252 | | pncan3 10289 |
. . . 4
|
253 | 101, 100,
252 | sylancr 695 |
. . 3
|
254 | 253 | mpteq2dva 4744 |
. 2
|
255 | 64, 251, 254 | 3eqtrd 2660 |
1
|