Proof of Theorem pntrlog2bndlem5
Step | Hyp | Ref
| Expression |
1 | | elioore 11440 |
. . . . . . . . . . . . 13
   
  |
2 | 1 | adantl 466 |
. . . . . . . . . . . 12
 
      |
3 | | 1rp 11105 |
. . . . . . . . . . . . 13
 |
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
 
      |
5 | | 1red 9511 |
. . . . . . . . . . . . 13
 
      |
6 | | eliooord 11465 |
. . . . . . . . . . . . . . 15
   
    |
7 | 6 | adantl 466 |
. . . . . . . . . . . . . 14
 
    
   |
8 | 7 | simpld 459 |
. . . . . . . . . . . . 13
 
      |
9 | 5, 2, 8 | ltled 9632 |
. . . . . . . . . . . 12
 
      |
10 | 2, 4, 9 | rpgecld 11172 |
. . . . . . . . . . 11
 
      |
11 | | pntrlog2bnd.r |
. . . . . . . . . . . . 13
  ψ     |
12 | 11 | pntrf 22944 |
. . . . . . . . . . . 12
     |
13 | 12 | ffvelrni 5950 |
. . . . . . . . . . 11

      |
14 | 10, 13 | syl 16 |
. . . . . . . . . 10
 
          |
15 | 14 | recnd 9522 |
. . . . . . . . 9
 
          |
16 | 15 | abscld 13039 |
. . . . . . . 8
 
              |
17 | 16 | recnd 9522 |
. . . . . . 7
 
              |
18 | 10 | relogcld 22204 |
. . . . . . . 8
 
          |
19 | 18 | recnd 9522 |
. . . . . . 7
 
          |
20 | 17, 19 | mulcld 9516 |
. . . . . 6
 
                    |
21 | | 2cnd 10504 |
. . . . . . . 8
 
      |
22 | 2, 8 | rplogcld 22210 |
. . . . . . . . 9
 
          |
23 | 22 | rpne0d 11142 |
. . . . . . . 8
 
          |
24 | 21, 19, 23 | divcld 10217 |
. . . . . . 7
 
            |
25 | | fzfid 11911 |
. . . . . . . 8
 
              |
26 | 10 | adantr 465 |
. . . . . . . . . . . . . 14
               
  |
27 | | elfznn 11594 |
. . . . . . . . . . . . . . . 16
           |
28 | 27 | adantl 466 |
. . . . . . . . . . . . . . 15
               
  |
29 | 28 | nnrpd 11136 |
. . . . . . . . . . . . . 14
               
  |
30 | 26, 29 | rpdivcld 11154 |
. . . . . . . . . . . . 13
               
    |
31 | 12 | ffvelrni 5950 |
. . . . . . . . . . . . 13
  
        |
32 | 30, 31 | syl 16 |
. . . . . . . . . . . 12
               
        |
33 | 32 | recnd 9522 |
. . . . . . . . . . 11
               
        |
34 | 33 | abscld 13039 |
. . . . . . . . . 10
               
            |
35 | 29 | relogcld 22204 |
. . . . . . . . . . 11
               
      |
36 | | 1red 9511 |
. . . . . . . . . . 11
               
  |
37 | 35, 36 | readdcld 9523 |
. . . . . . . . . 10
               
        |
38 | 34, 37 | remulcld 9524 |
. . . . . . . . 9
               
       
            |
39 | 38 | recnd 9522 |
. . . . . . . 8
               
       
            |
40 | 25, 39 | fsumcl 13327 |
. . . . . . 7
 
                                  |
41 | 24, 40 | mulcld 9516 |
. . . . . 6
 
                                          |
42 | 20, 41 | subcld 9829 |
. . . . 5
 
                                                          |
43 | 34 | recnd 9522 |
. . . . . . 7
               
            |
44 | 25, 43 | fsumcl 13327 |
. . . . . 6
 
                          |
45 | 24, 44 | mulcld 9516 |
. . . . 5
 
                                  |
46 | 2 | recnd 9522 |
. . . . 5
 
      |
47 | 10 | rpne0d 11142 |
. . . . 5
 
      |
48 | 42, 45, 46, 47 | divdird 10255 |
. . . 4
 
                                                                                                                                                                                |
49 | 16, 18 | remulcld 9524 |
. . . . . . . 8
 
                    |
50 | 49 | recnd 9522 |
. . . . . . 7
 
                    |
