Step | Hyp | Ref
| Expression |
1 | | oveq1 6206 |
. . . . . . . . . . 11
       |
2 | | 0p1e1 10543 |
. . . . . . . . . . 11
   |
3 | 1, 2 | syl6eq 2511 |
. . . . . . . . . 10
     |
4 | 3 | oveq2d 6215 |
. . . . . . . . 9
             |
5 | | 2cn 10502 |
. . . . . . . . . . 11
 |
6 | | exp1 11987 |
. . . . . . . . . . 11
       |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . 10
     |
8 | | df-2 10490 |
. . . . . . . . . 10
   |
9 | 7, 8 | eqtri 2483 |
. . . . . . . . 9
       |
10 | 4, 9 | syl6eq 2511 |
. . . . . . . 8
           |
11 | 10 | oveq1d 6214 |
. . . . . . 7
               |
12 | | ax-1cn 9450 |
. . . . . . . 8
 |
13 | | pncan 9726 |
. . . . . . . 8
 
       |
14 | 12, 12, 13 | mp2an 672 |
. . . . . . 7
     |
15 | 11, 14 | syl6eq 2511 |
. . . . . 6
           |
16 | 15 | fveq2d 5802 |
. . . . 5
                       |
17 | | fveq2 5798 |
. . . . 5
               |
18 | 16, 17 | breq12d 4412 |
. . . 4
                                     |
19 | 18 | imbi2d 316 |
. . 3
  
             
      
                 |
20 | | oveq1 6206 |
. . . . . . . 8
       |
21 | 20 | oveq2d 6215 |
. . . . . . 7
               |
22 | 21 | oveq1d 6214 |
. . . . . 6
                   |
23 | 22 | fveq2d 5802 |
. . . . 5
                               |
24 | | fveq2 5798 |
. . . . 5
               |
25 | 23, 24 | breq12d 4412 |
. . . 4
                                             |
26 | 25 | imbi2d 316 |
. . 3
  
             
      
                         |
27 | | oveq1 6206 |
. . . . . . . 8
           |
28 | 27 | oveq2d 6215 |
. . . . . . 7
                   |
29 | 28 | oveq1d 6214 |
. . . . . 6
                       |
30 | 29 | fveq2d 5802 |
. . . . 5
                                   |
31 | | fveq2 5798 |
. . . . 5
                   |
32 | 30, 31 | breq12d 4412 |
. . . 4
                                                   |
33 | 32 | imbi2d 316 |
. . 3
    
             
      
                             |
34 | | oveq1 6206 |
. . . . . . . 8
       |
35 | 34 | oveq2d 6215 |
. . . . . . 7
               |
36 | 35 | oveq1d 6214 |
. . . . . 6
                   |
37 | 36 | fveq2d 5802 |
. . . . 5
                        
      |
38 | | fveq2 5798 |
. . . . 5
               |
39 | 37, 38 | breq12d 4412 |
. . . 4
                                             |
40 | 39 | imbi2d 316 |
. . 3
  
             
      
                         |
41 | | 1nn 10443 |
. . . . . . 7
 |
42 | | climcnds.1 |
. . . . . . . 8
 

      |
43 | 42 | ralrimiva 2829 |
. . . . . . 7
        |
44 | | fveq2 5798 |
. . . . . . . . 9
           |
45 | 44 | eleq1d 2523 |
. . . . . . . 8
     
       |
46 | 45 | rspcv 3173 |
. . . . . . 7
  
           |
47 | 41, 43, 46 | mpsyl 63 |
. . . . . 6
       |
48 | 47 | leidd 10016 |
. . . . 5
    
      |
49 | 47 | recnd 9522 |
. . . . . 6
       |
50 | 49 | mulid2d 9514 |
. . . . 5
             |
51 | 48, 50 | breqtrrd 4425 |
. . . 4
    
        |
52 | | 1z 10786 |
. . . . 5
 |
53 | | eqidd 2455 |
. . . . 5
           |
54 | 52, 53 | seq1i 11936 |
. . . 4
             |
55 | | 0z 10767 |
. . . . 5
 |
56 | | 0nn0 10704 |
. . . . . 6
 |
57 | | climcnds.4 |
. . . . . . 7
 

                    |
58 | 57 | ralrimiva 2829 |
. . . . . 6
                      |
59 | | fveq2 5798 |
. . . . . . . 8
           |
60 | | oveq2 6207 |
. . . . . . . . . 10
           |
