Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . 7
  ψ     |
2 | | pntlem1.a |
. . . . . . 7
   |
3 | | pntlem1.b |
. . . . . . 7
   |
4 | | pntlem1.l |
. . . . . . 7
       |
5 | | pntlem1.d |
. . . . . . 7
   |
6 | | pntlem1.f |
. . . . . . 7
       ;          |
7 | | pntlem1.u |
. . . . . . 7
   |
8 | | pntlem1.u2 |
. . . . . . 7

  |
9 | | pntlem1.e |
. . . . . . 7
   |
10 | | pntlem1.k |
. . . . . . 7
       |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 24433 |
. . . . . 6
  
    
     |
12 | 11 | simp3d 1022 |
. . . . 5
           |
13 | 12 | simp3d 1022 |
. . . 4
     |
14 | 1, 2, 3, 4, 5, 6 | pntlemd 24432 |
. . . . . . . 8
     |
15 | 14 | simp1d 1020 |
. . . . . . 7
   |
16 | 11 | simp1d 1020 |
. . . . . . . 8
   |
17 | | 2z 10969 |
. . . . . . . 8
 |
18 | | rpexpcl 12291 |
. . . . . . . 8
         |
19 | 16, 17, 18 | sylancl 668 |
. . . . . . 7
       |
20 | 15, 19 | rpmulcld 11357 |
. . . . . 6
         |
21 | | 3nn0 10887 |
. . . . . . . . 9
 |
22 | | 2nn 10767 |
. . . . . . . . 9
 |
23 | 21, 22 | decnncl 11064 |
. . . . . . . 8
;  |
24 | | nnrp 11311 |
. . . . . . . 8
; ;   |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
;  |
26 | | rpmulcl 11324 |
. . . . . . 7
 ;  ;    |
27 | 25, 3, 26 | sylancr 669 |
. . . . . 6
 ;    |
28 | 20, 27 | rpdivcld 11358 |
. . . . 5
        ;     |
29 | | pntlem1.y |
. . . . . . . . . 10
 
   |
30 | | pntlem1.x |
. . . . . . . . . 10
     |
31 | | pntlem1.c |
. . . . . . . . . 10
   |
32 | | pntlem1.w |
. . . . . . . . . 10
                           ;                      |
33 | | pntlem1.z |
. . . . . . . . . 10
      |
34 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33 | pntlemb 24435 |
. . . . . . . . 9
  
             
 
                                           ;             |
35 | 34 | simp1d 1020 |
. . . . . . . 8
   |
36 | 35 | rpred 11341 |
. . . . . . 7
   |
37 | 34 | simp2d 1021 |
. . . . . . . 8
 
             |
38 | 37 | simp1d 1020 |
. . . . . . 7
   |
39 | 36, 38 | rplogcld 23578 |
. . . . . 6
       |
40 | | rpexpcl 12291 |
. . . . . 6
                 |
41 | 39, 17, 40 | sylancl 668 |
. . . . 5
           |
42 | 28, 41 | rpmulcld 11357 |
. . . 4
         ;              |
43 | 13, 42 | rpmulcld 11357 |
. . 3
            ;               |
44 | 43 | rpred 11341 |
. 2
            ;               |
45 | 15, 16 | rpmulcld 11357 |
. . . . . . 7
     |
46 | | 8re 10694 |
. . . . . . . 8
 |
47 | | 8pos 10710 |
. . . . . . . 8
 |
48 | 46, 47 | elrpii 11305 |
. . . . . . 7
 |
49 | | rpdivcl 11325 |
. . . . . . 7
           |
50 | 45, 48, 49 | sylancl 668 |
. . . . . 6
       |
51 | 50, 39 | rpmulcld 11357 |
. . . . 5
             |
52 | 13, 51 | rpmulcld 11357 |
. . . 4
                 |
53 | 52 | rpred 11341 |
. . 3
                 |
54 | | pntlem1.m |
. . . . . . . 8
                 |
55 | | pntlem1.n |
. . . . . . . 8
                 |
56 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55 | pntlemg 24436 |
. . . . . . 7
                  
    |
57 | 56 | simp1d 1020 |
. . . . . 6
   |
58 | 56 | simp2d 1021 |
. . . . . 6
       |
59 | | eluznn 11229 |
. . . . . 6
 
    
  |