51 | 50, 41, 45 | subsubd 9857 |
. . . . . 6
 
                                                                                                                                                                          |
52 | 24, 40, 44 | subdid 9910 |
. . . . . . . 8
 
                                                                      
                                                           |
53 | 25, 39, 43 | fsumsub 13372 |
. . . . . . . . . 10
 
                                                                                                |
54 | 37 | recnd 9522 |
. . . . . . . . . . . . 13
               
        |
55 | | 1cnd 9512 |
. . . . . . . . . . . . 13
               
  |
56 | 43, 54, 55 | subdid 9910 |
. . . . . . . . . . . 12
               
       
                                              |
57 | 35 | recnd 9522 |
. . . . . . . . . . . . . 14
               
      |
58 | 57, 55 | pncand 9830 |
. . . . . . . . . . . . 13
               
              |
59 | 58 | oveq2d 6215 |
. . . . . . . . . . . 12
               
       
                              |
60 | 43 | mulid1d 9513 |
. . . . . . . . . . . . 13
               
       
                |
61 | 60 | oveq2d 6215 |
. . . . . . . . . . . 12
               
                                                         
      |
62 | 56, 59, 61 | 3eqtr3rd 2504 |
. . . . . . . . . . 11
               
                         
                      |
63 | 62 | sumeq2dv 13297 |
. . . . . . . . . 10
 
                                            
                           |
64 | 53, 63 | eqtr3d 2497 |
. . . . . . . . 9
 
                                                      
                           |
65 | 64 | oveq2d 6215 |
. . . . . . . 8
 
                                                                                                  |
66 | 52, 65 | eqtr3d 2497 |
. . . . . . 7
 
                                                                                                          |
67 | 66 | oveq2d 6215 |
. . . . . 6
 
                                                                                                                                          |
68 | 51, 67 | eqtr3d 2497 |
. . . . 5
 
                                                                                                                                          |
69 | 68 | oveq1d 6214 |
. . . 4
 
                                                                                                                                              |
70 | 48, 69 | eqtr3d 2497 |
. . 3
 
                                                                                                                                                |
71 | 70 | mpteq2dva 4485 |
. 2
                                                                                                                                                       |
72 | | 2re 10501 |
. . . . . . . 8
 |
73 | 72 | a1i 11 |
. . . . . . 7
 
      |
74 | 73, 22 | rerpdivcld 11164 |
. . . . . 6
 
            |
75 | 25, 38 | fsumrecl 13328 |
. . . . . 6
 
                                  |
76 | 74, 75 | remulcld 9524 |
. . . . 5
 
                                          |
77 | 49, 76 | resubcld 9886 |
. . . 4
 
                                                          |
78 | 77, 10 | rerpdivcld 11164 |
. . 3
 
                                                            |
79 | 25, 34 | fsumrecl 13328 |
. . . . 5
 
                          |
80 | 74, 79 | remulcld 9524 |
. . . 4
 
                                  |
81 | 80, 10 | rerpdivcld 11164 |
. . 3
 
                                    |
82 | | 1red 9511 |
. . . 4
   |
83 | | pntsval.1 |
. . . . . 6
            Λ       ψ        |
84 | | pntrlog2bnd.t |
. . . . . 6
              |
85 | 83, 11, 84 | pntrlog2bndlem4 22961 |
. . . . 5
   
                                                                  |
86 | 85 | a1i 11 |
. . . 4
                                                                        |
87 | 28 | nnred 10447 |
. . . . . . . . . . 11
               
  |
88 | | simpl 457 |
. . . . . . . . . . . . . . 15
 
   |
89 | | simpr 461 |
. . . . . . . . . . . . . . . 16
 
   |
90 | 89 | relogcld 22204 |
. . . . . . . . . . . . . . 15
 
       |
91 | 88, 90 | remulcld 9524 |
. . . . . . . . . . . . . 14
 
         |
92 | | 0red 9497 |
. . . . . . . . . . . . . 14
 
   |
93 | 91, 92 | ifclda 3928 |
. . . . . . . . . . . . 13
              |
94 | 84, 93 | fmpti 5974 |
. . . . . . . . . . . 12
     |
95 | 94 | ffvelrni 5950 |
. . . . . . . . . . 11
       |
96 | 87, 95 | syl 16 |
. . . . . . . . . 10
               
      |
97 | 87, 36 | resubcld 9886 |
. . . . . . . . . . 11
               
    |
