Step | Hyp | Ref
| Expression |
1 | | fzfid 11911 |
. . . . . . . . 9
               |
2 | | elfznn 11594 |
. . . . . . . . . . . . 13
           |
3 | 2 | adantl 466 |
. . . . . . . . . . . 12
              
  |
4 | 3 | nnrpd 11136 |
. . . . . . . . . . 11
              
  |
5 | 4 | relogcld 22204 |
. . . . . . . . . 10
              
      |
6 | 5, 3 | nndivred 10480 |
. . . . . . . . 9
              
        |
7 | 1, 6 | fsumrecl 13328 |
. . . . . . . 8
                       |
8 | 7 | recnd 9522 |
. . . . . . 7
                       |
9 | | elioore 11440 |
. . . . . . . . . . . . 13
   
  |
10 | 9 | adantl 466 |
. . . . . . . . . . . 12
       |
11 | | 1rp 11105 |
. . . . . . . . . . . . 13
 |
12 | 11 | a1i 11 |
. . . . . . . . . . . 12
       |
13 | | 1red 9511 |
. . . . . . . . . . . . 13
       |
14 | | eliooord 11465 |
. . . . . . . . . . . . . . 15
   
    |
15 | 14 | adantl 466 |
. . . . . . . . . . . . . 14
     
   |
16 | 15 | simpld 459 |
. . . . . . . . . . . . 13
       |
17 | 13, 10, 16 | ltled 9632 |
. . . . . . . . . . . 12
       |
18 | 10, 12, 17 | rpgecld 11172 |
. . . . . . . . . . 11
       |
19 | 18 | relogcld 22204 |
. . . . . . . . . 10
           |
20 | 19 | resqcld 12150 |
. . . . . . . . 9
               |
21 | 20 | rehalfcld 10681 |
. . . . . . . 8
                 |
22 | 21 | recnd 9522 |
. . . . . . 7
                 |
23 | 19 | recnd 9522 |
. . . . . . 7
           |
24 | 10, 16 | rplogcld 22210 |
. . . . . . . 8
           |
25 | 24 | rpne0d 11142 |
. . . . . . 7
           |
26 | 8, 22, 23, 25 | divsubdird 10256 |
. . . . . 6
                                                                                 |
27 | 7, 21 | resubcld 9886 |
. . . . . . . 8
                                   |
28 | 27 | recnd 9522 |
. . . . . . 7
                                   |
29 | 28, 23, 25 | divrecd 10220 |
. . . . . 6
                                                                             |
30 | 20 | recnd 9522 |
. . . . . . . . 9
               |
31 | | 2cnd 10504 |
. . . . . . . . 9
       |
32 | | 2ne0 10524 |
. . . . . . . . . 10
 |
33 | 32 | a1i 11 |
. . . . . . . . 9
       |
34 | 30, 31, 23, 33, 25 | divdiv32d 10242 |
. . . . . . . 8
                                       |
35 | 23 | sqvald 12121 |
. . . . . . . . . . 11
                         |
36 | 35 | oveq1d 6214 |
. . . . . . . . . 10
                                     |
37 | 23, 23, 25 | divcan3d 10222 |
. . . . . . . . . 10
                           |
38 | 36, 37 | eqtrd 2495 |
. . . . . . . . 9
                         |
39 | 38 | oveq1d 6214 |
. . . . . . . 8
                             |
40 | 34, 39 | eqtrd 2495 |
. . . . . . 7
                             |
41 | 40 | oveq2d 6215 |
. . . . . 6
                                                                             |
42 | 26, 29, 41 | 3eqtr3rd 2504 |
. . . . 5
                                                                         |
43 | 42 | mpteq2dva 4485 |
. . . 4
                                                                              |
44 | 24 | rprecred 11148 |
. . . . 5
             |
45 | 18 | ex 434 |
. . . . . . 7
       |
46 | 45 | ssrdv 3469 |
. . . . . 6
     |
47 | | eqid 2454 |
. . . . . . . . 9

 
                                                          |
48 | 47 | logdivsum 22914 |
. . . . . . . 8
   
                                 
                              
 
                            
     
 
                                         |
49 | 48 | simp2i 998 |
. . . . . . 7

 
                             |
50 | | rlimdmo1 13212 |
. . . . . . 7
   
                                                               |
