Proof of Theorem dchrvmasumlem2
Step | Hyp | Ref
| Expression |
1 | | 1red 9658 |
. 2
   |
2 | | dchrvmasum.c |
. . . . . . 7
      |
3 | | elrege0 11738 |
. . . . . . 7
   
    |
4 | 2, 3 | sylib 200 |
. . . . . 6
 
   |
5 | 4 | simpld 461 |
. . . . 5
   |
6 | 5 | adantr 467 |
. . . 4
 

  |
7 | | fzfid 12186 |
. . . . 5
 

          |
8 | | simpr 463 |
. . . . . . . 8
 

  |
9 | | elfznn 11828 |
. . . . . . . . 9
           |
10 | 9 | nnrpd 11339 |
. . . . . . . 8
           |
11 | | rpdivcl 11325 |
. . . . . . . 8
       |
12 | 8, 10, 11 | syl2an 480 |
. . . . . . 7
            
    |
13 | | relogcl 23525 |
. . . . . . 7
  
        |
14 | 12, 13 | syl 17 |
. . . . . 6
            
        |
15 | 8 | adantr 467 |
. . . . . 6
            
  |
16 | 14, 15 | rerpdivcld 11369 |
. . . . 5
            
          |
17 | 7, 16 | fsumrecl 13800 |
. . . 4
 

                    |
18 | 6, 17 | remulcld 9671 |
. . 3
 

                      |
19 | | dchrvmasum.r |
. . . . 5
   |
20 | | 3nn 10768 |
. . . . . . 7
 |
21 | | nnrp 11311 |
. . . . . . 7
   |
22 | | relogcl 23525 |
. . . . . . 7

      |
23 | 20, 21, 22 | mp2b 10 |
. . . . . 6
     |
24 | | 1re 9642 |
. . . . . 6
 |
25 | 23, 24 | readdcli 9656 |
. . . . 5
       |
26 | | remulcl 9624 |
. . . . 5
                   |
27 | 19, 25, 26 | sylancl 668 |
. . . 4
           |
28 | 27 | adantr 467 |
. . 3
 

          |
29 | | rpssre 11312 |
. . . . 5
 |
30 | 5 | recnd 9669 |
. . . . 5
   |
31 | | o1const 13683 |
. . . . 5
          |
32 | 29, 30, 31 | sylancr 669 |
. . . 4
        |
33 | | logfacrlim2 24154 |
. . . . 5

                     |
34 | | rlimo1 13680 |
. . . . 5
                                               |
35 | 33, 34 | mp1i 13 |
. . . 4
                          |
36 | 6, 17, 32, 35 | o1mul2 13688 |
. . 3
  
                         |
37 | 27 | recnd 9669 |
. . . 4
           |
38 | | o1const 13683 |
. . . 4
  
                       |
39 | 29, 37, 38 | sylancr 669 |
. . 3
  
             |
40 | 18, 28, 36, 39 | o1add2 13687 |
. 2
                                      |
41 | 18, 28 | readdcld 9670 |
. 2
 

 
                              |
42 | | dchrvmasum.f |
. . . . . . . . . 10
 

  |
43 | 42 | ralrimiva 2802 |
. . . . . . . . 9
    |
44 | 43 | ad2antrr 732 |
. . . . . . . 8
            
   |
45 | | dchrvmasum.g |
. . . . . . . . . 10
     |
46 | 45 | eleq1d 2513 |
. . . . . . . . 9
   
   |
47 | 46 | rspcv 3146 |
. . . . . . . 8
  
 
   |
48 | 12, 44, 47 | sylc 62 |
. . . . . . 7
            
  |
49 | | dchrvmasum.t |
. . . . . . . 8
   |
50 | 49 | ad2antrr 732 |
. . . . . . 7
            
  |
51 | 48, 50 | subcld 9986 |
. . . . . 6
            
    |
52 | 51 | abscld 13498 |
. . . . 5
            
        |
53 | 9 | adantl 468 |
. . . . 5
            
  |