98 | 94 | ffvelrni 5950 |
. . . . . . . . . . 11
           |
99 | 97, 98 | syl 16 |
. . . . . . . . . 10
               
        |
100 | 96, 99 | resubcld 9886 |
. . . . . . . . 9
               
        
     |
101 | 34, 100 | remulcld 9524 |
. . . . . . . 8
               
       
                  |
102 | 25, 101 | fsumrecl 13328 |
. . . . . . 7
 
                                        |
103 | 74, 102 | remulcld 9524 |
. . . . . 6
 
                                                |
104 | 49, 103 | resubcld 9886 |
. . . . 5
 
                                                                |
105 | 104, 10 | rerpdivcld 11164 |
. . . 4
 
                                                                  |
106 | | 2rp 11106 |
. . . . . . . . . . 11
 |
107 | 106 | a1i 11 |
. . . . . . . . . 10
 
      |
108 | 107 | rpge0d 11141 |
. . . . . . . . 9
 
      |
109 | 73, 22, 108 | divge0d 11173 |
. . . . . . . 8
 
            |
110 | 33 | absge0d 13047 |
. . . . . . . . . 10
               
            |
111 | 29 | adantr 465 |
. . . . . . . . . . . . . . . 16
   
                |
112 | 111 | rpcnd 11139 |
. . . . . . . . . . . . . . 15
   
                |
113 | 57 | adantr 465 |
. . . . . . . . . . . . . . 15
   
                    |
114 | 112, 113 | mulcld 9516 |
. . . . . . . . . . . . . 14
   
                      |
115 | | simpr 461 |
. . . . . . . . . . . . . . . . . 18
   
                |
116 | | 1re 9495 |
. . . . . . . . . . . . . . . . . . 19
 |
117 | 111 | rpred 11137 |
. . . . . . . . . . . . . . . . . . 19
   
                |
118 | | difrp 11134 |
. . . . . . . . . . . . . . . . . . 19
 
       |
119 | 116, 117,
118 | sylancr 663 |
. . . . . . . . . . . . . . . . . 18
   
              
     |
120 | 115, 119 | mpbid 210 |
. . . . . . . . . . . . . . . . 17
   
                  |
121 | 120 | relogcld 22204 |
. . . . . . . . . . . . . . . 16
   
                      |
122 | 121 | recnd 9522 |
. . . . . . . . . . . . . . 15
   
                      |
123 | 112, 122 | mulcld 9516 |
. . . . . . . . . . . . . 14
   
                        |
124 | 114, 123,
122 | subsubd 9857 |
. . . . . . . . . . . . 13
   
                                                                |
125 | | rpre 11107 |
. . . . . . . . . . . . . . . . 17

  |
126 | | eleq1 2526 |
. . . . . . . . . . . . . . . . . . 19
 
   |
127 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
   |
128 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . 20
           |
129 | 127, 128 | oveq12d 6217 |
. . . . . . . . . . . . . . . . . . 19
               |
130 | 126, 129 | ifbieq1d 3919 |
. . . . . . . . . . . . . . . . . 18
                         |
131 | | ovex 6224 |
. . . . . . . . . . . . . . . . . . 19
       |
132 | | c0ex 9490 |
. . . . . . . . . . . . . . . . . . 19
 |
133 | 131, 132 | ifex 3965 |
. . . . . . . . . . . . . . . . . 18
            |
134 | 130, 84, 133 | fvmpt 5882 |
. . . . . . . . . . . . . . . . 17
                  |
135 | 125, 134 | syl 16 |
. . . . . . . . . . . . . . . 16

                 |
136 | | iftrue 3904 |
. . . . . . . . . . . . . . . 16

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

            |
138 | 111, 137 | syl 16 |
. . . . . . . . . . . . . 14
   
                          |
139 | | rpre 11107 |
. . . . . . . . . . . . . . . . . 18
  
    |
140 | | eleq1 2526 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
141 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
       |
142 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . 21
               |
143 | 141, 142 | oveq12d 6217 |
. . . . . . . . . . . . . . . . . . . 20
                     |
144 | 140, 143 | ifbieq1d 3919 |
. . . . . . . . . . . . . . . . . . 19
                                 |
145 | | ovex 6224 |
. . . . . . . . . . . . . . . . . . . 20
           |
146 | 145, 132 | ifex 3965 |
. . . . . . . . . . . . . . . . . . 19
                  |
