Step | Hyp | Ref
| Expression |
1 | | reelprrecn 9631 |
. . . 4
    |
2 | 1 | a1i 11 |
. . 3
      |
3 | | reopn 37502 |
. . . . 5
     |
4 | | eqid 2451 |
. . . . . 6
  ℂfld   ℂfld |
5 | 4 | tgioo2 21821 |
. . . . 5
       ℂfld
↾t   |
6 | 3, 5 | eleqtri 2527 |
. . . 4
   ℂfld
↾t   |
7 | 6 | a1i 11 |
. . 3
    ℂfld ↾t    |
8 | | etransclem35.p |
. . 3
   |
9 | | etransclem35.m |
. . 3
   |
10 | | etransclem35.f |
. . 3
                       |
11 | | nnm1nn0 10911 |
. . . 4
 
   |
12 | 8, 11 | syl 17 |
. . 3
     |
13 | | etransclem5 38104 |
. . 3
                                           |
14 | | etransclem35.c |
. . 3
      
                  |
15 | | 0red 9644 |
. . 3
   |
16 | 2, 7, 8, 9, 10, 12, 13, 14, 15 | etransclem31 38130 |
. 2
               
            
                                                               
                                                |
17 | | nfv 1761 |
. . 3
   |
18 | | nfcv 2592 |
. . 3
                                         
      
                                             
                        |
19 | 14, 12 | etransclem16 38115 |
. . 3
    
    |
20 | | simpr 463 |
. . . . . . . . . . . . 13
 
      
        |
21 | 14, 12 | etransclem12 38111 |
. . . . . . . . . . . . . 14
    
               
              |
22 | 21 | adantr 467 |
. . . . . . . . . . . . 13
 
      
                                  |
23 | 20, 22 | eleqtrd 2531 |
. . . . . . . . . . . 12
 
      
                            |
24 | | rabid 2967 |
. . . . . . . . . . . 12
                                
                      |
25 | 23, 24 | sylib 200 |
. . . . . . . . . . 11
 
      
                            |
26 | 25 | simprd 465 |
. . . . . . . . . 10
 
      
              |
27 | 26 | eqcomd 2457 |
. . . . . . . . 9
 
      
              |
28 | 27 | fveq2d 5869 |
. . . . . . . 8
 
      
                      |
29 | 28 | oveq1d 6305 |
. . . . . . 7
 
      
                          
                           |
30 | | nfcv 2592 |
. . . . . . . 8
   |
31 | | fzfid 12186 |
. . . . . . . 8
 
      
      |
32 | | nn0ex 10875 |
. . . . . . . . . 10
 |
33 | | fzssnn0 37539 |
. . . . . . . . . 10
       |
34 | | mapss 7514 |
. . . . . . . . . 10
     
 
                     |
35 | 32, 33, 34 | mp2an 678 |
. . . . . . . . 9
                   |
36 | 25 | simpld 461 |
. . . . . . . . 9
 
      
              |
37 | 35, 36 | sseldi 3430 |
. . . . . . . 8
 
      
        |
38 | 30, 31, 37 | mccl 37678 |
. . . . . . 7
 
      
                                |
39 | 29, 38 | eqeltrd 2529 |
. . . . . 6
 
      
                        |
40 | 39 | nnzd 11039 |
. . . . 5
 
      
                        |
41 | 8 | adantr 467 |
. . . . . . 7
 
      
  |
42 | 9 | adantr 467 |
. . . . . . 7
 
      
  |
43 | | elmapi 7493 |
. . . . . . . 8
                             |
44 | 36, 43 | syl 17 |
. . . . . . 7
 
      
                |
45 | | 0zd 10949 |
. . . . . . 7
 
      
  |
46 | 41, 42, 44, 45 | etransclem10 38109 |
. . . . . 6
 
      
               
                               |
47 | | fzfid 12186 |
. . . . . . 7
 
      
      |
48 | 8 | ad2antrr 732 |
. . . . . . . 8
      
          |
