Step | Hyp | Ref
| Expression |
1 | | fzfid 12186 |
. . . . 5
 
   ![[,] [,]](_icc.gif)                        |
2 | | inss2 3653 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)    |
3 | | simpr 463 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)     |
4 | 2, 3 | sseldi 3430 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)   
  |
5 | | prmnn 14625 |
. . . . . . . . 9

  |
6 | 4, 5 | syl 17 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)   
  |
7 | 6 | nnrpd 11339 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)   
  |
8 | 7 | relogcld 23572 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)          |
9 | 8 | recnd 9669 |
. . . . 5
 
   ![[,] [,]](_icc.gif)          |
10 | | fsumconst 13851 |
. . . . 5
                                                                               |
11 | 1, 9, 10 | syl2anc 667 |
. . . 4
 
   ![[,] [,]](_icc.gif)                                                          |
12 | | simpl 459 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)   
  |
13 | | 1red 9658 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)      |
14 | 6 | nnred 10624 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)   
  |
15 | | prmuz2 14642 |
. . . . . . . . . . . . 13

      |
16 | 4, 15 | syl 17 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)   
      |
17 | | eluz2b2 11231 |
. . . . . . . . . . . . 13
         |
18 | 17 | simprbi 466 |
. . . . . . . . . . . 12
    
  |
19 | 16, 18 | syl 17 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)   
  |
20 | | inss1 3652 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   |
21 | 20, 3 | sseldi 3430 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)    |
22 | | 0re 9643 |
. . . . . . . . . . . . . 14
 |
23 | | elicc2 11699 |
. . . . . . . . . . . . . 14
 
    ![[,] [,]](_icc.gif)  
    |
24 | 22, 12, 23 | sylancr 669 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)  
    |
25 | 21, 24 | mpbid 214 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)    
   |
26 | 25 | simp3d 1022 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)      |
27 | 13, 14, 12, 19, 26 | ltletrd 9795 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)   
  |
28 | 12, 27 | rplogcld 23578 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)          |
29 | 14, 19 | rplogcld 23578 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)          |
30 | 28, 29 | rpdivcld 11358 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)                |
31 | 30 | rpred 11341 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)                |
32 | 30 | rpge0d 11345 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)   
            |
33 | | flge0nn0 12054 |
. . . . . . 7
                                       |
34 | 31, 32, 33 | syl2anc 667 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)                    |
35 | | hashfz1 12529 |
. . . . . 6
                                                     |
36 | 34, 35 | syl 17 |
. . . . 5
 
   ![[,] [,]](_icc.gif)                                          |
37 | 36 | oveq1d 6305 |
. . . 4
 
   ![[,] [,]](_icc.gif)                                                      |
38 | 31 | flcld 12034 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)                    |
39 | 38 | zcnd 11041 |
. . . . 5
 
   ![[,] [,]](_icc.gif)                    |
40 | 39, 9 | mulcomd 9664 |
. . . 4
 
   ![[,] [,]](_icc.gif)                                              |
41 | 11, 37, 40 | 3eqtrrd 2490 |
. . 3
 
   ![[,] [,]](_icc.gif)                        
                         |
42 | 41 | sumeq2dv 13769 |
. 2
     ![[,] [,]](_icc.gif)                            ![[,] [,]](_icc.gif)                              |
43 | | chpval2 24146 |
. 2
 ψ      ![[,] [,]](_icc.gif)                          |
44 | | simpl 459 |
. . . . . 6
 
           |
45 | | 0red 9644 |
. . . . . . 7
 
           |
46 | | 1red 9658 |
. . . . . . . 8
 
           |
47 | | 0lt1 10136 |
. . . . . . . . 9
 |
48 | 47 | a1i 11 |
. . . . . . . 8
 
           |
49 | | elfzuz2 11804 |
. . . . . . . . 9
                   |
50 | | eluzle 11171 |
. . . . . . . . . . 11
        
      |
51 | 50 | adantl 468 |
. . . . . . . . . 10
                 |
52 | | simpl 459 |
. . . . . . . . . . 11
             |
53 | | 1z 10967 |
. . . . . . . . . . 11
 |
54 | | flge 12041 |
. . . . . . . . . . 11
 
         |
55 | 52, 53, 54 | sylancl 668 |
. . . . . . . . . 10
           
       |
56 | 51, 55 | mpbird 236 |
. . . . . . . . 9
             |
