Step | Hyp | Ref
| Expression |
1 | | 1red 9683 |
. 2
   |
2 | | elioore 11694 |
. . . . . . . 8
   
  |
3 | 2 | adantl 472 |
. . . . . . 7
 
      |
4 | | chpcl 24099 |
. . . . . . 7
 ψ    |
5 | 3, 4 | syl 17 |
. . . . . 6
 
    ψ    |
6 | 5 | recnd 9694 |
. . . . 5
 
    ψ    |
7 | | fzfid 12217 |
. . . . . . 7
 
              |
8 | 3 | adantr 471 |
. . . . . . . . . 10
               
  |
9 | | elfznn 11856 |
. . . . . . . . . . . 12
           |
10 | 9 | adantl 472 |
. . . . . . . . . . 11
               
  |
11 | 10 | peano2nnd 10653 |
. . . . . . . . . 10
               
    |
12 | 8, 11 | nndivred 10685 |
. . . . . . . . 9
               
      |
13 | | chpcl 24099 |
. . . . . . . . 9
     ψ        |
14 | 12, 13 | syl 17 |
. . . . . . . 8
               
ψ        |
15 | 14, 12 | readdcld 9695 |
. . . . . . 7
               
 ψ             |
16 | 7, 15 | fsumrecl 13848 |
. . . . . 6
 
               ψ             |
17 | 16 | recnd 9694 |
. . . . 5
 
               ψ             |
18 | 3 | recnd 9694 |
. . . . . 6
 
      |
19 | | eliooord 11722 |
. . . . . . . . . 10
   
    |
20 | 19 | adantl 472 |
. . . . . . . . 9
 
    
   |
21 | 20 | simpld 465 |
. . . . . . . 8
 
      |
22 | 3, 21 | rplogcld 23626 |
. . . . . . 7
 
          |
23 | 22 | rpcnd 11371 |
. . . . . 6
 
          |
24 | 18, 23 | mulcld 9688 |
. . . . 5
 
            |
25 | | 1rp 11334 |
. . . . . . . . 9
 |
26 | 25 | a1i 11 |
. . . . . . . 8
 
      |
27 | | 1red 9683 |
. . . . . . . . 9
 
      |
28 | 27, 3, 21 | ltled 9808 |
. . . . . . . 8
 
      |
29 | 3, 26, 28 | rpgecld 11405 |
. . . . . . 7
 
      |
30 | 29 | rpne0d 11374 |
. . . . . 6
 
      |
31 | 22 | rpne0d 11374 |
. . . . . 6
 
          |
32 | 18, 23, 30, 31 | mulne0d 10291 |
. . . . 5
 
            |
33 | 6, 17, 24, 32 | divdird 10448 |
. . . 4
 
      ψ             ψ                     ψ                     ψ                     |
34 | 33 | mpteq2dva 4502 |
. . 3
       ψ             ψ                       
  ψ                     ψ                      |
35 | 29, 22 | rpmulcld 11385 |
. . . . 5
 
            |
36 | 5, 35 | rerpdivcld 11397 |
. . . 4
 
     ψ           |
37 | 16, 35 | rerpdivcld 11397 |
. . . 4
 
                ψ                    |
38 | 6, 18, 23, 30, 31 | divdiv1d 10441 |
. . . . . . 7
 
      ψ         ψ           |
39 | 5, 29 | rerpdivcld 11397 |
. . . . . . . . 9
 
     ψ     |
40 | 39 | recnd 9694 |
. . . . . . . 8
 
     ψ     |
41 | 40, 23, 31 | divrecd 10413 |
. . . . . . 7
 
      ψ          ψ            |
42 | 38, 41 | eqtr3d 2497 |
. . . . . 6
 
     ψ           ψ            |
43 | 42 | mpteq2dva 4502 |
. . . . 5
      ψ                ψ             |
44 | 22 | rprecred 11380 |
. . . . . 6
 
            |
45 | 29 | ex 440 |
. . . . . . . 8
        |
46 | 45 | ssrdv 3449 |
. . . . . . 7
      |
47 | | chpo1ub 24366 |
. . . . . . . 8

 ψ        |
48 | 47 | a1i 11 |
. . . . . . 7
   ψ         |