49 | 44 | adantr 467 |
. . . . . . . 8
      
                        |
50 | | fz1ssfz0 37528 |
. . . . . . . . . 10
         |
51 | 50 | sseli 3428 |
. . . . . . . . 9
           |
52 | 51 | adantl 468 |
. . . . . . . 8
      
              |
53 | | 0zd 10949 |
. . . . . . . 8
      
          |
54 | 48, 49, 52, 53 | etransclem3 38102 |
. . . . . . 7
      
         
                                       |
55 | 47, 54 | fprodzcl 14008 |
. . . . . 6
 
      
                       
            
          |
56 | 46, 55 | zmulcld 11046 |
. . . . 5
 
      
                
      
                                             
            
           |
57 | 40, 56 | zmulcld 11046 |
. . . 4
 
      
     
                                                               
                                                |
58 | 57 | zcnd 11041 |
. . 3
 
      
     
                                                               
                                                |
59 | | nn0uz 11193 |
. . . . . . . . . . 11
     |
60 | 12, 59 | syl6eleq 2539 |
. . . . . . . . . 10
         |
61 | | eluzfz2 11807 |
. . . . . . . . . 10
      
     
    |
62 | 60, 61 | syl 17 |
. . . . . . . . 9
           |
63 | | eluzfz1 11806 |
. . . . . . . . . 10
      
   
    |
64 | 60, 63 | syl 17 |
. . . . . . . . 9
         |
65 | 62, 64 | ifcld 3924 |
. . . . . . . 8
                |
66 | 65 | adantr 467 |
. . . . . . 7
 
                    |
67 | | etransclem35.d |
. . . . . . 7
              |
68 | 66, 67 | fmptd 6046 |
. . . . . 6
                 |
69 | | ovex 6318 |
. . . . . . 7
       |
70 | | ovex 6318 |
. . . . . . 7
     |
71 | 69, 70 | elmap 7500 |
. . . . . 6
            
                |
72 | 68, 71 | sylibr 216 |
. . . . 5
               |
73 | 9, 59 | syl6eleq 2539 |
. . . . . . 7
       |
74 | | fzsscn 37531 |
. . . . . . . 8
       |
75 | 68 | ffvelrnda 6022 |
. . . . . . . 8
 
            
    |
76 | 74, 75 | sseldi 3430 |
. . . . . . 7
 
           |
77 | | fveq2 5865 |
. . . . . . 7
           |
78 | 73, 76, 77 | fsum1p 13814 |
. . . . . 6
                               |
79 | 67 | a1i 11 |
. . . . . . . 8
                |
80 | | simpr 463 |
. . . . . . . . 9
 
   |
81 | 80 | iftrued 3889 |
. . . . . . . 8
 
            |
82 | | eluzfz1 11806 |
. . . . . . . . 9
    
      |
83 | 73, 82 | syl 17 |
. . . . . . . 8
       |
84 | 79, 81, 83, 12 | fvmptd 5954 |
. . . . . . 7
         |
85 | | 0p1e1 10721 |
. . . . . . . . . . 11
   |
86 | 85 | oveq1i 6300 |
. . . . . . . . . 10
           |
87 | 86 | sumeq1i 13764 |
. . . . . . . . 9
            
          |
88 | 87 | a1i 11 |
. . . . . . . 8
                         |
89 | 67 | fvmpt2 5957 |
. . . . . . . . . . 11
                                 |
90 | 51, 65, 89 | syl2anr 481 |
. . . . . . . . . 10
 
                  |
91 | | 0red 9644 |
. . . . . . . . . . . . . 14
       |
92 | | 1red 9658 |
. . . . . . . . . . . . . . 15
       |
93 | | elfzelz 11800 |
. . . . . . . . . . . . . . . 16
       |
94 | 93 | zred 11040 |
. . . . . . . . . . . . . . 15
       |
95 | | 0lt1 10136 |
. . . . . . . . . . . . . . . 16
 |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . . 15
       |
