Step | Hyp | Ref
| Expression |
1 | | 1red 9676 |
. 2
   |
2 | | pntrlog2bndlem3.1 |
. . . . 5
   |
3 | 2 | rpred 11364 |
. . . 4
   |
4 | 3 | adantr 472 |
. . 3
 
      |
5 | | fzfid 12224 |
. . . . 5
 
              |
6 | | elfznn 11854 |
. . . . . . . 8
           |
7 | 6 | adantl 473 |
. . . . . . 7
               
  |
8 | 7 | nnred 10646 |
. . . . . 6
               
  |
9 | | elioore 11691 |
. . . . . . . . . . . . . 14
   
  |
10 | 9 | adantl 473 |
. . . . . . . . . . . . 13
 
      |
11 | | 1rp 11329 |
. . . . . . . . . . . . . 14
 |
12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
 
      |
13 | | 1red 9676 |
. . . . . . . . . . . . . 14
 
      |
14 | | eliooord 11719 |
. . . . . . . . . . . . . . . 16
   
    |
15 | 14 | adantl 473 |
. . . . . . . . . . . . . . 15
 
    
   |
16 | 15 | simpld 466 |
. . . . . . . . . . . . . 14
 
      |
17 | 13, 10, 16 | ltled 9800 |
. . . . . . . . . . . . 13
 
      |
18 | 10, 12, 17 | rpgecld 11400 |
. . . . . . . . . . . 12
 
      |
19 | 18 | adantr 472 |
. . . . . . . . . . 11
               
  |
20 | 7 | nnrpd 11362 |
. . . . . . . . . . . 12
               
  |
21 | 11 | a1i 11 |
. . . . . . . . . . . 12
               
  |
22 | 20, 21 | rpaddcld 11379 |
. . . . . . . . . . 11
               
    |
23 | 19, 22 | rpdivcld 11381 |
. . . . . . . . . 10
               
      |
24 | | pntrlog2bnd.r |
. . . . . . . . . . . 12
  ψ     |
25 | 24 | pntrf 24480 |
. . . . . . . . . . 11
     |
26 | 25 | ffvelrni 6036 |
. . . . . . . . . 10
    
          |
27 | 23, 26 | syl 17 |
. . . . . . . . 9
               
          |
28 | 27 | recnd 9687 |
. . . . . . . 8
               
          |
29 | 19, 20 | rpdivcld 11381 |
. . . . . . . . . 10
               
    |
30 | 25 | ffvelrni 6036 |
. . . . . . . . . 10
  
        |
31 | 29, 30 | syl 17 |
. . . . . . . . 9
               
        |
32 | 31 | recnd 9687 |
. . . . . . . 8
               
        |
33 | 28, 32 | subcld 10005 |
. . . . . . 7
               
            
     |
34 | 33 | abscld 13575 |
. . . . . 6
               
       
              |
35 | 8, 34 | remulcld 9689 |
. . . . 5
               
                        |
36 | 5, 35 | fsumrecl 13877 |
. . . 4
 
                                      |
37 | 10, 16 | rplogcld 23657 |
. . . . 5
 
          |
38 | 18, 37 | rpmulcld 11380 |
. . . 4
 
            |
39 | 36, 38 | rerpdivcld 11392 |
. . 3
 
                       
                      |
40 | | ioossre 11721 |
. . . 4
    |
41 | 2 | rpcnd 11366 |
. . . 4
   |
42 | | o1const 13760 |
. . . 4
                |
43 | 40, 41, 42 | sylancr 676 |
. . 3
           |
44 | | chpo1ubb 24398 |
. . . 4
  ψ     |
45 | | pntsval.1 |
. . . . . 6
            Λ       ψ        |
46 | | simpl 464 |
. . . . . 6
  
ψ    
  |
47 | | simpr 468 |
. . . . . 6
  
ψ    
 ψ 
    |
48 | 45, 24, 46, 47 | pntrlog2bndlem2 24495 |
. . . . 5
  
ψ    
                                                  |
49 | 48 | rexlimiva 2868 |
. . . 4
   ψ 
       
                 
                          |
50 | 44, 49 | mp1i 13 |
. . 3
                                                   |
51 | 4, 39, 43, 50 | o1mul2 13765 |
. 2
                         
                           |
52 | 4, 39 | remulcld 9689 |
. 2
 
    
                                           |
53 | 32 | abscld 13575 |
. . . . . . 7
               
            |
54 | 28 | abscld 13575 |
. . . . . . 7
               
              |
55 | 53, 54 | resubcld 10068 |
. . . . . 6
               
       
                  |
56 | 45 | pntsf 24490 |
. . . . . . . . 9
     |
57 | 56 | ffvelrni 6036 |
. . . . . . . 8
       |
58 | 8, 57 | syl 17 |
. . . . . . 7
               
      |
59 | | 2re 10701 |
. . . . . . . . 9
 |
