Proof of Theorem pntrlog2bndlem5
Step | Hyp | Ref
| Expression |
1 | | elioore 11673 |
. . . . . . . . . . . . 13
   
  |
2 | 1 | adantl 468 |
. . . . . . . . . . . 12
 
      |
3 | | 1rp 11313 |
. . . . . . . . . . . . 13
 |
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
 
      |
5 | | 1red 9663 |
. . . . . . . . . . . . 13
 
      |
6 | | eliooord 11701 |
. . . . . . . . . . . . . . 15
   
    |
7 | 6 | adantl 468 |
. . . . . . . . . . . . . 14
 
    
   |
8 | 7 | simpld 461 |
. . . . . . . . . . . . 13
 
      |
9 | 5, 2, 8 | ltled 9788 |
. . . . . . . . . . . 12
 
      |
10 | 2, 4, 9 | rpgecld 11384 |
. . . . . . . . . . 11
 
      |
11 | | pntrlog2bnd.r |
. . . . . . . . . . . . 13
  ψ     |
12 | 11 | pntrf 24413 |
. . . . . . . . . . . 12
     |
13 | 12 | ffvelrni 6026 |
. . . . . . . . . . 11

      |
14 | 10, 13 | syl 17 |
. . . . . . . . . 10
 
          |
15 | 14 | recnd 9674 |
. . . . . . . . 9
 
          |
16 | 15 | abscld 13510 |
. . . . . . . 8
 
              |
17 | 16 | recnd 9674 |
. . . . . . 7
 
              |
18 | 10 | relogcld 23584 |
. . . . . . . 8
 
          |
19 | 18 | recnd 9674 |
. . . . . . 7
 
          |
20 | 17, 19 | mulcld 9668 |
. . . . . 6
 
                    |
21 | | 2cnd 10689 |
. . . . . . . 8
 
      |
22 | 2, 8 | rplogcld 23590 |
. . . . . . . . 9
 
          |
23 | 22 | rpne0d 11353 |
. . . . . . . 8
 
          |
24 | 21, 19, 23 | divcld 10390 |
. . . . . . 7
 
            |
25 | | fzfid 12193 |
. . . . . . . 8
 
              |
26 | 10 | adantr 467 |
. . . . . . . . . . . . . 14
               
  |
27 | | elfznn 11835 |
. . . . . . . . . . . . . . . 16
           |
28 | 27 | adantl 468 |
. . . . . . . . . . . . . . 15
               
  |
29 | 28 | nnrpd 11346 |
. . . . . . . . . . . . . 14
               
  |
30 | 26, 29 | rpdivcld 11365 |
. . . . . . . . . . . . 13
               
    |
31 | 12 | ffvelrni 6026 |
. . . . . . . . . . . . 13
  
        |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
               
        |
33 | 32 | recnd 9674 |
. . . . . . . . . . 11
               
        |
34 | 33 | abscld 13510 |
. . . . . . . . . 10
               
            |
35 | 29 | relogcld 23584 |
. . . . . . . . . . 11
               
      |
36 | | 1red 9663 |
. . . . . . . . . . 11
               
  |
37 | 35, 36 | readdcld 9675 |
. . . . . . . . . 10
               
        |
38 | 34, 37 | remulcld 9676 |
. . . . . . . . 9
               
       
            |
39 | 38 | recnd 9674 |
. . . . . . . 8
               
       
            |
40 | 25, 39 | fsumcl 13811 |
. . . . . . 7
 
                                  |
41 | 24, 40 | mulcld 9668 |
. . . . . 6
 
                                          |
42 | 20, 41 | subcld 9991 |
. . . . 5
 
                                                          |
43 | 34 | recnd 9674 |
. . . . . . 7
               
            |
44 | 25, 43 | fsumcl 13811 |
. . . . . 6
 
                          |
45 | 24, 44 | mulcld 9668 |
. . . . 5
 
                                  |
46 | 2 | recnd 9674 |
. . . . 5
 
      |
47 | 10 | rpne0d 11353 |
. . . . 5
 
      |
48 | 42, 45, 46, 47 | divdird 10428 |
. . . 4
 
                                                                                                                                                                                |
49 | 16, 18 | remulcld 9676 |
. . . . . . . 8
 
                    |
50 | 49 | recnd 9674 |
. . . . . . 7
 
                    |