54 | 52, 53 | nndivred 10658 |
. . . 4
            
          |
55 | 7, 54 | fsumrecl 13800 |
. . 3
 

              
     |
56 | 55 | recnd 9669 |
. 2
 

              
     |
57 | 53 | nnrpd 11339 |
. . . . . . . 8
            
  |
58 | 51 | absge0d 13506 |
. . . . . . . 8
            
        |
59 | 52, 57, 58 | divge0d 11378 |
. . . . . . 7
            
    
     |
60 | 7, 54, 59 | fsumge0 13855 |
. . . . . 6
 

              
     |
61 | 55, 60 | absidd 13484 |
. . . . 5
 

                 
                  
     |
62 | 61, 55 | eqeltrd 2529 |
. . . 4
 

                 
      |
63 | 41 | recnd 9669 |
. . . . 5
 

 
                              |
64 | 63 | abscld 13498 |
. . . 4
 

                                    |
65 | | 3re 10683 |
. . . . . . . 8
 |
66 | 65 | a1i 11 |
. . . . . . 7
 

  |
67 | | 1le3 10826 |
. . . . . . 7
 |
68 | 66, 67 | jctir 541 |
. . . . . 6
 

    |
69 | 19 | adantr 467 |
. . . . . . 7
 

  |
70 | 24 | rexri 9693 |
. . . . . . . . . 10
 |
71 | 65 | rexri 9693 |
. . . . . . . . . 10
 |
72 | | 1lt3 10778 |
. . . . . . . . . 10
 |
73 | | lbico1 11689 |
. . . . . . . . . 10
         |
74 | 70, 71, 72, 73 | mp3an 1364 |
. . . . . . . . 9
     |
75 | | 0red 9644 |
. . . . . . . . . . 11
 
       |
76 | | elico2 11698 |
. . . . . . . . . . . . . . 15
 
      
    |
77 | 24, 71, 76 | mp2an 678 |
. . . . . . . . . . . . . 14
    
    |
78 | 77 | simp1bi 1023 |
. . . . . . . . . . . . 13
       |
79 | | 0red 9644 |
. . . . . . . . . . . . . 14
       |
80 | | 1red 9658 |
. . . . . . . . . . . . . 14
       |
81 | | 0lt1 10136 |
. . . . . . . . . . . . . . 15
 |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . 14
       |
83 | 77 | simp2bi 1024 |
. . . . . . . . . . . . . 14
       |
84 | 79, 80, 78, 82, 83 | ltletrd 9795 |
. . . . . . . . . . . . 13
       |
85 | 78, 84 | elrpd 11338 |
. . . . . . . . . . . 12
       |
86 | 49 | adantr 467 |
. . . . . . . . . . . . . 14
 

  |
87 | 42, 86 | subcld 9986 |
. . . . . . . . . . . . 13
 

    |
88 | 87 | abscld 13498 |
. . . . . . . . . . . 12
 

        |
89 | 85, 88 | sylan2 477 |
. . . . . . . . . . 11
 
             |
90 | 19 | adantr 467 |
. . . . . . . . . . 11
 
       |
91 | 87 | absge0d 13506 |
. . . . . . . . . . . 12
 

        |
92 | 85, 91 | sylan2 477 |
. . . . . . . . . . 11
 
        
    |
93 | | dchrvmasum.2 |
. . . . . . . . . . . 12
          
 
  |
94 | 93 | r19.21bi 2757 |
. . . . . . . . . . 11
 
             |
95 | 75, 89, 90, 92, 94 | letrd 9792 |
. . . . . . . . . 10
 
       |
96 | 95 | ralrimiva 2802 |
. . . . . . . . 9
      
  |
97 | | biidd 241 |
. . . . . . . . . 10
 
   |
98 | 97 | rspcv 3146 |
. . . . . . . . 9
      
    
   |
99 | 74, 96, 98 | mpsyl 65 |
. . . . . . . 8

  |
100 | 99 | adantr 467 |
. . . . . . 7
 

  |
101 | 69, 100 | jca 535 |
. . . . . 6
 

    |
