Step | Hyp | Ref
| Expression |
1 | | nnuz 11201 |
. . . . . 6
     |
2 | | 1zzd 10975 |
. . . . . 6
   |
3 | | fzfid 12193 |
. . . . . 6
       |
4 | | 1zzd 10975 |
. . . . . . . . . 10
           |
5 | | plyeq0.3 |
. . . . . . . . . . . . . . . . 17
         |
6 | | plyeq0.1 |
. . . . . . . . . . . . . . . . . . . 20

  |
7 | | 0cn 9640 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   |
9 | 8 | snssd 4120 |
. . . . . . . . . . . . . . . . . . . 20
     |
10 | 6, 9 | unssd 3612 |
. . . . . . . . . . . . . . . . . . 19
       |
11 | | cnex 9625 |
. . . . . . . . . . . . . . . . . . 19
 |
12 | | ssexg 4552 |
. . . . . . . . . . . . . . . . . . 19
             |
13 | 10, 11, 12 | sylancl 669 |
. . . . . . . . . . . . . . . . . 18
       |
14 | | nn0ex 10882 |
. . . . . . . . . . . . . . . . . 18
 |
15 | | elmapg 7490 |
. . . . . . . . . . . . . . . . . 18
     
                   |
16 | 13, 14, 15 | sylancl 669 |
. . . . . . . . . . . . . . . . 17
                   |
17 | 5, 16 | mpbid 214 |
. . . . . . . . . . . . . . . 16
           |
18 | 17, 10 | fssd 5743 |
. . . . . . . . . . . . . . 15
       |
19 | | elfznn0 11894 |
. . . . . . . . . . . . . . 15
       |
20 | | ffvelrn 6025 |
. . . . . . . . . . . . . . 15
     
       |
21 | 18, 19, 20 | syl2an 480 |
. . . . . . . . . . . . . 14
 
           |
22 | 21 | adantr 467 |
. . . . . . . . . . . . 13
               |
23 | 22 | abscld 13510 |
. . . . . . . . . . . 12
                   |
24 | 23 | recnd 9674 |
. . . . . . . . . . 11
                   |
25 | | divcnv 13923 |
. . . . . . . . . . 11
                       |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
                       |
27 | | nnex 10622 |
. . . . . . . . . . . 12
 |
28 | 27 | mptex 6141 |
. . . . . . . . . . 11
                   |
29 | 28 | a1i 11 |
. . . . . . . . . 10
                             |
30 | | oveq2 6303 |
. . . . . . . . . . . . 13
                       |
31 | | eqid 2453 |
. . . . . . . . . . . . 13
                         |
32 | | ovex 6323 |
. . . . . . . . . . . . 13
           |
33 | 30, 31, 32 | fvmpt 5953 |
. . . . . . . . . . . 12
                             |
34 | 33 | adantl 468 |
. . . . . . . . . . 11
   
     

                            |
35 | | nndivre 10652 |
. . . . . . . . . . . 12
         
             |
36 | 23, 35 | sylan 474 |
. . . . . . . . . . 11
   
     

            |
37 | 34, 36 | eqeltrd 2531 |
. . . . . . . . . 10
   
     

                  |
38 | | oveq1 6302 |
. . . . . . . . . . . . . 14
               |
39 | 38 | oveq2d 6311 |
. . . . . . . . . . . . 13
                                   |
40 | | eqid 2453 |
. . . . . . . . . . . . 13
                                     |
41 | | ovex 6323 |
. . . . . . . . . . . . 13
                 |
42 | 39, 40, 41 | fvmpt 5953 |
. . . . . . . . . . . 12
                                         |
43 | 42 | adantl 468 |
. . . . . . . . . . 11
   
     

                                        |
44 | 21 | ad2antrr 733 |
. . . . . . . . . . . . 13
   
     

      |
45 | 44 | abscld 13510 |
. . . . . . . . . . . 12
   
     

          |
46 | | nnrp 11318 |
. . . . . . . . . . . . . . 15
   |
47 | 46 | adantl 468 |
. . . . . . . . . . . . . 14
   
     

  |
