Step | Hyp | Ref
| Expression |
1 | | nn0uz 9521 |
. 2
|
2 | | 0zd 9224 |
. 2
|
3 | | seqex 10403 |
. . 3
|
4 | 3 | a1i 9 |
. 2
|
5 | | mertens.6 |
. . . . 5
|
6 | | 0zd 9224 |
. . . . . . 7
|
7 | | nn0z 9232 |
. . . . . . . 8
|
8 | 7 | adantl 275 |
. . . . . . 7
|
9 | 6, 8 | fzfigd 10387 |
. . . . . 6
|
10 | | simpl 108 |
. . . . . . . 8
|
11 | | elfznn0 10070 |
. . . . . . . 8
|
12 | | mertens.3 |
. . . . . . . 8
|
13 | 10, 11, 12 | syl2an 287 |
. . . . . . 7
|
14 | | fveq2 5496 |
. . . . . . . . 9
|
15 | 14 | eleq1d 2239 |
. . . . . . . 8
|
16 | | mertens.4 |
. . . . . . . . . . . 12
|
17 | | mertens.5 |
. . . . . . . . . . . 12
|
18 | 16, 17 | eqeltrd 2247 |
. . . . . . . . . . 11
|
19 | 18 | ralrimiva 2543 |
. . . . . . . . . 10
|
20 | | fveq2 5496 |
. . . . . . . . . . . 12
|
21 | 20 | eleq1d 2239 |
. . . . . . . . . . 11
|
22 | 21 | cbvralv 2696 |
. . . . . . . . . 10
|
23 | 19, 22 | sylib 121 |
. . . . . . . . 9
|
24 | 23 | ad2antrr 485 |
. . . . . . . 8
|
25 | | fznn0sub 10013 |
. . . . . . . . 9
|
26 | 25 | adantl 275 |
. . . . . . . 8
|
27 | 15, 24, 26 | rspcdva 2839 |
. . . . . . 7
|
28 | 13, 27 | mulcld 7940 |
. . . . . 6
|
29 | 9, 28 | fsumcl 11363 |
. . . . 5
|
30 | 5, 29 | eqeltrd 2247 |
. . . 4
|
31 | 1, 2, 30 | serf 10430 |
. . 3
|
32 | 31 | ffvelrnda 5631 |
. 2
|
33 | | mertens.1 |
. . . . . 6
|
34 | 33 | adantlr 474 |
. . . . 5
|
35 | | mertens.2 |
. . . . . 6
|
36 | 35 | adantlr 474 |
. . . . 5
|
37 | 12 | adantlr 474 |
. . . . 5
|
38 | 16 | adantlr 474 |
. . . . 5
|
39 | 17 | adantlr 474 |
. . . . 5
|
40 | 5 | adantlr 474 |
. . . . 5
|
41 | | mertens.7 |
. . . . . 6
|
42 | 41 | adantr 274 |
. . . . 5
|
43 | | mertens.8 |
. . . . . 6
|
44 | 43 | adantr 274 |
. . . . 5
|
45 | | simpr 109 |
. . . . 5
|
46 | | fveq2 5496 |
. . . . . . . . . . . 12
|
47 | 46 | cbvsumv 11324 |
. . . . . . . . . . 11
|
48 | | fvoveq1 5876 |
. . . . . . . . . . . 12
|
49 | 48 | sumeq1d 11329 |
. . . . . . . . . . 11
|
50 | 47, 49 | eqtrid 2215 |
. . . . . . . . . 10
|
51 | 50 | fveq2d 5500 |
. . . . . . . . 9
|
52 | 51 | eqeq2d 2182 |
. . . . . . . 8
|
53 | 52 | cbvrexv 2697 |
. . . . . . 7
|
54 | | eqeq1 2177 |
. . . . . . . 8
|
55 | 54 | rexbidv 2471 |
. . . . . . 7
|
56 | 53, 55 | syl5bb 191 |
. . . . . 6
|
57 | 56 | cbvabv 2295 |
. . . . 5
|
58 | | fveq2 5496 |
. . . . . . . . . . . 12
|
59 | 58 | cbvsumv 11324 |
. . . . . . . . . . 11
|
60 | 59 | oveq1i 5863 |
. . . . . . . . . 10
|
61 | 60 | oveq2i 5864 |
. . . . . . . . 9
|
62 | 61 | breq2i 3997 |
. . . . . . . 8
|
63 | | fveq2 5496 |
. . . . . . . . . . . 12
|
64 | 63 | cbvsumv 11324 |
. . . . . . . . . . 11
|
65 | | fvoveq1 5876 |
. . . . . . . . . . . 12
|
66 | 65 | sumeq1d 11329 |
. . . . . . . . . . 11
|
67 | 64, 66 | eqtrid 2215 |
. . . . . . . . . 10
|
68 | 67 | fveq2d 5500 |
. . . . . . . . 9
|
69 | 68 | breq1d 3999 |
. . . . . . . 8
|
70 | 62, 69 | syl5bb 191 |
. . . . . . 7
|
71 | 70 | cbvralv 2696 |
. . . . . 6
|
72 | 71 | anbi2i 454 |
. . . . 5
|
73 | 34, 36, 37, 38, 39, 40, 42, 44, 45, 57, 72 | mertenslem2 11499 |
. . . 4
|
74 | | eluznn0 9558 |
. . . . . . . . 9
|
75 | | 0zd 9224 |
. . . . . . . . . . . . . 14
|
76 | | nn0z 9232 |
. . . . . . . . . . . . . . 15
|
77 | 76 | adantl 275 |
. . . . . . . . . . . . . 14
|
78 | 75, 77 | fzfigd 10387 |
. . . . . . . . . . . . 13
|
79 | | simpll 524 |
. . . . . . . . . . . . . 14
|
80 | | elfznn0 10070 |
. . . . . . . . . . . . . . 15
|
81 | 80 | adantl 275 |
. . . . . . . . . . . . . 14
|
82 | 1, 2, 16, 17, 43 | isumcl 11388 |
. . . . . . . . . . . . . . . 16
|
83 | 82 | adantr 274 |
. . . . . . . . . . . . . . 15
|
84 | 33, 12 | eqeltrd 2247 |
. . . . . . . . . . . . . . 15
|
85 | 83, 84 | mulcld 7940 |
. . . . . . . . . . . . . 14
|
86 | 79, 81, 85 | syl2anc 409 |
. . . . . . . . . . . . 13
|
87 | | 0zd 9224 |
. . . . . . . . . . . . . . 15
|
88 | 77 | adantr 274 |
. . . . . . . . . . . . . . . 16
|
89 | 81 | nn0zd 9332 |
. . . . . . . . . . . . . . . 16
|
90 | 88, 89 | zsubcld 9339 |
. . . . . . . . . . . . . . 15
|
91 | 87, 90 | fzfigd 10387 |
. . . . . . . . . . . . . 14
|
92 | | simplll 528 |
. . . . . . . . . . . . . . . 16
|
93 | 80 | ad2antlr 486 |
. . . . . . . . . . . . . . . 16
|
94 | 92, 93, 12 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
95 | | elfznn0 10070 |
. . . . . . . . . . . . . . . . 17
|
96 | 95 | adantl 275 |
. . . . . . . . . . . . . . . 16
|
97 | 92, 96, 18 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
98 | 94, 97 | mulcld 7940 |
. . . . . . . . . . . . . 14
|
99 | 91, 98 | fsumcl 11363 |
. . . . . . . . . . . . 13
|
100 | 78, 86, 99 | fsumsub 11415 |
. . . . . . . . . . . 12
|
101 | 79, 81, 12 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
102 | 82 | ad2antrr 485 |
. . . . . . . . . . . . . . 15
|
103 | 91, 97 | fsumcl 11363 |
. . . . . . . . . . . . . . 15
|
104 | 101, 102,
103 | subdid 8333 |
. . . . . . . . . . . . . 14
|
105 | | eqid 2170 |
. . . . . . . . . . . . . . . . . . 19
|
106 | | fznn0sub 10013 |
. . . . . . . . . . . . . . . . . . . . 21
|
107 | 106 | adantl 275 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | | peano2nn0 9175 |
. . . . . . . . . . . . . . . . . . . 20
|
109 | 107, 108 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
|
110 | 79, 16 | sylan 281 |
. . . . . . . . . . . . . . . . . . 19
|
111 | 79, 17 | sylan 281 |
. . . . . . . . . . . . . . . . . . 19
|
112 | 43 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . 19
|
113 | 1, 105, 109, 110, 111, 112 | isumsplit 11454 |
. . . . . . . . . . . . . . . . . 18
|
114 | 107 | nn0cnd 9190 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
115 | | ax-1cn 7867 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
116 | | pncan 8125 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
117 | 114, 115,
116 | sylancl 411 |
. . . . . . . . . . . . . . . . . . . . . 22
|
118 | 117 | oveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . 21
|
119 | 118 | sumeq1d 11329 |
. . . . . . . . . . . . . . . . . . . 20
|
120 | 92, 96, 16 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . 21
|
121 | 120 | sumeq2dv 11331 |
. . . . . . . . . . . . . . . . . . . 20
|
122 | 119, 121 | eqtr4d 2206 |
. . . . . . . . . . . . . . . . . . 19
|
123 | 122 | oveq1d 5868 |
. . . . . . . . . . . . . . . . . 18
|
124 | 113, 123 | eqtrd 2203 |
. . . . . . . . . . . . . . . . 17
|
125 | 124 | oveq1d 5868 |
. . . . . . . . . . . . . . . 16
|
126 | 109 | nn0zd 9332 |
. . . . . . . . . . . . . . . . . 18
|
127 | | simplll 528 |
. . . . . . . . . . . . . . . . . . 19
|
128 | | eluznn0 9558 |
. . . . . . . . . . . . . . . . . . . 20
|
129 | 109, 128 | sylan 281 |
. . . . . . . . . . . . . . . . . . 19
|
130 | 127, 129,
16 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
|
131 | 127, 129,
17 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
|
132 | 110, 111 | eqeltrd 2247 |
. . . . . . . . . . . . . . . . . . . 20
|
133 | 1, 109, 132 | iserex 11302 |
. . . . . . . . . . . . . . . . . . 19
|
134 | 112, 133 | mpbid 146 |
. . . . . . . . . . . . . . . . . 18
|
135 | 105, 126,
130, 131, 134 | isumcl 11388 |
. . . . . . . . . . . . . . . . 17
|
136 | 103, 135 | pncan2d 8232 |
. . . . . . . . . . . . . . . 16
|
137 | 125, 136 | eqtrd 2203 |
. . . . . . . . . . . . . . 15
|
138 | 137 | oveq2d 5869 |
. . . . . . . . . . . . . 14
|
139 | 12, 83 | mulcomd 7941 |
. . . . . . . . . . . . . . . . 17
|
140 | 33 | oveq2d 5869 |
. . . . . . . . . . . . . . . . 17
|
141 | 139, 140 | eqtr4d 2206 |
. . . . . . . . . . . . . . . 16
|
142 | 79, 81, 141 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
143 | 91, 101, 97 | fsummulc2 11411 |
. . . . . . . . . . . . . . 15
|
144 | 142, 143 | oveq12d 5871 |
. . . . . . . . . . . . . 14
|
145 | 104, 138,
144 | 3eqtr3rd 2212 |
. . . . . . . . . . . . 13
|
146 | 145 | sumeq2dv 11331 |
. . . . . . . . . . . 12
|
147 | | elnn0uz 9524 |
. . . . . . . . . . . . . . . 16
|
148 | 147 | biimpri 132 |
. . . . . . . . . . . . . . 15
|
149 | 82 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
|
150 | 148, 84 | sylan2 284 |
. . . . . . . . . . . . . . . . 17
|
151 | 150 | adantlr 474 |
. . . . . . . . . . . . . . . 16
|
152 | 149, 151 | mulcld 7940 |
. . . . . . . . . . . . . . 15
|
153 | | fveq2 5496 |
. . . . . . . . . . . . . . . . 17
|
154 | 153 | oveq2d 5869 |
. . . . . . . . . . . . . . . 16
|
155 | | eqid 2170 |
. . . . . . . . . . . . . . . 16
|
156 | 154, 155 | fvmptg 5572 |
. . . . . . . . . . . . . . 15
|
157 | 148, 152,
156 | syl2an2 589 |
. . . . . . . . . . . . . 14
|
158 | | simpr 109 |
. . . . . . . . . . . . . . 15
|
159 | 158, 1 | eleqtrdi 2263 |
. . . . . . . . . . . . . 14
|
160 | 157, 159,
152 | fsum3ser 11360 |
. . . . . . . . . . . . 13
|
161 | | fveq2 5496 |
. . . . . . . . . . . . . . . 16
|
162 | 161 | oveq2d 5869 |
. . . . . . . . . . . . . . 15
|
163 | | fveq2 5496 |
. . . . . . . . . . . . . . . 16
|
164 | 163 | oveq2d 5869 |
. . . . . . . . . . . . . . 15
|
165 | 98 | anasss 397 |
. . . . . . . . . . . . . . 15
|
166 | 162, 164,
165, 77 | fisum0diag2 11410 |
. . . . . . . . . . . . . 14
|
167 | | simpll 524 |
. . . . . . . . . . . . . . . 16
|
168 | | elnn0uz 9524 |
. . . . . . . . . . . . . . . . . 18
|
169 | 168 | biimpri 132 |
. . . . . . . . . . . . . . . . 17
|
170 | 169 | adantl 275 |
. . . . . . . . . . . . . . . 16
|
171 | 167, 170,
5 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
172 | 167, 170,
29 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
173 | 171, 159,
172 | fsum3ser 11360 |
. . . . . . . . . . . . . 14
|
174 | 166, 173 | eqtrd 2203 |
. . . . . . . . . . . . 13
|
175 | 160, 174 | oveq12d 5871 |
. . . . . . . . . . . 12
|
176 | 100, 146,
175 | 3eqtr3rd 2212 |
. . . . . . . . . . 11
|
177 | 176 | fveq2d 5500 |
. . . . . . . . . 10
|
178 | 177 | breq1d 3999 |
. . . . . . . . 9
|
179 | 74, 178 | sylan2 284 |
. . . . . . . 8
|
180 | 179 | anassrs 398 |
. . . . . . 7
|
181 | 180 | ralbidva 2466 |
. . . . . 6
|
182 | 181 | rexbidva 2467 |
. . . . 5
|
183 | 182 | adantr 274 |
. . . 4
|
184 | 73, 183 | mpbird 166 |
. . 3
|
185 | 184 | ralrimiva 2543 |
. 2
|
186 | | mertens.f |
. . . . 5
|
187 | 1, 2, 33, 12, 186 | isumclim2 11385 |
. . . 4
|
188 | 84 | ralrimiva 2543 |
. . . . 5
|
189 | | fveq2 5496 |
. . . . . . 7
|
190 | 189 | eleq1d 2239 |
. . . . . 6
|
191 | 190 | rspccva 2833 |
. . . . 5
|
192 | 188, 191 | sylan 281 |
. . . 4
|
193 | 82 | adantr 274 |
. . . . . 6
|
194 | 193, 192 | mulcld 7940 |
. . . . 5
|
195 | | fveq2 5496 |
. . . . . . 7
|
196 | 195 | oveq2d 5869 |
. . . . . 6
|
197 | 196, 155 | fvmptg 5572 |
. . . . 5
|
198 | 158, 194,
197 | syl2anc 409 |
. . . 4
|
199 | 1, 2, 82, 187, 192, 198 | isermulc2 11303 |
. . 3
|
200 | 1, 2, 33, 12, 186 | isumcl 11388 |
. . . 4
|
201 | 82, 200 | mulcomd 7941 |
. . 3
|
202 | 199, 201 | breqtrd 4015 |
. 2
|
203 | 1, 2, 4, 32, 185, 202 | 2clim 11264 |
1
|