51 | 50, 41, 45 | subsubd 10019 |
. . . . . 6
 
                                                                                                                                                                          |
52 | 24, 40, 44 | subdid 10081 |
. . . . . . . 8
 
                                                                      
                                                           |
53 | 25, 39, 43 | fsumsub 13861 |
. . . . . . . . . 10
 
                                                                                                |
54 | 37 | recnd 9674 |
. . . . . . . . . . . . 13
               
        |
55 | | 1cnd 9664 |
. . . . . . . . . . . . 13
               
  |
56 | 43, 54, 55 | subdid 10081 |
. . . . . . . . . . . 12
               
       
                                              |
57 | 35 | recnd 9674 |
. . . . . . . . . . . . . 14
               
      |
58 | 57, 55 | pncand 9992 |
. . . . . . . . . . . . 13
               
              |
59 | 58 | oveq2d 6311 |
. . . . . . . . . . . 12
               
       
                              |
60 | 43 | mulid1d 9665 |
. . . . . . . . . . . . 13
               
       
                |
61 | 60 | oveq2d 6311 |
. . . . . . . . . . . 12
               
                                                         
      |
62 | 56, 59, 61 | 3eqtr3rd 2496 |
. . . . . . . . . . 11
               
                         
                      |
63 | 62 | sumeq2dv 13781 |
. . . . . . . . . 10
 
                                            
                           |
64 | 53, 63 | eqtr3d 2489 |
. . . . . . . . 9
 
                                                      
                           |
65 | 64 | oveq2d 6311 |
. . . . . . . 8
 
                                                                                                  |
66 | 52, 65 | eqtr3d 2489 |
. . . . . . 7
 
                                                                                                          |
67 | 66 | oveq2d 6311 |
. . . . . 6
 
                                                                                                                                          |
68 | 51, 67 | eqtr3d 2489 |
. . . . 5
 
                                                                                                                                          |
69 | 68 | oveq1d 6310 |
. . . 4
 
                                                                                                                                              |
70 | 48, 69 | eqtr3d 2489 |
. . 3
 
                                                                                                                                                |
71 | 70 | mpteq2dva 4492 |
. 2
                                                                                                                                                       |
72 | | 2re 10686 |
. . . . . . . 8
 |
73 | 72 | a1i 11 |
. . . . . . 7
 
      |
74 | 73, 22 | rerpdivcld 11376 |
. . . . . 6
 
            |
75 | 25, 38 | fsumrecl 13812 |
. . . . . 6
 
                                  |
76 | 74, 75 | remulcld 9676 |
. . . . 5
 
                                          |
77 | 49, 76 | resubcld 10054 |
. . . 4
 
                                                          |
78 | 77, 10 | rerpdivcld 11376 |
. . 3
 
                                                            |
79 | 25, 34 | fsumrecl 13812 |
. . . . 5
 
                          |
80 | 74, 79 | remulcld 9676 |
. . . 4
 
                                  |
81 | 80, 10 | rerpdivcld 11376 |
. . 3
 
                                    |
82 | | 1red 9663 |
. . . 4
   |
83 | | pntsval.1 |
. . . . . 6
            Λ       ψ        |
84 | | pntrlog2bnd.t |
. . . . . 6
              |
85 | 83, 11, 84 | pntrlog2bndlem4 24430 |
. . . . 5
   
                                                                  |
86 | 85 | a1i 11 |
. . . 4
                                                                        |
87 | 28 | nnred 10631 |
. . . . . . . . . . 11
               
  |
88 | | simpl 459 |
. . . . . . . . . . . . . . 15
 
   |
89 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
   |
90 | 89 | relogcld 23584 |
. . . . . . . . . . . . . . 15
 
       |
91 | 88, 90 | remulcld 9676 |
. . . . . . . . . . . . . 14
 
         |
92 | | 0red 9649 |
. . . . . . . . . . . . . 14
 
   |
93 | 91, 92 | ifclda 3915 |
. . . . . . . . . . . . 13
              |
94 | 84, 93 | fmpti 6050 |
. . . . . . . . . . . 12
     |
95 | 94 | ffvelrni 6026 |
. . . . . . . . . . 11
       |
96 | 87, 95 | syl 17 |
. . . . . . . . . 10
               
      |
97 | 87, 36 | resubcld 10054 |
. . . . . . . . . . 11
               
    |
98 | 94 | ffvelrni 6026 |
. . . . . . . . . . 11
           |
