Step | Hyp | Ref
| Expression |
1 | | esum 11015 |
. . . . . . . . . . 11
        |
2 | | faccl 10206 |
. . . . . . . . . . . . . 14

      |
3 | 2 | nnrecred 8532 |
. . . . . . . . . . . . 13

        |
4 | | fveq2 5320 |
. . . . . . . . . . . . . . 15
           |
5 | 4 | oveq2d 5684 |
. . . . . . . . . . . . . 14
               |
6 | | eirr.1 |
. . . . . . . . . . . . . 14
         |
7 | 5, 6 | fvmptg 5395 |
. . . . . . . . . . . . 13
                     |
8 | 3, 7 | mpdan 413 |
. . . . . . . . . . . 12

            |
9 | 8 | sumeq2i 10816 |
. . . . . . . . . . 11
     
       |
10 | 1, 9 | eqtr4i 2112 |
. . . . . . . . . 10
      |
11 | | nn0uz 9116 |
. . . . . . . . . . 11
     |
12 | | eqid 2089 |
. . . . . . . . . . 11
   
         |
13 | | eirr.3 |
. . . . . . . . . . . . 13
   |
14 | 13 | peano2nnd 8500 |
. . . . . . . . . . . 12
     |
15 | 14 | nnnn0d 8789 |
. . . . . . . . . . 11
     |
16 | | eqidd 2090 |
. . . . . . . . . . 11
 

          |
17 | | ax-1cn 7501 |
. . . . . . . . . . . . . 14
 |
18 | | nn0z 8833 |
. . . . . . . . . . . . . . . . . . 19

  |
19 | | 1exp 10047 |
. . . . . . . . . . . . . . . . . . 19
       |
20 | 18, 19 | syl 14 |
. . . . . . . . . . . . . . . . . 18

      |
21 | 20 | oveq1d 5683 |
. . . . . . . . . . . . . . . . 17

                  |
22 | 21 | mpteq2ia 3932 |
. . . . . . . . . . . . . . . 16

                    |
23 | 6, 22 | eqtr4i 2112 |
. . . . . . . . . . . . . . 15
             |
24 | 23 | eftvalcn 11010 |
. . . . . . . . . . . . . 14
 
                 |
25 | 17, 24 | mpan 416 |
. . . . . . . . . . . . 13

                |
26 | 25 | adantl 272 |
. . . . . . . . . . . 12
 

                |
27 | 17 | a1i 9 |
. . . . . . . . . . . . 13
   |
28 | | eftcl 11007 |
. . . . . . . . . . . . 13
 
             |
29 | 27, 28 | sylan 278 |
. . . . . . . . . . . 12
 

            |
30 | 26, 29 | eqeltrd 2165 |
. . . . . . . . . . 11
 

      |
31 | 23 | efcllem 11012 |
. . . . . . . . . . . 12
     |
32 | 27, 31 | syl 14 |
. . . . . . . . . . 11
     |
33 | 11, 12, 15, 16, 30, 32 | isumsplit 10948 |
. . . . . . . . . 10
                     
   
          |
34 | 10, 33 | syl5eq 2133 |
. . . . . . . . 9
  
                            |
35 | 13 | nncnd 8499 |
. . . . . . . . . . . . 13
   |
36 | | pncan 7751 |
. . . . . . . . . . . . 13
 
       |
37 | 35, 17, 36 | sylancl 405 |
. . . . . . . . . . . 12
       |
38 | 37 | oveq2d 5684 |
. . . . . . . . . . 11
               |
39 | 38 | sumeq1d 10818 |
. . . . . . . . . 10
                           |
40 | 39 | oveq1d 5683 |
. . . . . . . . 9
                                                       |
41 | 34, 40 | eqtrd 2121 |
. . . . . . . 8
  
                        |
42 | 41 | oveq1d 5683 |
. . . . . . 7
  
                                   
            |
43 | | 0zd 8825 |
. . . . . . . . . 10
   |
44 | 13 | nnzd 8930 |
. . . . . . . . . 10
   |
45 | 43, 44 | fzfigd 9901 |
. . . . . . . . 9
       |
46 | | elfznn0 9591 |
. . . . . . . . . 10
       |
47 | 46, 30 | sylan2 281 |
. . . . . . . . 9
 
           |
