Step | Hyp | Ref
| Expression |
1 | | eftl.5 |
. . . 4
   |
2 | | eftl.4 |
. . . . 5
   |
3 | 2 | nnnn0d 9229 |
. . . 4
   |
4 | | eftl.1 |
. . . . 5
             |
5 | 4 | eftlcl 11696 |
. . . 4
 
             |
6 | 1, 3, 5 | syl2anc 411 |
. . 3
             |
7 | 6 | abscld 11190 |
. 2
    
            |
8 | 1 | abscld 11190 |
. . 3
       |
9 | | eftl.2 |
. . . 4
                 |
10 | 9 | reeftlcl 11697 |
. . 3
     
             |
11 | 8, 3, 10 | syl2anc 411 |
. 2
             |
12 | 8, 3 | reexpcld 10671 |
. . 3
           |
13 | | peano2nn0 9216 |
. . . . . 6

    |
14 | 3, 13 | syl 14 |
. . . . 5
     |
15 | 14 | nn0red 9230 |
. . . 4
     |
16 | 3 | faccld 10716 |
. . . . 5
       |
17 | 16, 2 | nnmulcld 8968 |
. . . 4
         |
18 | 15, 17 | nndivred 8969 |
. . 3
             |
19 | 12, 18 | remulcld 7988 |
. 2
                       |
20 | | eqid 2177 |
. . 3
         |
21 | 2 | nnzd 9374 |
. . . 4
   |
22 | | eqidd 2178 |
. . . 4
 
    
          |
23 | | eluznn0 9599 |
. . . . . 6
 
       |
24 | 3, 23 | sylan 283 |
. . . . 5
 
    
  |
25 | 4 | eftvalcn 11665 |
. . . . . . 7
 
                 |
26 | 1, 25 | sylan 283 |
. . . . . 6
 

                |
27 | | eftcl 11662 |
. . . . . . 7
 
             |
28 | 1, 27 | sylan 283 |
. . . . . 6
 

            |
29 | 26, 28 | eqeltrd 2254 |
. . . . 5
 

      |
30 | 24, 29 | syldan 282 |
. . . 4
 
    
      |
31 | 4 | eftlcvg 11695 |
. . . . 5
 
     |
32 | 1, 3, 31 | syl2anc 411 |
. . . 4
     |
33 | 20, 21, 22, 30, 32 | isumclim2 11430 |
. . 3
                |
34 | | eqidd 2178 |
. . . 4
 
    
          |
35 | 8 | recnd 7986 |
. . . . . . . 8
       |
36 | 9 | eftvalcn 11665 |
. . . . . . . 8
     
                     |
37 | 35, 36 | sylan 283 |
. . . . . . 7
 

                    |
38 | | reeftcl 11663 |
. . . . . . . 8
     
                 |
39 | 8, 38 | sylan 283 |
. . . . . . 7
 

                |
40 | 37, 39 | eqeltrd 2254 |
. . . . . 6
 

      |
41 | 24, 40 | syldan 282 |
. . . . 5
 
    
      |
42 | 41 | recnd 7986 |
. . . 4
 
    
      |
43 | 9 | eftlcvg 11695 |
. . . . 5
     
     |
44 | 35, 3, 43 | syl2anc 411 |
. . . 4
     |
45 | 20, 21, 34, 42, 44 | isumclim2 11430 |
. . 3
                |
46 | | eftabs 11664 |
. . . . . 6
 
                               |
47 | 1, 46 | sylan 283 |
. . . . 5
 

                              |
48 | 26 | fveq2d 5520 |
. . . . 5
 

                        |
49 | 47, 48, 37 | 3eqtr4rd 2221 |
. . . 4
 

              |
50 | 24, 49 | syldan 282 |
. . 3
 
    
              |
51 | 20, 33, 45, 21, 30, 50 | iserabs 11483 |
. 2
    
                      |