48 | | elfzelz 11807 |
. . . . . . . . . . . . . . . 16
       |
49 | | cnvimass 5191 |
. . . . . . . . . . . . . . . . . . 19
          |
50 | | fdm 5738 |
. . . . . . . . . . . . . . . . . . . 20
        
  |
51 | 17, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   |
52 | 49, 51 | syl5sseq 3482 |
. . . . . . . . . . . . . . . . . 18
            |
53 | | plyeq0.6 |
. . . . . . . . . . . . . . . . . . 19
              |
54 | | nn0ssz 10965 |
. . . . . . . . . . . . . . . . . . . . 21
 |
55 | 52, 54 | syl6ss 3446 |
. . . . . . . . . . . . . . . . . . . 20
            |
56 | | plyeq0.7 |
. . . . . . . . . . . . . . . . . . . 20
            |
57 | | plyeq0.2 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
58 | 57 | nn0red 10933 |
. . . . . . . . . . . . . . . . . . . . 21
   |
59 | 52 | sselda 3434 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
            |
60 | | plyeq0.4 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
61 | | plyco0 23158 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              
    
     
    |
62 | 57, 18, 61 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   
    |
63 | 60, 62 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
   |
64 | 63 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
          
    
   |
65 | | ffn 5733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
  |
66 | 17, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
67 | | elpreima 6007 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

                       |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
             |
69 | 68 | simplbda 630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                    |
70 | | eldifsni 4101 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                |
72 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
73 | 72 | neeq1d 2685 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
74 | | breq1 4408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
75 | 73, 74 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
     
    |
76 | 75 | rspcv 3148 |
. . . . . . . . . . . . . . . . . . . . . . 23

 
          
    |
77 | 59, 64, 71, 76 | syl3c 63 |
. . . . . . . . . . . . . . . . . . . . . 22
 
         
  |
78 | 77 | ralrimiva 2804 |
. . . . . . . . . . . . . . . . . . . . 21
              |
79 | | breq2 4409 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
80 | 79 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . . . . 22
  
                        |
81 | 80 | rspcev 3152 |
. . . . . . . . . . . . . . . . . . . . 21
                         
  |
82 | 58, 78, 81 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
               |
83 | | suprzcl 11022 |
. . . . . . . . . . . . . . . . . . . 20
          
         
          
                         |
84 | 55, 56, 82, 83 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . . 19
                         |
85 | 53, 84 | syl5eqel 2535 |
. . . . . . . . . . . . . . . . . 18
            |
86 | 52, 85 | sseldd 3435 |
. . . . . . . . . . . . . . . . 17
   |
87 | 86 | nn0zd 11045 |
. . . . . . . . . . . . . . . 16
   |
88 | | zsubcl 10986 |
. . . . . . . . . . . . . . . 16
 
     |
89 | 48, 87, 88 | syl2anr 481 |
. . . . . . . . . . . . . . 15
 
         |
90 | 89 | ad2antrr 733 |
. . . . . . . . . . . . . 14
   
     

    |
91 | 47, 90 | rpexpcld 12446 |
. . . . . . . . . . . . 13
   
     

        |
92 | 91 | rpred 11348 |
. . . . . . . . . . . 12
   
     

        |
93 | 45, 92 | remulcld 9676 |
. . . . . . . . . . 11
   
     

                  |
94 | 43, 93 | eqeltrd 2531 |
. . . . . . . . . 10
   
     

                        |
95 | | nnrecre 10653 |
. . . . . . . . . . . . 13
     |
96 | 95 | adantl 468 |
. . . . . . . . . . . 12
   
     

    |
97 | 22 | absge0d 13518 |
. . . . . . . . . . . . 13
                   |
98 | 97 | adantr 467 |
. . . . . . . . . . . 12
   
     

          |
99 | | nnre 10623 |
. . . . . . . . . . . . . . 15
   |
100 | 99 | adantl 468 |
. . . . . . . . . . . . . 14
   
     

  |
101 | | nnge1 10642 |
. . . . . . . . . . . . . . 15
   |