48 | 45, 47 | fsumcl 10857 |
. . . . . . . 8
             |
49 | 8 | adantl 272 |
. . . . . . . . . . . 12
 

            |
50 | 2 | adantl 272 |
. . . . . . . . . . . . . 14
 

      |
51 | 50 | nnrpd 9235 |
. . . . . . . . . . . . 13
 

      |
52 | 51 | rpreccld 9247 |
. . . . . . . . . . . 12
 

        |
53 | 49, 52 | eqeltrd 2165 |
. . . . . . . . . . 11
 

      |
54 | 11, 12, 15, 16, 53, 32 | isumrpcl 10951 |
. . . . . . . . . 10
               |
55 | 54 | rpred 9236 |
. . . . . . . . 9
               |
56 | 55 | recnd 7579 |
. . . . . . . 8
               |
57 | 48, 56 | pncan2d 7858 |
. . . . . . 7
             
   
                   
   
         |
58 | 42, 57 | eqtrd 2121 |
. . . . . 6
  
                        |
59 | 58 | oveq2d 5684 |
. . . . 5
      
                                |
60 | 13 | nnnn0d 8789 |
. . . . . . . 8
   |
61 | 60 | faccld 10207 |
. . . . . . 7
       |
62 | 61 | nncnd 8499 |
. . . . . 6
       |
63 | | ere 11023 |
. . . . . . . 8
 |
64 | 63 | recni 7563 |
. . . . . . 7
 |
65 | 64 | a1i 9 |
. . . . . 6
   |
66 | 62, 65, 48 | subdid 7955 |
. . . . 5
      
                        
             |
67 | 59, 66 | eqtr3d 2123 |
. . . 4
      
   
                    
             |
68 | 61 | nnrpd 9235 |
. . . . . . 7
       |
69 | 68, 54 | rpmulcld 9253 |
. . . . . 6
      
   
          |
70 | 69 | rpred 9236 |
. . . . 5
      
   
          |
71 | | eirr.2 |
. . . . . . . . 9
   |
72 | 71 | zcnd 8932 |
. . . . . . . 8
   |
73 | 13 | nnap0d 8531 |
. . . . . . . 8
 #   |
74 | 62, 72, 35, 73 | div12apd 8357 |
. . . . . . 7
                   |
75 | 13 | nnred 8498 |
. . . . . . . . . . 11
   |
76 | 75 | leidd 8055 |
. . . . . . . . . 10

  |
77 | | facdiv 10209 |
. . . . . . . . . 10
 
         |
78 | 60, 13, 76, 77 | syl3anc 1175 |
. . . . . . . . 9
         |
79 | 78 | nnzd 8930 |
. . . . . . . 8
         |
80 | 71, 79 | zmulcld 8937 |
. . . . . . 7
           |
81 | 74, 80 | eqeltrd 2165 |
. . . . . 6
           |
82 | 45, 62, 47 | fsummulc2 10905 |
. . . . . . 7
      
                            |
83 | 46 | adantl 272 |
. . . . . . . . . . . . 13
 
       |
84 | 83, 8 | syl 14 |
. . . . . . . . . . . 12
 
                 |
85 | 84 | oveq2d 5684 |
. . . . . . . . . . 11
 
                             |
86 | 62 | adantr 271 |
. . . . . . . . . . . 12
 
           |
87 | 46, 50 | sylan2 281 |
. . . . . . . . . . . . 13
 
           |
88 | 87 | nncnd 8499 |
. . . . . . . . . . . 12
 
           |
89 | 87 | nnap0d 8531 |
. . . . . . . . . . . 12
 
         #   |
90 | 86, 88, 89 | divrecapd 8323 |
. . . . . . . . . . 11
 
                             |
91 | 85, 90 | eqtr4d 2124 |
. . . . . . . . . 10
 
                           |
92 | | permnn 10242 |
. . . . . . . . . . 11
                 |
93 | 92 | adantl 272 |
. . . . . . . . . 10
 
                 |
94 | 91, 93 | eqeltrd 2165 |
. . . . . . . . 9
 
                 |
95 | 94 | nnzd 8930 |
. . . . . . . 8
 
                 |
96 | 45, 95 | fsumzcl 10859 |
. . . . . . 7
                   |