49 | 46, 48 | o1res2 13675 |
. . . . . 6
      ψ         |
50 | | divlogrlim 23628 |
. . . . . . 7
   
         |
51 | | rlimo1 13728 |
. . . . . . 7
                             |
52 | 50, 51 | mp1i 13 |
. . . . . 6
                 |
53 | 39, 44, 49, 52 | o1mul2 13736 |
. . . . 5
       ψ                |
54 | 43, 53 | eqeltrd 2539 |
. . . 4
      ψ               |
55 | | pntrlog2bndlem2.1 |
. . . . . . . . 9
   |
56 | 55 | rpred 11369 |
. . . . . . . 8
   |
57 | 56, 1 | readdcld 9695 |
. . . . . . 7
     |
58 | 57 | adantr 471 |
. . . . . 6
 
    
   |
59 | 27, 44 | readdcld 9695 |
. . . . . 6
 
              |
60 | | ioossre 11724 |
. . . . . . 7
    |
61 | 57 | recnd 9694 |
. . . . . . 7
     |
62 | | o1const 13731 |
. . . . . . 7
     
              |
63 | 60, 61, 62 | sylancr 674 |
. . . . . 6
             |
64 | | 1cnd 9684 |
. . . . . . . 8
   |
65 | | o1const 13731 |
. . . . . . . 8
                |
66 | 60, 64, 65 | sylancr 674 |
. . . . . . 7
           |
67 | 27, 44, 66, 52 | o1add2 13735 |
. . . . . 6
                   |
68 | 58, 59, 63, 67 | o1mul2 13736 |
. . . . 5
                       |
69 | 58, 59 | remulcld 9696 |
. . . . 5
 
                  |
70 | 37 | recnd 9694 |
. . . . 5
 
                ψ                    |
71 | | chpge0 24101 |
. . . . . . . . . . . 12
     ψ        |
72 | 12, 71 | syl 17 |
. . . . . . . . . . 11
               
ψ        |
73 | 10 | nnrpd 11367 |
. . . . . . . . . . . . 13
               
  |
74 | 25 | a1i 11 |
. . . . . . . . . . . . 13
               
  |
75 | 73, 74 | rpaddcld 11384 |
. . . . . . . . . . . 12
               
    |
76 | 29 | adantr 471 |
. . . . . . . . . . . . 13
               
  |
77 | 76 | rpge0d 11373 |
. . . . . . . . . . . 12
               
  |
78 | 8, 75, 77 | divge0d 11406 |
. . . . . . . . . . 11
               
      |
79 | 14, 12, 72, 78 | addge0d 10216 |
. . . . . . . . . 10
               
 ψ             |
80 | 7, 15, 79 | fsumge0 13903 |
. . . . . . . . 9
 
    
          ψ             |
81 | 16, 35, 80 | divge0d 11406 |
. . . . . . . 8
 
                ψ                    |
82 | 37, 81 | absidd 13532 |
. . . . . . 7
 
                   ψ                               ψ                    |
83 | 69 | recnd 9694 |
. . . . . . . . 9
 
                  |
84 | 83 | abscld 13546 |
. . . . . . . 8
 
                      |
85 | 16, 29 | rerpdivcld 11397 |
. . . . . . . . . 10
 
                ψ              |
86 | 29 | relogcld 23620 |
. . . . . . . . . . . 12
 
          |
87 | 86, 27 | readdcld 9695 |
. . . . . . . . . . 11
 
            |
88 | 58, 87 | remulcld 9696 |
. . . . . . . . . 10
 
                |
89 | 58, 3 | remulcld 9696 |
. . . . . . . . . . . . . 14
 
          |
90 | 10 | nnrecred 10682 |
. . . . . . . . . . . . . . 15
               
    |
91 | 7, 90 | fsumrecl 13848 |
. . . . . . . . . . . . . 14
 
                  |
92 | 89, 91 | remulcld 9696 |
. . . . . . . . . . . . 13
 
                        |
93 | 89, 87 | remulcld 9696 |
. . . . . . . . . . . . 13
 
                  |
94 | 56 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
               
  |
95 | | 1red 9683 |
. . . . . . . . . . . . . . . . . 18
               
  |