97 | | elfzle1 11802 |
. . . . . . . . . . . . . . 15
       |
98 | 91, 92, 94, 96, 97 | ltletrd 9795 |
. . . . . . . . . . . . . 14
       |
99 | 91, 98 | gtned 9770 |
. . . . . . . . . . . . 13
       |
100 | 99 | neneqd 2629 |
. . . . . . . . . . . 12
    
  |
101 | 100 | iffalsed 3892 |
. . . . . . . . . . 11
              |
102 | 101 | adantl 468 |
. . . . . . . . . 10
 
              |
103 | 90, 102 | eqtrd 2485 |
. . . . . . . . 9
 
           |
104 | 103 | sumeq2dv 13769 |
. . . . . . . 8
                   |
105 | | fzfi 12185 |
. . . . . . . . . 10
     |
106 | 105 | olci 393 |
. . . . . . . . 9
               |
107 | | sumz 13788 |
. . . . . . . . 9
     
                 |
108 | 106, 107 | mp1i 13 |
. . . . . . . 8
         |
109 | 88, 104, 108 | 3eqtrd 2489 |
. . . . . . 7
               |
110 | 84, 109 | oveq12d 6308 |
. . . . . 6
      
                  |
111 | 8 | nncnd 10625 |
. . . . . . . 8
   |
112 | | 1cnd 9659 |
. . . . . . . 8
   |
113 | 111, 112 | subcld 9986 |
. . . . . . 7
     |
114 | 113 | addid1d 9833 |
. . . . . 6
         |
115 | 78, 110, 114 | 3eqtrd 2489 |
. . . . 5
               |
116 | | fveq1 5864 |
. . . . . . . 8
           |
117 | 116 | sumeq2ad 37644 |
. . . . . . 7
           
           |
118 | 117 | eqeq1d 2453 |
. . . . . 6
             
               |
119 | 118 | elrab 3196 |
. . . . 5
                                
                      |
120 | 72, 115, 119 | sylanbrc 670 |
. . . 4
              
              |
121 | 120, 21 | eleqtrrd 2532 |
. . 3
         |
122 | 116 | fveq2d 5869 |
. . . . . 6
                   |
123 | 122 | prodeq2ad 37672 |
. . . . 5
               
               |
124 | 123 | oveq2d 6306 |
. . . 4
     
                     
                   |
125 | | fveq1 5864 |
. . . . . . 7
           |
126 | 125 | breq2d 4414 |
. . . . . 6
       
         |
127 | 125 | oveq2d 6306 |
. . . . . . . . 9
                   |
128 | 127 | fveq2d 5869 |
. . . . . . . 8
     
                     |
129 | 128 | oveq2d 6306 |
. . . . . . 7
     
                                     |
130 | 127 | oveq2d 6306 |
. . . . . . 7
                           |
131 | 129, 130 | oveq12d 6308 |
. . . . . 6
      
      
                                                         |
132 | 126, 131 | ifbieq2d 3906 |
. . . . 5
                
      
                                     
                               |
133 | 116 | breq2d 4414 |
. . . . . . 7
     
       |
134 | 116 | oveq2d 6306 |
. . . . . . . . . 10
 
             |
135 | 134 | fveq2d 5869 |
. . . . . . . . 9
              
        |
136 | 135 | oveq2d 6306 |
. . . . . . . 8
                         
         |
137 | 134 | oveq2d 6306 |
. . . . . . . 8
                           |
138 | 136, 137 | oveq12d 6308 |
. . . . . . 7
                                        
            
         |
139 | 133, 138 | ifbieq2d 3906 |
. . . . . 6
  
                                                      
            
          |
140 | 139 | prodeq2ad 37672 |
. . . . 5
                                                                     
                       |
141 | 132, 140 | oveq12d 6308 |
. . . 4
                 
      
                                             
            
                                                       
                                               |