147 | 144, 84, 146 | fvmpt 5882 |
. . . . . . . . . . . . . . . . . 18
                            |
148 | 139, 147 | syl 16 |
. . . . . . . . . . . . . . . . 17
  
                         |
149 | | iftrue 3904 |
. . . . . . . . . . . . . . . . 17
  
                             |
150 | 148, 149 | eqtrd 2495 |
. . . . . . . . . . . . . . . 16
  
                  |
151 | 120, 150 | syl 16 |
. . . . . . . . . . . . . . 15
   
                                |
152 | | 1cnd 9512 |
. . . . . . . . . . . . . . . 16
   
                |
153 | 112, 152,
122 | subdird 9911 |
. . . . . . . . . . . . . . 15
   
                                            |
154 | 122 | mulid2d 9514 |
. . . . . . . . . . . . . . . 16
   
                              |
155 | 154 | oveq2d 6215 |
. . . . . . . . . . . . . . 15
   
                                                  |
156 | 151, 153,
155 | 3eqtrd 2499 |
. . . . . . . . . . . . . 14
   
                                      |
157 | 138, 156 | oveq12d 6217 |
. . . . . . . . . . . . 13
   
                                                    |
158 | 112, 113,
122 | subdid 9910 |
. . . . . . . . . . . . . 14
   
                                              |
159 | 158 | oveq1d 6214 |
. . . . . . . . . . . . 13
   
                                                              |
160 | 124, 157,
159 | 3eqtr4d 2505 |
. . . . . . . . . . . 12
   
                                                  |
161 | 111 | relogcld 22204 |
. . . . . . . . . . . . . . . . . 18
   
                    |
162 | 161, 121 | resubcld 9886 |
. . . . . . . . . . . . . . . . 17
   
                            |
163 | 162 | recnd 9522 |
. . . . . . . . . . . . . . . 16
   
                            |
164 | 112, 152,
163 | subdird 9911 |
. . . . . . . . . . . . . . 15
   
                                                              |
165 | 163 | mulid2d 9514 |
. . . . . . . . . . . . . . . 16
   
                                          |
166 | 165 | oveq2d 6215 |
. . . . . . . . . . . . . . 15
   
                                                                          |
167 | 117, 162 | remulcld 9524 |
. . . . . . . . . . . . . . . . 17
   
                              |
168 | 167 | recnd 9522 |
. . . . . . . . . . . . . . . 16
   
                              |
169 | 168, 113,
122 | subsub3d 9859 |
. . . . . . . . . . . . . . 15
   
                                                                        |
170 | 164, 166,
169 | 3eqtrd 2499 |
. . . . . . . . . . . . . 14
   
                                                            |
171 | 112, 152 | npcand 9833 |
. . . . . . . . . . . . . . . . . 18
   
                    |
172 | 171 | fveq2d 5802 |
. . . . . . . . . . . . . . . . 17
   
                            |
173 | 172 | oveq1d 6214 |
. . . . . . . . . . . . . . . 16
   
                                            |
174 | | logdifbnd 22519 |
. . . . . . . . . . . . . . . . 17
  
                      |
175 | 120, 174 | syl 16 |
. . . . . . . . . . . . . . . 16
   
                                    |
176 | 173, 175 | eqbrtrrd 4421 |
. . . . . . . . . . . . . . 15
   
                                |
177 | | 1red 9511 |
. . . . . . . . . . . . . . . 16
   
                |
178 | 162, 177,
120 | lemuldiv2d 11183 |
. . . . . . . . . . . . . . 15
   
                              
           
       |
179 | 176, 178 | mpbird 232 |
. . . . . . . . . . . . . 14
   
                                |
180 | 170, 179 | eqbrtrrd 4421 |
. . . . . . . . . . . . 13
   
                                            |
181 | 167, 121 | readdcld 9523 |
. . . . . . . . . . . . . 14
   
                                      |
182 | 181, 161,
177 | lesubadd2d 10048 |
. . . . . . . . . . . . 13
   
                                          
                               |
183 | 180, 182 | mpbid 210 |
. . . . . . . . . . . 12
   
                                            |
184 | 160, 183 | eqbrtrd 4419 |
. . . . . . . . . . 11
   
                                  |
185 | | fveq2 5798 |
. . . . . . . . . . . . . . . . 17
           |
186 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
187 | 186, 3 | syl6eqel 2550 |
. . . . . . . . . . . . . . . . . . . . 21
   |