99 | 97, 98 | syl 17 |
. . . . . . . . . 10
               
        |
100 | 96, 99 | resubcld 10054 |
. . . . . . . . 9
               
        
     |
101 | 34, 100 | remulcld 9676 |
. . . . . . . 8
               
       
                  |
102 | 25, 101 | fsumrecl 13812 |
. . . . . . 7
 
                                        |
103 | 74, 102 | remulcld 9676 |
. . . . . 6
 
                                                |
104 | 49, 103 | resubcld 10054 |
. . . . 5
 
                                                                |
105 | 104, 10 | rerpdivcld 11376 |
. . . 4
 
                                                                  |
106 | | 2rp 11314 |
. . . . . . . . . . 11
 |
107 | 106 | a1i 11 |
. . . . . . . . . 10
 
      |
108 | 107 | rpge0d 11352 |
. . . . . . . . 9
 
      |
109 | 73, 22, 108 | divge0d 11385 |
. . . . . . . 8
 
            |
110 | 33 | absge0d 13518 |
. . . . . . . . . 10
               
            |
111 | 29 | adantr 467 |
. . . . . . . . . . . . . . . 16
   
                |
112 | 111 | rpcnd 11350 |
. . . . . . . . . . . . . . 15
   
                |
113 | 57 | adantr 467 |
. . . . . . . . . . . . . . 15
   
                    |
114 | 112, 113 | mulcld 9668 |
. . . . . . . . . . . . . 14
   
                      |
115 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
   
                |
116 | | 1re 9647 |
. . . . . . . . . . . . . . . . . . 19
 |
117 | 111 | rpred 11348 |
. . . . . . . . . . . . . . . . . . 19
   
                |
118 | | difrp 11344 |
. . . . . . . . . . . . . . . . . . 19
 
       |
119 | 116, 117,
118 | sylancr 670 |
. . . . . . . . . . . . . . . . . 18
   
              
     |
120 | 115, 119 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
   
                  |
121 | 120 | relogcld 23584 |
. . . . . . . . . . . . . . . 16
   
                      |
122 | 121 | recnd 9674 |
. . . . . . . . . . . . . . 15
   
                      |
123 | 112, 122 | mulcld 9668 |
. . . . . . . . . . . . . 14
   
                        |
124 | 114, 123,
122 | subsubd 10019 |
. . . . . . . . . . . . 13
   
                                                                |
125 | | rpre 11315 |
. . . . . . . . . . . . . . . . 17

  |
126 | | eleq1 2519 |
. . . . . . . . . . . . . . . . . . 19
 
   |
127 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
   |
128 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . 20
           |
129 | 127, 128 | oveq12d 6313 |
. . . . . . . . . . . . . . . . . . 19
               |
130 | 126, 129 | ifbieq1d 3906 |
. . . . . . . . . . . . . . . . . 18
                         |
131 | | ovex 6323 |
. . . . . . . . . . . . . . . . . . 19
       |
132 | | c0ex 9642 |
. . . . . . . . . . . . . . . . . . 19
 |
133 | 131, 132 | ifex 3951 |
. . . . . . . . . . . . . . . . . 18
            |
134 | 130, 84, 133 | fvmpt 5953 |
. . . . . . . . . . . . . . . . 17
                  |
135 | 125, 134 | syl 17 |
. . . . . . . . . . . . . . . 16

                 |
136 | | iftrue 3889 |
. . . . . . . . . . . . . . . 16

                   |
137 | 135, 136 | eqtrd 2487 |
. . . . . . . . . . . . . . 15

            |
138 | 111, 137 | syl 17 |
. . . . . . . . . . . . . 14
   
                          |
139 | | rpre 11315 |
. . . . . . . . . . . . . . . . . 18
  
    |
140 | | eleq1 2519 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
141 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
       |
142 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . 21
               |
143 | 141, 142 | oveq12d 6313 |
. . . . . . . . . . . . . . . . . . . 20
                     |
144 | 140, 143 | ifbieq1d 3906 |
. . . . . . . . . . . . . . . . . . 19
                                 |
145 | | ovex 6323 |
. . . . . . . . . . . . . . . . . . . 20
           |
146 | 145, 132 | ifex 3951 |
. . . . . . . . . . . . . . . . . . 19
                  |
147 | 144, 84, 146 | fvmpt 5953 |
. . . . . . . . . . . . . . . . . 18
                            |
