Proof of Theorem mertenslemi1
Step | Hyp | Ref
| Expression |
1 | | mertens.i12 |
. . . . . . 7
                  
      |
2 | 1 | simpld 112 |
. . . . . 6
   |
3 | | mertens.11 |
. . . . . 6
                                      |
4 | 2, 3 | sylib 122 |
. . . . 5
                            
         |
5 | 4 | simpld 112 |
. . . 4
   |
6 | 5 | nnnn0d 9205 |
. . 3
   |
7 | 1 | simprd 114 |
. . . 4
                       |
8 | 7 | simpld 112 |
. . 3
   |
9 | 6, 8 | nn0addcld 9209 |
. 2
     |
10 | | 0zd 9241 |
. . . . . . 7
 
      
  |
11 | | eluzelz 9513 |
. . . . . . . 8
      
  |
12 | 11 | adantl 277 |
. . . . . . 7
 
      
  |
13 | 10, 12 | fzfigd 10404 |
. . . . . 6
 
      
      |
14 | | simpl 109 |
. . . . . . . 8
 
      
  |
15 | | elfznn0 10087 |
. . . . . . . 8
       |
16 | | mertens.3 |
. . . . . . . 8
 

  |
17 | 14, 15, 16 | syl2an 289 |
. . . . . . 7
                 |
18 | | eqid 2177 |
. . . . . . . 8
                 |
19 | | fznn0sub 10030 |
. . . . . . . . . . 11
         |
20 | 19 | adantl 277 |
. . . . . . . . . 10
                   |
21 | | peano2nn0 9192 |
. . . . . . . . . 10
  
      |
22 | 20, 21 | syl 14 |
. . . . . . . . 9
                     |
23 | 22 | nn0zd 9349 |
. . . . . . . 8
                     |
24 | | simplll 533 |
. . . . . . . . 9
   
      
                |
25 | | eluznn0 9575 |
. . . . . . . . . 10
     
           |
26 | 22, 25 | sylan 283 |
. . . . . . . . 9
   
      
                |
27 | | mertens.4 |
. . . . . . . . 9
 

      |
28 | 24, 26, 27 | syl2anc 411 |
. . . . . . . 8
   
      
                    |
29 | | mertens.5 |
. . . . . . . . 9
 

  |
30 | 24, 26, 29 | syl2anc 411 |
. . . . . . . 8
   
      
                |
31 | | mertens.8 |
. . . . . . . . . 10
     |
32 | 31 | ad2antrr 488 |
. . . . . . . . 9
                   |
33 | | nn0uz 9538 |
. . . . . . . . . 10
     |
34 | | simpll 527 |
. . . . . . . . . . 11
                 |
35 | 27, 29 | eqeltrd 2254 |
. . . . . . . . . . 11
 

      |
36 | 34, 35 | sylan 283 |
. . . . . . . . . 10
   
      
            |
37 | 33, 22, 36 | iserex 11318 |
. . . . . . . . 9
                           |
38 | 32, 37 | mpbid 147 |
. . . . . . . 8
                       |
39 | 18, 23, 28, 30, 38 | isumcl 11404 |
. . . . . . 7
                           |
40 | 17, 39 | mulcld 7955 |
. . . . . 6
               
             |
41 | 13, 40 | fsumcl 11379 |
. . . . 5
 
      
                    |
42 | 41 | abscld 11161 |
. . . 4
 
      
          
             |
43 | 40 | abscld 11161 |
. . . . 5
                                 |
44 | 13, 43 | fsumrecl 11380 |
. . . 4
 
      
         
              |
45 | | mertens.9 |
. . . . . 6
   |
46 | 45 | rpred 9670 |
. . . . 5
   |
47 | 46 | adantr 276 |
. . . 4
 
      
  |
48 | 13, 40 | fsumabs 11444 |
. . . 4
 
      
          
          
         
              |
49 | 5 | nnzd 9350 |
. . . . . . . . . 10
   |
50 | 49 | adantr 276 |
. . . . . . . . 9
 
      
  |
51 | 12, 50 | zsubcld 9356 |
. . . . . . . 8
 
      
    |
52 | 10, 51 | fzfigd 10404 |
. . . . . . 7
 
      
        |