96 | 94, 95 | readdcld 9695 |
. . . . . . . . . . . . . . . . 17
               
    |
97 | 96, 8 | remulcld 9696 |
. . . . . . . . . . . . . . . 16
               
 
    |
98 | 97, 90 | remulcld 9696 |
. . . . . . . . . . . . . . 15
               
          |
99 | 97, 11 | nndivred 10685 |
. . . . . . . . . . . . . . . . 17
               
          |
100 | 97, 10 | nndivred 10685 |
. . . . . . . . . . . . . . . . 17
               
        |
101 | 94, 12 | remulcld 9696 |
. . . . . . . . . . . . . . . . . . 19
               
        |
102 | 76, 75 | rpdivcld 11386 |
. . . . . . . . . . . . . . . . . . . 20
               
      |
103 | | pntrlog2bndlem2.2 |
. . . . . . . . . . . . . . . . . . . . 21
  ψ      |
104 | 103 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . 20
               
 ψ 
    |
105 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . . . . . 22
     ψ  ψ        |
106 | | oveq2 6322 |
. . . . . . . . . . . . . . . . . . . . . 22
     
  
      |
107 | 105, 106 | breq12d 4428 |
. . . . . . . . . . . . . . . . . . . . 21
      ψ    ψ       
       |
108 | 107 | rspcv 3157 |
. . . . . . . . . . . . . . . . . . . 20
    
 
ψ  
 ψ       
       |
109 | 102, 104,
108 | sylc 62 |
. . . . . . . . . . . . . . . . . . 19
               
ψ     
        |
110 | 14, 101, 12, 109 | leadd1dd 10254 |
. . . . . . . . . . . . . . . . . 18
               
 ψ          
 
            |
111 | 61 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . 20
               
    |
112 | 18 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
               
  |
113 | 10 | nncnd 10652 |
. . . . . . . . . . . . . . . . . . . . 21
               
  |
114 | | 1cnd 9684 |
. . . . . . . . . . . . . . . . . . . . 21
               
  |
115 | 113, 114 | addcld 9687 |
. . . . . . . . . . . . . . . . . . . 20
               
    |
116 | 11 | nnne0d 10681 |
. . . . . . . . . . . . . . . . . . . 20
               
    |
117 | 111, 112,
115, 116 | divassd 10445 |
. . . . . . . . . . . . . . . . . . 19
               
                  |
118 | 94 | recnd 9694 |
. . . . . . . . . . . . . . . . . . . 20
               
  |
119 | 112, 115,
116 | divcld 10410 |
. . . . . . . . . . . . . . . . . . . 20
               
      |
120 | 118, 114,
119 | adddird 9693 |
. . . . . . . . . . . . . . . . . . 19
               
 
        
             |
121 | 119 | mulid2d 9686 |
. . . . . . . . . . . . . . . . . . . 20
               
            |
122 | 121 | oveq2d 6330 |
. . . . . . . . . . . . . . . . . . 19
               
 
              
           |
123 | 117, 120,
122 | 3eqtrd 2499 |
. . . . . . . . . . . . . . . . . 18
               
          
           |
124 | 110, 123 | breqtrrd 4442 |
. . . . . . . . . . . . . . . . 17
               
 ψ          
          |
125 | 56 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
 
      |
126 | 55 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
 
      |
127 | 126 | rpge0d 11373 |
. . . . . . . . . . . . . . . . . . . . 21
 
      |
128 | 26 | rpge0d 11373 |
. . . . . . . . . . . . . . . . . . . . 21
 
      |
129 | 125, 27, 127, 128 | addge0d 10216 |
. . . . . . . . . . . . . . . . . . . 20
 
        |
130 | 29 | rpge0d 11373 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
131 | 58, 3, 129, 130 | mulge0d 10217 |
. . . . . . . . . . . . . . . . . . 19
 
          |
132 | 131 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
               
      |
133 | 10 | nnred 10651 |
. . . . . . . . . . . . . . . . . . 19
               
  |
134 | 133 | lep1d 10565 |
. . . . . . . . . . . . . . . . . 18
               
    |
135 | 73, 75, 97, 132, 134 | lediv2ad 11391 |
. . . . . . . . . . . . . . . . 17
               
                |
