Step | Hyp | Ref
| Expression |
1 | | imasdsf1o.u |
. . . 4
  s    |
2 | | imasdsf1o.v |
. . . 4
       |
3 | | imasdsf1o.f |
. . . . 5
       |
4 | | f1ofo 5835 |
. . . . 5
    
      |
5 | 3, 4 | syl 17 |
. . . 4
       |
6 | | imasdsf1o.r |
. . . 4
   |
7 | | eqid 2471 |
. . . 4
         |
8 | | imasdsf1o.d |
. . . 4
     |
9 | | f1of 5828 |
. . . . . 6
    
      |
10 | 3, 9 | syl 17 |
. . . . 5
       |
11 | | imasdsf1o.x |
. . . . 5
   |
12 | 10, 11 | ffvelrnd 6038 |
. . . 4
       |
13 | | imasdsf1o.y |
. . . . 5
   |
14 | 10, 13 | ffvelrnd 6038 |
. . . 4
       |
15 | | imasdsf1o.s |
. . . 4
   
                                                                           |
16 | | imasdsf1o.e |
. . . 4
         |
17 | 1, 2, 5, 6, 7, 8, 12, 14, 15, 16 | imasdsval2 15495 |
. . 3
             inf 
   g         |
18 | | imasdsf1o.t |
. . . 4
    g      |
19 | 18 | infeq1i 8012 |
. . 3
inf   inf     g      
 |
20 | 17, 19 | syl6eqr 2523 |
. 2
             inf     |
21 | | xrsbas 19061 |
. . . . . . . . . . . 12
      |
22 | | xrsadd 19062 |
. . . . . . . . . . . 12
      |
23 | | imasdsf1o.w |
. . . . . . . . . . . 12
  ↾s      |
24 | | xrsex 19060 |
. . . . . . . . . . . . 13
  |
25 | 24 | a1i 11 |
. . . . . . . . . . . 12
        |
26 | | fzfid 12224 |
. . . . . . . . . . . 12
           |
27 | | difss 3549 |
. . . . . . . . . . . . 13
    |
28 | 27 | a1i 11 |
. . . . . . . . . . . 12
       
  |
29 | | imasdsf1o.m |
. . . . . . . . . . . . . . . 16
        |
30 | | xmetf 21422 |
. . . . . . . . . . . . . . . 16
              |
31 | | ffn 5739 |
. . . . . . . . . . . . . . . 16
           |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . . 15
     |
33 | | xmetcl 21424 |
. . . . . . . . . . . . . . . . . . 19
      

      |
34 | | xmetge0 21437 |
. . . . . . . . . . . . . . . . . . . 20
      

      |
35 | | ge0nemnf 11491 |
. . . . . . . . . . . . . . . . . . . 20
                 |
36 | 33, 34, 35 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
      

      |
37 | | eldifsn 4088 |
. . . . . . . . . . . . . . . . . . 19
       
    
       |
38 | 33, 36, 37 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . 18
      

    
    |
39 | 38 | 3expb 1232 |
. . . . . . . . . . . . . . . . 17
                   |
40 | 29, 39 | sylan 479 |
. . . . . . . . . . . . . . . 16
 

           |
41 | 40 | ralrimivva 2814 |
. . . . . . . . . . . . . . 15
  
         |
42 | | ffnov 6419 |
. . . . . . . . . . . . . . 15
              
          |
43 | 32, 41, 42 | sylanbrc 677 |
. . . . . . . . . . . . . 14
       
    |
44 | 43 | ad2antrr 740 |
. . . . . . . . . . . . 13
                |
45 | | ssrab2 3500 |
. . . . . . . . . . . . . . . . 17
                                                                                
      |
46 | 15, 45 | eqsstri 3448 |
. . . . . . . . . . . . . . . 16
         |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . 15
 

          |
48 | 47 | sselda 3418 |
. . . . . . . . . . . . . 14
               |
49 | | elmapi 7511 |
. . . . . . . . . . . . . 14
                     |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
                 |
51 | | fco 5751 |
. . . . . . . . . . . . 13
        
 
                     
    |
52 | 44, 50, 51 | syl2anc 673 |
. . . . . . . . . . . 12
     
              |