52 | | nn0uz 9562 |
. . . 4
     |
53 | | 0zd 9265 |
. . . 4
   |
54 | 2 | nncnd 8933 |
. . . . 5
   |
55 | | nn0cn 9186 |
. . . . 5

  |
56 | | nn0ex 9182 |
. . . . . . . 8
 |
57 | 56 | mptex 5743 |
. . . . . . 7

                |
58 | 9, 57 | eqeltri 2250 |
. . . . . 6
 |
59 | 58 | shftval4 10837 |
. . . . 5
 
                |
60 | 54, 55, 59 | syl2an 289 |
. . . 4
 

               |
61 | 35 | adantr 276 |
. . . . . 6
 

      |
62 | | nn0addcl 9211 |
. . . . . . 7
 
     |
63 | 3, 62 | sylan 283 |
. . . . . 6
 

    |
64 | 9 | eftvalcn 11665 |
. . . . . 6
      
     
                
     |
65 | 61, 63, 64 | syl2anc 411 |
. . . . 5
 

                    
     |
66 | 8 | adantr 276 |
. . . . . 6
 

      |
67 | | reeftcl 11663 |
. . . . . 6
      
          
           |
68 | 66, 63, 67 | syl2anc 411 |
. . . . 5
 

              
     |
69 | 65, 68 | eqeltrd 2254 |
. . . 4
 

        |
70 | | simpr 110 |
. . . . 5
 

  |
71 | 12, 16 | nndivred 8969 |
. . . . . . 7
                 |
72 | 71 | adantr 276 |
. . . . . 6
 

                |
73 | 2 | peano2nnd 8934 |
. . . . . . . 8
     |
74 | 73 | nnrecred 8966 |
. . . . . . 7
  
    |
75 | | reexpcl 10537 |
. . . . . . 7
   
 
           |
76 | 74, 75 | sylan 283 |
. . . . . 6
 

          |
77 | 72, 76 | remulcld 7988 |
. . . . 5
 

                          |
78 | | oveq2 5883 |
. . . . . . 7
   
               |
79 | 78 | oveq2d 5891 |
. . . . . 6
                                          
        |
80 | | eftl.3 |
. . . . . 6
                  
        |
81 | 79, 80 | fvmptg 5593 |
. . . . 5
                   
                                     |
82 | 70, 77, 81 | syl2anc 411 |
. . . 4
 

                              |
83 | 66, 63 | reexpcld 10671 |
. . . . . . 7
 

            |
84 | 12 | adantr 276 |
. . . . . . 7
 

          |
85 | 63 | faccld 10716 |
. . . . . . . . 9
 

        |
86 | 85 | nnred 8932 |
. . . . . . . 8
 

        |
87 | 86, 77 | remulcld 7988 |
. . . . . . 7
 

                                  |
88 | 3 | adantr 276 |
. . . . . . . 8
 

  |
89 | | uzid 9542 |
. . . . . . . . . 10
       |
90 | 21, 89 | syl 14 |
. . . . . . . . 9
       |
91 | | uzaddcl 9586 |
. . . . . . . . 9
       
       |
92 | 90, 91 | sylan 283 |
. . . . . . . 8
 

        |
93 | 1 | absge0d 11193 |
. . . . . . . . 9

      |
94 | 93 | adantr 276 |
. . . . . . . 8
 

      |
95 | | eftl.6 |
. . . . . . . . 9
    
  |
96 | 95 | adantr 276 |
. . . . . . . 8
 

      |
97 | 66, 88, 92, 94, 96 | leexp2rd 10684 |
. . . . . . 7
 

                    |
98 | 16 | adantr 276 |
. . . . . . . . . . . 12
 

      |
99 | | nnexpcl 10533 |
. . . . . . . . . . . . 13
   
         |
100 | 73, 99 | sylan 283 |
. . . . . . . . . . . 12
 

 
      |