53 | 6 | adantr 276 |
. . . . . . . . . . . . 13
 
      
  |
54 | 53 | nn0ge0d 9208 |
. . . . . . . . . . . 12
 
      
  |
55 | 12 | zred 9351 |
. . . . . . . . . . . . 13
 
      
  |
56 | 53 | nn0red 9206 |
. . . . . . . . . . . . 13
 
      
  |
57 | 55, 56 | subge02d 8471 |
. . . . . . . . . . . 12
 
      

     |
58 | 54, 57 | mpbid 147 |
. . . . . . . . . . 11
 
      
    |
59 | 53, 33 | eleqtrdi 2270 |
. . . . . . . . . . . . . . 15
 
      
      |
60 | | uzid 9518 |
. . . . . . . . . . . . . . . . . 18
       |
61 | 49, 60 | syl 14 |
. . . . . . . . . . . . . . . . 17
       |
62 | | uzaddcl 9562 |
. . . . . . . . . . . . . . . . 17
               |
63 | 61, 8, 62 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
         |
64 | | eqid 2177 |
. . . . . . . . . . . . . . . . 17
         |
65 | 64 | uztrn2 9521 |
. . . . . . . . . . . . . . . 16
              
      |
66 | 63, 65 | sylan 283 |
. . . . . . . . . . . . . . 15
 
      
      |
67 | | elfzuzb 9992 |
. . . . . . . . . . . . . . 15
    
    
       |
68 | 59, 66, 67 | sylanbrc 417 |
. . . . . . . . . . . . . 14
 
      
      |
69 | | fznn0sub2 10101 |
. . . . . . . . . . . . . 14
             |
70 | 68, 69 | syl 14 |
. . . . . . . . . . . . 13
 
      
        |
71 | | elfzelz 9998 |
. . . . . . . . . . . . 13
           |
72 | 70, 71 | syl 14 |
. . . . . . . . . . . 12
 
      
    |
73 | | eluz 9517 |
. . . . . . . . . . . 12
   
       
     |
74 | 72, 12, 73 | syl2anc 411 |
. . . . . . . . . . 11
 
      
        
   |
75 | 58, 74 | mpbird 167 |
. . . . . . . . . 10
 
      
        |
76 | | fzss2 10037 |
. . . . . . . . . 10
      
            |
77 | 75, 76 | syl 14 |
. . . . . . . . 9
 
      
            |
78 | 77 | sselda 3155 |
. . . . . . . 8
                       |
79 | 16 | abscld 11161 |
. . . . . . . . . 10
 

      |
80 | 14, 15, 79 | syl2an 289 |
. . . . . . . . 9
                     |
81 | 39 | abscld 11161 |
. . . . . . . . 9
                               |
82 | 80, 81 | remulcld 7965 |
. . . . . . . 8
                                     |
83 | 78, 82 | syldan 282 |
. . . . . . 7
                                       |
84 | 52, 83 | fsumrecl 11380 |
. . . . . 6
 
      
                              |
85 | 51 | peano2zd 9354 |
. . . . . . . 8
 
      
      |
86 | 85, 12 | fzfigd 10404 |
. . . . . . 7
 
      
          |
87 | | elfznn0 10087 |
. . . . . . . . . . . . 13
           |
88 | 70, 87 | syl 14 |
. . . . . . . . . . . 12
 
      
    |
89 | | peano2nn0 9192 |
. . . . . . . . . . . 12
  
      |
90 | 88, 89 | syl 14 |
. . . . . . . . . . 11
 
      
      |
91 | 90, 33 | eleqtrdi 2270 |
. . . . . . . . . 10
 
      
          |
92 | | fzss1 10036 |
. . . . . . . . . 10
        
              |
93 | 91, 92 | syl 14 |
. . . . . . . . 9
 
      
              |
94 | 93 | sselda 3155 |
. . . . . . . 8
                         |
95 | 94, 82 | syldan 282 |
. . . . . . 7
                                         |
96 | 86, 95 | fsumrecl 11380 |
. . . . . 6
 
      
                                |
97 | 45 | rphalfcld 9683 |
. . . . . . . 8
     |
98 | 97 | rpred 9670 |
. . . . . . 7
     |
99 | 98 | adantr 276 |
. . . . . 6
 
      
    |