102 | 101 | adantl 468 |
. . . . . . . . . . . . . 14
   
     

  |
103 | | 1red 9663 |
. . . . . . . . . . . . . . . 16
   
     

  |
104 | 90 | zred 11047 |
. . . . . . . . . . . . . . . 16
   
     

    |
105 | | simplr 763 |
. . . . . . . . . . . . . . . . . . 19
   
     

  |
106 | 48 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
107 | 106 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . 20
   
     

  |
108 | 87 | ad3antrrr 737 |
. . . . . . . . . . . . . . . . . . . 20
   
     

  |
109 | | zltp1le 10993 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
110 | 107, 108,
109 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
   
     


     |
111 | 105, 110 | mpbid 214 |
. . . . . . . . . . . . . . . . . 18
   
     

    |
112 | 19 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
113 | 112 | nn0red 10933 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
114 | 113 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . 19
   
     

  |
115 | 86 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
116 | 115 | nn0red 10933 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
117 | 116 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . 19
   
     

  |
118 | 114, 103,
117 | leaddsub2d 10222 |
. . . . . . . . . . . . . . . . . 18
   
     

  
     |
119 | 111, 118 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
   
     

    |
120 | 113 | recnd 9674 |
. . . . . . . . . . . . . . . . . . 19
 
       |
121 | 120 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . 18
   
     

  |
122 | 116 | recnd 9674 |
. . . . . . . . . . . . . . . . . . 19
 
       |
123 | 122 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . 18
   
     

  |
124 | 121, 123 | negsubdi2d 10007 |
. . . . . . . . . . . . . . . . 17
   
     

       |
125 | 119, 124 | breqtrrd 4432 |
. . . . . . . . . . . . . . . 16
   
     

     |
126 | 103, 104,
125 | lenegcon2d 10203 |
. . . . . . . . . . . . . . 15
   
     

     |
127 | | neg1z 10980 |
. . . . . . . . . . . . . . . 16
  |
128 | | eluz 11179 |
. . . . . . . . . . . . . . . 16
             
      |
129 | 90, 127, 128 | sylancl 669 |
. . . . . . . . . . . . . . 15
   
     

       
      |
130 | 126, 129 | mpbird 236 |
. . . . . . . . . . . . . 14
   
     

         |
131 | 100, 102,
130 | leexp2ad 12455 |
. . . . . . . . . . . . 13
   
     

             |
132 | | nncn 10624 |
. . . . . . . . . . . . . . 15
   |
133 | 132 | adantl 468 |
. . . . . . . . . . . . . 14
   
     

  |
134 | | expn1 12289 |
. . . . . . . . . . . . . 14
          |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . 13
   
     

         |
136 | 131, 135 | breqtrd 4430 |
. . . . . . . . . . . 12
   
     

          |
137 | 92, 96, 45, 98, 136 | lemul2ad 10554 |
. . . . . . . . . . 11
   
     

                              |
138 | 24 | adantr 467 |
. . . . . . . . . . . . 13
   
     

          |
139 | | nnne0 10649 |
. . . . . . . . . . . . . 14
   |
140 | 139 | adantl 468 |
. . . . . . . . . . . . 13
   
     

  |
141 | 138, 133,
140 | divrecd 10393 |
. . . . . . . . . . . 12
   
     

                        |
142 | 34, 141 | eqtrd 2487 |
. . . . . . . . . . 11
   
     

                              |
143 | 137, 43, 142 | 3brtr4d 4436 |
. . . . . . . . . 10
   
     

                                        |
144 | 91 | rpge0d 11352 |
. . . . . . . . . . . 12
   
     

        |
145 | 45, 92, 98, 144 | mulge0d 10197 |
. . . . . . . . . . 11
   
     

                  |
146 | 145, 43 | breqtrrd 4432 |
. . . . . . . . . 10
   
     

                        |
147 | 1, 4, 26, 29, 37, 94, 143, 146 | climsqz2 13717 |
. . . . . . . . 9
                             |
148 | 27 | mptex 6141 |
. . . . . . . . . . 11
               |