60 | 57, 58, 59 | syl2anc 667 |
. . . . 5
   |
61 | 60 | nnred 10624 |
. . . 4
   |
62 | 57 | nnred 10624 |
. . . 4
   |
63 | 61, 62 | resubcld 10047 |
. . 3
     |
64 | 53, 63 | remulcld 9671 |
. 2
                     |
65 | | fzfid 12186 |
. . 3
             |
66 | 7 | rpred 11341 |
. . . . . 6
   |
67 | | elfznn 11828 |
. . . . . 6
          
  |
68 | | nndivre 10645 |
. . . . . 6
 
     |
69 | 66, 67, 68 | syl2an 480 |
. . . . 5
 
          
    |
70 | 35 | adantr 467 |
. . . . . . . . . 10
 
          
  |
71 | 67 | adantl 468 |
. . . . . . . . . . 11
 
          
  |
72 | 71 | nnrpd 11339 |
. . . . . . . . . 10
 
          
  |
73 | 70, 72 | rpdivcld 11358 |
. . . . . . . . 9
 
          
    |
74 | 1 | pntrf 24401 |
. . . . . . . . . 10
     |
75 | 74 | ffvelrni 6021 |
. . . . . . . . 9
  
        |
76 | 73, 75 | syl 17 |
. . . . . . . 8
 
          
        |
77 | 76, 70 | rerpdivcld 11369 |
. . . . . . 7
 
          
          |
78 | 77 | recnd 9669 |
. . . . . 6
 
          
          |
79 | 78 | abscld 13498 |
. . . . 5
 
          
       
      |
80 | 69, 79 | resubcld 10047 |
. . . 4
 
          
                  |
81 | 72 | relogcld 23572 |
. . . 4
 
          
      |
82 | 80, 81 | remulcld 9671 |
. . 3
 
          
           
            |
83 | 65, 82 | fsumrecl 13800 |
. 2
 
      
                            |
84 | 45 | rpcnd 11343 |
. . . . . . . . 9
     |
85 | 11 | simp2d 1021 |
. . . . . . . . . . . . 13
   |
86 | 85 | rpred 11341 |
. . . . . . . . . . . 12
   |
87 | 12 | simp2d 1021 |
. . . . . . . . . . . 12
   |
88 | 86, 87 | rplogcld 23578 |
. . . . . . . . . . 11
       |
89 | 39, 88 | rpdivcld 11358 |
. . . . . . . . . 10
             |
90 | 89 | rpcnd 11343 |
. . . . . . . . 9
             |
91 | | rpcnne0 11319 |
. . . . . . . . . 10

    |
92 | 48, 91 | mp1i 13 |
. . . . . . . . 9
     |
93 | | 4re 10686 |
. . . . . . . . . . 11
 |
94 | | 4pos 10705 |
. . . . . . . . . . 11
 |
95 | 93, 94 | elrpii 11305 |
. . . . . . . . . 10
 |
96 | | rpcnne0 11319 |
. . . . . . . . . 10

    |
97 | 95, 96 | mp1i 13 |
. . . . . . . . 9
     |
98 | | divmuldiv 10307 |
. . . . . . . . 9
                                                             |
99 | 84, 90, 92, 97, 98 | syl22anc 1269 |
. . . . . . . 8
                                       |
100 | 10 | fveq2i 5868 |
. . . . . . . . . . . . . 14
               |
101 | 3, 16 | rpdivcld 11358 |
. . . . . . . . . . . . . . . 16
     |
102 | 101 | rpred 11341 |
. . . . . . . . . . . . . . 15
     |
103 | 102 | relogefd 23577 |
. . . . . . . . . . . . . 14
               |
104 | 100, 103 | syl5eq 2497 |
. . . . . . . . . . . . 13
         |
105 | 104 | oveq2d 6306 |
. . . . . . . . . . . 12
                     |
106 | 39 | rpcnd 11343 |
. . . . . . . . . . . . 13
       |
107 | 3 | rpcnne0d 11350 |
. . . . . . . . . . . . 13
     |
108 | 16 | rpcnne0d 11350 |
. . . . . . . . . . . . 13
     |
109 | | divdiv2 10319 |
. . . . . . . . . . . . 13
      
                      |
110 | 106, 107,
108, 109 | syl3anc 1268 |
. . . . . . . . . . . 12
                   |
