Step | Hyp | Ref
| Expression |
1 | | ioossre 11696 |
. . 3
    |
2 | 1 | a1i 11 |
. 2
        |
3 | | 1red 9658 |
. 2
     |
4 | 2 | sselda 3432 |
. . . . . . . . 9
  

 
 
  |
5 | | 1rp 11306 |
. . . . . . . . . 10
 |
6 | 5 | a1i 11 |
. . . . . . . . 9
  

 
 
  |
7 | | 1red 9658 |
. . . . . . . . . 10
  

 
 
  |
8 | | eliooord 11694 |
. . . . . . . . . . . 12
   
    |
9 | 8 | adantl 468 |
. . . . . . . . . . 11
  

 
 
    |
10 | 9 | simpld 461 |
. . . . . . . . . 10
  

 
 
  |
11 | 7, 4, 10 | ltled 9783 |
. . . . . . . . 9
  

 
 
  |
12 | 4, 6, 11 | rpgecld 11377 |
. . . . . . . 8
  

 
 
  |
13 | | pntpbnd.r |
. . . . . . . . . 10
  ψ     |
14 | 13 | pntrf 24401 |
. . . . . . . . 9
     |
15 | 14 | ffvelrni 6021 |
. . . . . . . 8

      |
16 | 12, 15 | syl 17 |
. . . . . . 7
  

 
 
      |
17 | 16 | recnd 9669 |
. . . . . 6
  

 
 
      |
18 | 17 | abscld 13498 |
. . . . 5
  

 
 
          |
19 | 12 | relogcld 23572 |
. . . . 5
  

 
 
      |
20 | 18, 19 | remulcld 9671 |
. . . 4
  

 
 
                |
21 | | 2re 10679 |
. . . . . . 7
 |
22 | 21 | a1i 11 |
. . . . . 6
  

 
 
  |
23 | 4, 10 | rplogcld 23578 |
. . . . . 6
  

 
 
      |
24 | 22, 23 | rerpdivcld 11369 |
. . . . 5
  

 
 
        |
25 | | fzfid 12186 |
. . . . . 6
  

 
 
      
     |
26 | 12 | adantr 467 |
. . . . . . . . . . 11
                   
  |
27 | | elfznn 11828 |
. . . . . . . . . . . . 13
             |
28 | 27 | adantl 468 |
. . . . . . . . . . . 12
                   
  |
29 | 28 | nnrpd 11339 |
. . . . . . . . . . 11
                   
  |
30 | 26, 29 | rpdivcld 11358 |
. . . . . . . . . 10
                   
    |
31 | 14 | ffvelrni 6021 |
. . . . . . . . . 10
  
        |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
                   
        |
33 | 32 | recnd 9669 |
. . . . . . . 8
                   
        |
34 | 33 | abscld 13498 |
. . . . . . 7
                   
            |
35 | 29 | relogcld 23572 |
. . . . . . 7
                   
      |
36 | 34, 35 | remulcld 9671 |
. . . . . 6
                   
       
          |
37 | 25, 36 | fsumrecl 13800 |
. . . . 5
  

 
 
                              |
38 | 24, 37 | remulcld 9671 |
. . . 4
  

 
 
       
      
                       |
39 | 20, 38 | resubcld 10047 |
. . 3
  

 
 
                                                      |
40 | 39, 12 | rerpdivcld 11369 |
. 2
  

 
 
                                                        |
41 | 13 | pntrmax 24402 |
. . 3
           
 |
42 | | eqid 2451 |
. . . . 5
            Λ       ψ                   Λ       ψ        |
43 | | eqid 2451 |
. . . . 5
                           |
44 | | simprl 764 |
. . . . 5
  
                 |
45 | | simprr 766 |
. . . . 5
  
                            |
46 | | simpll 760 |
. . . . 5
  
                 |
47 | | simplr 762 |
. . . . 5
  
                 |
48 | 42, 13, 43, 44, 45, 46, 47 | pntrlog2bndlem6 24421 |
. . . 4
  
                                                                                |
49 | 48 | rexlimdvaa 2880 |
. . 3
                                                                                  |
50 | 41, 49 | mpi 20 |
. 2
                                                                    |
51 | | simprl 764 |
. . . . 5
  
 
 
  |
52 | | chpcl 24051 |
. . . . 5
 ψ    |
53 | 51, 52 | syl 17 |
. . . 4
  
 
 
ψ    |
54 | 53, 51 | readdcld 9670 |
. . 3
  
 
 
 ψ     |