149 | 148 | a1i 11 |
. . . . . . . . . 10
                         |
150 | 38 | oveq2d 6311 |
. . . . . . . . . . . . . . 15
                           |
151 | | eqid 2453 |
. . . . . . . . . . . . . . 15
                             |
152 | | ovex 6323 |
. . . . . . . . . . . . . . 15
             |
153 | 150, 151,
152 | fvmpt 5953 |
. . . . . . . . . . . . . 14
                                 |
154 | 153 | ad2antlr 734 |
. . . . . . . . . . . . 13
                                         |
155 | 18 | adantr 467 |
. . . . . . . . . . . . . . 15
 

      |
156 | 155, 19, 20 | syl2an 480 |
. . . . . . . . . . . . . 14
               |
157 | 132 | ad2antlr 734 |
. . . . . . . . . . . . . . 15
           |
158 | 139 | ad2antlr 734 |
. . . . . . . . . . . . . . 15
           |
159 | 87 | adantr 467 |
. . . . . . . . . . . . . . . 16
 

  |
160 | 48, 159, 88 | syl2anr 481 |
. . . . . . . . . . . . . . 15
             |
161 | 157, 158,
160 | expclzd 12428 |
. . . . . . . . . . . . . 14
                 |
162 | 156, 161 | mulcld 9668 |
. . . . . . . . . . . . 13
                       |
163 | 154, 162 | eqeltrd 2531 |
. . . . . . . . . . . 12
                             |
164 | 163 | an32s 814 |
. . . . . . . . . . 11
                             |
165 | 164 | adantlr 722 |
. . . . . . . . . 10
   
     

                    |
166 | 92 | recnd 9674 |
. . . . . . . . . . . . 13
   
     

        |
167 | 44, 166 | absmuld 13528 |
. . . . . . . . . . . 12
   
     

                                      |
168 | 92, 144 | absidd 13496 |
. . . . . . . . . . . . 13
   
     

                  |
169 | 168 | oveq2d 6311 |
. . . . . . . . . . . 12
   
     

                                      |
170 | 167, 169 | eqtrd 2487 |
. . . . . . . . . . 11
   
     

                                  |
171 | 153 | adantl 468 |
. . . . . . . . . . . 12
   
     

                                |
172 | 171 | fveq2d 5874 |
. . . . . . . . . . 11
   
     

                                        |
173 | 170, 172,
43 | 3eqtr4rd 2498 |
. . . . . . . . . 10
   
     

                                              |
174 | 1, 4, 149, 29, 165, 173 | climabs0 13661 |
. . . . . . . . 9
                                             |
175 | 147, 174 | mpbird 236 |
. . . . . . . 8
                         |
176 | 113 | adantr 467 |
. . . . . . . . . . 11
           |
177 | | simpr 463 |
. . . . . . . . . . 11
           |
178 | 176, 177 | ltned 9776 |
. . . . . . . . . 10
           |
179 | | elsn 3984 |
. . . . . . . . . . 11
     |
180 | 179 | necon3bbii 2673 |
. . . . . . . . . 10
     |
181 | 178, 180 | sylibr 216 |
. . . . . . . . 9
        
    |
182 | 181 | iffalsed 3894 |
. . . . . . . 8
                      |
183 | 175, 182 | breqtrrd 4432 |
. . . . . . 7
                                    |
184 | | nncn 10624 |
. . . . . . . . . . . . . . 15
   |
185 | 184 | ad2antlr 734 |
. . . . . . . . . . . . . 14
          

    
  |
186 | | nnne0 10649 |
. . . . . . . . . . . . . . 15
   |
187 | 186 | ad2antlr 734 |
. . . . . . . . . . . . . 14
          

       |
188 | 89 | ad3antrrr 737 |
. . . . . . . . . . . . . 14
          

         |
189 | 185, 187,
188 | expclzd 12428 |
. . . . . . . . . . . . 13
          

             |
190 | 189 | mul02d 9836 |
. . . . . . . . . . . 12
          

               |
191 | | simpr 463 |
. . . . . . . . . . . . 13
          

           |