188 | | iftrue 3904 |
. . . . . . . . . . . . . . . . . . . . 21

                   |
189 | 187, 188 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
                    |
190 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
191 | | log1 22166 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
192 | 190, 191 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
193 | 186, 192 | oveq12d 6217 |
. . . . . . . . . . . . . . . . . . . . 21
           |
194 | | ax-1cn 9450 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
195 | 194 | mul01i 9669 |
. . . . . . . . . . . . . . . . . . . . 21
   |
196 | 193, 195 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . 20
         |
197 | 189, 196 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . . 19
              |
198 | 197, 84, 132 | fvmpt 5882 |
. . . . . . . . . . . . . . . . . 18
       |
199 | 116, 198 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     |
200 | 185, 199 | syl6eq 2511 |
. . . . . . . . . . . . . . . 16
       |
201 | | oveq1 6206 |
. . . . . . . . . . . . . . . . . . 19
       |
202 | | 1m1e0 10500 |
. . . . . . . . . . . . . . . . . . 19
   |
203 | 201, 202 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . 18
     |
204 | 203 | fveq2d 5802 |
. . . . . . . . . . . . . . . . 17
             |
205 | | 0re 9496 |
. . . . . . . . . . . . . . . . . 18
 |
206 | | rpne0 11116 |
. . . . . . . . . . . . . . . . . . . . 21

  |
207 | 206 | necon2bi 2688 |
. . . . . . . . . . . . . . . . . . . 20

  |
208 | | iffalse 3906 |
. . . . . . . . . . . . . . . . . . . 20
              |
209 | 207, 208 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
              |
210 | 209, 84, 132 | fvmpt 5882 |
. . . . . . . . . . . . . . . . . 18
       |
211 | 205, 210 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     |
212 | 204, 211 | syl6eq 2511 |
. . . . . . . . . . . . . . . 16
         |
213 | 200, 212 | oveq12d 6217 |
. . . . . . . . . . . . . . 15
                 |
214 | | 0m0e0 10541 |
. . . . . . . . . . . . . . 15
   |
215 | 213, 214 | syl6eq 2511 |
. . . . . . . . . . . . . 14
               |
216 | 215 | eqcoms 2466 |
. . . . . . . . . . . . 13
               |
217 | 216 | adantl 466 |
. . . . . . . . . . . 12
   
                            |
218 | | 0red 9497 |
. . . . . . . . . . . . . 14
               
  |
219 | 28 | nnge1d 10474 |
. . . . . . . . . . . . . . 15
               
  |
220 | 87, 219 | logge0d 22211 |
. . . . . . . . . . . . . 14
               
      |
221 | 35 | lep1d 10374 |
. . . . . . . . . . . . . 14
               
            |
222 | 218, 35, 37, 220, 221 | letrd 9638 |
. . . . . . . . . . . . 13
               
        |
223 | 222 | adantr 465 |
. . . . . . . . . . . 12
   
                      |
224 | 217, 223 | eqbrtrd 4419 |
. . . . . . . . . . 11
   
                                  |
225 | | elfzle1 11570 |
. . . . . . . . . . . . 13
           |
226 | 225 | adantl 466 |
. . . . . . . . . . . 12
               
  |
227 | 36, 87 | leloed 9627 |
. . . . . . . . . . . 12
               

     |
228 | 226, 227 | mpbid 210 |
. . . . . . . . . . 11
               
    |
229 | 184, 224,
228 | mpjaodan 784 |
. . . . . . . . . 10
               
        
           |
230 | 100, 37, 34, 110, 229 | lemul2ad 10383 |
. . . . . . . . 9
               
       
                                    |
231 | 25, 101, 38, 230 | fsumle 13379 |
. . . . . . . 8
 
                                                                    |
232 | 102, 75, 74, 109, 231 | lemul2ad 10383 |
. . . . . . 7
 
                                                                                    |
233 | 103, 76, 49, 232 | lesub2dd 10066 |
. . . . . 6
 
                                                                                                                    |
234 | 77, 104, 10, 233 | lediv1dd 11191 |
. . . . 5
 
                                                                                                                        |
235 | 234 | adantrr 716 |
. . . 4
 
                                                                                                                          |
236 | 82, 86, 105, 78, 235 | lo1le 13246 |
. . 3
                                                                  |
237 | 106 | a1i 11 |
. . . . . . . 8
   |