97 | 82, 96 | eqeltrd 2165 |
. . . . . 6
      
            |
98 | 81, 97 | zsubcld 8936 |
. . . . 5
                             |
99 | 69 | rpgt0d 9239 |
. . . . 5
                     |
100 | 14 | peano2nnd 8500 |
. . . . . . . . . 10
       |
101 | 100 | nnred 8498 |
. . . . . . . . 9
       |
102 | 15 | faccld 10207 |
. . . . . . . . . 10
    
    |
103 | 102, 14 | nnmulcld 8534 |
. . . . . . . . 9
     
  
    |
104 | 101, 103 | nndivred 8535 |
. . . . . . . 8
          
        |
105 | 61 | nnrecred 8532 |
. . . . . . . 8
         |
106 | | abs1 10568 |
. . . . . . . . . . . . . 14
     |
107 | 106 | oveq1i 5678 |
. . . . . . . . . . . . 13
             |
108 | 107 | oveq1i 5678 |
. . . . . . . . . . . 12
                         |
109 | 108 | mpteq2i 3933 |
. . . . . . . . . . 11

                            |
110 | 23, 109 | eqtr4i 2112 |
. . . . . . . . . 10
                 |
111 | | eqid 2089 |
. . . . . . . . . 10

               
                               
                |
112 | | 1le1 8112 |
. . . . . . . . . . . 12
 |
113 | 106, 112 | eqbrtri 3872 |
. . . . . . . . . . 11
     |
114 | 113 | a1i 9 |
. . . . . . . . . 10
    
  |
115 | 23, 110, 111, 14, 27, 114 | eftlub 11043 |
. . . . . . . . 9
    
   
                            
         |
116 | 54 | rprege0d 9244 |
. . . . . . . . . 10
                             |
117 | | absid 10567 |
. . . . . . . . . 10
                          
                              |
118 | 116, 117 | syl 14 |
. . . . . . . . 9
    
   
                      |
119 | 106 | oveq1i 5678 |
. . . . . . . . . . . 12
             
   |
120 | 14 | nnzd 8930 |
. . . . . . . . . . . . 13
     |
121 | | 1exp 10047 |
. . . . . . . . . . . . 13
           |
122 | 120, 121 | syl 14 |
. . . . . . . . . . . 12
    
    |
123 | 119, 122 | syl5eq 2133 |
. . . . . . . . . . 11
             |
124 | 123 | oveq1d 5683 |
. . . . . . . . . 10
                                       
  
      |
125 | 104 | recnd 7579 |
. . . . . . . . . . 11
          
        |
126 | 125 | mulid2d 7569 |
. . . . . . . . . 10
                                     |
127 | 124, 126 | eqtrd 2121 |
. . . . . . . . 9
                                               |
128 | 115, 118,
127 | 3brtr3d 3882 |
. . . . . . . 8
                      
  
     |
129 | 14 | nnred 8498 |
. . . . . . . . . . . 12
     |
130 | 129, 129 | readdcld 7580 |
. . . . . . . . . . 11
         |
131 | 129, 129 | remulcld 7581 |
. . . . . . . . . . 11
    
    |
132 | | 1red 7566 |
. . . . . . . . . . . 12
   |
133 | 13 | nnge1d 8528 |
. . . . . . . . . . . . 13

  |
134 | | 1nn 8496 |
. . . . . . . . . . . . . 14
 |
135 | | nnleltp1 8872 |
. . . . . . . . . . . . . 14
 
       |
136 | 134, 13, 135 | sylancr 406 |
. . . . . . . . . . . . 13
       |
137 | 133, 136 | mpbid 146 |
. . . . . . . . . . . 12
     |
138 | 132, 129,
129, 137 | ltadd2dd 7963 |
. . . . . . . . . . 11
             |
139 | 14 | nncnd 8499 |
. . . . . . . . . . . . 13
     |
140 | 139 | 2timesd 8721 |
. . . . . . . . . . . 12
  
          |
141 | | df-2 8544 |
. . . . . . . . . . . . . 14
   |
142 | 132, 75, 132, 133 | leadd1dd 8099 |
. . . . . . . . . . . . . 14
  
    |
143 | 141, 142 | syl5eqbr 3886 |
. . . . . . . . . . . . 13

    |