192 | 191 | oveq1d 6310 |
. . . . . . . . . . . 12
          

                           |
193 | 191 | ifeq1d 3901 |
. . . . . . . . . . . . 13
          

                         |
194 | | ifid 3920 |
. . . . . . . . . . . . 13
    
   |
195 | 193, 194 | syl6eq 2503 |
. . . . . . . . . . . 12
          

                  |
196 | 190, 192,
195 | 3eqtr4d 2497 |
. . . . . . . . . . 11
          

                     
        |
197 | 21 | adantr 467 |
. . . . . . . . . . . . . 14
               |
198 | 197 | ad2antrr 733 |
. . . . . . . . . . . . 13
          

           |
199 | 198 | mulid1d 9665 |
. . . . . . . . . . . 12
          

                 |
200 | | nn0ssre 10880 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
201 | 52, 200 | syl6ss 3446 |
. . . . . . . . . . . . . . . . . . . . . . 23
            |
202 | 201 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . 22
                        |
203 | 56 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . 22
                        |
204 | 82 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . 22
                        
  |
205 | 19 | ad2antlr 734 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
206 | | ffvelrn 6025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                     |
207 | 17, 19, 206 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
               |
208 | 207 | anim1i 572 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                             |
209 | | eldifsn 4100 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
                |
210 | 208, 209 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           |
211 | | difun2 3849 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
212 | 210, 211 | syl6eleq 2541 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
213 | | elpreima 6007 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

                       |
214 | 66, 213 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
             |
215 | 214 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . 23
                      
             |
216 | 205, 212,
215 | mpbir2and 934 |
. . . . . . . . . . . . . . . . . . . . . 22
                        |
217 | | suprub 10577 |
. . . . . . . . . . . . . . . . . . . . . 22
           
         
          

         
               |
218 | 202, 203,
204, 216, 217 | syl31anc 1272 |
. . . . . . . . . . . . . . . . . . . . 21
                            |
219 | 218, 53 | syl6breqr 4446 |
. . . . . . . . . . . . . . . . . . . 20
               |
220 | 219 | adantlr 722 |
. . . . . . . . . . . . . . . . . . 19
   
     
    
  |
221 | 220 | adantlr 722 |
. . . . . . . . . . . . . . . . . 18
          

       |
222 | | simpllr 770 |
. . . . . . . . . . . . . . . . . 18
          

       |
223 | 113 | ad3antrrr 737 |
. . . . . . . . . . . . . . . . . . 19
          

       |
224 | 116 | ad3antrrr 737 |
. . . . . . . . . . . . . . . . . . 19
          

       |
225 | 223, 224 | letri3d 9782 |
. . . . . . . . . . . . . . . . . 18
          

     
     |
226 | 221, 222,
225 | mpbir2and 934 |
. . . . . . . . . . . . . . . . 17
          

       |
227 | 226 | oveq1d 6310 |
. . . . . . . . . . . . . . . 16
          

           |
228 | 122 | ad3antrrr 737 |
. . . . . . . . . . . . . . . . 17
          

       |
229 | 228 | subidd 9979 |
. . . . . . . . . . . . . . . 16
          

     
   |
230 | 227, 229 | eqtrd 2487 |
. . . . . . . . . . . . . . 15
          

         |
231 | 230 | oveq2d 6311 |
. . . . . . . . . . . . . 14
          

                 |
232 | 184 | ad2antlr 734 |
. . . . . . . . . . . . . . 15
          

       |
233 | 232 | exp0d 12417 |
. . . . . . . . . . . . . 14
          

           |
234 | 231, 233 | eqtrd 2487 |
. . . . . . . . . . . . 13
          

             |
235 | 234 | oveq2d 6311 |
. . . . . . . . . . . 12
          

                         |
236 | 226, 179 | sylibr 216 |
. . . . . . . . . . . . 13
          

         |
237 | 236 | iftrued 3891 |
. . . . . . . . . . . 12
          

                      |
238 | 199, 235,
237 | 3eqtr4d 2497 |
. . . . . . . . . . 11
          

                              |