238 | | pntrlog2bndlem5.1 |
. . . . . . . 8
   |
239 | 237, 238 | rpmulcld 11153 |
. . . . . . 7
     |
240 | 239 | rpred 11137 |
. . . . . 6
     |
241 | 240 | adantr 465 |
. . . . 5
 
        |
242 | 5, 22 | rerpdivcld 11164 |
. . . . . 6
 
            |
243 | 5, 242 | readdcld 9523 |
. . . . 5
 
              |
244 | | ioossre 11467 |
. . . . . 6
    |
245 | | lo1const 13215 |
. . . . . 6
                     |
246 | 244, 240,
245 | sylancr 663 |
. . . . 5
              |
247 | | lo1const 13215 |
. . . . . . 7
                 |
248 | 244, 82, 247 | sylancr 663 |
. . . . . 6
            |
249 | | divlogrlim 22212 |
. . . . . . . 8
   
         |
250 | | rlimo1 13211 |
. . . . . . . 8
                             |
251 | 249, 250 | mp1i 12 |
. . . . . . 7
                 |
252 | 242, 251 | o1lo1d 13134 |
. . . . . 6
                  |
253 | 5, 242, 248, 252 | lo1add 13221 |
. . . . 5
                    |
254 | 239 | adantr 465 |
. . . . . 6
 
        |
255 | 254 | rpge0d 11141 |
. . . . 5
 
        |
256 | 241, 243,
246, 253, 255 | lo1mul 13222 |
. . . 4
                        |
257 | 241, 243 | remulcld 9524 |
. . . 4
 
                  |
258 | 79, 10 | rerpdivcld 11164 |
. . . . . . 7
 
                            |
259 | 18, 5 | readdcld 9523 |
. . . . . . . 8
 
            |
260 | 238 | adantr 465 |
. . . . . . . . 9
 
      |
261 | 260 | rpred 11137 |
. . . . . . . 8
 
      |
262 | 259, 261 | remulcld 9524 |
. . . . . . 7
 
              |
263 | 28 | nnrecred 10477 |
. . . . . . . . . 10
               
    |
264 | 25, 263 | fsumrecl 13328 |
. . . . . . . . 9
 
                  |
265 | 264, 261 | remulcld 9524 |
. . . . . . . 8
 
                    |
266 | 34, 26 | rerpdivcld 11164 |
. . . . . . . . . 10
               
       
      |
267 | 261 | adantr 465 |
. . . . . . . . . . 11
               
  |
268 | 263, 267 | remulcld 9524 |
. . . . . . . . . 10
               
      |
269 | 30 | rpcnd 11139 |
. . . . . . . . . . . . . . . 16
               
    |
270 | 30 | rpne0d 11142 |
. . . . . . . . . . . . . . . 16
               
    |
271 | 33, 269, 270 | absdivd 13058 |
. . . . . . . . . . . . . . 15
               
       
                          |
272 | 2 | adantr 465 |
. . . . . . . . . . . . . . . . . 18
               
  |
273 | 272, 28 | nndivred 10480 |
. . . . . . . . . . . . . . . . 17
               
    |
274 | 30 | rpge0d 11141 |
. . . . . . . . . . . . . . . . 17
               
    |
275 | 273, 274 | absidd 13026 |
. . . . . . . . . . . . . . . 16
               
          |
276 | 275 | oveq2d 6215 |
. . . . . . . . . . . . . . 15
               
       
                          |
277 | 271, 276 | eqtrd 2495 |
. . . . . . . . . . . . . 14
               
       
                      |
278 | 46 | adantr 465 |
. . . . . . . . . . . . . . 15
               
  |
279 | 87 | recnd 9522 |
. . . . . . . . . . . . . . 15
               
  |
280 | 47 | adantr 465 |
. . . . . . . . . . . . . . 15
               
  |
281 | 28 | nnne0d 10476 |
. . . . . . . . . . . . . . 15
               
  |
282 | 43, 278, 279, 280, 281 | divdiv2d 10249 |
. . . . . . . . . . . . . 14
               
       
                      |
283 | 43, 279, 278, 280 | div23d 10254 |
. . . . . . . . . . . . . 14
               
                              |
284 | 277, 282,
283 | 3eqtrd 2499 |
. . . . . . . . . . . . 13
               
       
                      |
285 | | pntrlog2bndlem5.2 |
. . . . . . . . . . . . . . 15
              |