57 | 49, 56 | sylan2 477 |
. . . . . . . 8
 
           |
58 | 45, 46, 44, 48, 57 | ltletrd 9795 |
. . . . . . 7
 
           |
59 | 45, 44, 58 | ltled 9783 |
. . . . . 6
 
           |
60 | | elfznn 11828 |
. . . . . . . 8
           |
61 | 60 | adantl 468 |
. . . . . . 7
 
           |
62 | 61 | nnrecred 10655 |
. . . . . 6
 
             |
63 | 44, 59, 62 | recxpcld 23668 |
. . . . 5
 
                |
64 | | chtval 24037 |
. . . . 5
                   ![[,] [,]](_icc.gif)               |
65 | 63, 64 | syl 17 |
. . . 4
 
                      ![[,] [,]](_icc.gif)               |
66 | 65 | sumeq2dv 13769 |
. . 3
               
              
   ![[,] [,]](_icc.gif)               |
67 | | ppifi 24032 |
. . . 4
    ![[,] [,]](_icc.gif) 
   |
68 | | fzfid 12186 |
. . . 4
           |
69 | 2 | sseli 3428 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)  
  |
70 | | elfznn 11828 |
. . . . . . . 8
                  
  |
71 | 69, 70 | anim12i 570 |
. . . . . . 7
     ![[,] [,]](_icc.gif)                          |
72 | 71 | a1i 11 |
. . . . . 6
      ![[,] [,]](_icc.gif) 

                        |
73 | | 0red 9644 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)      |
74 | 2 | a1i 11 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
   |
75 | 74 | sselda 3432 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)   
  |
76 | 75, 5 | syl 17 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)   
  |
77 | 76 | nnred 10624 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)   
  |
78 | 76 | nngt0d 10653 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)   
  |
79 | 73, 77, 12, 78, 26 | ltletrd 9795 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)   
  |
80 | 79 | ex 436 |
. . . . . . 7
     ![[,] [,]](_icc.gif)      |
81 | 80 | adantrd 470 |
. . . . . 6
      ![[,] [,]](_icc.gif) 

                      |
82 | 72, 81 | jcad 536 |
. . . . 5
      ![[,] [,]](_icc.gif) 

                          |
83 | | inss2 3653 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)         |
84 | 83 | sseli 3428 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)          |
85 | 60, 84 | anim12ci 571 |
. . . . . . 7
         
   ![[,] [,]](_icc.gif)        

   |
86 | 85 | a1i 11 |
. . . . . 6
              ![[,] [,]](_icc.gif)        

    |
87 | 58 | ex 436 |
. . . . . . 7
         
   |
88 | 87 | adantrd 470 |
. . . . . 6
              ![[,] [,]](_icc.gif)        
   |
89 | 86, 88 | jcad 536 |
. . . . 5
              ![[,] [,]](_icc.gif)        
       |
90 | | elin 3617 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif) 
   |
91 | | simprll 772 |
. . . . . . . . . . 11
         |
92 | 91 | biantrud 510 |
. . . . . . . . . 10
          ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif) 
    |
93 | | 0red 9644 |
. . . . . . . . . . 11
         |
94 | | simpl 459 |
. . . . . . . . . . 11
         |
95 | 91, 5 | syl 17 |
. . . . . . . . . . . 12
         |
96 | 95 | nnred 10624 |
. . . . . . . . . . 11
         |
97 | 95 | nnnn0d 10925 |
. . . . . . . . . . . 12
         |
98 | 97 | nn0ge0d 10928 |
. . . . . . . . . . 11
         |
99 | | df-3an 987 |
. . . . . . . . . . . . 13
  
      |
100 | 23, 99 | syl6bb 265 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif)         |
101 | 100 | baibd 920 |
. . . . . . . . . . 11
          ![[,] [,]](_icc.gif) 
   |
102 | 93, 94, 96, 98, 101 | syl22anc 1269 |
. . . . . . . . . 10
          ![[,] [,]](_icc.gif) 
   |
103 | 92, 102 | bitr3d 259 |
. . . . . . . . 9
           ![[,] [,]](_icc.gif)  
   |
104 | 90, 103 | syl5bb 261 |
. . . . . . . 8
           ![[,] [,]](_icc.gif)  
   |
105 | | simprr 766 |
. . . . . . . . . . . . 13
         |
106 | 94, 105 | elrpd 11338 |
. . . . . . . . . . . 12
         |
