Step | Hyp | Ref
| Expression |
1 | | 2nn 10790 |
. . . . . 6
 |
2 | | nnmulcl 10654 |
. . . . . 6
 
     |
3 | 1, 2 | mpan 684 |
. . . . 5
     |
4 | 3 | nnred 10646 |
. . . 4
     |
5 | | peano2rem 9961 |
. . . 4
         |
6 | 4, 5 | syl 17 |
. . 3
       |
7 | | chtcl 24115 |
. . 3
               |
8 | 6, 7 | syl 17 |
. 2
           |
9 | | nnre 10638 |
. . . 4
   |
10 | | chtcl 24115 |
. . . 4
       |
11 | 9, 10 | syl 17 |
. . 3
       |
12 | | nnnn0 10900 |
. . . . . . 7
   |
13 | | 2m1e1 10746 |
. . . . . . . . . . 11
   |
14 | 13 | oveq2i 6319 |
. . . . . . . . . 10
           |
15 | 3 | nncnd 10647 |
. . . . . . . . . . . 12
     |
16 | | 2cn 10702 |
. . . . . . . . . . . . 13
 |
17 | | ax-1cn 9615 |
. . . . . . . . . . . . 13
 |
18 | | subsub 9924 |
. . . . . . . . . . . . 13
   
               |
19 | 16, 17, 18 | mp3an23 1382 |
. . . . . . . . . . . 12
                 |
20 | 15, 19 | syl 17 |
. . . . . . . . . . 11
               |
21 | | nncn 10639 |
. . . . . . . . . . . . . 14
   |
22 | | subdi 10073 |
. . . . . . . . . . . . . . 15
 
             |
23 | 16, 17, 22 | mp3an13 1381 |
. . . . . . . . . . . . . 14
             |
24 | 21, 23 | syl 17 |
. . . . . . . . . . . . 13
             |
25 | | 2t1e2 10781 |
. . . . . . . . . . . . . 14
   |
26 | 25 | oveq2i 6319 |
. . . . . . . . . . . . 13
           |
27 | 24, 26 | syl6eq 2521 |
. . . . . . . . . . . 12
           |
28 | 27 | oveq1d 6323 |
. . . . . . . . . . 11
   
           |
29 | 20, 28 | eqtr4d 2508 |
. . . . . . . . . 10
               |
30 | 14, 29 | syl5eqr 2519 |
. . . . . . . . 9
             |
31 | | 2nn0 10910 |
. . . . . . . . . . 11
 |
32 | | nnm1nn0 10935 |
. . . . . . . . . . 11
 
   |
33 | | nn0mulcl 10930 |
. . . . . . . . . . 11
  
   
    |
34 | 31, 32, 33 | sylancr 676 |
. . . . . . . . . 10
       |
35 | | nn0p1nn 10933 |
. . . . . . . . . 10
    
        |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
   
     |
37 | 30, 36 | eqeltrd 2549 |
. . . . . . . 8
       |
38 | | nnnn0 10900 |
. . . . . . . 8
           |
39 | 37, 38 | syl 17 |
. . . . . . 7
       |
40 | | 1re 9660 |
. . . . . . . . . . 11
 |
41 | 40 | a1i 11 |
. . . . . . . . . 10
   |
42 | | nnge1 10657 |
. . . . . . . . . 10
   |
43 | 41, 9, 9, 42 | leadd2dd 10249 |
. . . . . . . . 9
 
     |
44 | 21 | 2timesd 10878 |
. . . . . . . . 9
       |
45 | 43, 44 | breqtrrd 4422 |
. . . . . . . 8
 
     |
46 | | leaddsub 10111 |
. . . . . . . . 9
 
       
       |
47 | 9, 41, 4, 46 | syl3anc 1292 |
. . . . . . . 8
   
 
       |
48 | 45, 47 | mpbid 215 |
. . . . . . 7
       |
49 | | elfz2nn0 11911 |
. . . . . . 7
        
    
       |
50 | 12, 39, 48, 49 | syl3anbrc 1214 |
. . . . . 6
           |
51 | | bccl2 12546 |
. . . . . 6
                 |
52 | 50, 51 | syl 17 |
. . . . 5
         |
53 | 52 | nnrpd 11362 |
. . . 4
         |
54 | 53 | relogcld 23651 |
. . 3
             |
55 | 11, 54 | readdcld 9688 |
. 2
                   |
56 | | 4re 10708 |
. . . . . 6
 |