136 | 15, 99, 100, 124, 135 | letrd 9817 |
. . . . . . . . . . . . . . . 16
               
 ψ          
        |
137 | 97 | recnd 9694 |
. . . . . . . . . . . . . . . . 17
               
 
    |
138 | 10 | nnne0d 10681 |
. . . . . . . . . . . . . . . . 17
               
  |
139 | 137, 113,
138 | divrecd 10413 |
. . . . . . . . . . . . . . . 16
               
                |
140 | 136, 139 | breqtrd 4440 |
. . . . . . . . . . . . . . 15
               
 ψ          
          |
141 | 7, 15, 98, 140 | fsumle 13907 |
. . . . . . . . . . . . . 14
 
               ψ                               |
142 | 89 | recnd 9694 |
. . . . . . . . . . . . . . 15
 
          |
143 | 113, 138 | reccld 10403 |
. . . . . . . . . . . . . . 15
               
    |
144 | 7, 142, 143 | fsummulc2 13893 |
. . . . . . . . . . . . . 14
 
                                          |
145 | 141, 144 | breqtrrd 4442 |
. . . . . . . . . . . . 13
 
               ψ                
              |
146 | | harmonicubnd 23983 |
. . . . . . . . . . . . . . 15
                       |
147 | 3, 28, 146 | syl2anc 671 |
. . . . . . . . . . . . . 14
 
               
        |
148 | 91, 87, 89, 131, 147 | lemul2ad 10574 |
. . . . . . . . . . . . 13
 
                                    |
149 | 16, 92, 93, 145, 148 | letrd 9817 |
. . . . . . . . . . . 12
 
               ψ                         |
150 | 61 | adantr 471 |
. . . . . . . . . . . . 13
 
    
   |
151 | 87 | recnd 9694 |
. . . . . . . . . . . . 13
 
            |
152 | 150, 18, 151 | mul32d 9868 |
. . . . . . . . . . . 12
 
                              |
153 | 149, 152 | breqtrd 4440 |
. . . . . . . . . . 11
 
               ψ                         |
154 | 16, 88, 29 | ledivmul2d 11420 |
. . . . . . . . . . 11
 
                 ψ                                 ψ                          |
155 | 153, 154 | mpbird 240 |
. . . . . . . . . 10
 
                ψ                        |
156 | 85, 88, 22, 155 | lediv1dd 11424 |
. . . . . . . . 9
 
                 ψ                                   |
157 | 17, 18, 23, 30, 31 | divdiv1d 10441 |
. . . . . . . . 9
 
                 ψ                  
          ψ                    |
158 | | 1cnd 9684 |
. . . . . . . . . . . 12
 
      |
159 | 23, 158 | addcld 9687 |
. . . . . . . . . . 11
 
            |
160 | 150, 159,
23, 31 | divassd 10445 |
. . . . . . . . . 10
 
                                      |
161 | 23, 158, 23, 31 | divdird 10448 |
. . . . . . . . . . . 12
 
                                    |
162 | 23, 31 | dividd 10408 |
. . . . . . . . . . . . 13
 
                |
163 | 162 | oveq1d 6329 |
. . . . . . . . . . . 12
 
                                |
164 | 161, 163 | eqtr2d 2496 |
. . . . . . . . . . 11
 
                          |
165 | 164 | oveq2d 6330 |
. . . . . . . . . 10
 
                                  |
166 | 160, 165 | eqtr4d 2498 |
. . . . . . . . 9
 
                                  |
167 | 156, 157,
166 | 3brtr3d 4445 |
. . . . . . . 8
 
                ψ                 
 
            |
168 | 69 | leabsd 13524 |
. . . . . . . 8
 
                                  |
169 | 37, 69, 84, 167, 168 | letrd 9817 |
. . . . . . 7
 
                ψ                 
                  |
170 | 82, 169 | eqbrtrd 4436 |
. . . . . 6
 
                   ψ                                     |
171 | 170 | adantrr 728 |
. . . . 5
 
                     ψ                                     |
172 | 1, 68, 69, 70, 171 | o1le 13764 |
. . . 4
                 ψ                        |
173 | 36, 37, 54, 172 | o1add2 13735 |
. . 3
       ψ                     ψ                         |