100 | | elfznn0 10087 |
. . . . . . . . . . 11
         |
101 | 14, 100, 79 | syl2an 289 |
. . . . . . . . . 10
                       |
102 | 52, 101 | fsumrecl 11380 |
. . . . . . . . 9
 
      
              |
103 | 102, 99 | remulcld 7965 |
. . . . . . . 8
 
      
 
                |
104 | | 0zd 9241 |
. . . . . . . . . . 11
   |
105 | | eqidd 2178 |
. . . . . . . . . . 11
 

          |
106 | | mertens.2 |
. . . . . . . . . . . 12
 

          |
107 | 106, 79 | eqeltrd 2254 |
. . . . . . . . . . 11
 

      |
108 | | mertens.7 |
. . . . . . . . . . 11
     |
109 | 33, 104, 105, 107, 108 | isumrecl 11408 |
. . . . . . . . . 10
        |
110 | 16 | absge0d 11164 |
. . . . . . . . . . . 12
 

      |
111 | 110, 106 | breqtrrd 4028 |
. . . . . . . . . . 11
 

      |
112 | 33, 104, 105, 107, 108, 111 | isumge0 11409 |
. . . . . . . . . 10

       |
113 | 109, 112 | ge0p1rpd 9701 |
. . . . . . . . 9
          |
114 | 113 | adantr 276 |
. . . . . . . 8
 
      
 
       |
115 | 103, 114 | rerpdivcld 9702 |
. . . . . . 7
 
      
                           |
116 | 97, 113 | rpdivcld 9688 |
. . . . . . . . . . . 12
              |
117 | 116 | rpred 9670 |
. . . . . . . . . . 11
              |
118 | 117 | ad2antrr 488 |
. . . . . . . . . 10
                     
        |
119 | 101, 118 | remulcld 7965 |
. . . . . . . . 9
                                    |
120 | 78, 23 | syldan 282 |
. . . . . . . . . . . 12
                       |
121 | | simplll 533 |
. . . . . . . . . . . . 13
   
      
                  |
122 | 78, 22 | syldan 282 |
. . . . . . . . . . . . . 14
                       |
123 | 122, 25 | sylan 283 |
. . . . . . . . . . . . 13
   
      
                  |
124 | 121, 123,
27 | syl2anc 411 |
. . . . . . . . . . . 12
   
      
                      |
125 | 121, 123,
29 | syl2anc 411 |
. . . . . . . . . . . 12
   
      
                  |
126 | 78, 38 | syldan 282 |
. . . . . . . . . . . 12
                         |
127 | 18, 120, 124, 125, 126 | isumcl 11404 |
. . . . . . . . . . 11
                             |
128 | 127 | abscld 11161 |
. . . . . . . . . 10
                                 |
129 | 79, 110 | jca 306 |
. . . . . . . . . . 11
 

            |
130 | 14, 100, 129 | syl2an 289 |
. . . . . . . . . 10
                             |
131 | 124 | sumeq2dv 11347 |
. . . . . . . . . . . . 13
                                           |
132 | 131 | fveq2d 5514 |
. . . . . . . . . . . 12
                                                   |
133 | | fvoveq1 5891 |
. . . . . . . . . . . . . . . 16
                   |
134 | 133 | sumeq1d 11345 |
. . . . . . . . . . . . . . 15
                               |
135 | 134 | fveq2d 5514 |
. . . . . . . . . . . . . 14
                                       |
136 | 135 | breq1d 4010 |
. . . . . . . . . . . . 13
       
   
                      
                            |
137 | 4 | simprd 114 |
. . . . . . . . . . . . . 14
                           
        |
138 | 137 | ad2antrr 488 |
. . . . . . . . . . . . 13
                          
   
                     |
139 | | elfzelz 9998 |
. . . . . . . . . . . . . . . . 17
         |
140 | 139 | adantl 277 |
. . . . . . . . . . . . . . . 16
                   |
141 | 140 | zred 9351 |
. . . . . . . . . . . . . . 15
                   |
142 | 11 | ad2antlr 489 |
. . . . . . . . . . . . . . . 16
                   |
143 | 142 | zred 9351 |
. . . . . . . . . . . . . . 15
                   |
144 | 49 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
                   |