61 | | exp0 11985 |
. . . . . . . . . . 11
       |
62 | 5, 61 | ax-mp 5 |
. . . . . . . . . 10
     |
63 | 60, 62 | syl6eq 2511 |
. . . . . . . . 9
       |
64 | 63 | fveq2d 5802 |
. . . . . . . . 9
               |
65 | 63, 64 | oveq12d 6217 |
. . . . . . . 8
                       |
66 | 59, 65 | eqeq12d 2476 |
. . . . . . 7
                   
             |
67 | 66 | rspcv 3173 |
. . . . . 6

 
                 
             |
68 | 56, 58, 67 | mpsyl 63 |
. . . . 5
             |
69 | 55, 68 | seq1i 11936 |
. . . 4
               |
70 | 51, 54, 69 | 3brtr4d 4429 |
. . 3
               |
71 | | fzfid 11911 |
. . . . . . . . 9
 

                      |
72 | | simpl 457 |
. . . . . . . . . . 11
 

  |
73 | 72 | adantr 465 |
. . . . . . . . . 10
                           |
74 | | 2nn 10589 |
. . . . . . . . . . . 12
 |
75 | | peano2nn0 10730 |
. . . . . . . . . . . . 13

    |
76 | 75 | adantl 466 |
. . . . . . . . . . . 12
 

    |
77 | | nnexpcl 11994 |
. . . . . . . . . . . 12
             |
78 | 74, 76, 77 | sylancr 663 |
. . . . . . . . . . 11
 

        |
79 | | elfzuz 11565 |
. . . . . . . . . . 11
                                 |
80 | | eluznn 11035 |
. . . . . . . . . . 11
       
             |
81 | 78, 79, 80 | syl2an 477 |
. . . . . . . . . 10
                           |
82 | 73, 81, 42 | syl2anc 661 |
. . . . . . . . 9
                               |
83 | 43 | adantr 465 |
. . . . . . . . . . 11
 

       |
84 | | fveq2 5798 |
. . . . . . . . . . . . 13
                       |
85 | 84 | eleq1d 2523 |
. . . . . . . . . . . 12
           
             |
86 | 85 | rspcv 3173 |
. . . . . . . . . . 11
        
                 |
87 | 78, 83, 86 | sylc 60 |
. . . . . . . . . 10
 

            |
88 | 87 | adantr 465 |
. . . . . . . . 9
                                     |
89 | | simpr 461 |
. . . . . . . . . . . 12
              
            |
90 | | simplll 757 |
. . . . . . . . . . . . 13
   

          
             |
91 | 78 | adantr 465 |
. . . . . . . . . . . . . 14
              
        |
92 | | elfzuz 11565 |
. . . . . . . . . . . . . 14
                       |
93 | 91, 92, 80 | syl2an 477 |
. . . . . . . . . . . . 13
   

          
             |
94 | 90, 93, 42 | syl2anc 661 |
. . . . . . . . . . . 12
   

          
                 |
95 | | simplll 757 |
. . . . . . . . . . . . 13
   

          
               |
96 | | elfzuz 11565 |
. . . . . . . . . . . . . 14
                         |
97 | 91, 96, 80 | syl2an 477 |
. . . . . . . . . . . . 13
   

          
               |
98 | | climcnds.3 |
. . . . . . . . . . . . 13
 

            |
99 | 95, 97, 98 | syl2anc 661 |
. . . . . . . . . . . 12
   

          
                         |
100 | 89, 94, 99 | monoord2 11953 |
. . . . . . . . . . 11
              
                |
101 | 100 | ralrimiva 2829 |
. . . . . . . . . 10
 

               
            |
102 | | fveq2 5798 |
. . . . . . . . . . . 12
           |
103 | 102 | breq1d 4409 |
. . . . . . . . . . 11
     
         
                 |
104 | 103 | rspccva 3176 |
. . . . . . . . . 10
                                      
                |
105 | 101, 79, 104 | syl2an 477 |
. . . . . . . . 9
                                         |
106 | 71, 82, 88, 105 | fsumle 13379 |
. . . . . . . 8
 

                                                            |
107 | | fzfid 11911 |
. . . . . . . . . . . . 13
 

              |
108 | | hashcl 12242 |
. . . . . . . . . . . . 13
                               |
109 | 107, 108 | syl 16 |
. . . . . . . . . . . 12
 

                  |
110 | 109 | nn0cnd 10748 |
. . . . . . . . . . 11
 

                  |