102 | 52 | recnd 9669 |
. . . . . 6
            
        |
103 | 5 | ad2antrr 732 |
. . . . . . 7
            
  |
104 | 103, 16 | remulcld 9671 |
. . . . . 6
            
            |
105 | 4 | ad2antrr 732 |
. . . . . . 7
            
    |
106 | | log1 23535 |
. . . . . . . . 9
     |
107 | 53 | nncnd 10625 |
. . . . . . . . . . . . 13
            
  |
108 | 107 | mulid2d 9661 |
. . . . . . . . . . . 12
            
    |
109 | | rpre 11308 |
. . . . . . . . . . . . . . 15

  |
110 | 109 | adantl 468 |
. . . . . . . . . . . . . 14
 

  |
111 | | fznnfl 12089 |
. . . . . . . . . . . . . 14
         
     |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . 13
 

         
    |
113 | 112 | simplbda 630 |
. . . . . . . . . . . 12
            
  |
114 | 108, 113 | eqbrtrd 4423 |
. . . . . . . . . . 11
            
    |
115 | | 1red 9658 |
. . . . . . . . . . . 12
            
  |
116 | 109 | ad2antlr 733 |
. . . . . . . . . . . 12
            
  |
117 | 115, 116,
57 | lemuldivd 11387 |
. . . . . . . . . . 11
            
  
     |
118 | 114, 117 | mpbid 214 |
. . . . . . . . . 10
            
    |
119 | | 1rp 11306 |
. . . . . . . . . . . 12
 |
120 | 119 | a1i 11 |
. . . . . . . . . . 11
            
  |
121 | 120, 12 | logled 23576 |
. . . . . . . . . 10
            
  
             |
122 | 118, 121 | mpbid 214 |
. . . . . . . . 9
            
            |
123 | 106, 122 | syl5eqbrr 4437 |
. . . . . . . 8
            
        |
124 | | rpregt0 11315 |
. . . . . . . . 9

    |
125 | 124 | ad2antlr 733 |
. . . . . . . 8
            
    |
126 | | divge0 10474 |
. . . . . . . 8
                             |
127 | 14, 123, 125, 126 | syl21anc 1267 |
. . . . . . 7
            
          |
128 | | mulge0 10132 |
. . . . . . 7
  
                   
            |
129 | 105, 16, 127, 128 | syl12anc 1266 |
. . . . . 6
            
            |
130 | | absidm 13386 |
. . . . . . . . 9
         
           |
131 | 51, 130 | syl 17 |
. . . . . . . 8
            
      
           |
132 | 131 | adantr 467 |
. . . . . . 7
   

           
      
           |
133 | | nndivre 10645 |
. . . . . . . . . . . 12
 
     |
134 | 110, 9, 133 | syl2an 480 |
. . . . . . . . . . 11
            
    |
135 | 134 | adantr 467 |
. . . . . . . . . 10
   

           
    |
136 | | simpr 463 |
. . . . . . . . . 10
   

           
    |
137 | | elicopnf 11730 |
. . . . . . . . . . 11
      
         |
138 | 65, 137 | ax-mp 5 |
. . . . . . . . . 10
     
        |
139 | 135, 136,
138 | sylanbrc 670 |
. . . . . . . . 9
   

           
       |
140 | | dchrvmasum.1 |
. . . . . . . . . . 11
 
                    |
141 | 140 | ralrimiva 2802 |
. . . . . . . . . 10
         
 
          |
142 | 141 | ad3antrrr 736 |
. . . . . . . . 9
   

           
        
 
          |
143 | 45 | oveq1d 6305 |
. . . . . . . . . . . 12
   
     |
144 | 143 | fveq2d 5869 |
. . . . . . . . . . 11
            
    |
145 | | fveq2 5865 |
. . . . . . . . . . . . 13
               |
146 | | id 22 |
. . . . . . . . . . . . 13
       |
147 | 145, 146 | oveq12d 6308 |
. . . . . . . . . . . 12
                     |