145 | 144 | zred 9351 |
. . . . . . . . . . . . . . 15
                   |
146 | | elfzle2 10001 |
. . . . . . . . . . . . . . . 16
           |
147 | 146 | adantl 277 |
. . . . . . . . . . . . . . 15
                     |
148 | 141, 143,
145, 147 | lesubd 8483 |
. . . . . . . . . . . . . 14
                     |
149 | 142, 140 | zsubcld 9356 |
. . . . . . . . . . . . . . 15
                     |
150 | | eluz 9517 |
. . . . . . . . . . . . . . 15
  
              |
151 | 144, 149,
150 | syl2anc 411 |
. . . . . . . . . . . . . 14
                       
     |
152 | 148, 151 | mpbird 167 |
. . . . . . . . . . . . 13
                         |
153 | 136, 138,
152 | rspcdva 2846 |
. . . . . . . . . . . 12
                                                |
154 | 132, 153 | eqbrtrrd 4024 |
. . . . . . . . . . 11
                                            |
155 | 128, 118,
154 | ltled 8053 |
. . . . . . . . . 10
                              
             |
156 | | lemul2a 8792 |
. . . . . . . . . 10
      
              
                                   
                                              |
157 | 128, 118,
130, 155, 156 | syl31anc 1241 |
. . . . . . . . 9
                                                        |
158 | 52, 83, 119, 157 | fsumle 11442 |
. . . . . . . 8
 
      
                                             
         |
159 | 102 | recnd 7963 |
. . . . . . . . . 10
 
      
              |
160 | 97 | rpcnd 9672 |
. . . . . . . . . . 11
     |
161 | 160 | adantr 276 |
. . . . . . . . . 10
 
      
    |
162 | | peano2re 8070 |
. . . . . . . . . . . . 13
 
   
 
       |
163 | 109, 162 | syl 14 |
. . . . . . . . . . . 12
          |
164 | 163 | recnd 7963 |
. . . . . . . . . . 11
          |
165 | 164 | adantr 276 |
. . . . . . . . . 10
 
      
 
       |
166 | 114 | rpap0d 9676 |
. . . . . . . . . 10
 
      
 
     #   |
167 | 159, 161,
165, 166 | divassapd 8759 |
. . . . . . . . 9
 
      
                                                    |
168 | | fveq2 5510 |
. . . . . . . . . . . . . . . . 17
           |
169 | 168 | cbvsumv 11340 |
. . . . . . . . . . . . . . . 16
     
     |
170 | 169 | oveq1i 5878 |
. . . . . . . . . . . . . . 15
 
      
      |
171 | 170 | oveq2i 5879 |
. . . . . . . . . . . . . 14
               
       |
172 | 171, 116 | eqeltrid 2264 |
. . . . . . . . . . . . 13
              |
173 | 172 | rpcnd 9672 |
. . . . . . . . . . . 12
              |
174 | 173 | adantr 276 |
. . . . . . . . . . 11
 
      
             |
175 | 79 | recnd 7963 |
. . . . . . . . . . . 12
 

      |
176 | 14, 100, 175 | syl2an 289 |
. . . . . . . . . . 11
                       |
177 | 52, 174, 176 | fsummulc1 11428 |
. . . . . . . . . 10
 
      
 
                                        
         |
178 | 171 | oveq2i 5879 |
. . . . . . . . . 10
 
                        
                        |
179 | 171 | oveq2i 5879 |
. . . . . . . . . . . 12
                                   |
180 | 179 | a1i 9 |
. . . . . . . . . . 11
                                           |
181 | 180 | sumeq2i 11343 |
. . . . . . . . . 10
                 
                                 |
182 | 177, 178,
181 | 3eqtr3g 2233 |
. . . . . . . . 9
 
      
 
                                        
         |
183 | 167, 182 | eqtrd 2210 |
. . . . . . . 8
 
      
                                                    |
184 | 158, 183 | breqtrrd 4028 |
. . . . . . 7
 
      
                                                       |
185 | 109 | adantr 276 |
. . . . . . . . . 10
 
      
       |
186 | 163 | adantr 276 |
. . . . . . . . . 10
 
      
 
       |
187 | | fz0ssnn0 10089 |
. . . . . . . . . . . . 13
       |