53 | | 0re 9661 |
. . . . . . . . . . . . 13
 |
54 | | rexr 9704 |
. . . . . . . . . . . . . 14
   |
55 | | renemnf 9707 |
. . . . . . . . . . . . . 14
   |
56 | | eldifsn 4088 |
. . . . . . . . . . . . . 14
   

   |
57 | 54, 55, 56 | sylanbrc 677 |
. . . . . . . . . . . . 13
 
    |
58 | 53, 57 | mp1i 13 |
. . . . . . . . . . . 12
     
    |
59 | | xaddid2 11557 |
. . . . . . . . . . . . . 14

       |
60 | | xaddid1 11556 |
. . . . . . . . . . . . . 14

       |
61 | 59, 60 | jca 541 |
. . . . . . . . . . . . 13

              |
62 | 61 | adantl 473 |
. . . . . . . . . . . 12
   



              |
63 | 21, 22, 23, 25, 26, 28, 52, 58, 62 | gsumress 16597 |
. . . . . . . . . . 11
      
g     g      |
64 | 23, 21 | ressbas2 15258 |
. . . . . . . . . . . . 13
 
 
         |
65 | 27, 64 | ax-mp 5 |
. . . . . . . . . . . 12
        |
66 | 23 | xrs10 19084 |
. . . . . . . . . . . 12
     |
67 | 23 | xrs1cmn 19085 |
. . . . . . . . . . . . 13
CMnd |
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
     CMnd |
69 | | c0ex 9655 |
. . . . . . . . . . . . . 14
 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
       |
71 | 52, 26, 70 | fdmfifsupp 7911 |
. . . . . . . . . . . 12
     
 finSupp   |
72 | 65, 66, 68, 26, 52, 71 | gsumcl 17627 |
. . . . . . . . . . 11
      g    
    |
73 | 63, 72 | eqeltrd 2549 |
. . . . . . . . . 10
      
g    
    |
74 | 73 | eldifad 3402 |
. . . . . . . . 9
      
g      |
75 | | eqid 2471 |
. . . . . . . . 9
   g        g      |
76 | 74, 75 | fmptd 6061 |
. . . . . . . 8
 

   g           |
77 | | frn 5747 |
. . . . . . . 8
    g        
   g       |
78 | 76, 77 | syl 17 |
. . . . . . 7
 

   g       |
79 | 78 | ralrimiva 2809 |
. . . . . 6
     g    
  |
80 | | iunss 4310 |
. . . . . 6
 
   g    
    g       |
81 | 79, 80 | sylibr 217 |
. . . . 5
     g    
  |
82 | 18, 81 | syl5eqss 3462 |
. . . 4

  |
83 | | infxrcl 11644 |
. . . 4

inf     |
84 | 82, 83 | syl 17 |
. . 3
 inf     |
85 | | xmetcl 21424 |
. . . 4
      

      |
86 | 29, 11, 13, 85 | syl3anc 1292 |
. . 3
       |
87 | | 1nn 10642 |
. . . . . . 7
 |
88 | | 1ex 9656 |
. . . . . . . . . . . 12
 |
89 | | opex 4664 |
. . . . . . . . . . . 12
    |
90 | 88, 89 | f1osn 5866 |
. . . . . . . . . . 11
  
                 |
91 | | f1of 5828 |
. . . . . . . . . . 11
                   
                     |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . 10
  
                 |
93 | | opelxpi 4871 |
. . . . . . . . . . . 12
 
        |
94 | 11, 13, 93 | syl2anc 673 |
. . . . . . . . . . 11
        |
95 | 94 | snssd 4108 |
. . . . . . . . . 10
     
    |
96 | | fss 5749 |
. . . . . . . . . 10
                                               |
97 | 92, 95, 96 | sylancr 676 |
. . . . . . . . 9
                   |
98 | 29 | elfvexd 5907 |
. . . . . . . . . . 11
   |
99 | | xpexg 6612 |
. . . . . . . . . . 11
 
     |
100 | 98, 98, 99 | syl2anc 673 |
. . . . . . . . . 10
     |