101 | 98, 100 | nnmulcld 8968 |
. . . . . . . . . . 11
 

              |
102 | 101 | nnred 8932 |
. . . . . . . . . 10
 

              |
103 | 8, 3, 93 | expge0d 10672 |
. . . . . . . . . . . 12

          |
104 | 12, 103 | jca 306 |
. . . . . . . . . . 11
                     |
105 | 104 | adantr 276 |
. . . . . . . . . 10
 

                    |
106 | | faclbnd6 10724 |
. . . . . . . . . . 11
 
            
        |
107 | 3, 106 | sylan 283 |
. . . . . . . . . 10
 

                    |
108 | | lemul1a 8815 |
. . . . . . . . . 10
                  
                                
                            
                  |
109 | 102, 86, 105, 107, 108 | syl31anc 1241 |
. . . . . . . . 9
 

                          
             |
110 | 86, 84 | remulcld 7988 |
. . . . . . . . . 10
 

                  |
111 | 101 | nnrpd 9694 |
. . . . . . . . . 10
 

              |
112 | 84, 110, 111 | lemuldiv2d 9747 |
. . . . . . . . 9
 

                                              
     
                           |
113 | 109, 112 | mpbid 147 |
. . . . . . . 8
 

             
                          |
114 | 85 | nncnd 8933 |
. . . . . . . . . 10
 

        |
115 | 12 | recnd 7986 |
. . . . . . . . . . 11
           |
116 | 115 | adantr 276 |
. . . . . . . . . 10
 

          |
117 | 101 | nncnd 8933 |
. . . . . . . . . 10
 

              |
118 | 101 | nnap0d 8965 |
. . . . . . . . . 10
 

            #   |
119 | 114, 116,
117, 118 | divassapd 8783 |
. . . . . . . . 9
 

     
                            
                           |
120 | 73 | nncnd 8933 |
. . . . . . . . . . . . . 14
     |
121 | 120 | adantr 276 |
. . . . . . . . . . . . 13
 

    |
122 | 73 | adantr 276 |
. . . . . . . . . . . . . 14
 

    |
123 | 122 | nnap0d 8965 |
. . . . . . . . . . . . 13
 

  #   |
124 | | nn0z 9273 |
. . . . . . . . . . . . . 14

  |
125 | 124 | adantl 277 |
. . . . . . . . . . . . 13
 

  |
126 | 121, 123,
125 | exprecapd 10662 |
. . . . . . . . . . . 12
 

                  |
127 | 126 | oveq2d 5891 |
. . . . . . . . . . 11
 

                                                  |
128 | 71 | recnd 7986 |
. . . . . . . . . . . . 13
                 |
129 | 128 | adantr 276 |
. . . . . . . . . . . 12
 

                |
130 | 100 | nncnd 8933 |
. . . . . . . . . . . 12
 

 
      |
131 | 100 | nnap0d 8965 |
. . . . . . . . . . . 12
 

 
    #   |
132 | 129, 130,
131 | divrecapd 8750 |
. . . . . . . . . . 11
 

                                                |
133 | 16 | nncnd 8933 |
. . . . . . . . . . . . 13
       |
134 | 133 | adantr 276 |
. . . . . . . . . . . 12
 

      |
135 | 98 | nnap0d 8965 |
. . . . . . . . . . . 12
 

    #   |
136 | 116, 134,
130, 135, 131 | divdivap1d 8779 |
. . . . . . . . . . 11
 

                                              |
137 | 127, 132,
136 | 3eqtr2rd 2217 |
. . . . . . . . . 10
 

                                       
        |
138 | 137 | oveq2d 5891 |
. . . . . . . . 9
 

                                  
                             |
139 | 119, 138 | eqtrd 2210 |
. . . . . . . 8
 

     
                            
                             |
140 | 113, 139 | breqtrd 4030 |
. . . . . . 7
 

            
                             |