111 | 105, 110 | eqtrd 2485 |
. . . . . . . . . . 11
                     |
112 | 111 | oveq2d 6306 |
. . . . . . . . . 10
                             |
113 | 16 | rpcnd 11343 |
. . . . . . . . . . . 12
   |
114 | 106, 113 | mulcld 9663 |
. . . . . . . . . . 11
         |
115 | | divass 10288 |
. . . . . . . . . . 11
          
                            |
116 | 84, 114, 107, 115 | syl3anc 1268 |
. . . . . . . . . 10
                           |
117 | 15 | rpcnd 11343 |
. . . . . . . . . . . . 13
   |
118 | 117, 113,
106, 113 | mul4d 9845 |
. . . . . . . . . . . 12
                       |
119 | 113 | sqvald 12413 |
. . . . . . . . . . . . 13
         |
120 | 119 | oveq2d 6306 |
. . . . . . . . . . . 12
                    
    |
121 | 113 | sqcld 12414 |
. . . . . . . . . . . . 13
       |
122 | 117, 106,
121 | mul32d 9843 |
. . . . . . . . . . . 12
                           |
123 | 118, 120,
122 | 3eqtr2d 2491 |
. . . . . . . . . . 11
                         |
124 | 123 | oveq1d 6305 |
. . . . . . . . . 10
                             |
125 | 112, 116,
124 | 3eqtr2d 2491 |
. . . . . . . . 9
                               |
126 | | 8t4e32 11141 |
. . . . . . . . . 10
  ;  |
127 | 126 | a1i 11 |
. . . . . . . . 9
   ;   |
128 | 125, 127 | oveq12d 6308 |
. . . . . . . 8
                                 
;    |
129 | 20 | rpcnd 11343 |
. . . . . . . . . . 11
         |
130 | 129, 106 | mulcld 9663 |
. . . . . . . . . 10
               |
131 | | rpcnne0 11319 |
. . . . . . . . . . 11
; ; ;    |
132 | 25, 131 | mp1i 13 |
. . . . . . . . . 10
 ; ;    |
133 | | divdiv1 10318 |
. . . . . . . . . 10
                ; ;                 
;               
;     |
134 | 130, 107,
132, 133 | syl3anc 1268 |
. . . . . . . . 9
               
;               
;     |
135 | 23 | nncni 10619 |
. . . . . . . . . . 11
;  |
136 | 3 | rpcnd 11343 |
. . . . . . . . . . 11
   |
137 | | mulcom 9625 |
. . . . . . . . . . 11
 ;
 ;   ;    |
138 | 135, 136,
137 | sylancr 669 |
. . . . . . . . . 10
 ;   ;    |
139 | 138 | oveq2d 6306 |
. . . . . . . . 9
              ;                
;     |
140 | 27 | rpcnne0d 11350 |
. . . . . . . . . 10
  ;  ;     |
141 | | div23 10289 |
. . . . . . . . . 10
             ;  ;                 ;           ;          |
142 | 129, 106,
140, 141 | syl3anc 1268 |
. . . . . . . . 9
              ;           ;          |
143 | 134, 139,
142 | 3eqtr2d 2491 |
. . . . . . . 8
               
;          ;          |
144 | 99, 128, 143 | 3eqtrd 2489 |
. . . . . . 7
                           ;          |
145 | 144 | oveq1d 6305 |
. . . . . 6
                                  ;               |
146 | 50 | rpcnd 11343 |
. . . . . . 7
       |
147 | 89 | rpred 11341 |
. . . . . . . . 9
             |
148 | | 4nn 10769 |
. . . . . . . . 9
 |
149 | | nndivre 10645 |
. . . . . . . . 9
                           |
150 | 147, 148,
149 | sylancl 668 |
. . . . . . . 8
               |
151 | 150 | recnd 9669 |
. . . . . . 7
               |
152 | 146, 106,
151 | mul32d 9843 |
. . . . . 6
                                                   |
153 | 106 | sqvald 12413 |
. . . . . . . 8
                     |
154 | 153 | oveq2d 6306 |
. . . . . . 7
         ;                    ;                |
155 | 28 | rpcnd 11343 |
. . . . . . . 8
        ;     |
156 | 155, 106,
106 | mulassd 9666 |
. . . . . . 7
          ;                     ;                |