239 | 196, 238 | pm2.61dane 2713 |
. . . . . . . . . 10
   
     

                         |
240 | 239 | mpteq2dva 4492 |
. . . . . . . . 9
                            
         |
241 | | fconstmpt 4881 |
. . . . . . . . 9
      
                      |
242 | 240, 241 | syl6eqr 2505 |
. . . . . . . 8
                             
          |
243 | | ifcl 3925 |
. . . . . . . . . 10
     
              |
244 | 197, 7, 243 | sylancl 669 |
. . . . . . . . 9
                      |
245 | | 1z 10974 |
. . . . . . . . 9
 |
246 | 1 | eqimss2i 3489 |
. . . . . . . . . 10
     |
247 | 246, 27 | climconst2 13624 |
. . . . . . . . 9
                    
            
        |
248 | 244, 245,
247 | sylancl 669 |
. . . . . . . 8
               
            
        |
249 | 242, 248 | eqbrtrd 4426 |
. . . . . . 7
                                    |
250 | 183, 249,
113, 116 | ltlecasei 9747 |
. . . . . 6
 
                                |
251 | | snex 4644 |
. . . . . . . 8
   |
252 | 27, 251 | xpex 6600 |
. . . . . . 7
     |
253 | 252 | a1i 11 |
. . . . . 6
       |
254 | 164 | anasss 653 |
. . . . . 6
 
    
                      |
255 | | plyeq0.5 |
. . . . . . . . . . . 12
                      |
256 | 255 | fveq1d 5872 |
. . . . . . . . . . 11
                              |
257 | 256 | adantr 467 |
. . . . . . . . . 10
 

                             |
258 | 132 | adantl 468 |
. . . . . . . . . . 11
 

  |
259 | | 0pval 22641 |
. . . . . . . . . . 11
        |
260 | 258, 259 | syl 17 |
. . . . . . . . . 10
 

       |
261 | | oveq1 6302 |
. . . . . . . . . . . . . 14
           |
262 | 261 | oveq2d 6311 |
. . . . . . . . . . . . 13
                       |
263 | 262 | sumeq2sdv 13782 |
. . . . . . . . . . . 12
                 
                 |
264 | | eqid 2453 |
. . . . . . . . . . . 12
                                     |
265 | | sumex 13766 |
. . . . . . . . . . . 12
                 |
266 | 263, 264,
265 | fvmpt 5953 |
. . . . . . . . . . 11
                                         |
267 | 258, 266 | syl 17 |
. . . . . . . . . 10
 

                                        |
268 | 257, 260,
267 | 3eqtr3d 2495 |
. . . . . . . . 9
 

                  |
269 | 268 | oveq1d 6310 |
. . . . . . . 8
 

                              |
270 | | expcl 12297 |
. . . . . . . . . 10
 
       |
271 | 132, 86, 270 | syl2anr 481 |
. . . . . . . . 9
 

      |
272 | 139 | adantl 468 |
. . . . . . . . . 10
 

  |
273 | 258, 272,
159 | expne0d 12429 |
. . . . . . . . 9
 

      |
274 | 271, 273 | div0d 10389 |
. . . . . . . 8
 

        |
275 | | fzfid 12193 |
. . . . . . . . 9
 

      |
276 | | expcl 12297 |
. . . . . . . . . . 11
 
       |
277 | 258, 19, 276 | syl2an 480 |
. . . . . . . . . 10
               |
278 | 156, 277 | mulcld 9668 |
. . . . . . . . 9
                     |
279 | 275, 271,
278, 273 | fsumdivc 13859 |
. . . . . . . 8
 

 
                                            |
280 | 269, 274,
279 | 3eqtr3d 2495 |
. . . . . . 7
 

                        |
281 | | fvconst2g 6123 |
. . . . . . . 8
 
           |
282 | 8, 281 | sylan 474 |
. . . . . . 7
 

          |
283 | 159 | adantr 467 |
. . . . . . . . . . 11
           |
284 | 48 | adantl 468 |
. . . . . . . . . . 11
           |