107 | 106 | relogcld 23572 |
. . . . . . . . . . 11
             |
108 | 91, 15 | syl 17 |
. . . . . . . . . . . . 13
             |
109 | 108, 18 | syl 17 |
. . . . . . . . . . . 12
         |
110 | 96, 109 | rplogcld 23578 |
. . . . . . . . . . 11
             |
111 | 107, 110 | rerpdivcld 11369 |
. . . . . . . . . 10
                   |
112 | | simprlr 773 |
. . . . . . . . . . 11
         |
113 | 112 | nnzd 11039 |
. . . . . . . . . 10
         |
114 | | flge 12041 |
. . . . . . . . . 10
             
         
                 |
115 | 111, 113,
114 | syl2anc 667 |
. . . . . . . . 9
       
         
                 |
116 | 112 | nnnn0d 10925 |
. . . . . . . . . . . . 13
         |
117 | 95, 116 | nnexpcld 12437 |
. . . . . . . . . . . 12
             |
118 | 117 | nnrpd 11339 |
. . . . . . . . . . 11
             |
119 | 118, 106 | logled 23576 |
. . . . . . . . . 10
           
               |
120 | 95 | nnrpd 11339 |
. . . . . . . . . . . 12
         |
121 | | relogexp 23545 |
. . . . . . . . . . . 12
                   |
122 | 120, 113,
121 | syl2anc 667 |
. . . . . . . . . . 11
                       |
123 | 122 | breq1d 4412 |
. . . . . . . . . 10
               
   
             |
124 | 112 | nnred 10624 |
. . . . . . . . . . 11
         |
125 | 124, 107,
110 | lemuldivd 11387 |
. . . . . . . . . 10
                               |
126 | 119, 123,
125 | 3bitrd 283 |
. . . . . . . . 9
           
             |
127 | | nnuz 11194 |
. . . . . . . . . . 11
     |
128 | 112, 127 | syl6eleq 2539 |
. . . . . . . . . 10
             |
129 | 111 | flcld 12034 |
. . . . . . . . . 10
                       |
130 | | elfz5 11792 |
. . . . . . . . . 10
                                       
                 |
131 | 128, 129,
130 | syl2anc 667 |
. . . . . . . . 9
                                           |
132 | 115, 126,
131 | 3bitr4rd 290 |
. . . . . . . 8
                                 |
133 | 104, 132 | anbi12d 717 |
. . . . . . 7
            ![[,] [,]](_icc.gif) 

                  
         |
134 | 94 | flcld 12034 |
. . . . . . . . . . 11
             |
135 | | elfz5 11792 |
. . . . . . . . . . 11
                   
       |
136 | 128, 134,
135 | syl2anc 667 |
. . . . . . . . . 10
               
       |
137 | | flge 12041 |
. . . . . . . . . . 11
 
         |
138 | 94, 113, 137 | syl2anc 667 |
. . . . . . . . . 10
       
       |
139 | 136, 138 | bitr4d 260 |
. . . . . . . . 9
               
   |
140 | | elin 3617 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)       
   ![[,] [,]](_icc.gif)          |
141 | 91 | biantrud 510 |
. . . . . . . . . . . 12
          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)           |
142 | 106 | rpge0d 11345 |
. . . . . . . . . . . . . 14
         |
143 | 112 | nnrecred 10655 |
. . . . . . . . . . . . . 14
           |
144 | 94, 142, 143 | recxpcld 23668 |
. . . . . . . . . . . . 13
              |
145 | | elicc2 11699 |
. . . . . . . . . . . . . . 15
  
        ![[,] [,]](_icc.gif)                 |
146 | | df-3an 987 |
. . . . . . . . . . . . . . 15
       
           |
147 | 145, 146 | syl6bb 265 |
. . . . . . . . . . . . . 14
  
        ![[,] [,]](_icc.gif)                   |
148 | 147 | baibd 920 |
. . . . . . . . . . . . 13
               ![[,] [,]](_icc.gif)      
        |
149 | 93, 144, 96, 98, 148 | syl22anc 1269 |
. . . . . . . . . . . 12
          ![[,] [,]](_icc.gif)      
 
      |
150 | 141, 149 | bitr3d 259 |
. . . . . . . . . . 11
           ![[,] [,]](_icc.gif)       
        |
151 | 94, 142, 143 | cxpge0d 23669 |
. . . . . . . . . . . 12
              |