57 | | 4pos 10727 |
. . . . . 6
 |
58 | 56, 57 | elrpii 11328 |
. . . . 5
 |
59 | | relogcl 23604 |
. . . . 5

      |
60 | 58, 59 | ax-mp 5 |
. . . 4
     |
61 | 32 | nn0red 10950 |
. . . 4
 
   |
62 | | remulcl 9642 |
. . . 4
      
            |
63 | 60, 61, 62 | sylancr 676 |
. . 3
           |
64 | 11, 63 | readdcld 9688 |
. 2
                 |
65 | | iftrue 3878 |
. . . . . . . . . . . 12
      
         |
66 | 65 | adantl 473 |
. . . . . . . . . . 11
   
                |
67 | | simpr 468 |
. . . . . . . . . . . . . . . 16
 

  |
68 | 52 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
         |
69 | 67, 68 | pccld 14879 |
. . . . . . . . . . . . . . 15
 
           |
70 | | nn0addge1 10940 |
. . . . . . . . . . . . . . 15
  
       
            |
71 | 40, 69, 70 | sylancr 676 |
. . . . . . . . . . . . . 14
 

            |
72 | | iftrue 3878 |
. . . . . . . . . . . . . . . 16
  
     |
73 | 72 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
                            |
74 | 73 | breq2d 4407 |
. . . . . . . . . . . . . 14
 
  
           
             |
75 | 71, 74 | syl5ibrcom 230 |
. . . . . . . . . . . . 13
 
 
  
               |
76 | 75 | adantr 472 |
. . . . . . . . . . . 12
   
                        |
77 | | prmnn 14704 |
. . . . . . . . . . . . . . . . . 18

  |
78 | 77 | ad2antlr 741 |
. . . . . . . . . . . . . . . . 17
          
  |
79 | | simprl 772 |
. . . . . . . . . . . . . . . . . 18
                 |
80 | | prmz 14705 |
. . . . . . . . . . . . . . . . . . . 20

  |
81 | 37 | nnzd 11062 |
. . . . . . . . . . . . . . . . . . . 20
       |
82 | | eluz 11196 |
. . . . . . . . . . . . . . . . . . . 20
                       |
83 | 80, 81, 82 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . 19
 
         
       |
84 | 83 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
                   
       |
85 | 79, 84 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
                     |
86 | | dvdsfac 14438 |
. . . . . . . . . . . . . . . . 17
                     |
87 | 78, 85, 86 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
                     |
88 | | id 22 |
. . . . . . . . . . . . . . . . . 18

  |
89 | | faccl 12507 |
. . . . . . . . . . . . . . . . . . 19
    
          |
90 | 39, 89 | syl 17 |
. . . . . . . . . . . . . . . . . 18
           |
91 | | pcelnn 14898 |
. . . . . . . . . . . . . . . . . 18
                     
           |
92 | 88, 90, 91 | syl2anr 486 |
. . . . . . . . . . . . . . . . 17
 
           
           |
93 | 92 | adantr 472 |
. . . . . . . . . . . . . . . 16
                     
           |
94 | 87, 93 | mpbird 240 |
. . . . . . . . . . . . . . 15
                       |
95 | 94 | nnge1d 10674 |
. . . . . . . . . . . . . 14
          
            |
96 | | iffalse 3881 |
. . . . . . . . . . . . . . . . 17

       |
97 | 96 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16

   
  
                    |
98 | 97 | ad2antll 743 |
. . . . . . . . . . . . . . 15
                                      |
99 | 69 | nn0cnd 10951 |
. . . . . . . . . . . . . . . . 17
 
           |
100 | 99 | addid2d 9852 |
. . . . . . . . . . . . . . . 16
 
  
                  |
101 | 100 | adantr 472 |
. . . . . . . . . . . . . . 15
            
                  |
102 | | bcval2 12528 |
. . . . . . . . . . . . . . . . . . . . . 22
                                           |
103 | 50, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
                                   |
104 | 44 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
105 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
106 | 21, 21, 105 | addsubassd 10025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
    |
107 | 104, 106 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
    |
108 | 107 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
109 | 32 | nn0cnd 10951 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
110 | 21, 109 | pncan2d 10007 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
111 | 108, 110 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
112 | 111 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
    |
113 | 112 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
114 | 113 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . 21
                                        
          |
115 | 103, 114 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . 20
                    
          |
116 | 115 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
                               |
117 | 116 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
 
                       
           |