174 | 34, 173 | eqeltrd 2539 |
. 2
       ψ             ψ                         |
175 | 5, 16 | readdcld 9695 |
. . 3
 
     ψ             ψ              |
176 | 175, 35 | rerpdivcld 11397 |
. 2
 
      ψ             ψ                     |
177 | | pntrlog2bnd.r |
. . . . . . . . . . . 12
  ψ     |
178 | 177 | pntrf 24449 |
. . . . . . . . . . 11
     |
179 | 178 | ffvelrni 6043 |
. . . . . . . . . 10
    
          |
180 | 102, 179 | syl 17 |
. . . . . . . . 9
               
          |
181 | 180 | recnd 9694 |
. . . . . . . 8
               
          |
182 | 76, 73 | rpdivcld 11386 |
. . . . . . . . . 10
               
    |
183 | 178 | ffvelrni 6043 |
. . . . . . . . . 10
  
        |
184 | 182, 183 | syl 17 |
. . . . . . . . 9
               
        |
185 | 184 | recnd 9694 |
. . . . . . . 8
               
        |
186 | 181, 185 | subcld 10011 |
. . . . . . 7
               
            
     |
187 | 186 | abscld 13546 |
. . . . . 6
               
       
              |
188 | 133, 187 | remulcld 9696 |
. . . . 5
               
                        |
189 | 7, 188 | fsumrecl 13848 |
. . . 4
 
                                      |
190 | 189, 35 | rerpdivcld 11397 |
. . 3
 
                       
                      |
191 | 190 | recnd 9694 |
. 2
 
                       
                      |
192 | 73 | rpge0d 11373 |
. . . . . . . 8
               
  |
193 | 186 | absge0d 13554 |
. . . . . . . 8
               
               
      |
194 | 133, 187,
192, 193 | mulge0d 10217 |
. . . . . . 7
               
        
               |
195 | 7, 188, 194 | fsumge0 13903 |
. . . . . 6
 
    
                 
               |
196 | 189, 35, 195 | divge0d 11406 |
. . . . 5
 
                                              |
197 | 190, 196 | absidd 13532 |
. . . 4
 
                                                 
                 
                      |
198 | 6, 17 | addcld 9687 |
. . . . . . 7
 
     ψ             ψ              |
199 | 198, 24, 32 | divcld 10410 |
. . . . . 6
 
      ψ             ψ                     |
200 | 199 | abscld 13546 |
. . . . 5
 
         ψ             ψ                      |
201 | 8, 10 | nndivred 10685 |
. . . . . . . . . . . 12
               
    |
202 | | chpcl 24099 |
. . . . . . . . . . . 12
   ψ      |
203 | 201, 202 | syl 17 |
. . . . . . . . . . 11
               
ψ      |
204 | 203, 201 | readdcld 9695 |
. . . . . . . . . 10
               
 ψ         |
205 | 204, 15 | resubcld 10074 |
. . . . . . . . 9
               
  ψ        ψ              |
206 | 133, 205 | remulcld 9696 |
. . . . . . . 8
               
   ψ 
      ψ               |
207 | 177 | pntrval 24448 |
. . . . . . . . . . . . . . 15
    
         ψ             |
208 | 102, 207 | syl 17 |
. . . . . . . . . . . . . 14
               
         ψ             |
209 | 177 | pntrval 24448 |
. . . . . . . . . . . . . . 15
  
       ψ         |
210 | 182, 209 | syl 17 |
. . . . . . . . . . . . . 14
               
       ψ    
    |
211 | 208, 210 | oveq12d 6332 |
. . . . . . . . . . . . 13
               
            
     ψ 
          ψ          |
212 | 14 | recnd 9694 |
. . . . . . . . . . . . . 14
               
ψ        |
213 | 203 | recnd 9694 |
. . . . . . . . . . . . . 14
               
ψ      |
214 | 112, 113,
138 | divcld 10410 |
. . . . . . . . . . . . . 14
               
    |
215 | 212, 119,
213, 214 | sub4d 10060 |
. . . . . . . . . . . . 13
               
  ψ            ψ    
     ψ 
    ψ                |