101 | | snex 4641 |
. . . . . . . . . 10
   |
102 | | elmapg 7503 |
. . . . . . . . . 10
          
       
  
                   |
103 | 100, 101,
102 | sylancl 675 |
. . . . . . . . 9
            
  
                   |
104 | 97, 103 | mpbird 240 |
. . . . . . . 8
                 |
105 | | op1stg 6824 |
. . . . . . . . . . 11
 
          |
106 | 11, 13, 105 | syl2anc 673 |
. . . . . . . . . 10
          |
107 | 106 | fveq2d 5883 |
. . . . . . . . 9
                  |
108 | | op2ndg 6825 |
. . . . . . . . . . 11
 
          |
109 | 11, 13, 108 | syl2anc 673 |
. . . . . . . . . 10
          |
110 | 109 | fveq2d 5883 |
. . . . . . . . 9
                  |
111 | 107, 110 | jca 541 |
. . . . . . . 8
                
                  |
112 | 24 | a1i 11 |
. . . . . . . . . 10
    |
113 | | snfi 7668 |
. . . . . . . . . . 11
   |
114 | 113 | a1i 11 |
. . . . . . . . . 10
     |
115 | 27 | a1i 11 |
. . . . . . . . . 10
 
 
  |
116 | | xmetge0 21437 |
. . . . . . . . . . . . . . 15
      

      |
117 | 29, 11, 13, 116 | syl3anc 1292 |
. . . . . . . . . . . . . 14

      |
118 | | ge0nemnf 11491 |
. . . . . . . . . . . . . 14
                 |
119 | 86, 117, 118 | syl2anc 673 |
. . . . . . . . . . . . 13
       |
120 | | eldifsn 4088 |
. . . . . . . . . . . . 13
       
    
       |
121 | 86, 119, 120 | sylanbrc 677 |
. . . . . . . . . . . 12
          |
122 | | fconst6g 5785 |
. . . . . . . . . . . 12
                        
    |
123 | 121, 122 | syl 17 |
. . . . . . . . . . 11
                      |
124 | | fcoconst 6076 |
. . . . . . . . . . . . . 14
     
    
                         |
125 | 32, 94, 124 | syl2anc 673 |
. . . . . . . . . . . . 13
                           |
126 | 88, 89 | xpsn 6082 |
. . . . . . . . . . . . . 14
           
      |
127 | 126 | coeq2i 5000 |
. . . . . . . . . . . . 13
                      |
128 | | df-ov 6311 |
. . . . . . . . . . . . . . . 16
            |
129 | 128 | eqcomi 2480 |
. . . . . . . . . . . . . . 15
            |
130 | 129 | sneqi 3970 |
. . . . . . . . . . . . . 14
                |
131 | 130 | xpeq2i 4860 |
. . . . . . . . . . . . 13
                        |
132 | 125, 127,
131 | 3eqtr3g 2528 |
. . . . . . . . . . . 12
                       |
133 | 132 | feq1d 5724 |
. . . . . . . . . . 11
                  
                        |
134 | 123, 133 | mpbird 240 |
. . . . . . . . . 10
                      |
135 | 53, 57 | mp1i 13 |
. . . . . . . . . 10
      |
136 | 61 | adantl 473 |
. . . . . . . . . 10
 

              |
137 | 21, 22, 23, 112, 114, 115, 134, 135, 136 | gsumress 16597 |
. . . . . . . . 9
   g             g              |
138 | | fconstmpt 4883 |
. . . . . . . . . . 11
                   |
139 | 132, 138 | syl6eq 2521 |
. . . . . . . . . 10
                     |
140 | 139 | oveq2d 6324 |
. . . . . . . . 9
  g             g            |
141 | | cmnmnd 17523 |
. . . . . . . . . . 11
 CMnd   |
142 | 67, 141 | mp1i 13 |
. . . . . . . . . 10
   |
143 | 87 | a1i 11 |
. . . . . . . . . 10
   |
144 | | eqidd 2472 |
. . . . . . . . . . 11
           |
145 | 65, 144 | gsumsn 17665 |
. . . . . . . . . 10
 
    
    g                |