55 | 5 | a1i 11 |
. . . . 5
  
 
 
  |
56 | | simprr 766 |
. . . . 5
  
 
 
  |
57 | 51, 55, 56 | rpgecld 11377 |
. . . 4
  
 
 
  |
58 | 57 | relogcld 23572 |
. . 3
  
 
 
      |
59 | 54, 58 | remulcld 9671 |
. 2
  
 
 
  ψ          |
60 | 40 | adantr 467 |
. . 3
          

 
                                                        |
61 | 53 | ad2ant2r 753 |
. . . . . 6
          

 
ψ    |
62 | | simprll 772 |
. . . . . 6
          

 
  |
63 | 61, 62 | readdcld 9670 |
. . . . 5
          

 
 ψ     |
64 | 57 | ad2ant2r 753 |
. . . . . 6
          

 
  |
65 | 64 | relogcld 23572 |
. . . . 5
          

 
      |
66 | 63, 65 | remulcld 9671 |
. . . 4
          

 
  ψ          |
67 | 12 | adantr 467 |
. . . 4
          

 
  |
68 | 66, 67 | rerpdivcld 11369 |
. . 3
          

 
   ψ           |
69 | 16 | adantr 467 |
. . . . . . . 8
          

 
      |
70 | 69 | recnd 9669 |
. . . . . . 7
          

 
      |
71 | 70 | abscld 13498 |
. . . . . 6
          

 
          |
72 | 67 | relogcld 23572 |
. . . . . 6
          

 
      |
73 | 71, 72 | remulcld 9671 |
. . . . 5
          

 
                |
74 | 24 | adantr 467 |
. . . . . 6
          

 
        |
75 | 37 | adantr 467 |
. . . . . 6
          

 
                              |
76 | 74, 75 | remulcld 9671 |
. . . . 5
          

 
       
      
                       |
77 | 73, 76 | resubcld 10047 |
. . . 4
          

 
                                                      |
78 | 21 | a1i 11 |
. . . . . . . 8
          

 
  |
79 | 4 | adantr 467 |
. . . . . . . . 9
          

 
  |
80 | 10 | adantr 467 |
. . . . . . . . 9
          

 
  |
81 | 79, 80 | rplogcld 23578 |
. . . . . . . 8
          

 
      |
82 | | 2rp 11307 |
. . . . . . . . . 10
 |
83 | 82 | a1i 11 |
. . . . . . . . 9
          

 
  |
84 | 83 | rpge0d 11345 |
. . . . . . . 8
          

 
  |
85 | 78, 81, 84 | divge0d 11378 |
. . . . . . 7
          

 
        |
86 | | fzfid 12186 |
. . . . . . . 8
          

 
      
     |
87 | 36 | adantlr 721 |
. . . . . . . 8
           

            
       
          |
88 | 33 | adantlr 721 |
. . . . . . . . . 10
           

            
        |
89 | 88 | abscld 13498 |
. . . . . . . . 9
           

            
            |
90 | 29 | adantlr 721 |
. . . . . . . . . 10
           

            
  |
91 | 90 | relogcld 23572 |
. . . . . . . . 9
           

            
      |
92 | 88 | absge0d 13506 |
. . . . . . . . 9
           

            
            |
93 | 90 | rpred 11341 |
. . . . . . . . . 10
           

            
  |
94 | 27 | adantl 468 |
. . . . . . . . . . 11
           

            
  |
95 | 94 | nnge1d 10652 |
. . . . . . . . . 10
           

            
  |
96 | 93, 95 | logge0d 23579 |
. . . . . . . . 9
           

            
      |
97 | 89, 91, 92, 96 | mulge0d 10190 |
. . . . . . . 8
           

            
                  |
98 | 86, 87, 97 | fsumge0 13855 |
. . . . . . 7
          

 
       
                      |
99 | 74, 75, 85, 98 | mulge0d 10190 |
. . . . . 6
          

 
                                      |
100 | 73, 76 | subge02d 10205 |
. . . . . 6
          

 
                                    
                                                                     |
101 | 99, 100 | mpbid 214 |
. . . . 5
          

 
                                                                    |
102 | 70 | absge0d 13506 |
. . . . . 6
          

 
          |
103 | 81 | rpge0d 11345 |
. . . . . 6
          

 
      |
104 | | chpcl 24051 |
. . . . . . . . 9
 ψ    |
105 | 79, 104 | syl 17 |
. . . . . . . 8
          

 
ψ    |
106 | 105, 79 | readdcld 9670 |
. . . . . . 7
          

 
 ψ     |