188 | 187 | a1i 9 |
. . . . . . . . . . . 12
 
      
        |
189 | 106 | adantlr 477 |
. . . . . . . . . . . 12
                     |
190 | | nn0z 9249 |
. . . . . . . . . . . . . . 15

  |
191 | 190 | adantl 277 |
. . . . . . . . . . . . . 14
             |
192 | | 0zd 9241 |
. . . . . . . . . . . . . 14
             |
193 | 51 | adantr 276 |
. . . . . . . . . . . . . 14
               |
194 | | fzdcel 10013 |
. . . . . . . . . . . . . 14
 
   DECID         |
195 | 191, 192,
193, 194 | syl3anc 1238 |
. . . . . . . . . . . . 13
          
DECID
        |
196 | 195 | ralrimiva 2550 |
. . . . . . . . . . . 12
 
      
 DECID         |
197 | 79 | adantlr 477 |
. . . . . . . . . . . 12
                 |
198 | 110 | adantlr 477 |
. . . . . . . . . . . 12
                 |
199 | 108 | adantr 276 |
. . . . . . . . . . . 12
 
      
    |
200 | 33, 10, 52, 188, 189, 196, 197, 198, 199 | isumlessdc 11475 |
. . . . . . . . . . 11
 
      
           
       |
201 | 106 | sumeq2dv 11347 |
. . . . . . . . . . . 12
             |
202 | 201 | adantr 276 |
. . . . . . . . . . 11
 
      
     
      |
203 | 200, 202 | breqtrrd 4028 |
. . . . . . . . . 10
 
      
           
       |
204 | 109 | ltp1d 8863 |
. . . . . . . . . . 11
               |
205 | 204 | adantr 276 |
. . . . . . . . . 10
 
      
              |
206 | 102, 185,
186, 203, 205 | lelttrd 8059 |
. . . . . . . . 9
 
      
           
 
       |
207 | 97 | rpregt0d 9677 |
. . . . . . . . . . 11
         |
208 | 207 | adantr 276 |
. . . . . . . . . 10
 
      
        |
209 | | ltmul1 8526 |
. . . . . . . . . 10
                                        
 
    
 
                            |
210 | 102, 186,
208, 209 | syl3anc 1238 |
. . . . . . . . 9
 
      
 
                                    
           |
211 | 206, 210 | mpbid 147 |
. . . . . . . 8
 
      
 
                           |
212 | 113 | rpregt0d 9677 |
. . . . . . . . . 10
                   |
213 | 212 | adantr 276 |
. . . . . . . . 9
 
      
                  |
214 | | ltdivmul 8809 |
. . . . . . . . 9
                                    
                           
 
                            |
215 | 103, 99, 213, 214 | syl3anc 1238 |
. . . . . . . 8
 
      
                           
 
                            |
216 | 211, 215 | mpbird 167 |
. . . . . . 7
 
      
                             |
217 | 84, 115, 99, 184, 216 | lelttrd 8059 |
. . . . . 6
 
      
                                |
218 | | mertens.p |
. . . . . . . . . 10
   |
219 | 98, 218 | remulcld 7965 |
. . . . . . . . 9
       |
220 | | mertens.pge0 |
. . . . . . . . . 10

  |
221 | 218, 220 | ge0p1rpd 9701 |
. . . . . . . . 9
     |
222 | 219, 221 | rerpdivcld 9702 |
. . . . . . . 8
      
    |
223 | 222 | adantr 276 |
. . . . . . 7
 
      
          |
224 | 5 | nnrpd 9668 |
. . . . . . . . . . . . . 14
   |
225 | 97, 224 | rpdivcld 9688 |
. . . . . . . . . . . . 13
       |
226 | 225, 221 | rpdivcld 9688 |
. . . . . . . . . . . 12
      
    |
227 | 226 | rpred 9670 |
. . . . . . . . . . 11
      
    |
228 | 227, 218 | remulcld 7965 |
. . . . . . . . . 10
             |
229 | 228 | ad2antrr 488 |
. . . . . . . . 9
                         
     |
230 | | simpll 527 |
. . . . . . . . . . . 12
                     |
231 | 94, 15 | syl 14 |
. . . . . . . . . . . 12
                     |