146 | 142, 143,
121, 145 | syl3anc 1292 |
. . . . . . . . 9
  g                |
147 | 137, 140,
146 | 3eqtrrd 2510 |
. . . . . . . 8
       g              |
148 | | fveq1 5878 |
. . . . . . . . . . . . . . 15
                
          |
149 | 88, 89 | fvsn 6113 |
. . . . . . . . . . . . . . 15
                |
150 | 148, 149 | syl6eq 2521 |
. . . . . . . . . . . . . 14
                  |
151 | 150 | fveq2d 5883 |
. . . . . . . . . . . . 13
                          |
152 | 151 | fveq2d 5883 |
. . . . . . . . . . . 12
                                  |
153 | 152 | eqeq1d 2473 |
. . . . . . . . . . 11
                         
                  |
154 | 150 | fveq2d 5883 |
. . . . . . . . . . . . 13
                          |
155 | 154 | fveq2d 5883 |
. . . . . . . . . . . 12
                                  |
156 | 155 | eqeq1d 2473 |
. . . . . . . . . . 11
                         
                  |
157 | 153, 156 | anbi12d 725 |
. . . . . . . . . 10
                                           
                                   |
158 | | coeq2 4998 |
. . . . . . . . . . . 12
         
             |
159 | 158 | oveq2d 6324 |
. . . . . . . . . . 11
          
g      g              |
160 | 159 | eqeq2d 2481 |
. . . . . . . . . 10
                g   
      g               |
161 | 157, 160 | anbi12d 725 |
. . . . . . . . 9
                                                   g    
                                       g                |
162 | 161 | rspcev 3136 |
. . . . . . . 8
                                                       g                                                               g       |
163 | 104, 111,
147, 162 | syl12anc 1290 |
. . . . . . 7
    
                                             g       |
164 | | ovex 6336 |
. . . . . . . . . 10
     |
165 | 75 | elrnmpt 5087 |
. . . . . . . . . 10
             g    

      g       |
166 | 164, 165 | ax-mp 5 |
. . . . . . . . 9
        g    

      g      |
167 | 15 | rexeqi 2978 |
. . . . . . . . . . 11
        g                                              
                                          g      |
168 | | fveq1 5878 |
. . . . . . . . . . . . . . . 16
           |
169 | 168 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
                   |
170 | 169 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                           |
171 | 170 | eqeq1d 2473 |
. . . . . . . . . . . . 13
                 
                   |
172 | | fveq1 5878 |
. . . . . . . . . . . . . . . 16
           |
173 | 172 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
                   |
174 | 173 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                           |
175 | 174 | eqeq1d 2473 |
. . . . . . . . . . . . 13
                 
                   |
176 | | fveq1 5878 |
. . . . . . . . . . . . . . . . 17
           |
177 | 176 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
                   |
178 | 177 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
                           |
179 | | fveq1 5878 |
. . . . . . . . . . . . . . . . 17
               |
180 | 179 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
                       |
181 | 180 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
                               |
182 | 178, 181 | eqeq12d 2486 |
. . . . . . . . . . . . . 14
                                                         |
183 | 182 | ralbidv 2829 |
. . . . . . . . . . . . 13
  
                                 
                                    |
184 | 171, 175,
183 | 3anbi123d 1365 |
. . . . . . . . . . . 12
                                  
                                  
                
                                                      |
185 | 184 | rexrab 3190 |
. . . . . . . . . . 11
                                                                                      g    
  
                                                                                 g       |
186 | 167, 185 | bitri 257 |
. . . . . . . . . 10
        g       
                                                                                 g       |
187 | | oveq2 6316 |
. . . . . . . . . . . . 13
           |
188 | | 1z 10991 |
. . . . . . . . . . . . . 14
 |
189 | | fzsn 11866 |
. . . . . . . . . . . . . 14
         |
190 | 188, 189 | ax-mp 5 |
. . . . . . . . . . . . 13
       |
191 | 187, 190 | syl6eq 2521 |
. . . . . . . . . . . 12
         |
192 | 191 | oveq2d 6324 |
. . . . . . . . . . 11
   
             |
193 | | df-3an 1009 |
. . . . . . . . . . . . 13
                                 
                                  
                                   
                                    |