148 | 139, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
  
                         |
149 | | iftrue 3889 |
. . . . . . . . . . . . . . . . 17
  
                             |
150 | 148, 149 | eqtrd 2487 |
. . . . . . . . . . . . . . . 16
  
                  |
151 | 120, 150 | syl 17 |
. . . . . . . . . . . . . . 15
   
                                |
152 | | 1cnd 9664 |
. . . . . . . . . . . . . . . 16
   
                |
153 | 112, 152,
122 | subdird 10082 |
. . . . . . . . . . . . . . 15
   
                                            |
154 | 122 | mulid2d 9666 |
. . . . . . . . . . . . . . . 16
   
                              |
155 | 154 | oveq2d 6311 |
. . . . . . . . . . . . . . 15
   
                                                  |
156 | 151, 153,
155 | 3eqtrd 2491 |
. . . . . . . . . . . . . 14
   
                                      |
157 | 138, 156 | oveq12d 6313 |
. . . . . . . . . . . . 13
   
                                                    |
158 | 112, 113,
122 | subdid 10081 |
. . . . . . . . . . . . . 14
   
                                              |
159 | 158 | oveq1d 6310 |
. . . . . . . . . . . . 13
   
                                                              |
160 | 124, 157,
159 | 3eqtr4d 2497 |
. . . . . . . . . . . 12
   
                                                  |
161 | 111 | relogcld 23584 |
. . . . . . . . . . . . . . . . . 18
   
                    |
162 | 161, 121 | resubcld 10054 |
. . . . . . . . . . . . . . . . 17
   
                            |
163 | 162 | recnd 9674 |
. . . . . . . . . . . . . . . 16
   
                            |
164 | 112, 152,
163 | subdird 10082 |
. . . . . . . . . . . . . . 15
   
                                                              |
165 | 163 | mulid2d 9666 |
. . . . . . . . . . . . . . . 16
   
                                          |
166 | 165 | oveq2d 6311 |
. . . . . . . . . . . . . . 15
   
                                                                          |
167 | 117, 162 | remulcld 9676 |
. . . . . . . . . . . . . . . . 17
   
                              |
168 | 167 | recnd 9674 |
. . . . . . . . . . . . . . . 16
   
                              |
169 | 168, 113,
122 | subsub3d 10021 |
. . . . . . . . . . . . . . 15
   
                                                                        |
170 | 164, 166,
169 | 3eqtrd 2491 |
. . . . . . . . . . . . . 14
   
                                                            |
171 | 112, 152 | npcand 9995 |
. . . . . . . . . . . . . . . . . 18
   
                    |
172 | 171 | fveq2d 5874 |
. . . . . . . . . . . . . . . . 17
   
                            |
173 | 172 | oveq1d 6310 |
. . . . . . . . . . . . . . . 16
   
                                            |
174 | | logdifbnd 23931 |
. . . . . . . . . . . . . . . . 17
  
                      |
175 | 120, 174 | syl 17 |
. . . . . . . . . . . . . . . 16
   
                                    |
176 | 173, 175 | eqbrtrrd 4428 |
. . . . . . . . . . . . . . 15
   
                                |
177 | | 1red 9663 |
. . . . . . . . . . . . . . . 16
   
                |
178 | 162, 177,
120 | lemuldiv2d 11395 |
. . . . . . . . . . . . . . 15
   
                              
           
       |
179 | 176, 178 | mpbird 236 |
. . . . . . . . . . . . . 14
   
                                |
180 | 170, 179 | eqbrtrrd 4428 |
. . . . . . . . . . . . 13
   
                                            |
181 | 167, 121 | readdcld 9675 |
. . . . . . . . . . . . . 14
   
                                      |
182 | 181, 161,
177 | lesubadd2d 10219 |
. . . . . . . . . . . . 13
   
                                          
                               |
183 | 180, 182 | mpbid 214 |
. . . . . . . . . . . 12
   
                                            |
184 | 160, 183 | eqbrtrd 4426 |
. . . . . . . . . . 11
   
                                  |
185 | | fveq2 5870 |
. . . . . . . . . . . . . . . . 17
           |
186 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
187 | 186, 3 | syl6eqel 2539 |
. . . . . . . . . . . . . . . . . . . . 21
   |
188 | 187 | iftrued 3891 |
. . . . . . . . . . . . . . . . . . . 20
                    |