232 | 230, 231,
79 | syl2anc 411 |
. . . . . . . . . . 11
                         |
233 | 227 | ad2antrr 488 |
. . . . . . . . . . 11
                             |
234 | 230, 231,
106 | syl2anc 411 |
. . . . . . . . . . . 12
                             |
235 | | fveq2 5510 |
. . . . . . . . . . . . . 14
           |
236 | 235 | breq1d 4010 |
. . . . . . . . . . . . 13
     
       
               |
237 | 7 | simprd 114 |
. . . . . . . . . . . . . 14
                     |
238 | 237 | ad2antrr 488 |
. . . . . . . . . . . . 13
                            
          |
239 | | elfzuz 9994 |
. . . . . . . . . . . . . 14
                   |
240 | | eluzle 9516 |
. . . . . . . . . . . . . . . . . 18
      
    |
241 | 240 | adantl 277 |
. . . . . . . . . . . . . . . . 17
 
      
    |
242 | 8 | nn0zd 9349 |
. . . . . . . . . . . . . . . . . . . 20
   |
243 | 242 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
 
      
  |
244 | 243 | zred 9351 |
. . . . . . . . . . . . . . . . . 18
 
      
  |
245 | 56, 244, 55 | leaddsub2d 8481 |
. . . . . . . . . . . . . . . . 17
 
      
  
     |
246 | 241, 245 | mpbid 147 |
. . . . . . . . . . . . . . . 16
 
      
    |
247 | | eluz 9517 |
. . . . . . . . . . . . . . . . 17
  
              |
248 | 243, 72, 247 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
 
      
            |
249 | 246, 248 | mpbird 167 |
. . . . . . . . . . . . . . 15
 
      
        |
250 | | peano2uz 9559 |
. . . . . . . . . . . . . . 15
      
          |
251 | 249, 250 | syl 14 |
. . . . . . . . . . . . . 14
 
      
          |
252 | | uztrn 9520 |
. . . . . . . . . . . . . 14
                         |
253 | 239, 251,
252 | syl2anr 290 |
. . . . . . . . . . . . 13
                         |
254 | 236, 238,
253 | rspcdva 2846 |
. . . . . . . . . . . 12
                            
    |
255 | 234, 254 | eqbrtrrd 4024 |
. . . . . . . . . . 11
                            
    |
256 | 232, 233,
255 | ltled 8053 |
. . . . . . . . . 10
                            
    |
257 | | breq1 4003 |
. . . . . . . . . . 11
    
              
             |
258 | | mertens.pub |
. . . . . . . . . . . 12
    |
259 | 258 | ad2antrr 488 |
. . . . . . . . . . 11
                   
  |
260 | 55 | adantr 276 |
. . . . . . . . . . . . . . 15
                     |
261 | | peano2zm 9267 |
. . . . . . . . . . . . . . . . . 18
     |
262 | 49, 261 | syl 14 |
. . . . . . . . . . . . . . . . 17
     |
263 | 262 | zred 9351 |
. . . . . . . . . . . . . . . 16
     |
264 | 263 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
                       |
265 | 231 | nn0red 9206 |
. . . . . . . . . . . . . . 15
                     |
266 | 12 | zcnd 9352 |
. . . . . . . . . . . . . . . . . 18
 
      
  |
267 | 56 | recnd 7963 |
. . . . . . . . . . . . . . . . . 18
 
      
  |
268 | | 1cnd 7951 |
. . . . . . . . . . . . . . . . . 18
 
      
  |
269 | 266, 267,
268 | subsubd 8273 |
. . . . . . . . . . . . . . . . 17
 
      
          |
270 | 269 | adantr 276 |
. . . . . . . . . . . . . . . 16
                             |
271 | | elfzle1 10000 |
. . . . . . . . . . . . . . . . 17
               |
272 | 271 | adantl 277 |
. . . . . . . . . . . . . . . 16
                         |
273 | 270, 272 | eqbrtrd 4022 |
. . . . . . . . . . . . . . 15
                         |
274 | 260, 264,
265, 273 | subled 8482 |
. . . . . . . . . . . . . 14
                         |
275 | 94, 19 | syl 14 |
. . . . . . . . . . . . . . . 16
                       |