148 | 147 | oveq2d 6306 |
. . . . . . . . . . 11
   
                     |
149 | 144, 148 | breq12d 4415 |
. . . . . . . . . 10
       
 
           
 
               |
150 | 149 | rspcv 3146 |
. . . . . . . . 9
     
 
                 
      
              |
151 | 139, 142,
150 | sylc 62 |
. . . . . . . 8
   

           
      
             |
152 | 14 | recnd 9669 |
. . . . . . . . . . . . 13
            
        |
153 | | rpcnne0 11319 |
. . . . . . . . . . . . . 14

    |
154 | 153 | ad2antlr 733 |
. . . . . . . . . . . . 13
            
    |
155 | 57 | rpcnne0d 11350 |
. . . . . . . . . . . . 13
            
    |
156 | | divdiv2 10319 |
. . . . . . . . . . . . 13
        
                          |
157 | 152, 154,
155, 156 | syl3anc 1268 |
. . . . . . . . . . . 12
            
                      |
158 | | div23 10289 |
. . . . . . . . . . . . 13
       
                         |
159 | 152, 107,
154, 158 | syl3anc 1268 |
. . . . . . . . . . . 12
            
                      |
160 | 157, 159 | eqtrd 2485 |
. . . . . . . . . . 11
            
                      |
161 | 160 | oveq2d 6306 |
. . . . . . . . . 10
            
                          |
162 | 30 | ad2antrr 732 |
. . . . . . . . . . 11
            
  |
163 | 16 | recnd 9669 |
. . . . . . . . . . 11
            
          |
164 | 162, 163,
107 | mulassd 9666 |
. . . . . . . . . 10
            
 
                        |
165 | 161, 164 | eqtr4d 2488 |
. . . . . . . . 9
            
                          |
166 | 165 | adantr 467 |
. . . . . . . 8
   

           
                          |
167 | 151, 166 | breqtrd 4427 |
. . . . . . 7
   

           
                    |
168 | 132, 167 | eqbrtrd 4423 |
. . . . . 6
   

           
      
                 |
169 | 131 | adantr 467 |
. . . . . . 7
   

           
      
           |
170 | 134 | adantr 467 |
. . . . . . . . 9
   

           
    |
171 | 118 | adantr 467 |
. . . . . . . . 9
   

           
    |
172 | | simpr 463 |
. . . . . . . . 9
   

           
    |
173 | | elico2 11698 |
. . . . . . . . . 10
 
          
  

    |
174 | 24, 71, 173 | mp2an 678 |
. . . . . . . . 9
      
    
     |
175 | 170, 171,
172, 174 | syl3anbrc 1192 |
. . . . . . . 8
   

           
        |
176 | 93 | ad3antrrr 736 |
. . . . . . . 8
   

           
         
 
  |
177 | 144 | breq1d 4412 |
. . . . . . . . 9
       
 
         |
178 | 177 | rspcv 3146 |
. . . . . . . 8
        
        
 
         |
179 | 175, 176,
178 | sylc 62 |
. . . . . . 7
   

           
        |
180 | 169, 179 | eqbrtrd 4423 |
. . . . . 6
   

           
      
     |
181 | 8, 68, 101, 102, 104, 129, 168, 180 | fsumharmonic 23937 |
. . . . 5
 

                 
   
 
                              |
182 | 30 | adantr 467 |
. . . . . . 7
 

  |
183 | 7, 182, 163 | fsummulc2 13845 |
. . . . . 6
 

                                          |
184 | 183 | oveq1d 6305 |
. . . . 5
 

 
                                                            |
185 | 181, 184 | breqtrrd 4429 |
. . . 4
 

                 
   
 
                              |
186 | 41 | leabsd 13476 |
. . . 4
 

 
                                 
                              |
187 | 62, 41, 64, 185, 186 | letrd 9792 |
. . 3
 

                 
   
                                    |
188 | 187 | adantrr 723 |
. 2
 
      
             
   
                                    |
189 | 1, 40, 41, 56, 188 | o1le 13716 |
1
                
         |