142 | 124, 141 | oveq12d 6308 |
. . 3
      
                                 
                                                    
                                                              
      
                                             
                         |
143 | 17, 18, 19, 58, 121, 142 | fsumsplit1 37651 |
. 2
                                                
      
                                             
            
                
                                 
      
                                             
                       
                                                  
      
                                             
            
             |
144 | 33, 75 | sseldi 3430 |
. . . . . . . . . . . 12
 
           |
145 | 144 | faccld 37533 |
. . . . . . . . . . 11
 
               |
146 | 145 | nncnd 10625 |
. . . . . . . . . 10
 
               |
147 | 77 | fveq2d 5869 |
. . . . . . . . . 10
                   |
148 | 73, 146, 147 | fprod1p 14022 |
. . . . . . . . 9
                                           |
149 | 84 | fveq2d 5869 |
. . . . . . . . . 10
                 |
150 | 86 | prodeq1i 13972 |
. . . . . . . . . . . 12
                               |
151 | 150 | a1i 11 |
. . . . . . . . . . 11
                                 |
152 | 103 | fveq2d 5869 |
. . . . . . . . . . . . 13
 
                   |
153 | | fac0 12462 |
. . . . . . . . . . . . 13
     |
154 | 152, 153 | syl6eq 2501 |
. . . . . . . . . . . 12
 
               |
155 | 154 | prodeq2dv 13977 |
. . . . . . . . . . 11
                       |
156 | | prod1 13998 |
. . . . . . . . . . . 12
     
                 |
157 | 106, 156 | mp1i 13 |
. . . . . . . . . . 11
         |
158 | 151, 155,
157 | 3eqtrd 2489 |
. . . . . . . . . 10
                   |
159 | 149, 158 | oveq12d 6308 |
. . . . . . . . 9
                               
     |
160 | 12 | faccld 37533 |
. . . . . . . . . . 11
    
    |
161 | 160 | nncnd 10625 |
. . . . . . . . . 10
    
    |
162 | 161 | mulid1d 9660 |
. . . . . . . . 9
     
           |
163 | 148, 159,
162 | 3eqtrd 2489 |
. . . . . . . 8
                       |
164 | 163 | oveq2d 6306 |
. . . . . . 7
     
                           
     |
165 | 160 | nnne0d 10654 |
. . . . . . . 8
    
    |
166 | 161, 165 | dividd 10381 |
. . . . . . 7
     
           |
167 | 164, 166 | eqtrd 2485 |
. . . . . 6
     
                   |
168 | 12 | nn0red 10926 |
. . . . . . . . . . . . 13
     |
169 | 84, 168 | eqeltrd 2529 |
. . . . . . . . . . . 12
       |
170 | 169, 168 | lttri3d 9775 |
. . . . . . . . . . 11
               
         |
171 | 84, 170 | mpbid 214 |
. . . . . . . . . 10
        
        |
172 | 171 | simprd 465 |
. . . . . . . . 9
         |
173 | 172 | iffalsed 3892 |
. . . . . . . 8
                                                   
      
                       |
174 | 84 | eqcomd 2457 |
. . . . . . . . . . . . . 14
         |
175 | 113, 174 | subeq0bd 10045 |
. . . . . . . . . . . . 13
           |
176 | 175 | fveq2d 5869 |
. . . . . . . . . . . 12
                   |
177 | 176, 153 | syl6eq 2501 |
. . . . . . . . . . 11
               |
178 | 177 | oveq2d 6306 |
. . . . . . . . . 10
     
      
                  |
179 | 161 | div1d 10375 |
. . . . . . . . . 10
     
           |
180 | 178, 179 | eqtrd 2485 |
. . . . . . . . 9
     
      
                |
181 | 175 | oveq2d 6306 |
. . . . . . . . . 10
                   |
182 | | 0cnd 9636 |
. . . . . . . . . . 11
   |
183 | 182 | exp0d 12410 |
. . . . . . . . . 10
       |