216 | 211, 215 | eqtrd 2495 |
. . . . . . . . . . . 12
               
            
     ψ 
    ψ                |
217 | 216 | fveq2d 5891 |
. . . . . . . . . . 11
               
       
                 ψ 
    ψ                 |
218 | 212, 213 | subcld 10011 |
. . . . . . . . . . . 12
               
 ψ      ψ       |
219 | 119, 214 | subcld 10011 |
. . . . . . . . . . . 12
               
          |
220 | 218, 219 | abs2dif2d 13568 |
. . . . . . . . . . 11
               
     ψ 
    ψ                    ψ      ψ                     |
221 | 217, 220 | eqbrtrd 4436 |
. . . . . . . . . 10
               
       
           
     ψ 
    ψ                     |
222 | 73, 75, 8, 77, 134 | lediv2ad 11391 |
. . . . . . . . . . . . . 14
               
        |
223 | | chpwordi 24132 |
. . . . . . . . . . . . . 14
      
 
  
   ψ      ψ      |
224 | 12, 201, 222, 223 | syl3anc 1276 |
. . . . . . . . . . . . 13
               
ψ     
ψ      |
225 | 14, 203, 224 | abssuble0d 13542 |
. . . . . . . . . . . 12
               
    ψ      ψ 
     ψ 
  ψ         |
226 | 12, 201, 222 | abssuble0d 13542 |
. . . . . . . . . . . 12
               
                      |
227 | 225, 226 | oveq12d 6332 |
. . . . . . . . . . 11
               
     ψ 
    ψ                     ψ    ψ 
                |
228 | 213, 214,
212, 119 | addsub4d 10058 |
. . . . . . . . . . 11
               
  ψ        ψ              ψ    ψ                  |
229 | 227, 228 | eqtr4d 2498 |
. . . . . . . . . 10
               
     ψ 
    ψ                     ψ        ψ 
            |
230 | 221, 229 | breqtrd 4440 |
. . . . . . . . 9
               
       
           
  ψ        ψ              |
231 | 187, 205,
133, 192, 230 | lemul2ad 10574 |
. . . . . . . 8
               
                         ψ        ψ               |
232 | 7, 188, 206, 231 | fsumle 13907 |
. . . . . . 7
 
                                                 ψ        ψ               |
233 | 205 | recnd 9694 |
. . . . . . . . . 10
               
  ψ        ψ              |
234 | 113, 233 | mulcld 9688 |
. . . . . . . . 9
               
   ψ 
      ψ               |
235 | 7, 234 | fsumcl 13847 |
. . . . . . . 8
 
                 ψ        ψ 
             |
236 | 6, 17 | negdi2d 10025 |
. . . . . . . . . 10
 
      ψ             ψ              ψ             ψ              |
237 | 29 | rprege0d 11376 |
. . . . . . . . . . . . . . . . . . . . 21
 
        |
238 | | flge0nn0 12085 |
. . . . . . . . . . . . . . . . . . . . 21
         |
239 | | nn0p1nn 10937 |
. . . . . . . . . . . . . . . . . . . . 21
    
        |
240 | 237, 238,
239 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
 
            |
241 | 3, 240 | nndivred 10685 |
. . . . . . . . . . . . . . . . . . 19
 
              |
242 | | 2re 10706 |
. . . . . . . . . . . . . . . . . . . 20
 |
243 | 242 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
      |
244 | | flltp1 12067 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
245 | 3, 244 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
            |
246 | 240 | nncnd 10652 |
. . . . . . . . . . . . . . . . . . . . . 22
 
            |
247 | 246 | mulid1d 9685 |
. . . . . . . . . . . . . . . . . . . . 21
 
                    |
248 | 245, 247 | breqtrrd 4442 |
. . . . . . . . . . . . . . . . . . . 20
 
              |
249 | 240 | nnrpd 11367 |
. . . . . . . . . . . . . . . . . . . . 21
 
            |
250 | 3, 27, 249 | ltdivmuld 11417 |
. . . . . . . . . . . . . . . . . . . 20
 
                        |
251 | 248, 250 | mpbird 240 |
. . . . . . . . . . . . . . . . . . 19
 
              |
252 | | 1lt2 10804 |
. . . . . . . . . . . . . . . . . . . 20
 |
