Step | Hyp | Ref
| Expression |
1 | | esum 14128 |
. . . . . . . . . 10
        |
2 | | fveq2 5863 |
. . . . . . . . . . . . 13
           |
3 | 2 | oveq2d 6304 |
. . . . . . . . . . . 12
               |
4 | | eirr.1 |
. . . . . . . . . . . 12
         |
5 | | ovex 6316 |
. . . . . . . . . . . 12
       |
6 | 3, 4, 5 | fvmpt 5946 |
. . . . . . . . . . 11

            |
7 | 6 | sumeq2i 13758 |
. . . . . . . . . 10
     
       |
8 | 1, 7 | eqtr4i 2475 |
. . . . . . . . 9
      |
9 | | nn0uz 11190 |
. . . . . . . . . 10
     |
10 | | eqid 2450 |
. . . . . . . . . 10
   
         |
11 | | eirr.3 |
. . . . . . . . . . . 12
   |
12 | 11 | peano2nnd 10623 |
. . . . . . . . . . 11
     |
13 | 12 | nnnn0d 10922 |
. . . . . . . . . 10
     |
14 | | eqidd 2451 |
. . . . . . . . . 10
 

          |
15 | | nn0z 10957 |
. . . . . . . . . . . . . . . . 17

  |
16 | | 1exp 12298 |
. . . . . . . . . . . . . . . . 17
       |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . 16

      |
18 | 17 | oveq1d 6303 |
. . . . . . . . . . . . . . 15

                  |
19 | 18 | mpteq2ia 4484 |
. . . . . . . . . . . . . 14

                    |
20 | 4, 19 | eqtr4i 2475 |
. . . . . . . . . . . . 13
             |
21 | 20 | eftval 14124 |
. . . . . . . . . . . 12

                |
22 | 21 | adantl 468 |
. . . . . . . . . . 11
 

                |
23 | | ax-1cn 9594 |
. . . . . . . . . . . . 13
 |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
   |
25 | | eftcl 14121 |
. . . . . . . . . . . 12
 
             |
26 | 24, 25 | sylan 474 |
. . . . . . . . . . 11
 

            |
27 | 22, 26 | eqeltrd 2528 |
. . . . . . . . . 10
 

      |
28 | 20 | efcllem 14125 |
. . . . . . . . . . 11
     |
29 | 24, 28 | syl 17 |
. . . . . . . . . 10
     |
30 | 9, 10, 13, 14, 27, 29 | isumsplit 13891 |
. . . . . . . . 9
                     
   
          |
31 | 8, 30 | syl5eq 2496 |
. . . . . . . 8
  
                            |
32 | 11 | nncnd 10622 |
. . . . . . . . . . . 12
   |
33 | | pncan 9878 |
. . . . . . . . . . . 12
 
       |
34 | 32, 23, 33 | sylancl 667 |
. . . . . . . . . . 11
       |
35 | 34 | oveq2d 6304 |
. . . . . . . . . 10
               |
36 | 35 | sumeq1d 13760 |
. . . . . . . . 9
                           |
37 | 36 | oveq1d 6303 |
. . . . . . . 8
                                                       |
38 | 31, 37 | eqtrd 2484 |
. . . . . . 7
  
                        |
39 | 38 | oveq1d 6303 |
. . . . . 6
  
                                   
            |
40 | | fzfid 12183 |
. . . . . . . 8
       |
41 | | elfznn0 11884 |
. . . . . . . . 9
       |
42 | 41, 27 | sylan2 477 |
. . . . . . . 8
 
           |
43 | 40, 42 | fsumcl 13792 |
. . . . . . 7
             |
44 | 6 | adantl 468 |
. . . . . . . . . . 11
 

            |
45 | | faccl 12466 |
. . . . . . . . . . . . . 14

      |
46 | 45 | adantl 468 |
. . . . . . . . . . . . 13
 

      |
47 | 46 | nnrpd 11336 |
. . . . . . . . . . . 12
 

      |
48 | 47 | rpreccld 11348 |
. . . . . . . . . . 11
 

        |
49 | 44, 48 | eqeltrd 2528 |
. . . . . . . . . 10
 

      |
50 | 9, 10, 13, 14, 49, 29 | isumrpcl 13894 |
. . . . . . . . 9
               |
51 | 50 | rpred 11338 |
. . . . . . . 8
               |
52 | 51 | recnd 9666 |
. . . . . . 7
               |
53 | 43, 52 | pncan2d 9985 |
. . . . . 6
             
   
                   
   
         |
54 | 39, 53 | eqtrd 2484 |
. . . . 5
  
                        |
55 | 54 | oveq2d 6304 |
. . . 4
      
                                |
56 | 11 | nnnn0d 10922 |
. . . . . . 7
   |
57 | | faccl 12466 |
. . . . . . 7

      |
58 | 56, 57 | syl 17 |
. . . . . 6
       |
59 | 58 | nncnd 10622 |
. . . . 5
       |
60 | | ere 14136 |
. . . . . . 7
 |
61 | 60 | recni 9652 |
. . . . . 6
 |