189 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
190 | | log1 23547 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
191 | 189, 190 | syl6eq 2503 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
192 | 186, 191 | oveq12d 6313 |
. . . . . . . . . . . . . . . . . . . . 21
           |
193 | | ax-1cn 9602 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
194 | 193 | mul01i 9828 |
. . . . . . . . . . . . . . . . . . . . 21
   |
195 | 192, 194 | syl6eq 2503 |
. . . . . . . . . . . . . . . . . . . 20
         |
196 | 188, 195 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . 19
              |
197 | 196, 84, 132 | fvmpt 5953 |
. . . . . . . . . . . . . . . . . 18
       |
198 | 116, 197 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     |
199 | 185, 198 | syl6eq 2503 |
. . . . . . . . . . . . . . . 16
       |
200 | | oveq1 6302 |
. . . . . . . . . . . . . . . . . . 19
       |
201 | | 1m1e0 10685 |
. . . . . . . . . . . . . . . . . . 19
   |
202 | 200, 201 | syl6eq 2503 |
. . . . . . . . . . . . . . . . . 18
     |
203 | 202 | fveq2d 5874 |
. . . . . . . . . . . . . . . . 17
             |
204 | | 0re 9648 |
. . . . . . . . . . . . . . . . . 18
 |
205 | | rpne0 11324 |
. . . . . . . . . . . . . . . . . . . . 21

  |
206 | 205 | necon2bi 2656 |
. . . . . . . . . . . . . . . . . . . 20

  |
207 | 206 | iffalsed 3894 |
. . . . . . . . . . . . . . . . . . 19
              |
208 | 207, 84, 132 | fvmpt 5953 |
. . . . . . . . . . . . . . . . . 18
       |
209 | 204, 208 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     |
210 | 203, 209 | syl6eq 2503 |
. . . . . . . . . . . . . . . 16
         |
211 | 199, 210 | oveq12d 6313 |
. . . . . . . . . . . . . . 15
                 |
212 | | 0m0e0 10726 |
. . . . . . . . . . . . . . 15
   |
213 | 211, 212 | syl6eq 2503 |
. . . . . . . . . . . . . 14
               |
214 | 213 | eqcoms 2461 |
. . . . . . . . . . . . 13
               |
215 | 214 | adantl 468 |
. . . . . . . . . . . 12
   
                            |
216 | | 0red 9649 |
. . . . . . . . . . . . . 14
               
  |
217 | 28 | nnge1d 10659 |
. . . . . . . . . . . . . . 15
               
  |
218 | 87, 217 | logge0d 23591 |
. . . . . . . . . . . . . 14
               
      |
219 | 35 | lep1d 10545 |
. . . . . . . . . . . . . 14
               
            |
220 | 216, 35, 37, 218, 219 | letrd 9797 |
. . . . . . . . . . . . 13
               
        |
221 | 220 | adantr 467 |
. . . . . . . . . . . 12
   
                      |
222 | 215, 221 | eqbrtrd 4426 |
. . . . . . . . . . 11
   
                                  |
223 | | elfzle1 11809 |
. . . . . . . . . . . . 13
           |
224 | 223 | adantl 468 |
. . . . . . . . . . . 12
               
  |
225 | 36, 87 | leloed 9783 |
. . . . . . . . . . . 12
               

     |
226 | 224, 225 | mpbid 214 |
. . . . . . . . . . 11
               
    |
227 | 184, 222,
226 | mpjaodan 796 |
. . . . . . . . . 10
               
        
           |
228 | 100, 37, 34, 110, 227 | lemul2ad 10554 |
. . . . . . . . 9
               
       
                                    |
229 | 25, 101, 38, 228 | fsumle 13871 |
. . . . . . . 8
 
                                                                    |
230 | 102, 75, 74, 109, 229 | lemul2ad 10554 |
. . . . . . 7
 
                                                                                    |
231 | 103, 76, 49, 230 | lesub2dd 10237 |
. . . . . 6
 
                                                                                                                    |
232 | 77, 104, 10, 231 | lediv1dd 11403 |
. . . . 5
 
                                                                                                                        |
233 | 232 | adantrr 724 |
. . . 4
 
                                                                                                                          |
234 | 82, 86, 105, 78, 233 | lo1le 13727 |
. . 3
                                                                  |
235 | 106 | a1i 11 |
. . . . . . . 8
   |