141 | 83, 84, 87, 97, 140 | letrd 8081 |
. . . . . 6
 

              
                             |
142 | 85 | nngt0d 8963 |
. . . . . . 7
 

        |
143 | | ledivmul 8834 |
. . . . . . 7
                                              
                   
                          
              
                              |
144 | 83, 77, 86, 142, 143 | syl112anc 1242 |
. . . . . 6
 

               
                    
             
 
                                   |
145 | 141, 144 | mpbird 167 |
. . . . 5
 

              
                    
        |
146 | 65, 145 | eqbrtrd 4026 |
. . . 4
 

                                |
147 | 58 | a1i 9 |
. . . . . 6
   |
148 | 21 | znegcld 9377 |
. . . . . 6
    |
149 | | 0cn 7949 |
. . . . . . . . . . . . 13
 |
150 | | subneg 8206 |
. . . . . . . . . . . . 13
 
        |
151 | 149, 150 | mpan 424 |
. . . . . . . . . . . 12
        |
152 | | addlid 8096 |
. . . . . . . . . . . 12
     |
153 | 151, 152 | eqtrd 2210 |
. . . . . . . . . . 11
      |
154 | 54, 153 | syl 14 |
. . . . . . . . . 10
      |
155 | 154 | fveq2d 5520 |
. . . . . . . . 9
              |
156 | 155 | eleq2d 2247 |
. . . . . . . 8
                |
157 | 156 | pm5.32i 454 |
. . . . . . 7
 
        
       |
158 | 157, 41 | sylbi 121 |
. . . . . 6
 
       
      |
159 | | readdcl 7937 |
. . . . . . 7
 
     |
160 | 159 | adantl 277 |
. . . . . 6
 
       |
161 | 147, 53, 148, 158, 160 | seq3shft 10847 |
. . . . 5
                 |
162 | | seqex 10447 |
. . . . . . 7
       |
163 | 54 | negcld 8255 |
. . . . . . 7
    |
164 | | ovshftex 10828 |
. . . . . . 7
                   |
165 | 162, 163,
164 | sylancr 414 |
. . . . . 6
           |
166 | 20, 21, 34, 41, 44 | isumrecl 11437 |
. . . . . 6
             |
167 | 154 | seqeq1d 10451 |
. . . . . . . 8
            |
168 | 167, 45 | eqbrtrd 4026 |
. . . . . . 7
                   |
169 | | climshft 11312 |
. . . . . . . 8
                                                |
170 | 148, 162,
169 | sylancl 413 |
. . . . . . 7
                                       |
171 | 168, 170 | mpbird 167 |
. . . . . 6
                     |
172 | | breldmg 4834 |
. . . . . 6
         
                                      |
173 | 165, 166,
171, 172 | syl3anc 1238 |
. . . . 5
          |
174 | 161, 173 | eqeltrd 2254 |
. . . 4
        |
175 | | seqex 10447 |
. . . . . 6
    |
176 | 175 | a1i 9 |
. . . . 5
      |
177 | 2 | nnge1d 8962 |
. . . . . . . . . 10

  |
178 | | 1nn 8930 |
. . . . . . . . . . 11
 |
179 | | nnleltp1 9312 |
. . . . . . . . . . 11
 
       |
180 | 178, 2, 179 | sylancr 414 |
. . . . . . . . . 10
       |
181 | 177, 180 | mpbid 147 |
. . . . . . . . 9
     |
182 | 14 | nn0ge0d 9232 |
. . . . . . . . . 10

    |
183 | 15, 182 | absidd 11176 |
. . . . . . . . 9
    
      |
184 | 181, 183 | breqtrrd 4032 |
. . . . . . . 8
         |
185 | 74 | adantr 276 |
. . . . . . . . . 10
 

      |
186 | 185, 70 | reexpcld 10671 |
. . . . . . . . 9
 

          |
187 | | eqid 2177 |
. . . . . . . . . 10

                    |