194 | | ral0 3865 |
. . . . . . . . . . . . . . . 16
                            |
195 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . 20
       |
196 | | 1m1e0 10700 |
. . . . . . . . . . . . . . . . . . . 20
   |
197 | 195, 196 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . 19
     |
198 | 197 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
             |
199 | | fz10 11846 |
. . . . . . . . . . . . . . . . . 18
     |
200 | 198, 199 | syl6eq 2521 |
. . . . . . . . . . . . . . . . 17
         |
201 | 200 | raleqdv 2979 |
. . . . . . . . . . . . . . . 16
  
                                 
                             |
202 | 194, 201 | mpbiri 241 |
. . . . . . . . . . . . . . 15
                                     |
203 | 202 | biantrud 515 |
. . . . . . . . . . . . . 14
                                   
                                   
                                     |
204 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . 18
           |
205 | 204 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
                   |
206 | 205 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
                           |
207 | 206 | eqeq1d 2473 |
. . . . . . . . . . . . . . 15
                 
                   |
208 | 207 | anbi2d 718 |
. . . . . . . . . . . . . 14
                                   
                
                    |
209 | 203, 208 | bitr3d 263 |
. . . . . . . . . . . . 13
                                                                       
                
                    |
210 | 193, 209 | syl5bb 265 |
. . . . . . . . . . . 12
                                  
                                  
                
                    |
211 | 210 | anbi1d 719 |
. . . . . . . . . . 11
                                                                             g                      
                       g        |
212 | 192, 211 | rexeqbidv 2988 |
. . . . . . . . . 10
  
  
                                                                                 g        
                                             g        |
213 | 186, 212 | syl5bb 265 |
. . . . . . . . 9
  
      g       
                                             g        |
214 | 166, 213 | syl5bb 265 |
. . . . . . . 8
         g    
                                                 g        |
215 | 214 | rspcev 3136 |
. . . . . . 7
                           
                       g              g       |
216 | 87, 163, 215 | sylancr 676 |
. . . . . 6
         g       |
217 | | eliun 4274 |
. . . . . 6
         g    
        g       |
218 | 216, 217 | sylibr 217 |
. . . . 5
         g       |
219 | 218, 18 | syl6eleqr 2560 |
. . . 4
       |
220 | | infxrlb 11645 |
. . . 4
 
     inf         |
221 | 82, 219, 220 | syl2anc 673 |
. . 3
 inf         |
222 | 18 | eleq2i 2541 |
. . . . . . 7

    g       |
223 | | eliun 4274 |
. . . . . . 7
     g    
    g       |
224 | 222, 223 | bitri 257 |
. . . . . 6

    g       |
225 | | vex 3034 |
. . . . . . . . 9
 |
226 | 75 | elrnmpt 5087 |
. . . . . . . . 9
     g    

  g       |
227 | 225, 226 | ax-mp 5 |
. . . . . . . 8
    g    

  g      |
228 | 184, 15 | elrab2 3186 |
. . . . . . . . . . . . . . . . 17

                                                                                |
229 | 228 | simprbi 471 |
. . . . . . . . . . . . . . . 16
                                 
                                     |
230 | 229 | adantl 473 |
. . . . . . . . . . . . . . 15
                                     
                                     |
231 | 230 | simp2d 1043 |
. . . . . . . . . . . . . 14
                       |
232 | 3 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
           |
233 | | f1of1 5827 |
. . . . . . . . . . . . . . . 16
    
      |
234 | 232, 233 | syl 17 |
. . . . . . . . . . . . . . 15
           |
235 | | simplr 770 |
. . . . . . . . . . . . . . . . . 18
       |
236 | | elfz1end 11855 |
. . . . . . . . . . . . . . . . . 18

      |
237 | 235, 236 | sylib 201 |
. . . . . . . . . . . . . . . . 17
           |
238 | 50, 237 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . 16
             |
239 | | xp2nd 6843 |
. . . . . . . . . . . . . . . 16
                 |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . 15
               |
241 | 13 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
       |
242 | | f1fveq 6181 |
. . . . . . . . . . . . . . 15
              
 
                            |