236 | | pntrlog2bndlem5.1 |
. . . . . . . 8
   |
237 | 235, 236 | rpmulcld 11364 |
. . . . . . 7
     |
238 | 237 | rpred 11348 |
. . . . . 6
     |
239 | 238 | adantr 467 |
. . . . 5
 
        |
240 | 5, 22 | rerpdivcld 11376 |
. . . . . 6
 
            |
241 | 5, 240 | readdcld 9675 |
. . . . 5
 
              |
242 | | ioossre 11703 |
. . . . . 6
    |
243 | | lo1const 13696 |
. . . . . 6
                     |
244 | 242, 238,
243 | sylancr 670 |
. . . . 5
              |
245 | | lo1const 13696 |
. . . . . . 7
                 |
246 | 242, 82, 245 | sylancr 670 |
. . . . . 6
            |
247 | | divlogrlim 23592 |
. . . . . . . 8
   
         |
248 | | rlimo1 13692 |
. . . . . . . 8
                             |
249 | 247, 248 | mp1i 13 |
. . . . . . 7
                 |
250 | 240, 249 | o1lo1d 13615 |
. . . . . 6
                  |
251 | 5, 240, 246, 250 | lo1add 13702 |
. . . . 5
                    |
252 | 237 | adantr 467 |
. . . . . 6
 
        |
253 | 252 | rpge0d 11352 |
. . . . 5
 
        |
254 | 239, 241,
244, 251, 253 | lo1mul 13703 |
. . . 4
                        |
255 | 239, 241 | remulcld 9676 |
. . . 4
 
                  |
256 | 79, 10 | rerpdivcld 11376 |
. . . . . . 7
 
                            |
257 | 18, 5 | readdcld 9675 |
. . . . . . . 8
 
            |
258 | 236 | adantr 467 |
. . . . . . . . 9
 
      |
259 | 258 | rpred 11348 |
. . . . . . . 8
 
      |
260 | 257, 259 | remulcld 9676 |
. . . . . . 7
 
              |
261 | 28 | nnrecred 10662 |
. . . . . . . . . 10
               
    |
262 | 25, 261 | fsumrecl 13812 |
. . . . . . . . 9
 
                  |
263 | 262, 259 | remulcld 9676 |
. . . . . . . 8
 
                    |
264 | 34, 26 | rerpdivcld 11376 |
. . . . . . . . . 10
               
       
      |
265 | 259 | adantr 467 |
. . . . . . . . . . 11
               
  |
266 | 261, 265 | remulcld 9676 |
. . . . . . . . . 10
               
      |
267 | 30 | rpcnd 11350 |
. . . . . . . . . . . . . . . 16
               
    |
268 | 30 | rpne0d 11353 |
. . . . . . . . . . . . . . . 16
               
    |
269 | 33, 267, 268 | absdivd 13529 |
. . . . . . . . . . . . . . 15
               
       
                          |
270 | 2 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
               
  |
271 | 270, 28 | nndivred 10665 |
. . . . . . . . . . . . . . . . 17
               
    |
272 | 30 | rpge0d 11352 |
. . . . . . . . . . . . . . . . 17
               
    |
273 | 271, 272 | absidd 13496 |
. . . . . . . . . . . . . . . 16
               
          |
274 | 273 | oveq2d 6311 |
. . . . . . . . . . . . . . 15
               
       
                          |
275 | 269, 274 | eqtrd 2487 |
. . . . . . . . . . . . . 14
               
       
                      |
276 | 46 | adantr 467 |
. . . . . . . . . . . . . . 15
               
  |
277 | 87 | recnd 9674 |
. . . . . . . . . . . . . . 15
               
  |
278 | 47 | adantr 467 |
. . . . . . . . . . . . . . 15
               
  |
279 | 28 | nnne0d 10661 |
. . . . . . . . . . . . . . 15
               
  |
280 | 43, 276, 277, 278, 279 | divdiv2d 10422 |
. . . . . . . . . . . . . 14
               
       
                      |
281 | 43, 277, 276, 278 | div23d 10427 |
. . . . . . . . . . . . . 14
               
                              |
282 | 275, 280,
281 | 3eqtrd 2491 |
. . . . . . . . . . . . 13
               
       
                      |
283 | | pntrlog2bndlem5.2 |
. . . . . . . . . . . . . . 15
              |