111 | 78 | nnred 10447 |
. . . . . . . . . . . 12
 

        |
112 | 111 | recnd 9522 |
. . . . . . . . . . 11
 

        |
113 | | hashcl 12242 |
. . . . . . . . . . . . 13
                                               |
114 | 71, 113 | syl 16 |
. . . . . . . . . . . 12
 

                          |
115 | 114 | nn0cnd 10748 |
. . . . . . . . . . 11
 

                          |
116 | | 2z 10788 |
. . . . . . . . . . . . . . . . . . . 20
 |
117 | | zexpcl 11996 |
. . . . . . . . . . . . . . . . . . . 20
             |
118 | 116, 76, 117 | sylancr 663 |
. . . . . . . . . . . . . . . . . . 19
 

        |
119 | | nn0p1nn 10729 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
120 | 119 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    |
121 | | nnuz 11006 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
122 | 120, 121 | syl6eleq 2552 |
. . . . . . . . . . . . . . . . . . . . 21
 

        |
123 | | 2re 10501 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
124 | | 1le2 10645 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
125 | | leexp2a 12035 |
. . . . . . . . . . . . . . . . . . . . . 22
                     |
126 | 123, 124,
125 | mp3an12 1305 |
. . . . . . . . . . . . . . . . . . . . 21
      
            |
127 | 122, 126 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
 

            |
128 | 7, 127 | syl5eqbrr 4433 |
. . . . . . . . . . . . . . . . . . 19
 

        |
129 | 116 | eluz1i 10978 |
. . . . . . . . . . . . . . . . . . 19
                           |
130 | 118, 128,
129 | sylanbrc 664 |
. . . . . . . . . . . . . . . . . 18
 

            |
131 | | uz2m1nn 11039 |
. . . . . . . . . . . . . . . . . 18
          
          |
132 | 130, 131 | syl 16 |
. . . . . . . . . . . . . . . . 17
 

          |
133 | 132, 121 | syl6eleq 2552 |
. . . . . . . . . . . . . . . 16
 

              |
134 | | peano2zm 10798 |
. . . . . . . . . . . . . . . . . 18
                 |
135 | 118, 134 | syl 16 |
. . . . . . . . . . . . . . . . 17
 

          |
136 | | peano2nn0 10730 |
. . . . . . . . . . . . . . . . . . . 20
  
      |
137 | 76, 136 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
 

      |
138 | | zexpcl 11996 |
. . . . . . . . . . . . . . . . . . 19
                 |
139 | 116, 137,
138 | sylancr 663 |
. . . . . . . . . . . . . . . . . 18
 

          |
140 | | peano2zm 10798 |
. . . . . . . . . . . . . . . . . 18
                     |
141 | 139, 140 | syl 16 |
. . . . . . . . . . . . . . . . 17
 

            |
142 | 118 | zred 10857 |
. . . . . . . . . . . . . . . . . 18
 

        |
143 | 139 | zred 10857 |
. . . . . . . . . . . . . . . . . 18
 

          |
144 | | 1red 9511 |
. . . . . . . . . . . . . . . . . 18
 

  |
145 | 76 | nn0zd 10855 |
. . . . . . . . . . . . . . . . . . 19
 

    |
146 | | uzid 10985 |
. . . . . . . . . . . . . . . . . . 19
             |
147 | | peano2uz 11018 |
. . . . . . . . . . . . . . . . . . 19
        
            |
148 | | leexp2a 12035 |
. . . . . . . . . . . . . . . . . . . 20
                             |
149 | 123, 124,
148 | mp3an12 1305 |
. . . . . . . . . . . . . . . . . . 19
          
                |
150 | 145, 146,
147, 149 | 4syl 21 |
. . . . . . . . . . . . . . . . . 18
 

                |
151 | 142, 143,
144, 150 | lesub1dd 10065 |
. . . . . . . . . . . . . . . . 17
 

                    |
152 | | eluz2 10977 |
. . . . . . . . . . . . . . . . 17
                                                               |
153 | 135, 141,
151, 152 | syl3anbrc 1172 |
. . . . . . . . . . . . . . . 16
 

                        |
154 | | elfzuzb 11563 |
. . . . . . . . . . . . . . . 16
                      
            
                         |
155 | 133, 153,
154 | sylanbrc 664 |
. . . . . . . . . . . . . . 15
 

                        |
156 | | fzsplit 11591 |
. . . . . . . . . . . . . . 15
                                                                             |