184 | 181, 183 | eqtrd 2485 |
. . . . . . . . 9
               |
185 | 180, 184 | oveq12d 6308 |
. . . . . . . 8
                                             |
186 | 173, 185,
162 | 3eqtrd 2489 |
. . . . . . 7
                                                      |
187 | | fzssre 37535 |
. . . . . . . . . . . 12
       |
188 | 68 | adantr 467 |
. . . . . . . . . . . . 13
 
                     |
189 | 51 | adantl 468 |
. . . . . . . . . . . . 13
 
           |
190 | 188, 189 | ffvelrnd 6023 |
. . . . . . . . . . . 12
 
            
    |
191 | 187, 190 | sseldi 3430 |
. . . . . . . . . . 11
 
           |
192 | 8 | nnred 10624 |
. . . . . . . . . . . 12
   |
193 | 192 | adantr 467 |
. . . . . . . . . . 11
 
       |
194 | 8 | nngt0d 10653 |
. . . . . . . . . . . . . 14
   |
195 | 15, 192, 194 | ltled 9783 |
. . . . . . . . . . . . 13

  |
196 | 195 | adantr 467 |
. . . . . . . . . . . 12
 
       |
197 | 103, 196 | eqbrtrd 4423 |
. . . . . . . . . . 11
 
           |
198 | 191, 193,
197 | lensymd 9786 |
. . . . . . . . . 10
 
           |
199 | 198 | iffalsed 3892 |
. . . . . . . . 9
 
      
                            
                                        |
200 | 103 | oveq2d 6306 |
. . . . . . . . . . . . . 14
 
     
         |
201 | 111 | adantr 467 |
. . . . . . . . . . . . . . 15
 
       |
202 | 201 | subid1d 9975 |
. . . . . . . . . . . . . 14
 
     
   |
203 | 200, 202 | eqtrd 2485 |
. . . . . . . . . . . . 13
 
     
       |
204 | 203 | fveq2d 5869 |
. . . . . . . . . . . 12
 
                     |
205 | 204 | oveq2d 6306 |
. . . . . . . . . . 11
 
                                 |
206 | 8 | nnnn0d 10925 |
. . . . . . . . . . . . . . 15
   |
207 | 206 | faccld 37533 |
. . . . . . . . . . . . . 14
       |
208 | 207 | nncnd 10625 |
. . . . . . . . . . . . 13
       |
209 | 207 | nnne0d 10654 |
. . . . . . . . . . . . 13
       |
210 | 208, 209 | dividd 10381 |
. . . . . . . . . . . 12
             |
211 | 210 | adantr 467 |
. . . . . . . . . . 11
 
                 |
212 | 205, 211 | eqtrd 2485 |
. . . . . . . . . 10
 
                       |
213 | | df-neg 9863 |
. . . . . . . . . . . . 13
    |
214 | 213 | eqcomi 2460 |
. . . . . . . . . . . 12
    |
215 | 214 | a1i 11 |
. . . . . . . . . . 11
 
          |
216 | 215, 203 | oveq12d 6308 |
. . . . . . . . . 10
 
                        |
217 | 212, 216 | oveq12d 6308 |
. . . . . . . . 9
 
                                            |
218 | 93 | znegcld 11042 |
. . . . . . . . . . . . 13
        |
219 | 218 | zcnd 11041 |
. . . . . . . . . . . 12
        |
220 | 219 | adantl 468 |
. . . . . . . . . . 11
 
        |
221 | 206 | adantr 467 |
. . . . . . . . . . 11
 
       |
222 | 220, 221 | expcld 12416 |
. . . . . . . . . 10
 
            |
223 | 222 | mulid2d 9661 |
. . . . . . . . 9
 
                   |
224 | 199, 217,
223 | 3eqtrd 2489 |
. . . . . . . 8
 
      
                            
               |
225 | 224 | prodeq2dv 13977 |
. . . . . . 7
                        
                                  |
226 | 186, 225 | oveq12d 6308 |
. . . . . 6
                                               
                                                                  |