152 | 112 | nnrpd 11339 |
. . . . . . . . . . . 12
         |
153 | 96, 98, 144, 151, 152 | cxple2d 23672 |
. . . . . . . . . . 11
       
 
                 |
154 | 95 | nncnd 10625 |
. . . . . . . . . . . . 13
         |
155 | | cxpexp 23613 |
. . . . . . . . . . . . 13
 
          |
156 | 154, 116,
155 | syl2anc 667 |
. . . . . . . . . . . 12
                |
157 | 112 | nncnd 10625 |
. . . . . . . . . . . . . . 15
         |
158 | 112 | nnne0d 10654 |
. . . . . . . . . . . . . . 15
         |
159 | 157, 158 | recid2d 10379 |
. . . . . . . . . . . . . 14
             |
160 | 159 | oveq2d 6306 |
. . . . . . . . . . . . 13
                   |
161 | 106, 143,
157 | cxpmuld 23679 |
. . . . . . . . . . . . 13
                        |
162 | 94 | recnd 9669 |
. . . . . . . . . . . . . 14
         |
163 | 162 | cxp1d 23651 |
. . . . . . . . . . . . 13
            |
164 | 160, 161,
163 | 3eqtr3d 2493 |
. . . . . . . . . . . 12
                 |
165 | 156, 164 | breq12d 4415 |
. . . . . . . . . . 11
                  
       |
166 | 150, 153,
165 | 3bitrd 283 |
. . . . . . . . . 10
           ![[,] [,]](_icc.gif)       
       |
167 | 140, 166 | syl5bb 261 |
. . . . . . . . 9
           ![[,] [,]](_icc.gif)               |
168 | 139, 167 | anbi12d 717 |
. . . . . . . 8
                    ![[,] [,]](_icc.gif)                  |
169 | 117 | nnred 10624 |
. . . . . . . . . . 11
             |
170 | | bernneq3 12400 |
. . . . . . . . . . . 12
             |
171 | 108, 116,
170 | syl2anc 667 |
. . . . . . . . . . 11
             |
172 | 124, 169,
171 | ltled 9783 |
. . . . . . . . . 10
             |
173 | | letr 9727 |
. . . . . . . . . . 11
     
      
        |
174 | 124, 169,
94, 173 | syl3anc 1268 |
. . . . . . . . . 10
                 
   |
175 | 172, 174 | mpand 681 |
. . . . . . . . 9
           
   |
176 | 175 | pm4.71rd 641 |
. . . . . . . 8
           
         |
177 | 154 | exp1d 12411 |
. . . . . . . . . . 11
             |
178 | 95 | nnge1d 10652 |
. . . . . . . . . . . 12
         |
179 | 96, 178, 128 | leexp2ad 12448 |
. . . . . . . . . . 11
                 |
180 | 177, 179 | eqbrtrrd 4425 |
. . . . . . . . . 10
             |
181 | | letr 9727 |
. . . . . . . . . . 11
     
      
        |
182 | 96, 169, 94, 181 | syl3anc 1268 |
. . . . . . . . . 10
                 
   |
183 | 180, 182 | mpand 681 |
. . . . . . . . 9
           
   |
184 | 183 | pm4.71rd 641 |
. . . . . . . 8
           
         |
185 | 168, 176,
184 | 3bitr2rd 286 |
. . . . . . 7
            
         
   ![[,] [,]](_icc.gif)            |
186 | 133, 185 | bitrd 257 |
. . . . . 6
            ![[,] [,]](_icc.gif) 

                  
            ![[,] [,]](_icc.gif)            |
187 | 186 | ex 436 |
. . . . 5
     
     ![[,] [,]](_icc.gif)                     
            ![[,] [,]](_icc.gif)             |
188 | 82, 89, 187 | pm5.21ndd 356 |
. . . 4
      ![[,] [,]](_icc.gif) 

                  
            ![[,] [,]](_icc.gif)            |
189 | 9 | adantrr 723 |
. . . 4
  
   ![[,] [,]](_icc.gif) 

                          |
190 | 67, 68, 1, 188, 189 | fsumcom2 13835 |
. . 3
     ![[,] [,]](_icc.gif)                            
             ![[,] [,]](_icc.gif)               |
191 | 66, 190 | eqtr4d 2488 |
. 2
               
        ![[,] [,]](_icc.gif)                              |
192 | 42, 43, 191 | 3eqtr4d 2495 |
1
 ψ  
                    |