157 | 154, 156 | eqtr4d 2488 |
. . . . . 6
         ;                     ;               |
158 | 145, 152,
157 | 3eqtr4d 2495 |
. . . . 5
                                 ;              |
159 | 56 | simp3d 1022 |
. . . . . 6
                 |
160 | 150, 63, 51 | lemul2d 11382 |
. . . . . 6
             
 
                                   
     |
161 | 159, 160 | mpbid 214 |
. . . . 5
                                    
    |
162 | 158, 161 | eqbrtrrd 4425 |
. . . 4
         ;           
                |
163 | 42 | rpred 11341 |
. . . . 5
         ;              |
164 | 51 | rpred 11341 |
. . . . . 6
             |
165 | 164, 63 | remulcld 9671 |
. . . . 5
            
    |
166 | 163, 165,
13 | lemul2d 11382 |
. . . 4
          ;           
             
 
         ;                                  |
167 | 162, 166 | mpbid 214 |
. . 3
            ;                                 |
168 | 13 | rpcnd 11343 |
. . . 4
     |
169 | 51 | rpcnd 11343 |
. . . 4
             |
170 | 63 | recnd 9669 |
. . . 4
     |
171 | 168, 169,
170 | mulassd 9666 |
. . 3
                                 
     |
172 | 167, 171 | breqtrrd 4429 |
. 2
            ;                                 |
173 | | fzfid 12186 |
. . . 4
                         |
174 | 60 | nnzd 11039 |
. . . . . . . . . . . 12
   |
175 | 85, 174 | rpexpcld 12439 |
. . . . . . . . . . 11
       |
176 | 35, 175 | rpdivcld 11358 |
. . . . . . . . . 10
         |
177 | 176 | rprege0d 11348 |
. . . . . . . . 9
       
         |
178 | | flge0nn0 12054 |
. . . . . . . . 9
              
            |
179 | | nn0p1nn 10909 |
. . . . . . . . 9
          
              |
180 | 177, 178,
179 | 3syl 18 |
. . . . . . . 8
     
         |
181 | | nnuz 11194 |
. . . . . . . 8
     |
182 | 180, 181 | syl6eleq 2539 |
. . . . . . 7
     
             |
183 | | fzss1 11837 |
. . . . . . 7
                                                   |
184 | 182, 183 | syl 17 |
. . . . . 6
                                   |
185 | 184 | sselda 3432 |
. . . . 5
 
                      
            |
186 | 185, 82 | syldan 473 |
. . . 4
 
                      
           
            |
187 | 173, 186 | fsumrecl 13800 |
. . 3
 
     
            
                            |
188 | | eluzfz2 11807 |
. . . . 5
    
      |
189 | 58, 188 | syl 17 |
. . . 4
       |
190 | | oveq1 6297 |
. . . . . . . 8
       |
191 | 190 | oveq2d 6306 |
. . . . . . 7
                                       |
192 | | oveq2 6298 |
. . . . . . . . . . . 12
           |
193 | 192 | oveq2d 6306 |
. . . . . . . . . . 11
               |
194 | 193 | fveq2d 5869 |
. . . . . . . . . 10
                       |
195 | 194 | oveq1d 6305 |
. . . . . . . . 9
                 
         |
196 | 195 | oveq1d 6305 |
. . . . . . . 8
      
            
                           |
197 | 196 | sumeq1d 13767 |
. . . . . . 7
                                               
     
            
                            |
198 | 191, 197 | breq12d 4415 |
. . . . . 6
                          
            
                         
                                                                   |
199 | 198 | imbi2d 318 |
. . . . 5
  
                                                                 
                                                                    |
200 | | oveq1 6297 |
. . . . . . . 8
       |
201 | 200 | oveq2d 6306 |
. . . . . . 7
                                       |
202 | | oveq2 6298 |
. . . . . . . . . . . 12
           |
203 | 202 | oveq2d 6306 |
. . . . . . . . . . 11
               |
204 | 203 | fveq2d 5869 |
. . . . . . . . . 10
                       |
205 | 204 | oveq1d 6305 |
. . . . . . . . 9
                 
         |
206 | 205 | oveq1d 6305 |
. . . . . . . 8
      
            
                           |
207 | 206 | sumeq1d 13767 |
. . . . . . 7
                                               
     
            
                            |