253 | 252 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
      |
254 | 241, 27, 243, 251, 253 | lttrd 9821 |
. . . . . . . . . . . . . . . . . 18
 
              |
255 | | chpeq0 24184 |
. . . . . . . . . . . . . . . . . . 19
          ψ         
           |
256 | 241, 255 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
     ψ         
           |
257 | 254, 256 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
 
    ψ            |
258 | 257 | oveq1d 6329 |
. . . . . . . . . . . . . . . 16
 
     ψ                               |
259 | 241 | recnd 9694 |
. . . . . . . . . . . . . . . . 17
 
              |
260 | 259 | addid2d 9859 |
. . . . . . . . . . . . . . . 16
 
                        |
261 | 258, 260 | eqtrd 2495 |
. . . . . . . . . . . . . . 15
 
     ψ                             |
262 | 261 | oveq2d 6330 |
. . . . . . . . . . . . . 14
 
            ψ                                      |
263 | 240 | nnne0d 10681 |
. . . . . . . . . . . . . . 15
 
            |
264 | 18, 246, 263 | divcan2d 10412 |
. . . . . . . . . . . . . 14
 
                      |
265 | 262, 264 | eqtrd 2495 |
. . . . . . . . . . . . 13
 
            ψ                      |
266 | 18 | div1d 10402 |
. . . . . . . . . . . . . . . . 17
 
        |
267 | 266 | fveq2d 5891 |
. . . . . . . . . . . . . . . 16
 
    ψ    ψ    |
268 | 267, 266 | oveq12d 6332 |
. . . . . . . . . . . . . . 15
 
     ψ        ψ     |
269 | 268 | oveq2d 6330 |
. . . . . . . . . . . . . 14
 
      ψ          ψ      |
270 | 5, 3 | readdcld 9695 |
. . . . . . . . . . . . . . . 16
 
     ψ     |
271 | 270 | recnd 9694 |
. . . . . . . . . . . . . . 15
 
     ψ     |
272 | 271 | mulid2d 9686 |
. . . . . . . . . . . . . 14
 
      ψ     ψ     |
273 | 269, 272 | eqtrd 2495 |
. . . . . . . . . . . . 13
 
      ψ         ψ     |
274 | 265, 273 | oveq12d 6332 |
. . . . . . . . . . . 12
 
             ψ                      ψ           ψ      |
275 | 271, 18 | negsubdi2d 10027 |
. . . . . . . . . . . 12
 
       ψ      ψ      |
276 | 6, 18 | pncand 10012 |
. . . . . . . . . . . . 13
 
      ψ    ψ    |
277 | 276 | negeqd 9894 |
. . . . . . . . . . . 12
 
       ψ     ψ    |
278 | 274, 275,
277 | 3eqtr2d 2501 |
. . . . . . . . . . 11
 
             ψ                      ψ          ψ    |
279 | 3 | flcld 12065 |
. . . . . . . . . . . . . 14
 
          |
280 | | fzval3 12013 |
. . . . . . . . . . . . . 14
              ..^         |
281 | 279, 280 | syl 17 |
. . . . . . . . . . . . 13
 
             ..^         |
282 | 281 | eqcomd 2467 |
. . . . . . . . . . . 12
 
     ..^                 |
283 | 113, 114 | pncan2d 10013 |
. . . . . . . . . . . . . 14
               
      |
284 | 283 | oveq1d 6329 |
. . . . . . . . . . . . 13
               
      ψ 
            ψ              |
285 | 15 | recnd 9694 |
. . . . . . . . . . . . . 14
               
 ψ             |
286 | 285 | mulid2d 9686 |
. . . . . . . . . . . . 13
               
  ψ 
           ψ             |
287 | 284, 286 | eqtrd 2495 |
. . . . . . . . . . . 12
               
      ψ 
           ψ             |
288 | 282, 287 | sumeq12rdv 13821 |
. . . . . . . . . . 11
 
      ..^              ψ                       ψ             |
289 | 278, 288 | oveq12d 6332 |
. . . . . . . . . 10
 
              ψ                      ψ 
         ..^              ψ 
             ψ             ψ              |
290 | | oveq2 6322 |
. . . . . . . . . . . . . . 15
       |