188 | 78, 187 | fvmptg 5593 |
. . . . . . . . 9
            
                      |
189 | 70, 186, 188 | syl2anc 411 |
. . . . . . . 8
 

                        |
190 | 120, 184,
189 | georeclim 11521 |
. . . . . . 7
                        |
191 | 76 | recnd 7986 |
. . . . . . . 8
 

          |
192 | 189, 191 | eqeltrd 2254 |
. . . . . . 7
 

                |
193 | 189 | oveq2d 5891 |
. . . . . . . 8
 

                                               
        |
194 | 82, 193 | eqtr4d 2213 |
. . . . . . 7
 

                    
               |
195 | 52, 53, 128, 190, 192, 194 | isermulc2 11348 |
. . . . . 6
                              |
196 | | ax-1cn 7904 |
. . . . . . . . . . 11
 |
197 | | pncan 8163 |
. . . . . . . . . . 11
 
       |
198 | 54, 196, 197 | sylancl 413 |
. . . . . . . . . 10
       |
199 | 198 | oveq2d 5891 |
. . . . . . . . 9
               |
200 | 199 | oveq2d 5891 |
. . . . . . . 8
                                               |
201 | 15, 2 | nndivred 8969 |
. . . . . . . . . 10
       |
202 | 201 | recnd 7986 |
. . . . . . . . 9
       |
203 | 16 | nnap0d 8965 |
. . . . . . . . 9
     #   |
204 | 115, 202,
133, 203 | div23apd 8785 |
. . . . . . . 8
                                           |
205 | 200, 204 | eqtr4d 2213 |
. . . . . . 7
                                               |
206 | 115, 202,
133, 203 | divassapd 8783 |
. . . . . . 7
                                           |
207 | 2 | nnap0d 8965 |
. . . . . . . . . 10
 #   |
208 | 120, 54, 133, 207, 203 | divdivap1d 8779 |
. . . . . . . . 9
                       |
209 | 54, 133 | mulcomd 7979 |
. . . . . . . . . 10
               |
210 | 209 | oveq2d 5891 |
. . . . . . . . 9
    
                  |
211 | 208, 210 | eqtrd 2210 |
. . . . . . . 8
                       |
212 | 211 | oveq2d 5891 |
. . . . . . 7
                                           |
213 | 205, 206,
212 | 3eqtrd 2214 |
. . . . . 6
                                               |
214 | 195, 213 | breqtrd 4030 |
. . . . 5
                          |
215 | | breldmg 4834 |
. . . . 5
   
                                                |
216 | 176, 19, 214, 215 | syl3anc 1238 |
. . . 4
     |
217 | 52, 53, 60, 69, 82, 77, 146, 174, 216 | isumle 11503 |
. . 3
                          
        |
218 | | eqid 2177 |
. . . . 5
             |
219 | | fveq2 5516 |
. . . . 5
          
    |
220 | 54 | addid2d 8107 |
. . . . . . . . 9
     |
221 | 220 | fveq2d 5520 |
. . . . . . . 8
             |
222 | 221 | eleq2d 2247 |
. . . . . . 7
       
       |
223 | 222 | biimpa 296 |
. . . . . 6
 
             |
224 | 223, 42 | syldan 282 |
. . . . 5
 
             |
225 | 52, 218, 219, 21, 53, 224 | isumshft 11498 |
. . . 4
                      |
226 | 221 | sumeq1d 11374 |
. . . 4
                         |
227 | 225, 226 | eqtr3d 2212 |
. . 3
                    |
228 | 77 | recnd 7986 |
. . . 4
 

                          |
229 | 52, 53, 82, 228, 214 | isumclim 11429 |
. . 3
                   
                            |
230 | 217, 227,
229 | 3brtr3d 4035 |
. 2
                                 |
231 | 7, 11, 19, 51, 230 | letrd 8081 |
1
    
                                |