60 | 59 | a1i 11 |
. . . . . . . 8
               
  |
61 | 20 | relogcld 23651 |
. . . . . . . . 9
               
      |
62 | 8, 61 | remulcld 9689 |
. . . . . . . 8
               
        |
63 | 60, 62 | remulcld 9689 |
. . . . . . 7
               
          |
64 | 58, 63 | resubcld 10068 |
. . . . . 6
               
                |
65 | 55, 64 | remulcld 9689 |
. . . . 5
               
                                          |
66 | 5, 65 | fsumrecl 13877 |
. . . 4
 
                                
                       |
67 | 66, 38 | rerpdivcld 11392 |
. . 3
 
                                                                |
68 | 67 | recnd 9687 |
. 2
 
                                                                |
69 | 68 | abscld 13575 |
. . . 4
 
                                    
                               |
70 | 52 | recnd 9687 |
. . . . 5
 
    
                                           |
71 | 70 | abscld 13575 |
. . . 4
 
                                                    |
72 | 66 | recnd 9687 |
. . . . . . 7
 
                                
                       |
73 | 72 | abscld 13575 |
. . . . . 6
 
                                   
                        |
74 | 4, 36 | remulcld 9689 |
. . . . . 6
 
    
                                   |
75 | 65 | recnd 9687 |
. . . . . . . . 9
               
                                          |
76 | 75 | abscld 13575 |
. . . . . . . 8
               
                     
                        |
77 | 5, 76 | fsumrecl 13877 |
. . . . . . 7
 
                                                            |
78 | 5, 75 | fsumabs 13938 |
. . . . . . 7
 
                                   
                                                                              |
79 | 4 | adantr 472 |
. . . . . . . . . 10
               
  |
80 | 79, 35 | remulcld 9689 |
. . . . . . . . 9
               
                          |
81 | 55 | recnd 9687 |
. . . . . . . . . . . 12
               
       
                  |
82 | 81 | abscld 13575 |
. . . . . . . . . . 11
               
                              |
83 | 64 | recnd 9687 |
. . . . . . . . . . . 12
               
                |
84 | 83 | abscld 13575 |
. . . . . . . . . . 11
               
                    |
85 | 79, 8 | remulcld 9689 |
. . . . . . . . . . 11
               
    |
86 | 81 | absge0d 13583 |
. . . . . . . . . . 11
               
                              |
87 | 83 | absge0d 13583 |
. . . . . . . . . . 11
               
                    |
88 | 32, 28 | abs2difabsd 13598 |
. . . . . . . . . . . 12
               
                                                  |
89 | 32, 28 | abssubd 13592 |
. . . . . . . . . . . 12
               
       
                           
      |
90 | 88, 89 | breqtrd 4420 |
. . . . . . . . . . 11
               
                                                  |
91 | 58 | recnd 9687 |
. . . . . . . . . . . . . . . 16
               
      |
92 | 8 | recnd 9687 |
. . . . . . . . . . . . . . . 16
               
  |
93 | 7 | nnne0d 10676 |
. . . . . . . . . . . . . . . 16
               
  |
94 | 91, 92, 93 | divcld 10405 |
. . . . . . . . . . . . . . 15
               
        |
95 | | 2cnd 10704 |
. . . . . . . . . . . . . . . 16
               
  |
96 | 61 | recnd 9687 |
. . . . . . . . . . . . . . . 16
               
      |
97 | 95, 96 | mulcld 9681 |
. . . . . . . . . . . . . . 15
               
        |
98 | 94, 97 | subcld 10005 |
. . . . . . . . . . . . . 14
               
                |
99 | 98, 92 | absmuld 13593 |
. . . . . . . . . . . . 13
               
                                              |
100 | 94, 97, 92 | subdird 10096 |
. . . . . . . . . . . . . . 15
               
                                    |
101 | 91, 92, 93 | divcan1d 10406 |
. . . . . . . . . . . . . . . 16
               
              |
102 | 95, 92, 96 | mul32d 9861 |
. . . . . . . . . . . . . . . . 17
               
                  |
103 | 95, 92, 96 | mulassd 9684 |
. . . . . . . . . . . . . . . . 17
               
                  |
104 | 102, 103 | eqtr3d 2507 |
. . . . . . . . . . . . . . . 16
               
                  |
105 | 101, 104 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
               
                                  |
106 | 100, 105 | eqtrd 2505 |
. . . . . . . . . . . . . 14
               
                                |
107 | 106 | fveq2d 5883 |
. . . . . . . . . . . . 13
               
                                        |
108 | 20 | rpge0d 11368 |
. . . . . . . . . . . . . . 15
               
  |
109 | 8, 108 | absidd 13561 |
. . . . . . . . . . . . . 14
               
      |
110 | 109 | oveq2d 6324 |
. . . . . . . . . . . . 13
               
                                              |