107 | 13 | pntrval 24400 |
. . . . . . . . . 10

     ψ     |
108 | 67, 107 | syl 17 |
. . . . . . . . 9
          

 
     ψ     |
109 | 108 | fveq2d 5869 |
. . . . . . . 8
          

 
            ψ      |
110 | 105 | recnd 9669 |
. . . . . . . . . 10
          

 
ψ    |
111 | 79 | recnd 9669 |
. . . . . . . . . 10
          

 
  |
112 | 110, 111 | abs2dif2d 13520 |
. . . . . . . . 9
          

 
    ψ   
    ψ          |
113 | | chpge0 24053 |
. . . . . . . . . . . 12
 ψ    |
114 | 79, 113 | syl 17 |
. . . . . . . . . . 11
          

 
ψ    |
115 | 105, 114 | absidd 13484 |
. . . . . . . . . 10
          

 
   ψ   ψ    |
116 | 67 | rpge0d 11345 |
. . . . . . . . . . 11
          

 
  |
117 | 79, 116 | absidd 13484 |
. . . . . . . . . 10
          

 
      |
118 | 115, 117 | oveq12d 6308 |
. . . . . . . . 9
          

 
    ψ         ψ     |
119 | 112, 118 | breqtrd 4427 |
. . . . . . . 8
          

 
    ψ   
 ψ     |
120 | 109, 119 | eqbrtrd 4423 |
. . . . . . 7
          

 
         ψ     |
121 | | simprr 766 |
. . . . . . . . . 10
          

 
  |
122 | 79, 62, 121 | ltled 9783 |
. . . . . . . . 9
          

 
  |
123 | | chpwordi 24084 |
. . . . . . . . 9
 
 ψ  ψ    |
124 | 79, 62, 122, 123 | syl3anc 1268 |
. . . . . . . 8
          

 
ψ 
ψ    |
125 | 105, 79, 61, 62, 124, 122 | le2addd 10232 |
. . . . . . 7
          

 
 ψ  
 ψ     |
126 | 71, 106, 63, 120, 125 | letrd 9792 |
. . . . . 6
          

 
         ψ     |
127 | 67, 64 | logled 23576 |
. . . . . . 7
          

 
    
       |
128 | 122, 127 | mpbid 214 |
. . . . . 6
          

 
          |
129 | 71, 63, 72, 65, 102, 103, 126, 128 | lemul12ad 10549 |
. . . . 5
          

 
                ψ          |
130 | 77, 73, 66, 101, 129 | letrd 9792 |
. . . 4
          

 
                                                      ψ          |
131 | 77, 66, 67, 130 | lediv1dd 11396 |
. . 3
          

 
                                                         ψ           |
132 | 5 | a1i 11 |
. . . . 5
          

 
  |
133 | | chpge0 24053 |
. . . . . . . 8
 ψ    |
134 | 62, 133 | syl 17 |
. . . . . . 7
          

 
ψ    |
135 | 64 | rpge0d 11345 |
. . . . . . 7
          

 
  |
136 | 61, 62, 134, 135 | addge0d 10189 |
. . . . . 6
          

 
 ψ     |
137 | | simprlr 773 |
. . . . . . 7
          

 
  |
138 | 62, 137 | logge0d 23579 |
. . . . . 6
          

 
      |
139 | 63, 65, 136, 138 | mulge0d 10190 |
. . . . 5
          

 
  ψ          |
140 | 11 | adantr 467 |
. . . . 5
          

 
  |
141 | 132, 67, 66, 139, 140 | lediv2ad 11363 |
. . . 4
          

 
   ψ        
   ψ           |
142 | 61 | recnd 9669 |
. . . . . . 7
          

 
ψ    |
143 | 62 | recnd 9669 |
. . . . . . 7
          

 
  |
144 | 142, 143 | addcld 9662 |
. . . . . 6
          

 
 ψ     |
145 | 65 | recnd 9669 |
. . . . . 6
          

 
      |
146 | 144, 145 | mulcld 9663 |
. . . . 5
          

 
  ψ          |
147 | 146 | div1d 10375 |
. . . 4
          

 
   ψ           ψ          |
148 | 141, 147 | breqtrd 4427 |
. . 3
          

 
   ψ        
  ψ          |
149 | 60, 68, 66, 131, 148 | letrd 9792 |
. 2
          

 
                                                        ψ          |
150 | 2, 3, 40, 50, 59, 149 | lo1bddrp 13589 |
1
   
                                                             |