51 | 49, 50 | mp1i 12 |
. . . . . 6
                                   |
52 | 46, 51 | o1res2 13158 |
. . . . 5
                                      |
53 | | divlogrlim 22212 |
. . . . . 6
   
         |
54 | | rlimo1 13211 |
. . . . . 6
                             |
55 | 53, 54 | mp1i 12 |
. . . . 5
                |
56 | 27, 44, 52, 55 | o1mul2 13219 |
. . . 4
                                              |
57 | 43, 56 | eqeltrd 2542 |
. . 3
                                        |
58 | 8, 23, 25 | divcld 10217 |
. . . . 5
                             |
59 | 23 | halfcld 10679 |
. . . . 5
             |
60 | 58, 59 | subcld 9829 |
. . . 4
                                     |
61 | | elfznn 11594 |
. . . . . . . . . . . 12
           |
62 | 61 | adantl 466 |
. . . . . . . . . . 11
              
  |
63 | | vmacl 22588 |
. . . . . . . . . . 11
 Λ    |
64 | 62, 63 | syl 16 |
. . . . . . . . . 10
              
Λ    |
65 | 64, 62 | nndivred 10480 |
. . . . . . . . 9
              
 Λ     |
66 | 18 | adantr 465 |
. . . . . . . . . . 11
              
  |
67 | 62 | nnrpd 11136 |
. . . . . . . . . . 11
              
  |
68 | 66, 67 | rpdivcld 11154 |
. . . . . . . . . 10
              
    |
69 | 68 | relogcld 22204 |
. . . . . . . . 9
              
        |
70 | 65, 69 | remulcld 9524 |
. . . . . . . 8
              
  Λ            |
71 | 1, 70 | fsumrecl 13328 |
. . . . . . 7
                 Λ            |
72 | 71 | recnd 9522 |
. . . . . 6
                 Λ            |
73 | 24 | rpcnd 11139 |
. . . . . 6
           |
74 | 72, 73, 25 | divcld 10217 |
. . . . 5
                  Λ                 |
75 | 73 | halfcld 10679 |
. . . . 5
             |
76 | 74, 75 | subcld 9829 |
. . . 4
                   Λ                        |
77 | 58, 74, 59 | nnncan2d 9864 |
. . . . . . 7
                                      
           Λ                                                           Λ                  |
78 | 8, 72, 23, 25 | divsubdird 10256 |
. . . . . . 7
                                   Λ                                                    Λ                  |
79 | | fzfid 11911 |
. . . . . . . . . . . 12
              
      
     |
80 | 64 | adantr 465 |
. . . . . . . . . . . . 13
  
                       
Λ    |
81 | 62 | adantr 465 |
. . . . . . . . . . . . . 14
  
                       
  |
82 | | elfznn 11594 |
. . . . . . . . . . . . . . 15
             |
83 | 82 | adantl 466 |
. . . . . . . . . . . . . 14
  
                       
  |
84 | 81, 83 | nnmulcld 10479 |
. . . . . . . . . . . . 13
  
                       
    |
85 | 80, 84 | nndivred 10480 |
. . . . . . . . . . . 12
  
                       
 Λ       |
86 | 79, 85 | fsumrecl 13328 |
. . . . . . . . . . 11
              
             Λ       |
87 | 86 | recnd 9522 |
. . . . . . . . . 10
              
             Λ       |
88 | 70 | recnd 9522 |
. . . . . . . . . 10
              
  Λ            |
89 | 1, 87, 88 | fsumsub 13372 |
. . . . . . . . 9
                             Λ       Λ                      
      
     Λ                 Λ             |
90 | 64 | recnd 9522 |
. . . . . . . . . . . . 13
              
Λ    |
91 | 62 | nncnd 10448 |
. . . . . . . . . . . . 13
              
  |
92 | 62 | nnne0d 10476 |
. . . . . . . . . . . . 13
              
  |
93 | 90, 91, 92 | divcld 10217 |
. . . . . . . . . . . 12
              
 Λ     |
94 | 83 | nnrecred 10477 |
. . . . . . . . . . . . . 14
  
                       
    |
95 | 79, 94 | fsumrecl 13328 |
. . . . . . . . . . . . 13
              
                |