62 | 61 | a1i 11 |
. . . . 5
   |
63 | 59, 62, 43 | subdid 10071 |
. . . 4
      
                        
             |
64 | 55, 63 | eqtr3d 2486 |
. . 3
      
   
                    
             |
65 | | eirr.4 |
. . . . . . 7
     |
66 | 65 | oveq2d 6304 |
. . . . . 6
      
          |
67 | | eirr.2 |
. . . . . . . 8
   |
68 | 67 | zcnd 11038 |
. . . . . . 7
   |
69 | 11 | nnne0d 10651 |
. . . . . . 7
   |
70 | 59, 68, 32, 69 | div12d 10416 |
. . . . . 6
                   |
71 | 66, 70 | eqtrd 2484 |
. . . . 5
      
          |
72 | 11 | nnred 10621 |
. . . . . . . . 9
   |
73 | 72 | leidd 10177 |
. . . . . . . 8

  |
74 | | facdiv 12469 |
. . . . . . . 8
 
         |
75 | 56, 11, 73, 74 | syl3anc 1267 |
. . . . . . 7
         |
76 | 75 | nnzd 11036 |
. . . . . 6
         |
77 | 67, 76 | zmulcld 11043 |
. . . . 5
           |
78 | 71, 77 | eqeltrd 2528 |
. . . 4
      
  |
79 | 40, 59, 42 | fsummulc2 13838 |
. . . . 5
      
                            |
80 | 41 | adantl 468 |
. . . . . . . . . . 11
 
       |
81 | 80, 6 | syl 17 |
. . . . . . . . . 10
 
                 |
82 | 81 | oveq2d 6304 |
. . . . . . . . 9
 
                             |
83 | 59 | adantr 467 |
. . . . . . . . . 10
 
           |
84 | 41, 46 | sylan2 477 |
. . . . . . . . . . 11
 
           |
85 | 84 | nncnd 10622 |
. . . . . . . . . 10
 
           |
86 | | facne0 12468 |
. . . . . . . . . . 11

      |
87 | 80, 86 | syl 17 |
. . . . . . . . . 10
 
           |
88 | 83, 85, 87 | divrecd 10383 |
. . . . . . . . 9
 
                             |
89 | 82, 88 | eqtr4d 2487 |
. . . . . . . 8
 
                           |
90 | | permnn 12508 |
. . . . . . . . 9
                 |
91 | 90 | adantl 468 |
. . . . . . . 8
 
                 |
92 | 89, 91 | eqeltrd 2528 |
. . . . . . 7
 
                 |
93 | 92 | nnzd 11036 |
. . . . . 6
 
                 |
94 | 40, 93 | fsumzcl 13794 |
. . . . 5
                   |
95 | 79, 94 | eqeltrd 2528 |
. . . 4
      
            |
96 | 78, 95 | zsubcld 11042 |
. . 3
                           |
97 | 64, 96 | eqeltrd 2528 |
. 2
      
   
          |
98 | | 0zd 10946 |
. . 3
   |
99 | 58 | nnrpd 11336 |
. . . . 5
       |
100 | 99, 50 | rpmulcld 11354 |
. . . 4
      
   
          |
101 | 100 | rpgt0d 11341 |
. . 3
                     |
102 | 12 | peano2nnd 10623 |
. . . . . . . 8
       |
103 | 102 | nnred 10621 |
. . . . . . 7
       |
104 | | faccl 12466 |
. . . . . . . . 9
  
        |
105 | 13, 104 | syl 17 |
. . . . . . . 8
    
    |
106 | 105, 12 | nnmulcld 10654 |
. . . . . . 7
     
  
    |
107 | 103, 106 | nndivred 10655 |
. . . . . 6
          
        |
108 | 58 | nnrecred 10652 |
. . . . . 6
         |
109 | | abs1 13353 |
. . . . . . . . . . . 12
     |
110 | 109 | oveq1i 6298 |
. . . . . . . . . . 11
             |
111 | 110 | oveq1i 6298 |
. . . . . . . . . 10
                         |
112 | 111 | mpteq2i 4485 |
. . . . . . . . 9

                            |
113 | 20, 112 | eqtr4i 2475 |
. . . . . . . 8
                 |
114 | | eqid 2450 |
. . . . . . . 8

               
                               
                |
115 | | 1le1 10237 |
. . . . . . . . . 10
 |
116 | 109, 115 | eqbrtri 4421 |
. . . . . . . . 9
     |
117 | 116 | a1i 11 |
. . . . . . . 8
    
  |
118 | 20, 113, 114, 12, 24, 117 | eftlub 14156 |
. . . . . . 7
    
   
                            
         |
119 | 50 | rprege0d 11345 |
. . . . . . . 8
                             |
120 | | absid 13352 |
. . . . . . . 8
                          
                              |
121 | 119, 120 | syl 17 |
. . . . . . 7
    
   
                      |
122 | 109 | oveq1i 6298 |
. . . . . . . . . 10
             
   |
123 | 12 | nnzd 11036 |
. . . . . . . . . . 11
     |
124 | | 1exp 12298 |
. . . . . . . . . . 11
           |