157 | 155, 156 | syl 16 |
. . . . . . . . . . . . . 14
 

                                                      |
158 | | npcan 9729 |
. . . . . . . . . . . . . . . . 17
       
                   |
159 | 112, 12, 158 | sylancl 662 |
. . . . . . . . . . . . . . . 16
 

                  |
160 | 159 | oveq1d 6214 |
. . . . . . . . . . . . . . 15
 

                                              |
161 | 160 | uneq2d 3617 |
. . . . . . . . . . . . . 14
 

                                                                          |
162 | 157, 161 | eqtrd 2495 |
. . . . . . . . . . . . 13
 

                                                  |
163 | 162 | fveq2d 5802 |
. . . . . . . . . . . 12
 

                                                          |
164 | | expp1 11988 |
. . . . . . . . . . . . . . . . 17
                       |
165 | 5, 76, 164 | sylancr 663 |
. . . . . . . . . . . . . . . 16
 

                  |
166 | 112 | times2d 10678 |
. . . . . . . . . . . . . . . 16
 

                        |
167 | 165, 166 | eqtrd 2495 |
. . . . . . . . . . . . . . 15
 

                        |
168 | 167 | oveq1d 6214 |
. . . . . . . . . . . . . 14
 

                            |
169 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
 

  |
170 | 112, 112,
169 | addsubd 9850 |
. . . . . . . . . . . . . 14
 

                                  |
171 | 168, 170 | eqtrd 2495 |
. . . . . . . . . . . . 13
 

                            |
172 | | uztrn 10987 |
. . . . . . . . . . . . . . . . 17
                                                     |
173 | 153, 133,
172 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
 

                |
174 | 173, 121 | syl6eleqr 2553 |
. . . . . . . . . . . . . . 15
 

            |
175 | 174 | nnnn0d 10746 |
. . . . . . . . . . . . . 14
 

            |
176 | | hashfz1 12233 |
. . . . . . . . . . . . . 14
          
                              |
177 | 175, 176 | syl 16 |
. . . . . . . . . . . . 13
 

                              |
178 | 132 | nnnn0d 10746 |
. . . . . . . . . . . . . . 15
 

          |
179 | | hashfz1 12233 |
. . . . . . . . . . . . . . 15
        
                          |
180 | 178, 179 | syl 16 |
. . . . . . . . . . . . . 14
 

                          |
181 | 180 | oveq1d 6214 |
. . . . . . . . . . . . 13
 

                                          |
182 | 171, 177,
181 | 3eqtr4d 2505 |
. . . . . . . . . . . 12
 

                                            |
183 | 111 | ltm1d 10375 |
. . . . . . . . . . . . . 14
 

                |
184 | | fzdisj 11592 |
. . . . . . . . . . . . . 14
                                                   |
185 | 183, 184 | syl 16 |
. . . . . . . . . . . . 13
 

                                    |
186 | | hashun 12262 |
. . . . . . . . . . . . 13
                                                                                                                                                       |
187 | 107, 71, 185, 186 | syl3anc 1219 |
. . . . . . . . . . . 12
 

                                                                                  |
188 | 163, 182,
187 | 3eqtr3d 2503 |
. . . . . . . . . . 11
 

                                                                    |
189 | 110, 112,
115, 188 | addcanad 9684 |
. . . . . . . . . 10
 

                                |
190 | 189 | oveq1d 6214 |
. . . . . . . . 9
 

                                                        |
191 | 58 | adantr 465 |
. . . . . . . . . 10
 

                     |
192 | | fveq2 5798 |
. . . . . . . . . . . 12
               |
193 | | oveq2 6207 |
. . . . . . . . . . . . 13
               |
194 | 193 | fveq2d 5802 |
. . . . . . . . . . . . 13
                       |
195 | 193, 194 | oveq12d 6217 |
. . . . . . . . . . . 12
                                     |
196 | 192, 195 | eqeq12d 2476 |
. . . . . . . . . . 11
                     
                           |
197 | 196 | rspcv 3173 |
. . . . . . . . . 10
  
 
                 
                           |
198 | 76, 191, 197 | sylc 60 |
. . . . . . . . 9
 

                          |
199 | 87 | recnd 9522 |
. . . . . . . . . 10
 

            |
200 | | fsumconst 13374 |
. . . . . . . . . 10
                                                                                                       |
201 | 71, 199, 200 | syl2anc 661 |
. . . . . . . . 9
 

                                                                      |