96 | 95 | recnd 9522 |
. . . . . . . . . . . 12
              
                |
97 | 69 | recnd 9522 |
. . . . . . . . . . . 12
              
        |
98 | 93, 96, 97 | subdid 9910 |
. . . . . . . . . . 11
              
  Λ           
                 Λ                    Λ             |
99 | 90 | adantr 465 |
. . . . . . . . . . . . . . . 16
  
                       
Λ    |
100 | 91 | adantr 465 |
. . . . . . . . . . . . . . . 16
  
                       
  |
101 | 83 | nncnd 10448 |
. . . . . . . . . . . . . . . 16
  
                       
  |
102 | 92 | adantr 465 |
. . . . . . . . . . . . . . . 16
  
                       
  |
103 | 83 | nnne0d 10476 |
. . . . . . . . . . . . . . . 16
  
                       
  |
104 | 99, 100, 101, 102, 103 | divdiv1d 10248 |
. . . . . . . . . . . . . . 15
  
                       
  Λ     Λ       |
105 | 99, 100, 102 | divcld 10217 |
. . . . . . . . . . . . . . . 16
  
                       
 Λ     |
106 | 105, 101,
103 | divrecd 10220 |
. . . . . . . . . . . . . . 15
  
                       
  Λ      Λ        |
107 | 104, 106 | eqtr3d 2497 |
. . . . . . . . . . . . . 14
  
                       
 Λ       Λ        |
108 | 107 | sumeq2dv 13297 |
. . . . . . . . . . . . 13
              
             Λ                   Λ        |
109 | 101, 103 | reccld 10210 |
. . . . . . . . . . . . . 14
  
                       
    |
110 | 79, 93, 109 | fsummulc2 13368 |
. . . . . . . . . . . . 13
              
  Λ                                Λ        |
111 | 108, 110 | eqtr4d 2498 |
. . . . . . . . . . . 12
              
             Λ       Λ                    |
112 | 111 | oveq1d 6214 |
. . . . . . . . . . 11
              
              Λ       Λ              Λ                    Λ             |
113 | 98, 112 | eqtr4d 2498 |
. . . . . . . . . 10
              
  Λ           
                            Λ       Λ             |
114 | 113 | sumeq2dv 13297 |
. . . . . . . . 9
                 Λ                                                  Λ       Λ             |
115 | | vmasum 22687 |
. . . . . . . . . . . . . . 15
  
 Λ        |
116 | 3, 115 | syl 16 |
. . . . . . . . . . . . . 14
              
 
 Λ        |
117 | 116 | oveq1d 6214 |
. . . . . . . . . . . . 13
              
   
Λ           |
118 | | fzfid 11911 |
. . . . . . . . . . . . . . 15
              
      |
119 | | sgmss 22576 |
. . . . . . . . . . . . . . . 16
         |
120 | 3, 119 | syl 16 |
. . . . . . . . . . . . . . 15
              
 
      |
121 | | ssfi 7643 |
. . . . . . . . . . . . . . 15
      
          |
122 | 118, 120,
121 | syl2anc 661 |
. . . . . . . . . . . . . 14
              
 
  |
123 | 3 | nncnd 10448 |
. . . . . . . . . . . . . 14
              
  |
124 | | ssrab2 3544 |
. . . . . . . . . . . . . . . . . 18
   |
125 | | simprr 756 |
. . . . . . . . . . . . . . . . . 18
              
   
    |
126 | 124, 125 | sseldi 3461 |
. . . . . . . . . . . . . . . . 17
              
   
  |
127 | 126, 63 | syl 16 |
. . . . . . . . . . . . . . . 16
              
    Λ    |
128 | 127 | recnd 9522 |
. . . . . . . . . . . . . . 15
              
    Λ    |
129 | 128 | anassrs 648 |
. . . . . . . . . . . . . 14
  
             
 
Λ    |
130 | 3 | nnne0d 10476 |
. . . . . . . . . . . . . 14
              
  |
131 | 122, 123,
129, 130 | fsumdivc 13370 |
. . . . . . . . . . . . 13
              
   
Λ    
  Λ     |
132 | 117, 131 | eqtr3d 2497 |
. . . . . . . . . . . 12
              
        
 Λ     |
133 | 132 | sumeq2dv 13297 |
. . . . . . . . . . 11
                               
   Λ     |