227 | 167, 226 | oveq12d 6308 |
. . . . 5
                                        
      
                                             
                                              |
228 | | fzfid 12186 |
. . . . . . . . 9
       |
229 | | zexpcl 12287 |
. . . . . . . . . 10
           |
230 | 218, 206,
229 | syl2anr 481 |
. . . . . . . . 9
 
            |
231 | 228, 230 | fprodzcl 14008 |
. . . . . . . 8
              |
232 | 231 | zcnd 11041 |
. . . . . . 7
              |
233 | 161, 232 | mulcld 9663 |
. . . . . 6
     
                |
234 | 233 | mulid2d 9661 |
. . . . 5
      
                      
             |
235 | 227, 234 | eqtrd 2485 |
. . . 4
                                        
      
                                             
                           
                |
236 | | eldifi 3555 |
. . . . . . . . . . . . . . 15
                   |
237 | 83 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
      
      |
238 | 44, 237 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
 
      
       
    |
239 | 236, 238 | sylan2 477 |
. . . . . . . . . . . . . 14
 
    
                  |
240 | 187, 239 | sseldi 3430 |
. . . . . . . . . . . . 13
 
    
            |
241 | 168 | adantr 467 |
. . . . . . . . . . . . 13
 
    
          |
242 | | elfzle2 11803 |
. . . . . . . . . . . . . 14
                   |
243 | 239, 242 | syl 17 |
. . . . . . . . . . . . 13
 
    
         
    |
244 | 240, 241,
243 | lensymd 9786 |
. . . . . . . . . . . 12
 
    
              |
245 | 244 | iffalsed 3892 |
. . . . . . . . . . 11
 
    
                     
      
                           
                              |
246 | 12 | nn0zd 11038 |
. . . . . . . . . . . . . . . 16
     |
247 | 246 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
          |
248 | 239 | elfzelzd 37536 |
. . . . . . . . . . . . . . 15
 
    
            |
249 | 247, 248 | zsubcld 11045 |
. . . . . . . . . . . . . 14
 
    
                |
250 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . . 22
                     |
251 | 44, 250 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
      |
252 | 251 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
      
   
            |
253 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . . 22
              
      |
254 | 68, 253 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
       |
255 | 254 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
      
   
     
      |
256 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
257 | 256 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
     
           |
258 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
       |
259 | 258 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
260 | 259 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
     
         |
261 | 77 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
           |
262 | 84 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
         |
263 | 261, 262 | eqtr2d 2486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 
       |
264 | 263 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
     
         |
265 | 257, 260,
264 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
     
           |
266 | 265 | adantllr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       
      
          |
267 | 266 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . . 21
                                   |
268 | 26 | ad4antr 738 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                  
                    |
269 | 168 | ad5antr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
                  
      
   |
270 | 168 | ad4antr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                           |
271 | 44 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      
                        |
272 | 50 | sseli 3428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           |
273 | 272 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      
              |
274 | 271, 273 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
               
    |
275 | 33, 274 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      
              |
276 | 47, 275 | fsumnn0cl 13802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
      
            |
277 | 276 | nn0red 10926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
      
            |
278 | 277 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                                   |
279 | | 0red 9644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                         |
280 | 44 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
               
    |
281 | 187, 280 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      
              |
282 | 281 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                             |
283 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
           
       |
284 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
285 | | fzfid 12186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                             |
286 | | simp-4l 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
           
                     |
287 | 74, 274 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      
              |
288 | 286, 287 | sylancom 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
           
                 |
289 | | 1zzd 10968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     

  |
290 | | elfzel2 11798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
       |
291 | 290 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     

  |
292 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
       |
293 | 292 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     

  |
294 | 289, 291,
293 | 3jca 1188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
     

    |
295 | | elfznn0 11887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
       |
296 | 295 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     

  |
297 | | neqne 37374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   |
298 | 297 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     

  |