118 | | nnz 10983 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
119 | | nnne0 10664 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
120 | 118, 119 | jca 541 |
. . . . . . . . . . . . . . . . . . . . 21
                             |
121 | 90, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                     |
122 | 121 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
                     |
123 | | faccl 12507 |
. . . . . . . . . . . . . . . . . . . . . 22
  
        |
124 | 32, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
         |
125 | | faccl 12507 |
. . . . . . . . . . . . . . . . . . . . . 22

      |
126 | 12, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
       |
127 | 124, 126 | nnmulcld 10679 |
. . . . . . . . . . . . . . . . . . . 20
     
         |
128 | 127 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
     
         |
129 | | pcdiv 14881 |
. . . . . . . . . . . . . . . . . . 19
                        
                                 
         
                |
130 | 67, 122, 128, 129 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
 
                          
         
                |
131 | | nnz 10983 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
132 | | nnne0 10664 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
133 | 131, 132 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . 22
           
           |
134 | 124, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
     
           |
135 | 134 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
     
     
     |
136 | | nnz 10983 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
137 | | nnne0 10664 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
138 | 136, 137 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
139 | 126, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
             |
140 | 139 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
             |
141 | | pcmul 14880 |
. . . . . . . . . . . . . . . . . . . 20
      
                   
     
                          |
142 | 67, 135, 140, 141 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . 19
 
      
         
                |
143 | 142 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
 
                                                         |
144 | 117, 130,
143 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . 17
 
          
                            |
145 | 144 | adantr 472 |
. . . . . . . . . . . . . . . 16
                    
                            |
146 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . . . 22
          
  |
147 | | prmfac1 14750 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
148 | 147 | 3expia 1233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     
   |
149 | 12, 148 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
   |
150 | 149 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
               
   |
151 | 146, 150 | mtod 182 |
. . . . . . . . . . . . . . . . . . . . 21
          
      |
152 | 80 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
153 | 135 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
    |
154 | | nnz 10983 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
155 | 154 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
156 | | dvdsmultr1 14415 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
          
      |
157 | 152, 153,
155, 156 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
            
      |
158 | | facnn2 12506 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
159 | 158 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
               |
160 | 159 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                 |
161 | 157, 160 | sylibrd 242 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
162 | 161 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
163 | 151, 162 | mtod 182 |
. . . . . . . . . . . . . . . . . . . 20
          
        |
164 | | pceq0 14899 |
. . . . . . . . . . . . . . . . . . . . . 22
                     
     |
165 | 88, 124, 164 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . . . 21
 
             
     |
166 | 165 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
                       
     |
167 | 163, 166 | mpbird 240 |
. . . . . . . . . . . . . . . . . . 19
                     |
168 | | pceq0 14899 |
. . . . . . . . . . . . . . . . . . . . . 22
                     |
169 | 88, 126, 168 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . . . 21
 
               |
170 | 169 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
                         |
171 | 151, 170 | mpbird 240 |
. . . . . . . . . . . . . . . . . . 19
                   |
172 | 167, 171 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
                               |
173 | | 00id 9826 |
. . . . . . . . . . . . . . . . . 18
   |
174 | 172, 173 | syl6eq 2521 |
. . . . . . . . . . . . . . . . 17
                             |
175 | 174 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
                       
                             |
176 | | pccl 14878 |
. . . . . . . . . . . . . . . . . . . 20
                       |
177 | 88, 90, 176 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . 19
 
             |
178 | 177 | nn0cnd 10951 |
. . . . . . . . . . . . . . . . . 18
 
             |
179 | 178 | subid1d 9994 |
. . . . . . . . . . . . . . . . 17
 
                         |
180 | 179 | adantr 472 |
. . . . . . . . . . . . . . . 16
                                   |
181 | 145, 175,
180 | 3eqtrd 2509 |
. . . . . . . . . . . . . . 15
                               |
182 | 98, 101, 181 | 3eqtrd 2509 |
. . . . . . . . . . . . . 14
                          
           |
183 | 95, 182 | breqtrrd 4422 |
. . . . . . . . . . . . 13
          
  
              |
184 | 183 | expr 626 |
. . . . . . . . . . . 12
   
     
   
  
           |
185 | 76, 184 | pm2.61d 163 |
. . . . . . . . . . 11
   
                      |
186 | 66, 185 | eqbrtrd 4416 |
. . . . . . . . . 10
   
                               |
187 | 186 | ex 441 |
. . . . . . . . 9
 
                                 |