111 | 99, 107, 110 | 3eqtr3d 2513 |
. . . . . . . . . . . 12
               
                                        |
112 | 98 | abscld 13575 |
. . . . . . . . . . . . 13
               
                    |
113 | 7 | nnge1d 10674 |
. . . . . . . . . . . . . . 15
               
  |
114 | | 1re 9660 |
. . . . . . . . . . . . . . . 16
 |
115 | | elicopnf 11755 |
. . . . . . . . . . . . . . . 16
    
     |
116 | 114, 115 | ax-mp 5 |
. . . . . . . . . . . . . . 15
   
    |
117 | 8, 113, 116 | sylanbrc 677 |
. . . . . . . . . . . . . 14
               
     |
118 | | pntrlog2bndlem3.2 |
. . . . . . . . . . . . . . 15
                          |
119 | 118 | ad2antrr 740 |
. . . . . . . . . . . . . 14
               
                         |
120 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
121 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
   |
122 | 120, 121 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
               |
123 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
124 | 123 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
               |
125 | 122, 124 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
                               |
126 | 125 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
                                       |
127 | 126 | breq1d 4405 |
. . . . . . . . . . . . . . 15
                   
                 
   |
128 | 127 | rspcv 3132 |
. . . . . . . . . . . . . 14
   
 
                                           |
129 | 117, 119,
128 | sylc 61 |
. . . . . . . . . . . . 13
               
                 
  |
130 | 112, 79, 8, 108, 129 | lemul1ad 10568 |
. . . . . . . . . . . 12
               
                   
    |
131 | 111, 130 | eqbrtrd 4416 |
. . . . . . . . . . 11
               
                 
    |
132 | 82, 34, 84, 85, 86, 87, 90, 131 | lemul12ad 10571 |
. . . . . . . . . 10
               
                     
                                                    |
133 | 81, 83 | absmuld 13593 |
. . . . . . . . . 10
               
                     
                                                                        |
134 | 41 | ad2antrr 740 |
. . . . . . . . . . . 12
               
  |
135 | 34 | recnd 9687 |
. . . . . . . . . . . 12
               
       
              |
136 | 134, 92, 135 | mulassd 9684 |
. . . . . . . . . . 11
               
 
                                                |
137 | 134, 92 | mulcld 9681 |
. . . . . . . . . . . 12
               
    |
138 | 137, 135 | mulcomd 9682 |
. . . . . . . . . . 11
               
 
                                                |
139 | 136, 138 | eqtr3d 2507 |
. . . . . . . . . 10
               
                                
                 |
140 | 132, 133,
139 | 3brtr4d 4426 |
. . . . . . . . 9
               
                     
                               
                |
141 | 5, 76, 80, 140 | fsumle 13936 |
. . . . . . . 8
 
                                                                             
                |
142 | 41 | adantr 472 |
. . . . . . . . 9
 
      |
143 | 35 | recnd 9687 |
. . . . . . . . 9
               
                        |
144 | 5, 142, 143 | fsummulc2 13922 |
. . . . . . . 8
 
    
                                                    
                |
145 | 141, 144 | breqtrrd 4422 |
. . . . . . 7
 
                                                          
                                   |
146 | 73, 77, 74, 78, 145 | letrd 9809 |
. . . . . 6
 
                                   
                                                          |
147 | 73, 74, 38, 146 | lediv1dd 11419 |
. . . . 5
 
                                                                                                              |
148 | 38 | rpcnd 11366 |
. . . . . . 7
 
            |
149 | 38 | rpne0d 11369 |
. . . . . . 7
 
            |
150 | 72, 148, 149 | absdivd 13594 |
. . . . . 6
 
                                    
                                                             
                                   |
151 | 38 | rpred 11364 |
. . . . . . . 8
 
            |
152 | 38 | rpge0d 11368 |
. . . . . . . 8
 
            |
153 | 151, 152 | absidd 13561 |
. . . . . . 7
 
                      |
154 | 153 | oveq2d 6324 |
. . . . . 6
 
                                                                                                      
                               |
155 | 150, 154 | eqtr2d 2506 |
. . . . 5
 
                                                                                                                                  |
156 | 36 | recnd 9687 |
. . . . . 6
 
                                      |
157 | 142, 156,
148, 149 | divassd 10440 |
. . . . 5
 
                                                                                          |
158 | 147, 155,
157 | 3brtr3d 4425 |
. . . 4
 
                                    
                            
                                            |
159 | 52 | leabsd 13553 |
. . . 4
 
    
                                        
                       
                        |
160 | 69, 52, 71, 158, 159 | letrd 9809 |
. . 3
 
                                    
                            
                       
                        |
161 | 160 | adantrr 731 |
. 2
 
                                      
                            
                       
                        |
162 | 1, 51, 52, 68, 161 | o1le 13793 |
1
                                  
                                  |