243 | 234, 240,
241, 242 | syl12anc 1290 |
. . . . . . . . . . . . . 14
                     
           |
244 | 231, 243 | mpbid 215 |
. . . . . . . . . . . . 13
               |
245 | 244 | oveq2d 6324 |
. . . . . . . . . . . 12
                       |
246 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
     
       |
247 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
           |
248 | 247 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
                   |
249 | 248 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
                           |
250 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . 21
           |
251 | 250, 190 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . 20
         |
252 | 251 | reseq2d 5111 |
. . . . . . . . . . . . . . . . . . 19
                 |
253 | 252 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
  g           g          |
254 | 249, 253 | breq12d 4408 |
. . . . . . . . . . . . . . . . 17
             
 g                     
 g           |
255 | 246, 254 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
                    g          
                  g            |
256 | 255 | imbi2d 323 |
. . . . . . . . . . . . . . 15
      
    
             g           
  
                  
 g             |
257 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
     
       |
258 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
           |
259 | 258 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
                   |
260 | 259 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
                           |
261 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . 20
           |
262 | 261 | reseq2d 5111 |
. . . . . . . . . . . . . . . . . . 19
                   |
263 | 262 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
  g           g            |
264 | 260, 263 | breq12d 4408 |
. . . . . . . . . . . . . . . . 17
             
 g                     
 g             |
265 | 257, 264 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
                    g          
    
             g              |
266 | 265 | imbi2d 323 |
. . . . . . . . . . . . . . 15
      
    
             g           
  
                  
 g               |
267 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
       
         |
268 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
          
    |
269 | 268 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
                       |
270 | 269 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
                               |
271 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . 20
               |
272 | 271 | reseq2d 5111 |
. . . . . . . . . . . . . . . . . . 19
                       |
273 | 272 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
    g           g              |
274 | 270, 273 | breq12d 4408 |
. . . . . . . . . . . . . . . . 17
               
 g                       
 g               |
275 | 267, 274 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
                      g          
                      g                |
276 | 275 | imbi2d 323 |
. . . . . . . . . . . . . . 15
        
    
             g           
  
                      
 g                 |
277 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
     
       |
278 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
           |
279 | 278 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
                   |
280 | 279 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
                           |
281 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . 20
           |
282 | 281 | reseq2d 5111 |
. . . . . . . . . . . . . . . . . . 19
                   |
283 | 282 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
  g           g            |
284 | 280, 283 | breq12d 4408 |
. . . . . . . . . . . . . . . . 17
             
 g                     
 g             |
285 | 277, 284 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
                    g          
    
             g              |
286 | 285 | imbi2d 323 |
. . . . . . . . . . . . . . 15
      
    
             g           
  
                  
 g               |
287 | 29 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
            |
288 | 11 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
       |
289 | | nnuz 11218 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
290 | 235, 289 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
291 | | eluzfz1 11832 |
. . . . . . . . . . . . . . . . . . . . . 22
    
      |
292 | 290, 291 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
           |
293 | 50, 292 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . 20
             |
294 | | xp2nd 6843 |
. . . . . . . . . . . . . . . . . . . 20
                 |
295 | 293, 294 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
               |
296 | | xmetcl 21424 |
. . . . . . . . . . . . . . . . . . 19
                              |
297 | 287, 288,
295, 296 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
                   |
298 | | xrleid 11472 |
. . . . . . . . . . . . . . . . . 18
                                       |
299 | 297, 298 | syl 17 |
. . . . . . . . . . . . . . . . 17
                               |
300 | 142 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
       |
301 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
       |
302 | 44, 293 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . 19
                  |
303 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
304 | 303 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . 20
                   |
305 | 65, 304 | gsumsn 17665 |
. . . . . . . . . . . . . . . . . . 19
 
             g                        |
306 | 300, 301,
302, 305 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
      g                        |
307 | 287, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
308 | | fcompt 6075 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
                 |
309 | 307, 50, 308 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
     
                 |
310 | 309 | reseq1d 5110 |
. . . . . . . . . . . . . . . . . . . 20
                         
     |
311 | 292 | snssd 4108 |
. . . . . . . . . . . . . . . . . . . . 21
      
      |