125 | 123, 124 | syl 17 |
. . . . . . . . . 10
    
    |
126 | 122, 125 | syl5eq 2496 |
. . . . . . . . 9
             |
127 | 126 | oveq1d 6303 |
. . . . . . . 8
                                       
  
      |
128 | 107 | recnd 9666 |
. . . . . . . . 9
          
        |
129 | 128 | mulid2d 9658 |
. . . . . . . 8
                                     |
130 | 127, 129 | eqtrd 2484 |
. . . . . . 7
                                               |
131 | 118, 121,
130 | 3brtr3d 4431 |
. . . . . 6
                      
  
     |
132 | 12 | nnred 10621 |
. . . . . . . . . 10
     |
133 | 132, 132 | readdcld 9667 |
. . . . . . . . 9
         |
134 | 132, 132 | remulcld 9668 |
. . . . . . . . 9
    
    |
135 | | 1red 9655 |
. . . . . . . . . 10
   |
136 | 11 | nnge1d 10649 |
. . . . . . . . . . 11

  |
137 | | 1nn 10617 |
. . . . . . . . . . . 12
 |
138 | | nnleltp1 10988 |
. . . . . . . . . . . 12
 
       |
139 | 137, 11, 138 | sylancr 668 |
. . . . . . . . . . 11
       |
140 | 136, 139 | mpbid 214 |
. . . . . . . . . 10
     |
141 | 135, 132,
132, 140 | ltadd2dd 9791 |
. . . . . . . . 9
             |
142 | 12 | nncnd 10622 |
. . . . . . . . . . 11
     |
143 | 142 | 2timesd 10852 |
. . . . . . . . . 10
  
          |
144 | | df-2 10665 |
. . . . . . . . . . . 12
   |
145 | 135, 72, 135, 136 | leadd1dd 10224 |
. . . . . . . . . . . 12
  
    |
146 | 144, 145 | syl5eqbr 4435 |
. . . . . . . . . . 11

    |
147 | | 2re 10676 |
. . . . . . . . . . . . 13
 |
148 | 147 | a1i 11 |
. . . . . . . . . . . 12
   |
149 | 12 | nngt0d 10650 |
. . . . . . . . . . . 12
     |
150 | | lemul1 10454 |
. . . . . . . . . . . 12
  
       
  
       
     |
151 | 148, 132,
132, 149, 150 | syl112anc 1271 |
. . . . . . . . . . 11
  
  
 
 
       |
152 | 146, 151 | mpbid 214 |
. . . . . . . . . 10
  
 
 
      |
153 | 143, 152 | eqbrtrrd 4424 |
. . . . . . . . 9
      
 
      |
154 | 103, 133,
134, 141, 153 | ltletrd 9792 |
. . . . . . . 8
             |
155 | | facp1 12461 |
. . . . . . . . . . . . 13

           
    |
156 | 56, 155 | syl 17 |
. . . . . . . . . . . 12
    
            |
157 | 156 | oveq1d 6303 |
. . . . . . . . . . 11
     
                       |
158 | 105 | nncnd 10622 |
. . . . . . . . . . . 12
    
    |
159 | 58 | nnne0d 10651 |
. . . . . . . . . . . 12
       |
160 | 158, 59, 159 | divrecd 10383 |
. . . . . . . . . . 11
     
                       |
161 | 142, 59, 159 | divcan3d 10385 |
. . . . . . . . . . 11
                   |
162 | 157, 160,
161 | 3eqtr3rd 2493 |
. . . . . . . . . 10
                   |
163 | 162 | oveq1d 6303 |
. . . . . . . . 9
    
       
              |
164 | 108 | recnd 9666 |
. . . . . . . . . 10
         |
165 | 158, 164,
142 | mul32d 9840 |
. . . . . . . . 9
                
       
              |
166 | 163, 165 | eqtrd 2484 |
. . . . . . . 8
    
       
              |
167 | 154, 166 | breqtrd 4426 |
. . . . . . 7
          
              |
168 | 106 | nnred 10621 |
. . . . . . . 8
     
  
    |
169 | 106 | nngt0d 10650 |
. . . . . . . 8
             |
170 | | ltdivmul 10477 |
. . . . . . . 8
                                  
                      
 
                       |
171 | 103, 108,
168, 169, 170 | syl112anc 1271 |
. . . . . . 7
           
  
                  
               |
172 | 167, 171 | mpbird 236 |
. . . . . 6
          
              |
173 | 51, 107, 108, 131, 172 | lelttrd 9790 |
. . . . 5
                     |
174 | 51, 135, 99 | ltmuldiv2d 11383 |
. . . . 5
                    
   
                |
175 | 173, 174 | mpbird 236 |
. . . 4
      
   
          |
176 | | 0p1e1 10718 |
. . . 4
   |
177 | 175, 176 | syl6breqr 4442 |
. . 3
      
   
            |
178 | | btwnnz 11009 |
. . 3
                                        
                    |
179 | 98, 101, 177, 178 | syl3anc 1267 |
. 2
                     |
180 | 97, 179 | pm2.65i 177 |
1
 |