276 | 275, 33 | eleqtrdi 2270 |
. . . . . . . . . . . . . . 15
                           |
277 | 262 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
                       |
278 | | elfz5 9990 |
. . . . . . . . . . . . . . 15
                     
     |
279 | 276, 277,
278 | syl2anc 411 |
. . . . . . . . . . . . . 14
                           
       |
280 | 274, 279 | mpbird 167 |
. . . . . . . . . . . . 13
                             |
281 | | simplll 533 |
. . . . . . . . . . . . . . . . 17
   
      
                    |
282 | 94, 22 | syldan 282 |
. . . . . . . . . . . . . . . . . 18
                         |
283 | 282, 25 | sylan 283 |
. . . . . . . . . . . . . . . . 17
   
      
                    |
284 | 281, 283,
27 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
   
      
                        |
285 | 284 | sumeq2dv 11347 |
. . . . . . . . . . . . . . 15
                                             |
286 | 285 | eqcomd 2183 |
. . . . . . . . . . . . . 14
                                             |
287 | 286 | fveq2d 5514 |
. . . . . . . . . . . . 13
                                                     |
288 | 135 | rspceeqv 2859 |
. . . . . . . . . . . . 13
                                           
                                       |
289 | 280, 287,
288 | syl2anc 411 |
. . . . . . . . . . . 12
                              
             
   
          |
290 | 94, 39 | syldan 282 |
. . . . . . . . . . . . . 14
                               |
291 | 290 | abscld 11161 |
. . . . . . . . . . . . 13
                                   |
292 | | eqeq1 2184 |
. . . . . . . . . . . . . . 15
    
              
   
           
             
   
           |
293 | 292 | rexbidv 2478 |
. . . . . . . . . . . . . 14
    
                                  
           
             
   
           |
294 | | mertens.10 |
. . . . . . . . . . . . . 14
 
          
   
          |
295 | 293, 294 | elab2g 2884 |
. . . . . . . . . . . . 13
                   
         
           
             
   
           |
296 | 291, 295 | syl 14 |
. . . . . . . . . . . 12
                       
         
           
             
   
           |
297 | 289, 296 | mpbird 167 |
. . . . . . . . . . 11
                                   |
298 | 257, 259,
297 | rspcdva 2846 |
. . . . . . . . . 10
                                
  |
299 | 230, 231,
129 | syl2anc 411 |
. . . . . . . . . . 11
                               |
300 | 94, 81 | syldan 282 |
. . . . . . . . . . . 12
                                   |
301 | 39 | absge0d 11164 |
. . . . . . . . . . . . 13
                  
            |
302 | 94, 301 | syldan 282 |
. . . . . . . . . . . 12
                      
            |
303 | 300, 302 | jca 306 |
. . . . . . . . . . 11
                       
             
             |
304 | 218 | ad2antrr 488 |
. . . . . . . . . . 11
                     |
305 | | lemul12a 8795 |
. . . . . . . . . . 11
       
          
                  
                                  
                                     
      |
306 | 299, 233,
303, 304, 305 | syl22anc 1239 |
. . . . . . . . . 10
                        
                      
        
          
             |
307 | 256, 298,
306 | mp2and 433 |
. . . . . . . . 9
                                             
     |
308 | 86, 95, 229, 307 | fsumle 11442 |
. . . . . . . 8
 
      
                                                    |
309 | 228 | recnd 7963 |
. . . . . . . . . . 11
             |
310 | 309 | adantr 276 |
. . . . . . . . . 10
 
      
            |
311 | | fsumconst 11433 |
. . . . . . . . . 10
                                          ♯                
      |
312 | 86, 310, 311 | syl2anc 411 |
. . . . . . . . 9
 
      
                     ♯                       |
313 | | 1zzd 9256 |
. . . . . . . . . . . . . 14
 
      
  |
314 | | fzen 10016 |
. . . . . . . . . . . . . 14
 
      
              |
315 | 313, 50, 72, 314 | syl3anc 1238 |
. . . . . . . . . . . . 13
 
      
                  |
316 | | ax-1cn 7882 |
. . . . . . . . . . . . . . 15
 |
317 | 72 | zcnd 9352 |
. . . . . . . . . . . . . . 15
 
      
    |