134 | | oveq2 6207 |
. . . . . . . . . . . 12
    Λ    Λ       |
135 | 2 | ad2antrl 727 |
. . . . . . . . . . . . . 14
              
      |
136 | 135 | nncnd 10448 |
. . . . . . . . . . . . 13
              
      |
137 | 135 | nnne0d 10476 |
. . . . . . . . . . . . 13
              
      |
138 | 128, 136,
137 | divcld 10217 |
. . . . . . . . . . . 12
              
     Λ     |
139 | 134, 10, 138 | dvdsflsumcom 22660 |
. . . . . . . . . . 11
               
   Λ                          Λ       |
140 | 133, 139 | eqtrd 2495 |
. . . . . . . . . 10
                               
      
     Λ       |
141 | 140 | oveq1d 6214 |
. . . . . . . . 9
                                  Λ                      
      
     Λ                 Λ             |
142 | 89, 114, 141 | 3eqtr4rd 2506 |
. . . . . . . 8
                                  Λ           
           Λ                            |
143 | 142 | oveq1d 6214 |
. . . . . . 7
                                   Λ                 
           Λ                                 |
144 | 77, 78, 143 | 3eqtr2d 2501 |
. . . . . 6
                                      
           Λ                                    Λ                                 |
145 | 144 | mpteq2dva 4485 |
. . . . 5
       
                             
           Λ                                         Λ                                  |
146 | | 1red 9511 |
. . . . . . 7
  |
147 | 1, 65 | fsumrecl 13328 |
. . . . . . . . 9
                Λ     |
148 | 147, 24 | rerpdivcld 11164 |
. . . . . . . 8
                 Λ          |
149 | | ioossre 11467 |
. . . . . . . . . . 11
    |
150 | | ax-1cn 9450 |
. . . . . . . . . . 11
 |
151 | | o1const 13214 |
. . . . . . . . . . 11
                |
152 | 149, 150,
151 | mp2an 672 |
. . . . . . . . . 10
   
     |
153 | 152 | a1i 11 |
. . . . . . . . 9
          |
154 | 148 | recnd 9522 |
. . . . . . . . . 10
                 Λ          |
155 | 12 | rpcnd 11139 |
. . . . . . . . . 10
       |
156 | 147 | recnd 9522 |
. . . . . . . . . . . . . 14
                Λ     |
157 | 156, 23, 23, 25 | divsubdird 10256 |
. . . . . . . . . . . . 13
                  Λ                          Λ                     |
158 | 156, 23 | subcld 9829 |
. . . . . . . . . . . . . 14
                 Λ          |
159 | 158, 23, 25 | divrecd 10220 |
. . . . . . . . . . . . 13
                  Λ                          Λ                 |
160 | 23, 25 | dividd 10215 |
. . . . . . . . . . . . . 14
                 |
161 | 160 | oveq2d 6215 |
. . . . . . . . . . . . 13
                  Λ                                Λ           |
162 | 157, 159,
161 | 3eqtr3rd 2504 |
. . . . . . . . . . . 12
                  Λ           
          Λ                 |
163 | 162 | mpteq2dva 4485 |
. . . . . . . . . . 11
                 Λ                           Λ                  |
164 | 147, 19 | resubcld 9886 |
. . . . . . . . . . . 12
                 Λ          |
165 | | vmadivsum 22863 |
. . . . . . . . . . . . . 14

            Λ             |
166 | 165 | a1i 11 |
. . . . . . . . . . . . 13
             Λ              |
167 | 46, 166 | o1res2 13158 |
. . . . . . . . . . . 12
                Λ              |
168 | 164, 44, 167, 55 | o1mul2 13219 |
. . . . . . . . . . 11
                 Λ                     |
169 | 163, 168 | eqeltrd 2542 |
. . . . . . . . . 10
                 Λ               |
170 | 154, 155,
169 | o1dif 13224 |
. . . . . . . . 9
                 Λ                       |
171 | 153, 170 | mpbird 232 |
. . . . . . . 8
                Λ              |
172 | 148, 171 | o1lo1d 13134 |
. . . . . . 7
                Λ               |
173 | 95, 69 | resubcld 9886 |
. . . . . . . . . 10
              
                        |