188 | | 1nn0 10909 |
. . . . . . . . . . . . 13
 |
189 | | 0nn0 10908 |
. . . . . . . . . . . . 13
 |
190 | 188, 189 | keepel 3939 |
. . . . . . . . . . . 12
 
    |
191 | | nn0addcl 10929 |
. . . . . . . . . . . 12
    
                            |
192 | 190, 69, 191 | sylancr 676 |
. . . . . . . . . . 11
 
                  |
193 | 192 | nn0ge0d 10952 |
. . . . . . . . . 10
 

  
              |
194 | | iffalse 3881 |
. . . . . . . . . . 11

               |
195 | 194 | breq1d 4405 |
. . . . . . . . . 10

                            
   
  
           |
196 | 193, 195 | syl5ibrcom 230 |
. . . . . . . . 9
 
     
 
         
               |
197 | 187, 196 | pm2.61d 163 |
. . . . . . . 8
 
         
  
              |
198 | | eqid 2471 |
. . . . . . . . . . . . 13
               |
199 | 198 | prmorcht 24184 |
. . . . . . . . . . . 12
                                    |
200 | 37, 199 | syl 17 |
. . . . . . . . . . 11
                                |
201 | 200 | oveq2d 6324 |
. . . . . . . . . 10
 
             
                    |
202 | 201 | adantr 472 |
. . . . . . . . 9
 
                                    |
203 | | nncn 10639 |
. . . . . . . . . . . . . 14
   |
204 | 203 | exp1d 12449 |
. . . . . . . . . . . . 13
       |
205 | 204 | ifeq1d 3890 |
. . . . . . . . . . . 12
  
              |
206 | 205 | mpteq2ia 4478 |
. . . . . . . . . . 11
                   |
207 | 206 | eqcomi 2480 |
. . . . . . . . . 10
                   |
208 | 188 | a1i 11 |
. . . . . . . . . . 11
   
   |
209 | 208 | ralrimiva 2809 |
. . . . . . . . . 10
 
 
  |
210 | 37 | adantr 472 |
. . . . . . . . . 10
 
       |
211 | | eqidd 2472 |
. . . . . . . . . 10
   |
212 | 207, 209,
210, 67, 211 | pcmpt 14916 |
. . . . . . . . 9
 
                               |
213 | 202, 212 | eqtrd 2505 |
. . . . . . . 8
 
                          |
214 | | efchtcl 24117 |
. . . . . . . . . . . . 13
           |
215 | 9, 214 | syl 17 |
. . . . . . . . . . . 12
           |
216 | 215 | adantr 472 |
. . . . . . . . . . 11
 
           |
217 | | nnz 10983 |
. . . . . . . . . . . 12
        
          |
218 | | nnne0 10664 |
. . . . . . . . . . . 12
        
          |
219 | 217, 218 | jca 541 |
. . . . . . . . . . 11
        
                    |
220 | 216, 219 | syl 17 |
. . . . . . . . . 10
 
                     |
221 | | nnz 10983 |
. . . . . . . . . . . 12
               |
222 | | nnne0 10664 |
. . . . . . . . . . . 12
               |
223 | 221, 222 | jca 541 |
. . . . . . . . . . 11
                       |
224 | 68, 223 | syl 17 |
. . . . . . . . . 10
 
                 |
225 | | pcmul 14880 |
. . . . . . . . . 10
                   
                                                       |
226 | 67, 220, 224, 225 | syl3anc 1292 |
. . . . . . . . 9
 
                                         |
227 | 198 | prmorcht 24184 |
. . . . . . . . . . . . 13
                        |
228 | 227 | oveq2d 6324 |
. . . . . . . . . . . 12
 
         
                |
229 | 228 | adantr 472 |
. . . . . . . . . . 11
 
                            |
230 | | simpl 464 |
. . . . . . . . . . . 12
 

  |
231 | 207, 209,
230, 67, 211 | pcmpt 14916 |
. . . . . . . . . . 11
 
                       |
232 | 229, 231 | eqtrd 2505 |
. . . . . . . . . 10
 
             
    |
233 | 232 | oveq1d 6323 |
. . . . . . . . 9
 
                        
  
          |
234 | 226, 233 | eqtrd 2505 |
. . . . . . . 8
 
                     
              |
235 | 197, 213,
234 | 3brtr4d 4426 |
. . . . . . 7
 
                                   |
236 | 235 | ralrimiva 2809 |
. . . . . 6
                                    |