318 | | addcom 8071 |
. . . . . . . . . . . . . . 15
  
            |
319 | 316, 317,
318 | sylancr 414 |
. . . . . . . . . . . . . 14
 
      
          |
320 | 267, 266 | pncan3d 8248 |
. . . . . . . . . . . . . 14
 
      
      |
321 | 319, 320 | oveq12d 5886 |
. . . . . . . . . . . . 13
 
      
                      |
322 | 315, 321 | breqtrd 4026 |
. . . . . . . . . . . 12
 
      
              |
323 | 313, 50 | fzfigd 10404 |
. . . . . . . . . . . . 13
 
      
      |
324 | | hashen 10735 |
. . . . . . . . . . . . 13
                ♯      ♯                         |
325 | 323, 86, 324 | syl2anc 411 |
. . . . . . . . . . . 12
 
      
 ♯      ♯         
               |
326 | 322, 325 | mpbird 167 |
. . . . . . . . . . 11
 
      
♯      ♯            |
327 | | hashfz1 10734 |
. . . . . . . . . . . 12

♯        |
328 | 53, 327 | syl 14 |
. . . . . . . . . . 11
 
      
♯        |
329 | 326, 328 | eqtr3d 2212 |
. . . . . . . . . 10
 
      
♯            |
330 | 329 | oveq1d 5883 |
. . . . . . . . 9
 
      
 ♯                
                  |
331 | 218 | recnd 7963 |
. . . . . . . . . . . 12
   |
332 | 221 | rpcnd 9672 |
. . . . . . . . . . . 12
     |
333 | 221 | rpap0d 9676 |
. . . . . . . . . . . 12
   #   |
334 | 160, 331,
332, 333 | div23apd 8761 |
. . . . . . . . . . 11
      
            |
335 | 49 | zcnd 9352 |
. . . . . . . . . . . . . 14
   |
336 | 225 | rpcnd 9672 |
. . . . . . . . . . . . . 14
       |
337 | 335, 336,
332, 333 | divassapd 8759 |
. . . . . . . . . . . . 13
        
              |
338 | 5 | nnap0d 8941 |
. . . . . . . . . . . . . . 15
 #   |
339 | 160, 335,
338 | divcanap2d 8725 |
. . . . . . . . . . . . . 14
           |
340 | 339 | oveq1d 5883 |
. . . . . . . . . . . . 13
        
          |
341 | 337, 340 | eqtr3d 2212 |
. . . . . . . . . . . 12
                   |
342 | 341 | oveq1d 5883 |
. . . . . . . . . . 11
        
              |
343 | 226 | rpcnd 9672 |
. . . . . . . . . . . 12
      
    |
344 | 335, 343,
331 | mulassd 7958 |
. . . . . . . . . . 11
        
                  |
345 | 334, 342,
344 | 3eqtr2rd 2217 |
. . . . . . . . . 10
        
              |
346 | 345 | adantr 276 |
. . . . . . . . 9
 
      
                      |
347 | 312, 330,
346 | 3eqtrd 2214 |
. . . . . . . 8
 
      
                              |
348 | 308, 347 | breqtrd 4026 |
. . . . . . 7
 
      
                                        |
349 | | peano2re 8070 |
. . . . . . . . . . 11
 
   |
350 | 218, 349 | syl 14 |
. . . . . . . . . 10
     |
351 | 218 | ltp1d 8863 |
. . . . . . . . . 10
     |
352 | 218, 350,
97, 351 | ltmul2dd 9727 |
. . . . . . . . 9
    
        |
353 | 219, 98, 221 | ltdivmul2d 9723 |
. . . . . . . . 9
           
             |
354 | 352, 353 | mpbird 167 |
. . . . . . . 8
      
      |
355 | 354 | adantr 276 |
. . . . . . 7
 
      
            |
356 | 96, 223, 99, 348, 355 | lelttrd 8059 |
. . . . . 6
 
      
                                  |
357 | 84, 96, 99, 99, 217, 356 | lt2addd 8501 |
. . . . 5
 
      
 
                           
                                      |
358 | 17, 39 | absmuld 11174 |
. . . . . . 7
                                       
             |
359 | 358 | sumeq2dv 11347 |
. . . . . 6
 
      
 ![]() |