144 | | 2re 8555 |
. . . . . . . . . . . . . . 15
 |
145 | 144 | a1i 9 |
. . . . . . . . . . . . . 14
   |
146 | 14 | nngt0d 8529 |
. . . . . . . . . . . . . 14
     |
147 | | lemul1 8133 |
. . . . . . . . . . . . . 14
  
       
  
       
     |
148 | 145, 129,
129, 146, 147 | syl112anc 1179 |
. . . . . . . . . . . . 13
  
  
 
 
       |
149 | 143, 148 | mpbid 146 |
. . . . . . . . . . . 12
  
 
 
      |
150 | 140, 149 | eqbrtrrd 3875 |
. . . . . . . . . . 11
      
 
      |
151 | 101, 130,
131, 138, 150 | ltletrd 7964 |
. . . . . . . . . 10
             |
152 | | facp1 10201 |
. . . . . . . . . . . . . . 15

           
    |
153 | 60, 152 | syl 14 |
. . . . . . . . . . . . . 14
    
            |
154 | 153 | oveq1d 5683 |
. . . . . . . . . . . . 13
     
                       |
155 | 102 | nncnd 8499 |
. . . . . . . . . . . . . 14
    
    |
156 | 61 | nnap0d 8531 |
. . . . . . . . . . . . . 14
     #   |
157 | 155, 62, 156 | divrecapd 8323 |
. . . . . . . . . . . . 13
     
                       |
158 | 139, 62, 156 | divcanap3d 8325 |
. . . . . . . . . . . . 13
                   |
159 | 154, 157,
158 | 3eqtr3rd 2130 |
. . . . . . . . . . . 12
                   |
160 | 159 | oveq1d 5683 |
. . . . . . . . . . 11
    
       
              |
161 | 105 | recnd 7579 |
. . . . . . . . . . . 12
         |
162 | 155, 161,
139 | mul32d 7698 |
. . . . . . . . . . 11
                
       
              |
163 | 160, 162 | eqtrd 2121 |
. . . . . . . . . 10
    
       
              |
164 | 151, 163 | breqtrd 3877 |
. . . . . . . . 9
          
              |
165 | 103 | nnred 8498 |
. . . . . . . . . 10
     
  
    |
166 | 103 | nngt0d 8529 |
. . . . . . . . . 10
             |
167 | | ltdivmul 8400 |
. . . . . . . . . 10
                                  
                      
 
                       |
168 | 101, 105,
165, 166, 167 | syl112anc 1179 |
. . . . . . . . 9
           
  
                  
               |
169 | 164, 168 | mpbird 166 |
. . . . . . . 8
          
              |
170 | 55, 104, 105, 128, 169 | lelttrd 7671 |
. . . . . . 7
                     |
171 | 55, 132, 68 | ltmuldiv2d 9285 |
. . . . . . 7
                    
   
                |
172 | 170, 171 | mpbird 166 |
. . . . . 6
      
   
          |
173 | | 0p1e1 8599 |
. . . . . 6
   |
174 | 172, 173 | syl6breqr 3893 |
. . . . 5
      
   
            |
175 | 43, 70, 98, 99, 174 | btwnapz 8939 |
. . . 4
      
   
        #                             |
176 | 67, 175 | eqbrtrrd 3875 |
. . 3
                         #                             |
177 | 62, 65 | mulcld 7571 |
. . . 4
      
  |
178 | 81 | zcnd 8932 |
. . . 4
           |
179 | 62, 48 | mulcld 7571 |
. . . 4
      
            |
180 | | apsub1 8180 |
. . . 4
       
                                #                                 #                              |
181 | 177, 178,
179, 180 | syl3anc 1175 |
. . 3
        #        
                        #                              |
182 | 176, 181 | mpbird 166 |
. 2
       #           |
183 | | znq 9172 |
. . . . 5
 
     |
184 | 71, 13, 183 | syl2anc 404 |
. . . 4
     |
185 | | qcn 9182 |
. . . 4
       |
186 | 184, 185 | syl 14 |
. . 3
     |
187 | | apmul2 8319 |
. . 3
  
          #    #  
      #            |
188 | 65, 186, 62, 156, 187 | syl112anc 1179 |
. 2
  #  
      #            |
189 | 182, 188 | mpbird 166 |
1
 #     |