237 | | efchtcl 24117 |
. . . . . . . . 9
                   |
238 | 6, 237 | syl 17 |
. . . . . . . 8
               |
239 | 238 | nnzd 11062 |
. . . . . . 7
               |
240 | 215, 52 | nnmulcld 10679 |
. . . . . . . 8
                   |
241 | 240 | nnzd 11062 |
. . . . . . 7
                   |
242 | | pc2dvds 14907 |
. . . . . . 7
                                                            

             
                    |
243 | 239, 241,
242 | syl2anc 673 |
. . . . . 6
                              

             
                    |
244 | 236, 243 | mpbird 240 |
. . . . 5
                               |
245 | | dvdsle 14427 |
. . . . . 6
                                                                                           |
246 | 239, 240,
245 | syl2anc 673 |
. . . . 5
                                                             |
247 | 244, 246 | mpd 15 |
. . . 4
                               |
248 | 11 | recnd 9687 |
. . . . . 6
       |
249 | 54 | recnd 9687 |
. . . . . 6
             |
250 | | efadd 14225 |
. . . . . 6
                                                               |
251 | 248, 249,
250 | syl2anc 673 |
. . . . 5
                                               |
252 | 53 | reeflogd 23652 |
. . . . . 6
                       |
253 | 252 | oveq2d 6324 |
. . . . 5
                                           |
254 | 251, 253 | eqtrd 2505 |
. . . 4
                                       |
255 | 247, 254 | breqtrrd 4422 |
. . 3
                                   |
256 | | efle 14249 |
. . . 4
                                                   
           
                       |
257 | 8, 55, 256 | syl2anc 673 |
. . 3
                                                             |
258 | 255, 257 | mpbird 240 |
. 2
                           |
259 | | fzfid 12224 |
. . . . . . . . 9
           |
260 | | elfzelz 11826 |
. . . . . . . . . . 11
           |
261 | | bccl 12545 |
. . . . . . . . . . 11
     
         |
262 | 39, 260, 261 | syl2an 485 |
. . . . . . . . . 10
 
                 |
263 | 262 | nn0red 10950 |
. . . . . . . . 9
 
                 |
264 | 262 | nn0ge0d 10952 |
. . . . . . . . 9
 
                 |
265 | | nn0uz 11217 |
. . . . . . . . . . . 12
     |
266 | 32, 265 | syl6eleq 2559 |
. . . . . . . . . . 11
 
       |
267 | | fzss1 11863 |
. . . . . . . . . . 11
      
 
          |
268 | 266, 267 | syl 17 |
. . . . . . . . . 10
             |
269 | | eluz 11196 |
. . . . . . . . . . . . 13
                       |
270 | 154, 81, 269 | syl2anc 673 |
. . . . . . . . . . . 12
         
       |
271 | 48, 270 | mpbird 240 |
. . . . . . . . . . 11
           |
272 | | fzss2 11864 |
. . . . . . . . . . 11
        
              |
273 | 271, 272 | syl 17 |
. . . . . . . . . 10
               |
274 | 268, 273 | sstrd 3428 |
. . . . . . . . 9
                 |
275 | 259, 263,
264, 274 | fsumless 13933 |
. . . . . . . 8
                                 |
276 | 32 | nn0zd 11061 |
. . . . . . . . . . . 12
 
   |
277 | | bccmpl 12532 |
. . . . . . . . . . . . . . 15
     
                     |
278 | 39, 154, 277 | syl2anc 673 |
. . . . . . . . . . . . . 14
                     |
279 | 111 | oveq2d 6324 |
. . . . . . . . . . . . . 14
                       |
280 | 278, 279 | eqtrd 2505 |
. . . . . . . . . . . . 13
                 |
281 | 52 | nncnd 10647 |
. . . . . . . . . . . . 13
         |
282 | 280, 281 | eqeltrrd 2550 |
. . . . . . . . . . . 12
           |
283 | | oveq2 6316 |
. . . . . . . . . . . . 13
                   |
284 | 283 | fsum1 13885 |
. . . . . . . . . . . 12
         
                             |
285 | 276, 282,
284 | syl2anc 673 |
. . . . . . . . . . 11
       
                   |
286 | 285, 280 | eqtr4d 2508 |
. . . . . . . . . 10
       
                 |
287 | 286 | oveq1d 6323 |
. . . . . . . . 9
                                         |