286 | 285 | ad2antrr 725 |
. . . . . . . . . . . . . 14
               
          
  |
287 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . 18
          
    |
288 | | id 22 |
. . . . . . . . . . . . . . . . . 18
       |
289 | 287, 288 | oveq12d 6217 |
. . . . . . . . . . . . . . . . 17
                     |
290 | 289 | fveq2d 5802 |
. . . . . . . . . . . . . . . 16
                             |
291 | 290 | breq1d 4409 |
. . . . . . . . . . . . . . 15
             
       
         |
292 | 291 | rspcv 3173 |
. . . . . . . . . . . . . 14
  
 
                       
   |
293 | 30, 286, 292 | sylc 60 |
. . . . . . . . . . . . 13
               
       
        |
294 | 284, 293 | eqbrtrrd 4421 |
. . . . . . . . . . . 12
               
                |
295 | 266, 267,
29 | lemuldivd 11182 |
. . . . . . . . . . . 12
               
                                |
296 | 294, 295 | mpbid 210 |
. . . . . . . . . . 11
               
       
        |
297 | 267 | recnd 9522 |
. . . . . . . . . . . 12
               
  |
298 | 297, 279,
281 | divrec2d 10221 |
. . . . . . . . . . 11
               
        |
299 | 296, 298 | breqtrd 4423 |
. . . . . . . . . 10
               
       
          |
300 | 25, 266, 268, 299 | fsumle 13379 |
. . . . . . . . 9
 
                                          |
301 | 25, 46, 43, 47 | fsumdivc 13370 |
. . . . . . . . 9
 
                          
                       |
302 | 260 | rpcnd 11139 |
. . . . . . . . . 10
 
      |
303 | 263 | recnd 9522 |
. . . . . . . . . 10
               
    |
304 | 25, 302, 303 | fsummulc1 13369 |
. . . . . . . . 9
 
                  
               |
305 | 300, 301,
304 | 3brtr4d 4429 |
. . . . . . . 8
 
                                          |
306 | 260 | rpge0d 11141 |
. . . . . . . . 9
 
      |
307 | | harmonicubnd 22535 |
. . . . . . . . . 10
                       |
308 | 2, 9, 307 | syl2anc 661 |
. . . . . . . . 9
 
               
        |
309 | 264, 259,
261, 306, 308 | lemul1ad 10382 |
. . . . . . . 8
 
                            |
310 | 258, 265,
262, 305, 309 | letrd 9638 |
. . . . . . 7
 
                                    |
311 | 258, 262,
74, 109, 310 | lemul2ad 10383 |
. . . . . 6
 
                                                    |
312 | 24, 44, 46, 47 | divassd 10252 |
. . . . . 6
 
                                                                  |
313 | 243 | recnd 9522 |
. . . . . . . 8
 
              |
314 | 21, 302, 313 | mul32d 9689 |
. . . . . . 7
 
                              |
315 | | 1cnd 9512 |
. . . . . . . . . . . 12
 
      |
316 | 19, 315, 19, 23 | divdird 10255 |
. . . . . . . . . . 11
 
                                    |
317 | 19, 23 | dividd 10215 |
. . . . . . . . . . . 12
 
                |
318 | 317 | oveq1d 6214 |
. . . . . . . . . . 11
 
                                |
319 | 316, 318 | eqtr2d 2496 |
. . . . . . . . . 10
 
                          |
320 | 319 | oveq2d 6215 |
. . . . . . . . 9
 
                              |
321 | 19, 315 | addcld 9515 |
. . . . . . . . . 10
 
            |
322 | 21, 19, 321, 23 | div32d 10240 |
. . . . . . . . 9
 
                                  |
323 | 320, 322 | eqtr4d 2498 |
. . . . . . . 8
 
                              |
324 | 323 | oveq1d 6214 |
. . . . . . 7
 
                                  |
325 | 24, 321, 302 | mulassd 9519 |
. . . . . . 7
 
                                      |
326 | 314, 324,
325 | 3eqtrd 2499 |
. . . . . 6
 
                                  |
327 | 311, 312,
326 | 3brtr4d 4429 |
. . . . 5
 
                                                |
328 | 327 | adantrr 716 |
. . . 4
 
                                                  |
329 | 82, 256, 257, 81, 328 | lo1le 13246 |
. . 3
                                          |
330 | 78, 81, 236, 329 | lo1add 13221 |
. 2
                                          ![]() |