299 | | elnnne0 10883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40

    |
300 | 296, 298,
299 | sylanbrc 670 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     

  |
301 | 300 | nnge1d 10652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
     

  |
302 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       |
303 | 302 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
     

  |
304 | 294, 301,
303 | jca32 538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     

 
 
    |
305 | | elfz2 11791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
 
 
    |
306 | 304, 305 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     

      |
307 | 306 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                   |
308 | 307 | adantlll 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                             |
309 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           |
310 | 283, 284,
285, 288, 308, 309 | fsumsplit1 37651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                           
           |
311 | 310 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                 
                     |
312 | 311, 278 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                 
           |
313 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 |
314 | 280, 313 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
              |
315 | 314 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                             |
316 | | neqne 37374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           |
317 | 316 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                             |
318 | 279, 282,
315, 317 | leneltd 9789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                             |
319 | | diffi 7803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
         
     |
320 | 105, 319 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
      
          |
321 | | eldifi 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
               |
322 | 321 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
      
                  |
323 | 50, 322 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
      
                  |
324 | 44 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
      
               
    |
325 | 187, 324 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
      
              |
326 | 323, 325 | syldan 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      
                  |
327 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                 |
328 | 324, 327 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
      
              |
329 | 323, 328 | syldan 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      
                  |
330 | 320, 326,
329 | fsumge0 13855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
      
                |
331 | 330 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
             
          |
332 | 320, 326 | fsumrecl 13800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
      
                |
333 | 332 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      
                        |
334 | 281, 333 | addge01d 10201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
        
                 
          
            |
335 | 331, 334 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      
                 
                |
336 | 335 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                                 |
337 | 279, 282,
312, 318, 336 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                             |
338 | 337, 311 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                       
           |
339 | 278, 338 | elrpd 11338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                   |
340 | 270, 339 | ltaddrpd 11371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                         |
341 | 340 | adantlllr 37361 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                  
      
                 |
342 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
343 | 342 | cbvsumv 13762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          
          |
344 | 343 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                  
                
           |
345 | 73 | ad5antr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                  
            |
346 | | simp-5l 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
   
     
               
          |
347 | 74, 324 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
              |
348 | 346, 347 | sylancom 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          
   
     
               
      |
349 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
350 | 345, 348,
349 | fsum1p 13814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                  
                                    |
351 | 259 | ad4antlr 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                  
              |
352 | 86 | sumeq1i 13764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            
          |
353 | 352 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                  
                  
           |
354 | 351, 353 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                  
                           
            |
355 | 344, 350,
354 | 3eqtrrd 2490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                  
                                |
356 | 341, 355 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
                  
      
             |
357 | 269, 356 | gtned 9770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                  
                
   |
358 | 357 | neneqd 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                  
                    |
359 | 268, 358 | condan 803 |
. . . . . . . . . . . . . . . . . . . . . 22
                       
       |
360 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
           |
361 | 33, 66 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
              |
362 | 67 | fvmpt2 5957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                           |
363 | 360, 361,
362 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                  |
364 | 363 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
              |
365 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       

  |
366 | 365 | iffalsed 3892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
          |
367 | 364, 366 | eqtr2d 2486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
       |
368 | 367 | adantllr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      
            |
369 | 368 | adantllr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
                       
       |
370 | 359, 369 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . . 21
                       
           |
371 | 267, 370 | pm2.61dan 800 |
. . . . . . . . . . . . . . . . . . . 20
   
       
          
          |
372 | 252, 255,
371 | eqfnfvd 5979 |
. . . . . . . . . . . . . . . . . . 19
      
   
        |
373 | 236, 372 | sylanl2 657 |
. . . . . . . . . . . . . . . . . 18
       
      
        |
374 | | eldifsni 4098 |
. . . . . . . . . . . . . . . . . . . 20
             |
375 | 374 | neneqd 2629 |
. . . . . . . . . . . . . . . . . . 19
          
  |
376 | 375 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . 18
       
 |