288 | 21, 105 | npcand 10009 |
. . . . . . . . . . 11
       |
289 | | uzid 11197 |
. . . . . . . . . . . . 13
   
    
    |
290 | 276, 289 | syl 17 |
. . . . . . . . . . . 12
 
    
    |
291 | | peano2uz 11235 |
. . . . . . . . . . . 12
      
 
 
          |
292 | 290, 291 | syl 17 |
. . . . . . . . . . 11
        
    |
293 | 288, 292 | eqeltrrd 2550 |
. . . . . . . . . 10
         |
294 | 274 | sselda 3418 |
. . . . . . . . . . 11
 
 
               |
295 | 262 | nn0cnd 10951 |
. . . . . . . . . . 11
 
                 |
296 | 294, 295 | syldan 478 |
. . . . . . . . . 10
 
 
             |
297 | | oveq2 6316 |
. . . . . . . . . 10
               |
298 | 293, 296,
297 | fsumm1 13889 |
. . . . . . . . 9
                                         |
299 | 281 | 2timesd 10878 |
. . . . . . . . 9
                         |
300 | 287, 298,
299 | 3eqtr4rd 2516 |
. . . . . . . 8
                         |
301 | | binom11 13967 |
. . . . . . . . 9
    
                          |
302 | 39, 301 | syl 17 |
. . . . . . . 8
                           |
303 | 275, 300,
302 | 3brtr4d 4426 |
. . . . . . 7
                   |
304 | | mulcom 9643 |
. . . . . . . 8
                           |
305 | 16, 281, 304 | sylancr 676 |
. . . . . . 7
                   |
306 | 30 | oveq2d 6324 |
. . . . . . . 8
                     |
307 | | expp1 12317 |
. . . . . . . . 9
   
        
                |
308 | 16, 34, 307 | sylancr 676 |
. . . . . . . 8
                       |
309 | 16 | a1i 11 |
. . . . . . . . . . 11
   |
310 | 31 | a1i 11 |
. . . . . . . . . . 11
   |
311 | 309, 32, 310 | expmuld 12457 |
. . . . . . . . . 10
                     |
312 | | sq2 12409 |
. . . . . . . . . . 11
     |
313 | 312 | oveq1i 6318 |
. . . . . . . . . 10
             
   |
314 | 311, 313 | syl6eq 2521 |
. . . . . . . . 9
                 |
315 | 314 | oveq1d 6323 |
. . . . . . . 8
                     |
316 | 306, 308,
315 | 3eqtrd 2509 |
. . . . . . 7
                   |
317 | 303, 305,
316 | 3brtr3d 4425 |
. . . . . 6
                   |
318 | 52 | nnred 10646 |
. . . . . . 7
         |
319 | | reexpcl 12327 |
. . . . . . . 8
  
     
    |
320 | 56, 32, 319 | sylancr 676 |
. . . . . . 7
         |
321 | | 2re 10701 |
. . . . . . . . 9
 |
322 | | 2pos 10723 |
. . . . . . . . 9
 |
323 | 321, 322 | pm3.2i 462 |
. . . . . . . 8
   |
324 | 323 | a1i 11 |
. . . . . . 7
     |
325 | | lemul1 10479 |
. . . . . . 7
           
    
            
                   |
326 | 318, 320,
324, 325 | syl3anc 1292 |
. . . . . 6
       
     
                   |
327 | 317, 326 | mpbird 240 |
. . . . 5
               |
328 | 60 | recni 9673 |
. . . . . . . 8
     |
329 | | mulcom 9643 |
. . . . . . . 8
      
                    |
330 | 328, 109,
329 | sylancr 676 |
. . . . . . 7
                   |
331 | 330 | fveq2d 5883 |
. . . . . 6
                           |
332 | | reexplog 23623 |
. . . . . . 7
  
     
                |
333 | 58, 276, 332 | sylancr 676 |
. . . . . 6
                     |
334 | 331, 333 | eqtr4d 2508 |
. . . . 5
                
    |
335 | 327, 252,
334 | 3brtr4d 4426 |
. . . 4
                             |
336 | | efle 14249 |
. . . . 5
                               
       
                             |
337 | 54, 63, 336 | syl2anc 673 |
. . . 4
           
       
                             |
338 | 335, 337 | mpbird 240 |
. . 3
                     |
339 | 54, 63, 11, 338 | leadd2dd 10249 |
. 2
                                 |
340 | 8, 55, 64, 258, 339 | letrd 9809 |
1
                         |