202 | 190, 198,
201 | 3eqtr4d 2505 |
. . . . . . . 8
 

      
                                 |
203 | 106, 202 | breqtrrd 4425 |
. . . . . . 7
 

                                  |
204 | | elfznn 11594 |
. . . . . . . . . 10
               |
205 | 72, 204, 42 | syl2an 477 |
. . . . . . . . 9
                       |
206 | 107, 205 | fsumrecl 13328 |
. . . . . . . 8
 

                    |
207 | 71, 82 | fsumrecl 13328 |
. . . . . . . 8
 

                            |
208 | | nn0uz 11005 |
. . . . . . . . . 10
     |
209 | | 0zd 10768 |
. . . . . . . . . 10
   |
210 | | simpr 461 |
. . . . . . . . . . . . . 14
 

  |
211 | | nnexpcl 11994 |
. . . . . . . . . . . . . 14
 
       |
212 | 74, 210, 211 | sylancr 663 |
. . . . . . . . . . . . 13
 

      |
213 | 212 | nnred 10447 |
. . . . . . . . . . . 12
 

      |
214 | 43 | adantr 465 |
. . . . . . . . . . . . 13
 

       |
215 | | fveq2 5798 |
. . . . . . . . . . . . . . 15
                   |
216 | 215 | eleq1d 2523 |
. . . . . . . . . . . . . 14
         
           |
217 | 216 | rspcv 3173 |
. . . . . . . . . . . . 13
      
               |
218 | 212, 214,
217 | sylc 60 |
. . . . . . . . . . . 12
 

          |
219 | 213, 218 | remulcld 9524 |
. . . . . . . . . . 11
 

                |
220 | 57, 219 | eqeltrd 2542 |
. . . . . . . . . 10
 

      |
221 | 208, 209,
220 | serfre 11951 |
. . . . . . . . 9
          |
222 | 221 | ffvelrnda 5951 |
. . . . . . . 8
 

        |
223 | 142, 87 | remulcld 9524 |
. . . . . . . . 9
 

                    |
224 | 198, 223 | eqeltrd 2542 |
. . . . . . . 8
 

        |
225 | | le2add 9931 |
. . . . . . . 8
                                                                                        
                                
 
                                                             |
226 | 206, 207,
222, 224, 225 | syl22anc 1220 |
. . . . . . 7
 

                                                   
                                                                      |
227 | 203, 226 | mpan2d 674 |
. . . . . 6
 

 
                                                                                      |
228 | | eqidd 2455 |
. . . . . . . . 9
                           |
229 | 42 | recnd 9522 |
. . . . . . . . . 10
 

      |
230 | 72, 204, 229 | syl2an 477 |
. . . . . . . . 9
                       |
231 | 228, 133,
230 | fsumser 13324 |
. . . . . . . 8
 

                                  |
232 | 231 | eqcomd 2462 |
. . . . . . 7
 

                                  |
233 | 232 | breq1d 4409 |
. . . . . 6
 

              
                       
         |
234 | | eqidd 2455 |
. . . . . . . . 9
                             |
235 | | elfznn 11594 |
. . . . . . . . . 10
                 |
236 | 72, 235, 229 | syl2an 477 |
. . . . . . . . 9
                         |
237 | 234, 173,
236 | fsumser 13324 |
. . . . . . . 8
 

                                      |
238 | | fzfid 11911 |
. . . . . . . . 9
 

                |
239 | 185, 162,
238, 236 | fsumsplit 13333 |
. . . . . . . 8
 

                                                                    |
240 | 237, 239 | eqtr3d 2497 |
. . . . . . 7
 

                 
                                              |
241 | | simpr 461 |
. . . . . . . . 9
 

  |
242 | 241, 208 | syl6eleq 2552 |
. . . . . . . 8
 

      |
243 | | seqp1 11937 |
. . . . . . . 8
    
                        |
244 | 242, 243 | syl 16 |
. . . . . . 7
 

                        |
245 | 240, 244 | breq12d 4412 |
. . . . . 6
 

                
                           
                         
                 |
246 | 227, 233,
245 | 3imtr4d 268 |
. . . . 5
 

              
     
               
           |
247 | 246 | expcom 435 |
. . . 4

                                                  |
248 | 247 | a2d 26 |
. . 3

                      
                             |
249 | 19, 26, 33, 40, 70, 248 | nn0ind 10848 |
. 2

                        |
250 | 249 | impcom 430 |
1
 

         
   
        |