208 | 201, 207 | breq12d 4415 |
. . . . . 6
                          
            
                         
                                                                   |
209 | 208 | imbi2d 318 |
. . . . 5
  
                                                                 
                                                                    |
210 | | oveq1 6297 |
. . . . . . . 8
           |
211 | 210 | oveq2d 6306 |
. . . . . . 7
                                           |
212 | | oveq2 6298 |
. . . . . . . . . . . 12
               |
213 | 212 | oveq2d 6306 |
. . . . . . . . . . 11
                   |
214 | 213 | fveq2d 5869 |
. . . . . . . . . 10
                           |
215 | 214 | oveq1d 6305 |
. . . . . . . . 9
                   
           |
216 | 215 | oveq1d 6305 |
. . . . . . . 8
        
            
                             |
217 | 216 | sumeq1d 13767 |
. . . . . . 7
                                                 
     
              
                            |
218 | 211, 217 | breq12d 4415 |
. . . . . 6
                            
            
                         
                                                                       |
219 | 218 | imbi2d 318 |
. . . . 5
    
                                                                 
                                                                        |
220 | | oveq1 6297 |
. . . . . . . 8
       |
221 | 220 | oveq2d 6306 |
. . . . . . 7
                                       |
222 | | oveq2 6298 |
. . . . . . . . . . . 12
           |
223 | 222 | oveq2d 6306 |
. . . . . . . . . . 11
               |
224 | 223 | fveq2d 5869 |
. . . . . . . . . 10
                       |
225 | 224 | oveq1d 6305 |
. . . . . . . . 9
                 
         |
226 | 225 | oveq1d 6305 |
. . . . . . . 8
      
            
                           |
227 | 226 | sumeq1d 13767 |
. . . . . . 7
                                               
     
            
                            |
228 | 221, 227 | breq12d 4415 |
. . . . . 6
                          
            
                         
                                                                   |
229 | 228 | imbi2d 318 |
. . . . 5
  
                                                                 
                                                                    |
230 | 57 | nncnd 10625 |
. . . . . . . . . 10
   |
231 | 230 | subidd 9974 |
. . . . . . . . 9
     |
232 | 231 | oveq2d 6306 |
. . . . . . . 8
                                     |
233 | 52 | rpcnd 11343 |
. . . . . . . . 9
                 |
234 | 233 | mul01d 9832 |
. . . . . . . 8
                   |
235 | 232, 234 | eqtrd 2485 |
. . . . . . 7
                     |
236 | | fzfid 12186 |
. . . . . . . 8
                         |
237 | 57 | nnzd 11039 |
. . . . . . . . . . . . . . . 16
   |
238 | 85, 237 | rpexpcld 12439 |
. . . . . . . . . . . . . . 15
       |
239 | 35, 238 | rpdivcld 11358 |
. . . . . . . . . . . . . 14
         |
240 | 239 | rprege0d 11348 |
. . . . . . . . . . . . 13
       
         |
241 | | flge0nn0 12054 |
. . . . . . . . . . . . 13
              
            |
242 | | nn0p1nn 10909 |
. . . . . . . . . . . . 13
          
              |
243 | 240, 241,
242 | 3syl 18 |
. . . . . . . . . . . 12
     
         |
244 | 243, 181 | syl6eleq 2539 |
. . . . . . . . . . 11
     
             |
245 | | fzss1 11837 |
. . . . . . . . . . 11
                                                   |
246 | 244, 245 | syl 17 |
. . . . . . . . . 10
                                   |
247 | 246 | sselda 3432 |
. . . . . . . . 9
 
                      
            |
248 | 247, 82 | syldan 473 |
. . . . . . . 8
 
                      
           
            |
249 | | elfzle2 11803 |
. . . . . . . . . . . . 13
          
        |
250 | 249 | adantl 468 |
. . . . . . . . . . . 12
 
          
        |
251 | 29 | simpld 461 |
. . . . . . . . . . . . . . 15
   |
252 | 35, 251 | rpdivcld 11358 |
. . . . . . . . . . . . . 14
     |
253 | 252 | rpred 11341 |
. . . . . . . . . . . . 13
     |
254 | | elfzelz 11800 |
. . . . . . . . . . . . 13
          
  |
255 | | flge 12041 |
. . . . . . . . . . . . 13
   
   
         |