284 | 283 | ad2antrr 733 |
. . . . . . . . . . . . . 14
               
          
  |
285 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . 18
          
    |
286 | | id 22 |
. . . . . . . . . . . . . . . . . 18
       |
287 | 285, 286 | oveq12d 6313 |
. . . . . . . . . . . . . . . . 17
                     |
288 | 287 | fveq2d 5874 |
. . . . . . . . . . . . . . . 16
                             |
289 | 288 | breq1d 4415 |
. . . . . . . . . . . . . . 15
             
       
         |
290 | 289 | rspcv 3148 |
. . . . . . . . . . . . . 14
  
 
                       
   |
291 | 30, 284, 290 | sylc 62 |
. . . . . . . . . . . . 13
               
       
        |
292 | 282, 291 | eqbrtrrd 4428 |
. . . . . . . . . . . 12
               
                |
293 | 264, 265,
29 | lemuldivd 11394 |
. . . . . . . . . . . 12
               
                                |
294 | 292, 293 | mpbid 214 |
. . . . . . . . . . 11
               
       
        |
295 | 265 | recnd 9674 |
. . . . . . . . . . . 12
               
  |
296 | 295, 277,
279 | divrec2d 10394 |
. . . . . . . . . . 11
               
        |
297 | 294, 296 | breqtrd 4430 |
. . . . . . . . . 10
               
       
          |
298 | 25, 264, 266, 297 | fsumle 13871 |
. . . . . . . . 9
 
                                          |
299 | 25, 46, 43, 47 | fsumdivc 13859 |
. . . . . . . . 9
 
                          
                       |
300 | 258 | rpcnd 11350 |
. . . . . . . . . 10
 
      |
301 | 261 | recnd 9674 |
. . . . . . . . . 10
               
    |
302 | 25, 300, 301 | fsummulc1 13858 |
. . . . . . . . 9
 
                  
               |
303 | 298, 299,
302 | 3brtr4d 4436 |
. . . . . . . 8
 
                                          |
304 | 258 | rpge0d 11352 |
. . . . . . . . 9
 
      |
305 | | harmonicubnd 23947 |
. . . . . . . . . 10
                       |
306 | 2, 9, 305 | syl2anc 667 |
. . . . . . . . 9
 
               
        |
307 | 262, 257,
259, 304, 306 | lemul1ad 10553 |
. . . . . . . 8
 
                            |
308 | 256, 263,
260, 303, 307 | letrd 9797 |
. . . . . . 7
 
                                    |
309 | 256, 260,
74, 109, 308 | lemul2ad 10554 |
. . . . . 6
 
                                                    |
310 | 24, 44, 46, 47 | divassd 10425 |
. . . . . 6
 
                                                                  |
311 | 241 | recnd 9674 |
. . . . . . . 8
 
              |
312 | 21, 300, 311 | mul32d 9848 |
. . . . . . 7
 
                              |
313 | | 1cnd 9664 |
. . . . . . . . . . . 12
 
      |
314 | 19, 313, 19, 23 | divdird 10428 |
. . . . . . . . . . 11
 
                                    |
315 | 19, 23 | dividd 10388 |
. . . . . . . . . . . 12
 
                |
316 | 315 | oveq1d 6310 |
. . . . . . . . . . 11
 
                                |
317 | 314, 316 | eqtr2d 2488 |
. . . . . . . . . 10
 
                          |
318 | 317 | oveq2d 6311 |
. . . . . . . . 9
 
                              |
319 | 19, 313 | addcld 9667 |
. . . . . . . . . 10
 
            |
320 | 21, 19, 319, 23 | div32d 10413 |
. . . . . . . . 9
 
                                  |
321 | 318, 320 | eqtr4d 2490 |
. . . . . . . 8
 
                              |
322 | 321 | oveq1d 6310 |
. . . . . . 7
 
                                  |
323 | 24, 319, 300 | mulassd 9671 |
. . . . . . 7
 
                                      |
324 | 312, 322,
323 | 3eqtrd 2491 |
. . . . . 6
 
                                  |
325 | 309, 310,
324 | 3brtr4d 4436 |
. . . . 5
 
                                                |
326 | 325 | adantrr 724 |
. . . 4
 
                                                  |
327 | 82, 254, 255, 81, 326 | lo1le 13727 |
. . 3
                                          |
328 | 78, 81, 234, 327 | lo1add 13702 |
. 2
                                                                                              |