291 | 290 | fveq2d 5891 |
. . . . . . . . . . . . . 14
 ψ    ψ      |
292 | 291, 290 | oveq12d 6332 |
. . . . . . . . . . . . 13
  ψ        ψ         |
293 | 292 | ancli 558 |
. . . . . . . . . . . 12
   ψ        ψ          |
294 | | oveq2 6322 |
. . . . . . . . . . . . . . 15
           |
295 | 294 | fveq2d 5891 |
. . . . . . . . . . . . . 14
   ψ    ψ        |
296 | 295, 294 | oveq12d 6332 |
. . . . . . . . . . . . 13
    ψ        ψ             |
297 | 296 | ancli 558 |
. . . . . . . . . . . 12
       ψ        ψ              |
298 | | oveq2 6322 |
. . . . . . . . . . . . . . 15
       |
299 | 298 | fveq2d 5891 |
. . . . . . . . . . . . . 14
 ψ    ψ      |
300 | 299, 298 | oveq12d 6332 |
. . . . . . . . . . . . 13
  ψ        ψ         |
301 | 300 | ancli 558 |
. . . . . . . . . . . 12
   ψ        ψ 
        |
302 | | oveq2 6322 |
. . . . . . . . . . . . . . 15
                   |
303 | 302 | fveq2d 5891 |
. . . . . . . . . . . . . 14
       ψ    ψ            |
304 | 303, 302 | oveq12d 6332 |
. . . . . . . . . . . . 13
        ψ        ψ                     |
305 | 304 | ancli 558 |
. . . . . . . . . . . 12
               ψ        ψ                      |
306 | | nnuz 11222 |
. . . . . . . . . . . . 13
     |
307 | 240, 306 | syl6eleq 2549 |
. . . . . . . . . . . 12
 
                |
308 | | elfznn 11856 |
. . . . . . . . . . . . . 14
             |
309 | 308 | adantl 472 |
. . . . . . . . . . . . 13
                    |
310 | 309 | nncnd 10652 |
. . . . . . . . . . . 12
                    |
311 | 3 | adantr 471 |
. . . . . . . . . . . . . . . 16
                    |
312 | 311, 309 | nndivred 10685 |
. . . . . . . . . . . . . . 15
                      |
313 | | chpcl 24099 |
. . . . . . . . . . . . . . 15
   ψ      |
314 | 312, 313 | syl 17 |
. . . . . . . . . . . . . 14
                  ψ      |
315 | 314, 312 | readdcld 9695 |
. . . . . . . . . . . . 13
                   ψ         |
316 | 315 | recnd 9694 |
. . . . . . . . . . . 12
                   ψ         |
317 | 293, 297,
301, 305, 307, 310, 316 | fsumparts 13914 |
. . . . . . . . . . 11
 
      ..^           ψ            ψ 
                 ψ 
                    ψ           ..^              ψ 
             |
318 | 213, 214 | addcld 9687 |
. . . . . . . . . . . . . . 15
               
 ψ         |
319 | 212, 119 | addcld 9687 |
. . . . . . . . . . . . . . 15
               
 ψ             |
320 | 318, 319 | negsubdi2d 10027 |
. . . . . . . . . . . . . 14
               
   ψ        ψ              ψ            ψ          |
321 | 320 | oveq2d 6330 |
. . . . . . . . . . . . 13
               
    ψ        ψ                ψ            ψ 
         |
322 | 113, 233 | mulneg2d 10099 |
. . . . . . . . . . . . 13
               
    ψ        ψ                 ψ 
      ψ               |
323 | 321, 322 | eqtr3d 2497 |
. . . . . . . . . . . 12
               
   ψ 
          ψ             ψ 
      ψ               |
324 | 282, 323 | sumeq12rdv 13821 |
. . . . . . . . . . 11
 
      ..^           ψ            ψ 
       
          
  ψ        ψ 
             |
325 | 317, 324 | eqtr3d 2497 |
. . . . . . . . . 10
 
              ψ                      ψ 
         ..^              ψ 
           
          
  ψ        ψ 
             |
326 | 236, 289,
325 | 3eqtr2d 2501 |
. . . . . . . . 9
 
      ψ    |