285 | 157, 158,
283, 284 | expsubd 12434 |
. . . . . . . . . 10
                           |
286 | 285 | oveq2d 6311 |
. . . . . . . . 9
                                       |
287 | 271 | adantr 467 |
. . . . . . . . . 10
               |
288 | 273 | adantr 467 |
. . . . . . . . . 10
               |
289 | 156, 277,
287, 288 | divassd 10425 |
. . . . . . . . 9
                                           |
290 | 286, 154,
289 | 3eqtr4d 2497 |
. . . . . . . 8
                                             |
291 | 290 | sumeq2dv 13781 |
. . . . . . 7
 

                                                |
292 | 280, 282,
291 | 3eqtr4d 2497 |
. . . . . 6
 

                                  |
293 | 1, 2, 3, 250, 253, 254, 292 | climfsum 13892 |
. . . . 5
                        |
294 | | suprleub 10580 |
. . . . . . . . . . . 12
           
         
          

              
          
   |
295 | 201, 56, 82, 58, 294 | syl31anc 1272 |
. . . . . . . . . . 11
                             |
296 | 78, 295 | mpbird 236 |
. . . . . . . . . 10
                |
297 | 53, 296 | syl5eqbr 4439 |
. . . . . . . . 9

  |
298 | | nn0uz 11200 |
. . . . . . . . . . 11
     |
299 | 86, 298 | syl6eleq 2541 |
. . . . . . . . . 10
       |
300 | 57 | nn0zd 11045 |
. . . . . . . . . 10
   |
301 | | elfz5 11799 |
. . . . . . . . . 10
       
   
   |
302 | 299, 300,
301 | syl2anc 667 |
. . . . . . . . 9
     
   |
303 | 297, 302 | mpbird 236 |
. . . . . . . 8
       |
304 | 303 | snssd 4120 |
. . . . . . 7
         |
305 | 18, 86 | ffvelrnd 6028 |
. . . . . . . . 9
       |
306 | | elsni 3995 |
. . . . . . . . . . 11
     |
307 | 306 | fveq2d 5874 |
. . . . . . . . . 10
             |
308 | 307 | eleq1d 2515 |
. . . . . . . . 9
               |
309 | 305, 308 | syl5ibrcom 226 |
. . . . . . . 8
   
       |
310 | 309 | ralrimiv 2802 |
. . . . . . 7
   
      |
311 | 3 | olcd 395 |
. . . . . . 7
                 |
312 | | sumss2 13804 |
. . . . . . 7
        
            
                 
                  |
313 | 304, 310,
311, 312 | syl21anc 1268 |
. . . . . 6
   
    
                  |
314 | | ltso 9719 |
. . . . . . . . 9
 |
315 | 314 | supex 7982 |
. . . . . . . 8
              |
316 | 53, 315 | eqeltri 2527 |
. . . . . . 7
 |
317 | | fveq2 5870 |
. . . . . . . 8
           |
318 | 317 | sumsn 13819 |
. . . . . . 7
                    |
319 | 316, 305,
318 | sylancr 670 |
. . . . . 6
   
          |
320 | 313, 319 | eqtr3d 2489 |
. . . . 5
                        |
321 | 293, 320 | breqtrd 4430 |
. . . 4
           |
322 | 246, 27 | climconst2 13624 |
. . . . 5
 
       |
323 | 7, 245, 322 | mp2an 679 |
. . . 4
     |
324 | | climuni 13628 |
. . . 4
          
          |
325 | 321, 323,
324 | sylancl 669 |
. . 3
       |
326 | | fvex 5880 |
. . . 4
     |
327 | 326 | elsnc 3994 |
. . 3
             |
328 | 325, 327 | sylibr 216 |
. 2
         |
329 | | elpreima 6007 |
. . . . . 6

                       |
330 | 66, 329 | syl 17 |
. . . . 5
          
             |
331 | 85, 330 | mpbid 214 |
. . . 4
             |
332 | 331 | simprd 465 |
. . 3
           |
333 | 332 | eldifbd 3419 |
. 2
         |
334 | 328, 333 | pm2.65i 177 |
1
 |