312 | 311 | resmptd 5162 |
. . . . . . . . . . . . . . . . . . . 20
                                     |
313 | 310, 312 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . 19
                         |
314 | 313 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
      g         g                |
315 | | df-ov 6311 |
. . . . . . . . . . . . . . . . . . 19
                            |
316 | | 1st2nd2 6849 |
. . . . . . . . . . . . . . . . . . . . . 22
                                |
317 | 293, 316 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
                              |
318 | 230 | simp1d 1042 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
319 | | xp1st 6842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
320 | 293, 319 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
321 | | f1fveq 6181 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              
 
                            |
322 | 234, 320,
288, 321 | syl12anc 1290 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     
           |
323 | 318, 322 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
324 | 323 | opeq1d 4164 |
. . . . . . . . . . . . . . . . . . . . 21
                                     |
325 | 317, 324 | eqtr2d 2506 |
. . . . . . . . . . . . . . . . . . . 20
                      |
326 | 325 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
                              |
327 | 315, 326 | syl5eq 2517 |
. . . . . . . . . . . . . . . . . 18
                           |
328 | 306, 314,
327 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . . . 17
      g                      |
329 | 299, 328 | breqtrrd 4422 |
. . . . . . . . . . . . . . . 16
                  g          |
330 | 329 | a1d 25 |
. . . . . . . . . . . . . . 15
                     
 g           |
331 | | simprl 772 |
. . . . . . . . . . . . . . . . . . . . . 22
   


        
  |
332 | 331, 289 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . . . . . 21
   


        
      |
333 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . . 21
   


                 |
334 | | peano2fzr 11838 |
. . . . . . . . . . . . . . . . . . . . 21
            
      |
335 | 332, 333,
334 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
   


        
      |
336 | 335 | expr 626 |
. . . . . . . . . . . . . . . . . . 19
   



              |
337 | 336 | imim1d 77 |
. . . . . . . . . . . . . . . . . 18
   



                 
 g          
                    g              |
338 | 287 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   


        
       |
339 | 288 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   


        
  |
340 | 50 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   


                     |
341 | 340, 335 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   


                 |
342 | | xp2nd 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
343 | 341, 342 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   


                   |
344 | | xmetcl 21424 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                              |
345 | 338, 339,
343, 344 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . 23
   


                       |
346 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   


        
CMnd |
347 | | fzfid 12224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   


               |
348 | 52 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   


                   
    |
349 | | fzsuc 11869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
                  |
350 | 332, 349 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   


                           |
351 | | elfzuz3 11823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
               |
352 | 351 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   


        
   
    |
353 | | fzss2 11864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
            |
354 | 352, 353 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   


              
      |
355 | 350, 354 | eqsstr3d 3453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   


                         |
356 | 355 | unssad 3602 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   


            
      |
357 | 348, 356 | fssresd 5762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   


                              |
358 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   


           |
359 | 357, 347,
358 | fdmfifsupp 7911 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   


                 finSupp   |
360 | 65, 66, 346, 347, 357, 359 | gsumcl 17627 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   


          g               |
361 | 360 | eldifad 3402 |
. . . . . . . . . . . . . . . . . . . . . . 23
   


          g            |
362 | 338, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   


                 |
363 | 340, 333 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   


                   |
364 | 362, 363 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . 23
   


                     |
365 | | xleadd1a 11564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                g                                  g                                     
  g                          |
366 | 365 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . 23
               g                                 
 g                                       g                           |
367 | 345, 361,
364, 366 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . 22
   


                       g         
                             g                           |
368 | | xp2nd 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               
     |
369 | 363, 368 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   


                     |
370 | | xmettri 21444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                           
                                                       |
371 | 338, 339,
369, 343, 370 | syl13anc 1294 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   


                      
                                         |
372 | | 1st2nd2 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                                        |
373 | 363, 372 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   


                      
                 |
374 | | nnz 10983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
375 | 374 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   


        
  |
376 | | eluzp1m1 11206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
   
           |
377 | 375, 352,
376 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   


                 |
378 | | elfzuzb 11820 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      
              |
379 | 332, 377,
378 |