256 | 253, 254,
255 | syl2an 480 |
. . . . . . . . . . . 12
 
          
  
         |
257 | 250, 256 | mpbird 236 |
. . . . . . . . . . 11
 
          
    |
258 | 71, 257 | jca 535 |
. . . . . . . . . 10
 
          
      |
259 | | pntlem1.U |
. . . . . . . . . . 11
               
  |
260 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55, 259 | pntlemn 24438 |
. . . . . . . . . 10
 
    
           
            |
261 | 258, 260 | syldan 473 |
. . . . . . . . 9
 
          
                        |
262 | 247, 261 | syldan 473 |
. . . . . . . 8
 
                      
                        |
263 | 236, 248,
262 | fsumge0 13855 |
. . . . . . 7

                                                |
264 | 235, 263 | eqbrtrd 4423 |
. . . . . 6
                         
            
                            |
265 | 264 | a1i 11 |
. . . . 5
    
                         
            
                             |
266 | | pntlem1.K |
. . . . . . . . . 10
      
       
      ![[,] [,]](_icc.gif)                      |
267 | | eqid 2451 |
. . . . . . . . . 10
                                                         |
268 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55, 259, 266, 267 | pntlemi 24442 |
. . . . . . . . 9
 
 ..^               
                                                      |
269 | 52 | adantr 467 |
. . . . . . . . . . 11
 
 ..^                  |
270 | 269 | rpred 11341 |
. . . . . . . . . 10
 
 ..^                  |
271 | | elfzoelz 11920 |
. . . . . . . . . . . . . 14
  ..^
  |
272 | 271 | adantl 468 |
. . . . . . . . . . . . 13
 
 ..^    |
273 | 272 | zred 11040 |
. . . . . . . . . . . 12
 
 ..^    |
274 | 57 | adantr 467 |
. . . . . . . . . . . . 13
 
 ..^    |
275 | 274 | nnred 10624 |
. . . . . . . . . . . 12
 
 ..^    |
276 | 273, 275 | resubcld 10047 |
. . . . . . . . . . 11
 
 ..^      |
277 | 270, 276 | remulcld 9671 |
. . . . . . . . . 10
 
 ..^                      |
278 | | fzfid 12186 |
. . . . . . . . . . 11
 
 ..^                                |
279 | | ssun1 3597 |
. . . . . . . . . . . . . . 15
                           
      
              
            
            
     |
280 | 36 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^    |
281 | 85 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^    |
282 | 272 | peano2zd 11043 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^      |
283 | 281, 282 | rpexpcld 12439 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^          |
284 | 280, 283 | rerpdivcld 11369 |
. . . . . . . . . . . . . . . . . 18
 
 ..^            |
285 | 281, 272 | rpexpcld 12439 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^        |
286 | 280, 285 | rerpdivcld 11369 |
. . . . . . . . . . . . . . . . . 18
 
 ..^          |
287 | 86 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^    |
288 | | 1re 9642 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
289 | | ltle 9722 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
   |
290 | 288, 86, 289 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
291 | 87, 290 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21

  |
292 | 291 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^    |
293 | | uzid 11173 |
. . . . . . . . . . . . . . . . . . . . 21
       |
294 | | peano2uz 11212 |
. . . . . . . . . . . . . . . . . . . . 21
    
        |
295 | 272, 293,
294 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^          |
296 | 287, 292,
295 | leexp2ad 12448 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^              |
297 | 35 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^    |
298 | 285, 283,
297 | lediv2d 11365 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^                              |
299 | 296, 298 | mpbid 214 |
. . . . . . . . . . . . . . . . . 18
 
 ..^                  |
300 | | flword2 12048 |
. . . . . . . . . . . . . . . . . 18
                              
                            |
301 | 284, 286,
299, 300 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
 
 ..^     
                        |
302 | | eluzp1p1 11184 |
. . . . . . . . . . . . . . . . 17
                                                           |
303 | 301, 302 | syl 17 |
. . . . . . . . . . . . . . . 16
 
 ..^                                  |
304 | 286 | flcld 12034 |
. . . . . . . . . . . . . . . . 17
 
 ..^     
        |
305 | 252 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^      |
306 | 305 | rpred 11341 |
. . . . . . . . . . . . . . . . . 18
 
 ..^      |
307 | 306 | flcld 12034 |
. . . . . . . . . . . . . . . . 17
 
 ..^     
    |