174 | 65, 173 | remulcld 9524 |
. . . . . . . . 9
              
  Λ           
                |
175 | 1, 174 | fsumrecl 13328 |
. . . . . . . 8
                 Λ                            |
176 | 175, 24 | rerpdivcld 11164 |
. . . . . . 7
                  Λ                                 |
177 | | 1red 9511 |
. . . . . . . . . . . 12
              
  |
178 | | vmage0 22591 |
. . . . . . . . . . . . . 14
 Λ    |
179 | 62, 178 | syl 16 |
. . . . . . . . . . . . 13
              
Λ    |
180 | 64, 67, 179 | divge0d 11173 |
. . . . . . . . . . . 12
              
 Λ     |
181 | 68 | rpred 11137 |
. . . . . . . . . . . . . 14
              
    |
182 | 91 | mulid2d 9514 |
. . . . . . . . . . . . . . . 16
              
    |
183 | | fznnfl 11817 |
. . . . . . . . . . . . . . . . . 18
         
     |
184 | 10, 183 | syl 16 |
. . . . . . . . . . . . . . . . 17
             
     |
185 | 184 | simplbda 624 |
. . . . . . . . . . . . . . . 16
              
  |
186 | 182, 185 | eqbrtrd 4419 |
. . . . . . . . . . . . . . 15
              
    |
187 | 10 | adantr 465 |
. . . . . . . . . . . . . . . 16
              
  |
188 | 177, 187,
67 | lemuldivd 11182 |
. . . . . . . . . . . . . . 15
              
  
     |
189 | 186, 188 | mpbid 210 |
. . . . . . . . . . . . . 14
              
    |
190 | | harmonicubnd 22535 |
. . . . . . . . . . . . . 14
              
                |
191 | 181, 189,
190 | syl2anc 661 |
. . . . . . . . . . . . 13
              
             
          |
192 | 95, 69, 177 | lesubadd2d 10048 |
. . . . . . . . . . . . 13
              
         
                    
                 |
193 | 191, 192 | mpbird 232 |
. . . . . . . . . . . 12
              
                     
  |
194 | 173, 177,
65, 180, 193 | lemul2ad 10383 |
. . . . . . . . . . 11
              
  Λ           
                Λ      |
195 | 93 | mulid1d 9513 |
. . . . . . . . . . 11
              
  Λ     Λ     |
196 | 194, 195 | breqtrd 4423 |
. . . . . . . . . 10
              
  Λ           
               Λ     |
197 | 1, 174, 65, 196 | fsumle 13379 |
. . . . . . . . 9
                 Λ                                     Λ     |
198 | 175, 147,
24, 197 | lediv1dd 11191 |
. . . . . . . 8
                  Λ                                           Λ          |
199 | 198 | adantrr 716 |
. . . . . . 7
    
               Λ                                           Λ          |
200 | 146, 172,
148, 176, 199 | lo1le 13246 |
. . . . . 6
                 Λ                                      |
201 | | 0red 9497 |
. . . . . . 7
  |
202 | | harmoniclbnd 22534 |
. . . . . . . . . . . 12
  
                      |
203 | 68, 202 | syl 16 |
. . . . . . . . . . 11
              
                      |
204 | 95, 69 | subge0d 10039 |
. . . . . . . . . . 11
              
                      
                       |
205 | 203, 204 | mpbird 232 |
. . . . . . . . . 10
              
 
      
               |
206 | 65, 173, 180, 205 | mulge0d 10026 |
. . . . . . . . 9
              
  Λ                            |
207 | 1, 174, 206 | fsumge0 13375 |
. . . . . . . 8
     
           Λ                            |
208 | 175, 24, 207 | divge0d 11173 |
. . . . . . 7
                  Λ                                 |
209 | 176, 201,
208 | o1lo12 13133 |
. . . . . 6
                  Λ                                                    Λ                                       |
210 | 200, 209 | mpbird 232 |
. . . . 5
                 Λ                                     |
211 | 145, 210 | eqeltrd 2542 |
. . . 4
       
                             
           Λ                             |
212 | 60, 76, 211 | o1dif 13224 |
. . 3
       
                                                 Λ                             |
213 | 57, 212 | mpbid 210 |
. 2
                  Λ                            |
214 | 213 | trud 1379 |
1
   
  
           Λ                           |