308 | 251 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^    |
309 | 308 | rpred 11341 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^    |
310 | 285 | rpred 11341 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^        |
311 | 30 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
312 | 311 | rpred 11341 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
313 | 312 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^    |
314 | 30 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
315 | 314 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^    |
316 | | elfzofz 11935 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^
      |
317 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55 | pntlemh 24437 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    
    
           |
318 | 316, 317 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 ..^      
           |
319 | 318 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^        |
320 | 309, 313,
310, 315, 319 | lttrd 9796 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^        |
321 | 309, 310,
320 | ltled 9783 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^        |
322 | 308, 285,
297 | lediv2d 11365 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^                  |
323 | 321, 322 | mpbid 214 |
. . . . . . . . . . . . . . . . . 18
 
 ..^            |
324 | | flwordi 12047 |
. . . . . . . . . . . . . . . . . 18
                                     |
325 | 286, 306,
323, 324 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
 
 ..^     
     
        |
326 | | eluz2 11165 |
. . . . . . . . . . . . . . . . 17
                         
                               |
327 | 304, 307,
325, 326 | syl3anbrc 1192 |
. . . . . . . . . . . . . . . 16
 
 ..^     
        
         |
328 | | fzsplit2 11824 |
. . . . . . . . . . . . . . . 16
      
                            
        
                                                                                      |
329 | 303, 327,
328 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
 ..^                                
              
            
            
      |
330 | 279, 329 | syl5sseqr 3481 |
. . . . . . . . . . . . . 14
 
 ..^                             
                          |
331 | 297, 283 | rpdivcld 11358 |
. . . . . . . . . . . . . . . . . 18
 
 ..^            |
332 | 331 | rprege0d 11348 |
. . . . . . . . . . . . . . . . 17
 
 ..^                      |
333 | | flge0nn0 12054 |
. . . . . . . . . . . . . . . . 17
                  
              |
334 | | nn0p1nn 10909 |
. . . . . . . . . . . . . . . . 17
            
                |
335 | 332, 333,
334 | 3syl 18 |
. . . . . . . . . . . . . . . 16
 
 ..^                  |
336 | 335, 181 | syl6eleq 2539 |
. . . . . . . . . . . . . . 15
 
 ..^                      |
337 | | fzss1 11837 |
. . . . . . . . . . . . . . 15
                                                       |
338 | 336, 337 | syl 17 |
. . . . . . . . . . . . . 14
 
 ..^                         
      
     |
339 | 330, 338 | sstrd 3442 |
. . . . . . . . . . . . 13
 
 ..^                             
      
     |
340 | 339 | sselda 3432 |
. . . . . . . . . . . 12
    ..^                              
            |
341 | 82 | adantlr 721 |
. . . . . . . . . . . 12
    ..^            
           
            |
342 | 340, 341 | syldan 473 |
. . . . . . . . . . 11
    ..^                              
           
            |
343 | 278, 342 | fsumrecl 13800 |
. . . . . . . . . 10
 
 ..^        
              
                   
            |
344 | | fzfid 12186 |
. . . . . . . . . . 11
 
 ..^                          |
345 | | ssun2 3598 |
. . . . . . . . . . . . . . 15
                     
      
              
            
            
     |
346 | 345, 329 | syl5sseqr 3481 |
. . . . . . . . . . . . . 14
 
 ..^                       
                          |
347 | 346, 338 | sstrd 3442 |
. . . . . . . . . . . . 13
 
 ..^                       
      
     |
348 | 347 | sselda 3432 |
. . . . . . . . . . . 12
    ..^                        
            |
349 | 348, 341 | syldan 473 |
. . . . . . . . . . 11
    ..^                        
           
            |
350 | 344, 349 | fsumrecl 13800 |
. . . . . . . . . 10
 
 ..^        
            
                            |
351 | | le2add 10096 |
. . . . . . . . . 10
                                           
              
                   
          
     
            
                                           
                                                                            
            
                                                                    
              
                   
                                                            |
352 | 270, 277,
343, 350, 351 | syl22anc 1269 |
. . . . . . . . 9
 
 ..^                                                                                              
            
                                                                    
              
                   
                                                            |
353 | 268, 352 | mpand 681 |
. . . . . . . 8
 
 ..^                                                                                                       |