Step | Hyp | Ref
| Expression |
1 | | arch 10866 |
. . . . 5
    |
2 | 1 | ad2antlr 733 |
. . . 4
    
 
          
  |
3 | | df-ima 4847 |
. . . . . . . . . . . . . . . 16
                   |
4 | | ovolicc2.8 |
. . . . . . . . . . . . . . . . . . 19
       |
5 | | nnuz 11194 |
. . . . . . . . . . . . . . . . . . . . 21
     |
6 | | ovolicc2.15 |
. . . . . . . . . . . . . . . . . . . . 21
            |
7 | | 1zzd 10968 |
. . . . . . . . . . . . . . . . . . . . 21
   |
8 | | ovolicc2.14 |
. . . . . . . . . . . . . . . . . . . . 21
   |
9 | | ovolicc2.11 |
. . . . . . . . . . . . . . . . . . . . 21
       |
10 | 5, 6, 7, 8, 9 | algrf 14532 |
. . . . . . . . . . . . . . . . . . . 20
       |
11 | | ovolicc2.10 |
. . . . . . . . . . . . . . . . . . . . 21
    ![[,] [,]](_icc.gif)     |
12 | | ssrab2 3514 |
. . . . . . . . . . . . . . . . . . . . 21


  ![[,] [,]](_icc.gif)   
 |
13 | 11, 12 | eqsstri 3462 |
. . . . . . . . . . . . . . . . . . . 20
 |
14 | | fss 5737 |
. . . . . . . . . . . . . . . . . . . 20
             |
15 | 10, 13, 14 | sylancl 668 |
. . . . . . . . . . . . . . . . . . 19
       |
16 | | fco 5739 |
. . . . . . . . . . . . . . . . . . 19
                   |
17 | 4, 15, 16 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
         |
18 | | elfznn 11828 |
. . . . . . . . . . . . . . . . . . 19
       |
19 | 18 | ssriv 3436 |
. . . . . . . . . . . . . . . . . 18
     |
20 | | fssres 5749 |
. . . . . . . . . . . . . . . . . 18
           
                   |
21 | 17, 19, 20 | sylancl 668 |
. . . . . . . . . . . . . . . . 17
                   |
22 | | frn 5735 |
. . . . . . . . . . . . . . . . 17
                           |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
           |
24 | 3, 23 | syl5eqss 3476 |
. . . . . . . . . . . . . . 15
             |
25 | | nnssre 10613 |
. . . . . . . . . . . . . . 15
 |
26 | 24, 25 | syl6ss 3444 |
. . . . . . . . . . . . . 14
             |
27 | 26 | ad3antrrr 736 |
. . . . . . . . . . . . 13
   

           
 
          |
28 | | simpr 463 |
. . . . . . . . . . . . 13
   

           
            |
29 | 27, 28 | sseldd 3433 |
. . . . . . . . . . . 12
   

           
  |
30 | | simpllr 769 |
. . . . . . . . . . . 12
   

           
  |
31 | | nnre 10616 |
. . . . . . . . . . . . 13
   |
32 | 31 | ad2antlr 733 |
. . . . . . . . . . . 12
   

           
  |
33 | | lelttr 9724 |
. . . . . . . . . . . 12
 
  
    |
34 | 29, 30, 32, 33 | syl3anc 1268 |
. . . . . . . . . . 11
   

           
 

   |
35 | 34 | ancomsd 456 |
. . . . . . . . . 10
   

           
 

   |
36 | 35 | expdimp 439 |
. . . . . . . . 9
                   
   |
37 | 36 | an32s 813 |
. . . . . . . 8
       
          

   |
38 | 37 | ralimdva 2796 |
. . . . . . 7
   

 
 
 
                        |
39 | 38 | impancom 442 |
. . . . . 6
   

            
                 |
40 | 39 | an32s 813 |
. . . . 5
   
            

 
               |
41 | 40 | reximdva 2862 |
. . . 4
    
 
                            |
42 | 2, 41 | mpd 15 |
. . 3
    
 
          
              |
43 | | fzfid 12186 |
. . . . 5
       |
44 | | fvres 5879 |
. . . . . . . . . . . . . . 15
                         |
45 | 44 | adantl 468 |
. . . . . . . . . . . . . 14
 
                         |
46 | | fvco3 5942 |
. . . . . . . . . . . . . . 15
     
                 |
47 | 10, 18, 46 | syl2an 480 |
. . . . . . . . . . . . . 14
 
                     |
48 | 45, 47 | eqtrd 2485 |
. . . . . . . . . . . . 13
 
                           |
49 | 48 | adantrr 723 |
. . . . . . . . . . . 12
 
    
                            |
50 | | fvres 5879 |
. . . . . . . . . . . . . 14
                         |
51 | 50 | ad2antll 735 |
. . . . . . . . . . . . 13
 
    
                          |
52 | | elfznn 11828 |
. . . . . . . . . . . . . . 15
       |
53 | 52 | adantl 468 |
. . . . . . . . . . . . . 14
     
       |
54 | | fvco3 5942 |
. . . . . . . . . . . . . 14
     
                 |
55 | 10, 53, 54 | syl2an 480 |
. . . . . . . . . . . . 13
 
    
                      |
56 | 51, 55 | eqtrd 2485 |
. . . . . . . . . . . 12
 
    
                            |
57 | 49, 56 | eqeq12d 2466 |
. . . . . . . . . . 11
 
    
                              
                   |
58 | | fveq2 5865 |
. . . . . . . . . . . . 13
                
                          |
59 | 58 | fveq2d 5869 |
. . . . . . . . . . . 12
                
                                  |
60 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    
  |
61 | | elfznn 11828 |
. . . . . . . . . . . . . . . . . . . . 21
       |
62 | 61 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . 20
           |
63 | 62 | nnred 10624 |
. . . . . . . . . . . . . . . . . . 19
           |
64 | | ovolicc2.16 |
. . . . . . . . . . . . . . . . . . . . . . 23

      |
65 | | ssrab2 3514 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
66 | 64, 65 | eqsstri 3462 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
67 | 66, 25 | sstri 3441 |
. . . . . . . . . . . . . . . . . . . . 21
 |
68 | | ovolicc2lem4OLD.17 |
. . . . . . . . . . . . . . . . . . . . . 22
   
 |
69 | 66, 5 | sseqtri 3464 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
70 | | 1z 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
71 | 5 | uzinf 12179 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
73 | | ovolicc2.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        |
74 | | elin 3617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
   
   |
75 | 73, 74 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
   |
76 | 75 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
77 | | ssfi 7792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
  |
78 | 76, 13, 77 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
79 | 78 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

  |
80 | 10 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

      |
81 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                           |
82 | 81 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                   |
83 | 82 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                           |
84 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
 
  |
85 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
 
  |
86 | | ral0 3874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
  |
87 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
 
  |
88 | 87 | raleqdv 2993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
 
 
    |
89 | 86, 88 | mpbiri 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    
 

  |
90 | 89 | ralrimivw 2803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    
 
    |
91 | | rabid2 2968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  
     |
92 | 90, 91 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
 

    |
93 | 85, 92 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
 
 
   |
94 | | simprr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
 
  |
95 | 94, 92 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
 
 
   |
96 | | ovolicc.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
97 | | ovolicc.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
98 | | ovolicc.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
99 | | ovolicc2.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
   |
100 | | ovolicc2.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
          |
101 | | ovolicc2.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   ![[,] [,]](_icc.gif) 
   |
102 | | ovolicc2.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
  
          |
103 | | ovolicc2.12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
                                    |
104 | | ovolicc2.13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
105 | 96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64 | ovolicc2lem3 22472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   
 
                                       |
106 | 84, 93, 95, 105 | syl12anc 1266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
 

                                   |
107 | 83, 106 | syl5ibr 225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
 
            |
108 | 107 | ralrimivva 2809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

          
   |
109 | | dff13 6159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
     
         
    |
110 | 80, 108, 109 | sylanbrc 670 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

      |
111 | | f1domg 7589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
112 | 79, 110, 111 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

  |
113 | | domfi 7793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
114 | 79, 112, 113 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

  |
115 | 114 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
116 | 115 | necon3bd 2638 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
117 | 72, 116 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
118 | | infmssuzclOLD 11247 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
           |
119 | 69, 117, 118 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . 22
    
  |
120 | 68, 119 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . . . . 21
   |
121 | 67, 120 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . 20
   |
122 | 121 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
           |
123 | 67 | sseli 3428 |
. . . . . . . . . . . . . . . . . . . 20
   |
124 | 123 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
           |
125 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . . 20
       |
126 | 125 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . 19
           |
127 | | infmssuzleOLD 11246 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           |
128 | 69, 127 | mpan 676 |
. . . . . . . . . . . . . . . . . . . . 21
       |
129 | 68, 128 | syl5eqbr 4436 |
. . . . . . . . . . . . . . . . . . . 20
   |
130 | 129 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
           |
131 | 63, 122, 124, 126, 130 | letrd 9792 |
. . . . . . . . . . . . . . . . . 18
           |
132 | 131 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . 17
 
     
  |
133 | 60, 132 | ssrabdv 3508 |
. . . . . . . . . . . . . . . 16
    
 
   |
134 | 133 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
         
 
   |
135 | | simprl 764 |
. . . . . . . . . . . . . . 15
 
    
            |
136 | 134, 135 | sseldd 3433 |
. . . . . . . . . . . . . 14
 
    
       
   |
137 | | simprr 766 |
. . . . . . . . . . . . . . 15
 
    
            |
138 | 134, 137 | sseldd 3433 |
. . . . . . . . . . . . . 14
 
    
       
   |
139 | 136, 138 | jca 535 |
. . . . . . . . . . . . 13
 
    
        

 
    |
140 | 139, 105 | syldan 473 |
. . . . . . . . . . . 12
 
    
                                          |
141 | 59, 140 | syl5ibr 225 |
. . . . . . . . . . 11
 
    
                          |
142 | 57, 141 | sylbid 219 |
. . . . . . . . . 10
 
    
                                  |
143 | 142 | ralrimivva 2809 |
. . . . . . . . 9
                                         |
144 | | dff13 6159 |
. . . . . . . . 9
                
                                                          |
145 | 21, 143, 144 | sylanbrc 670 |
. . . . . . . 8
                   |
146 | | f1f1orn 5825 |
. . . . . . . 8
                
                          |
147 | 145, 146 | syl 17 |
. . . . . . 7
                           |
148 | | f1oeq3 5807 |
. . . . . . . 8
                                                                         |
149 | 3, 148 | ax-mp 5 |
. . . . . . 7
                                                     |
150 | 147, 149 | sylibr 216 |
. . . . . 6
                             |
151 | | f1ofo 5821 |
. . . . . 6
                                                       |
152 | 150, 151 | syl 17 |
. . . . 5
                             |
153 | | fofi 7860 |
. . . . 5
                                             |
154 | 43, 152, 153 | syl2anc 667 |
. . . 4
             |
155 | | fimaxre2 10552 |
. . . 4
           
           
              |
156 | 26, 154, 155 | syl2anc 667 |
. . 3
                |
157 | 42, 156 | r19.29a 2932 |
. 2
                |
158 | 97, 96 | resubcld 10047 |
. . . . 5
     |
159 | 158 | rexrd 9690 |
. . . 4
     |
160 | 159 | adantr 467 |
. . 3
 
              
    |
161 | | fzfid 12186 |
. . . . . 6
       |
162 | | elfznn 11828 |
. . . . . . . . 9
       |
163 | | eqid 2451 |
. . . . . . . . . . . 12
    
  |
164 | 163 | ovolfsf 22424 |
. . . . . . . . . . 11
         
          |
165 | 100, 164 | syl 17 |
. . . . . . . . . 10
  
          |
166 | 165 | ffvelrnda 6022 |
. . . . . . . . 9
 

  
         |
167 | 162, 166 | sylan2 477 |
. . . . . . . 8
 
       
         |
168 | | elrege0 11738 |
. . . . . . . 8
   
                         |
169 | 167, 168 | sylib 200 |
. . . . . . 7
 
        
              |
170 | 169 | simpld 461 |
. . . . . 6
 
       
      |
171 | 161, 170 | fsumrecl 13800 |
. . . . 5
         
      |
172 | 171 | adantr 467 |
. . . 4
 
              
               |
173 | 172 | rexrd 9690 |
. . 3
 
              
               |
174 | 163, 99 | ovolsf 22425 |
. . . . . . . . 9
                 |
175 | 100, 174 | syl 17 |
. . . . . . . 8
          |
176 | | frn 5735 |
. . . . . . . 8
       
     |
177 | 175, 176 | syl 17 |
. . . . . . 7
  
   |
178 | | rge0ssre 11740 |
. . . . . . 7
    |
179 | 177, 178 | syl6ss 3444 |
. . . . . 6
   |
180 | | ressxr 9684 |
. . . . . 6
 |
181 | 179, 180 | syl6ss 3444 |
. . . . 5
   |
182 | | supxrcl 11600 |
. . . . 5

      |
183 | 181, 182 | syl 17 |
. . . 4
       |
184 | 183 | adantr 467 |
. . 3
 
              
      |
185 | 158 | adantr 467 |
. . . 4
 
              
    |
186 | 24 | sselda 3432 |
. . . . . . 7
 
          
  |
187 | 178, 166 | sseldi 3430 |
. . . . . . 7
 

  
      |
188 | 186, 187 | syldan 473 |
. . . . . 6
 
          
  
      |
189 | 154, 188 | fsumrecl 13800 |
. . . . 5
               
      |
190 | 189 | adantr 467 |
. . . 4
 
              
              
      |
191 | | inss2 3653 |
. . . . . . . . . . 11
      |
192 | | fss 5737 |
. . . . . . . . . . 11
                   
   |
193 | 100, 191,
192 | sylancl 668 |
. . . . . . . . . 10
         |
194 | 66, 120 | sseldi 3430 |
. . . . . . . . . . . 12
   |
195 | 15, 194 | ffvelrnd 6023 |
. . . . . . . . . . 11
       |
196 | 4, 195 | ffvelrnd 6023 |
. . . . . . . . . 10
           |
197 | 193, 196 | ffvelrnd 6023 |
. . . . . . . . 9
                 |
198 | | xp2nd 6824 |
. . . . . . . . 9
              
                  |
199 | 197, 198 | syl 17 |
. . . . . . . 8
                   |
200 | 13, 8 | sseldi 3430 |
. . . . . . . . . . 11
   |
201 | 4, 200 | ffvelrnd 6023 |
. . . . . . . . . 10
       |
202 | 193, 201 | ffvelrnd 6023 |
. . . . . . . . 9
             |
203 | | xp1st 6823 |
. . . . . . . . 9
          
              |
204 | 202, 203 | syl 17 |
. . . . . . . 8
               |
205 | 199, 204 | resubcld 10047 |
. . . . . . 7
                                 |
206 | | fveq2 5865 |
. . . . . . . . . 10
        
  
      
              |
207 | 187 | recnd 9669 |
. . . . . . . . . . 11
 

  
      |
208 | 186, 207 | syldan 473 |
. . . . . . . . . 10
 
          
  
      |
209 | 206, 43, 150, 48, 208 | fsumf1o 13789 |
. . . . . . . . 9
               
                           |
210 | 100 | adantr 467 |
. . . . . . . . . . 11
 
         
    |
211 | 4 | adantr 467 |
. . . . . . . . . . . 12
 
           |
212 | | ffvelrn 6020 |
. . . . . . . . . . . . 13
     
       |
213 | 15, 18, 212 | syl2an 480 |
. . . . . . . . . . . 12
 
           |
214 | 211, 213 | ffvelrnd 6023 |
. . . . . . . . . . 11
 
               |
215 | 163 | ovolfsval 22423 |
. . . . . . . . . . 11
                    
                                                |
216 | 210, 214,
215 | syl2anc 667 |
. . . . . . . . . 10
 
       
                                                |
217 | 216 | sumeq2dv 13769 |
. . . . . . . . 9
         
                                                      |
218 | 193 | adantr 467 |
. . . . . . . . . . . . . . 15
 

        |
219 | 4 | adantr 467 |
. . . . . . . . . . . . . . . 16
 

      |
220 | 15 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . 16
 

      |
221 | 219, 220 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
 

          |
222 | 218, 221 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
 

                |
223 | | xp2nd 6824 |
. . . . . . . . . . . . . 14
              
                  |
224 | 222, 223 | syl 17 |
. . . . . . . . . . . . 13
 

                  |
225 | 18, 224 | sylan2 477 |
. . . . . . . . . . . 12
 
                       |
226 | 225 | recnd 9669 |
. . . . . . . . . . 11
 
                       |
227 | 193 | adantr 467 |
. . . . . . . . . . . . . 14
 
             |
228 | 227, 214 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
 
                     |
229 | | xp1st 6823 |
. . . . . . . . . . . . 13
              
                  |
230 | 228, 229 | syl 17 |
. . . . . . . . . . . 12
 
                       |
231 | 230 | recnd 9669 |
. . . . . . . . . . 11
 
                       |
232 | 43, 226, 231 | fsumsub 13849 |
. . . . . . . . . 10
                                          
                                              |
233 | 69, 120 | sseldi 3430 |
. . . . . . . . . . . . 13
       |
234 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
235 | 234 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
                   |
236 | 235 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                           |
237 | 236 | fveq2d 5869 |
. . . . . . . . . . . . 13
                                   |
238 | 233, 226,
237 | fsumm1 13812 |
. . . . . . . . . . . 12
                            
                                      |
239 | | fzfid 12186 |
. . . . . . . . . . . . . . 15
    
    |
240 | | elfznn 11828 |
. . . . . . . . . . . . . . . 16
         |
241 | 240, 224 | sylan2 477 |
. . . . . . . . . . . . . . 15
 
   
                     |
242 | 239, 241 | fsumrecl 13800 |
. . . . . . . . . . . . . 14
                           |
243 | 242 | recnd 9669 |
. . . . . . . . . . . . 13
                           |
244 | 199 | recnd 9669 |
. . . . . . . . . . . . 13
                   |
245 | 243, 244 | addcomd 9835 |
. . . . . . . . . . . 12
                                                                                       |
246 | 238, 245 | eqtrd 2485 |
. . . . . . . . . . 11
                                            
                      |
247 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
248 | 247 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
                   |
249 | 248 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                           |
250 | 249 | fveq2d 5869 |
. . . . . . . . . . . . 13
                                   |
251 | 233, 231,
250 | fsum1p 13814 |
. . . . . . . . . . . 12
                                        
                          |
252 | 5, 6, 7, 8 | algr0 14531 |
. . . . . . . . . . . . . . . 16
       |
253 | 252 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
               |
254 | 253 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                       |
255 | 254 | fveq2d 5869 |
. . . . . . . . . . . . 13
                               |
256 | 7 | peano2zd 11043 |
. . . . . . . . . . . . . . 15
     |
257 | 194 | nnzd 11039 |
. . . . . . . . . . . . . . 15
   |
258 | | fzp1ss 11847 |
. . . . . . . . . . . . . . . . . 18
             |
259 | 70, 258 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
      
      |
260 | 259 | sselda 3432 |
. . . . . . . . . . . . . . . 16
 
             |
261 | 260, 231 | syldan 473 |
. . . . . . . . . . . . . . 15
 
                         |
262 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
               |
263 | 262 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
                       |
264 | 263 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                               |
265 | 264 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
                                       |
266 | 7, 256, 257, 261, 265 | fsumshftm 13842 |
. . . . . . . . . . . . . 14
                                                         |
267 | | ax-1cn 9597 |
. . . . . . . . . . . . . . . . . 18
 |
268 | 267, 267 | pncan3oi 9891 |
. . . . . . . . . . . . . . . . 17
     |
269 | 268 | oveq1i 6300 |
. . . . . . . . . . . . . . . 16
             
   |
270 | 269 | sumeq1i 13764 |
. . . . . . . . . . . . . . 15
        
                                                |
271 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . 20
       |
272 | 271 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
               |
273 | 272 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
                       |
274 | 273 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
                               |
275 | 274 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                                       |
276 | 275 | cbvsumv 13762 |
. . . . . . . . . . . . . . 15
    
                                                |
277 | 270, 276 | eqtri 2473 |
. . . . . . . . . . . . . 14
        
                                                |
278 | 266, 277 | syl6eq 2501 |
. . . . . . . . . . . . 13
                                                     |
279 | 255, 278 | oveq12d 6308 |
. . . . . . . . . . . 12
                                                                                     |
280 | 251, 279 | eqtrd 2485 |
. . . . . . . . . . 11
                                    
                            |
281 | 246, 280 | oveq12d 6308 |
. . . . . . . . . 10
                                                                                                                                     |
282 | 204 | recnd 9669 |
. . . . . . . . . . 11
               |
283 | | peano2nn 10621 |
. . . . . . . . . . . . . . . . . 18
     |
284 | | ffvelrn 6020 |
. . . . . . . . . . . . . . . . . 18
                 |
285 | 15, 283, 284 | syl2an 480 |
. . . . . . . . . . . . . . . . 17
 

        |
286 | 219, 285 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
 

            |
287 | 218, 286 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
 

                  |
288 | | xp1st 6823 |
. . . . . . . . . . . . . . 15
                
                    |
289 | 287, 288 | syl 17 |
. . . . . . . . . . . . . 14
 

                    |
290 | 240, 289 | sylan2 477 |
. . . . . . . . . . . . 13
 
   
                       |
291 | 239, 290 | fsumrecl 13800 |
. . . . . . . . . . . 12
                             |
292 | 291 | recnd 9669 |
. . . . . . . . . . 11
                             |
293 | 244, 243,
282, 292 | addsub4d 10033 |
. . . . . . . . . 10
                       
                                                                                             
                                                     |
294 | 232, 281,
293 | 3eqtrd 2489 |
. . . . . . . . 9
                                                                         
                                                     |
295 | 209, 217,
294 | 3eqtrd 2489 |
. . . . . . . 8
               
                                    
                                                     |
296 | 295, 189 | eqeltrrd 2530 |
. . . . . . 7
                                                                                       |
297 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
298 | 297 | eleq2d 2514 |
. . . . . . . . . . . . . 14
 
   
       |
299 | 298, 64 | elrab2 3198 |
. . . . . . . . . . . . 13

        |
300 | 120, 299 | sylib 200 |
. . . . . . . . . . . 12
         |
301 | 300 | simprd 465 |
. . . . . . . . . . 11
       |
302 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 22470 |
. . . . . . . . . . . 12
 
    
                                          |
303 | 195, 302 | mpdan 674 |
. . . . . . . . . . 11
                                           |
304 | 301, 303 | mpbid 214 |
. . . . . . . . . 10
                                     |
305 | 304 | simp3d 1022 |
. . . . . . . . 9
                   |
306 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 22470 |
. . . . . . . . . . . 12
 
 
            
                |
307 | 200, 306 | mpdan 674 |
. . . . . . . . . . 11
                               |
308 | 104, 307 | mpbid 214 |
. . . . . . . . . 10
                             |
309 | 308 | simp2d 1021 |
. . . . . . . . 9
               |
310 | 97, 204, 199, 96, 305, 309 | lt2subd 10237 |
. . . . . . . 8
  
                                |
311 | 158, 205,
310 | ltled 9783 |
. . . . . . 7
  
                                |
312 | 240 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
   
     |
313 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
      
    |
314 | 257 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   
     |
315 | | elfzm11 11865 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
        
    |
316 | 70, 314, 315 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
         

    |
317 | 313, 316 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
       |
318 | 317 | simp3d 1022 |
. . . . . . . . . . . . . . . . . . . 20
 
   
     |
319 | 312 | nnred 10624 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
     |
320 | 121 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
     |
321 | 319, 320 | ltnled 9782 |
. . . . . . . . . . . . . . . . . . . 20
 
   
   
   |
322 | 318, 321 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
 
   
     |
323 | | infmssuzleOLD 11246 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
324 | 69, 323 | mpan 676 |
. . . . . . . . . . . . . . . . . . . 20
       |
325 | 68, 324 | syl5eqbr 4436 |
. . . . . . . . . . . . . . . . . . 19
   |
326 | 322, 325 | nsyl 125 |
. . . . . . . . . . . . . . . . . 18
 
   
  
  |
327 | 312, 326 | jca 535 |
. . . . . . . . . . . . . . . . 17
 
   
   
   |
328 | 96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64 | ovolicc2lem2 22471 |
. . . . . . . . . . . . . . . . 17
 
                     |
329 | 327, 328 | syldan 473 |
. . . . . . . . . . . . . . . 16
 
   
                     |
330 | 329 | iftrued 3889 |
. . . . . . . . . . . . . . 15
 
   
                                                          |
331 | | ffvelrn 6020 |
. . . . . . . . . . . . . . . . 17
     
       |
332 | 10, 240, 331 | syl2an 480 |
. . . . . . . . . . . . . . . 16
 
   
         |
333 | 103 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . 17
                                     |
334 | 333 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
   
   
                                   |
335 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
336 | 335 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
337 | 336 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
338 | 337 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . 19
                 
               
   |
339 | 338, 337 | ifbieq1d 3904 |
. . . . . . . . . . . . . . . . . 18
                                                   
                     |
340 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
                   |
341 | 339, 340 | eleq12d 2523 |
. . . . . . . . . . . . . . . . 17
                                                        
                              |
342 | 341 | rspcv 3146 |
. . . . . . . . . . . . . . . 16
      
                                
                                                |
343 | 332, 334,
342 | sylc 62 |
. . . . . . . . . . . . . . 15
 
   
                                                  |
344 | 330, 343 | eqeltrrd 2530 |
. . . . . . . . . . . . . 14
 
   
                             |
345 | 5, 6, 7, 8, 9 | algrp1 14533 |
. . . . . . . . . . . . . . 15
 

                |
346 | 240, 345 | sylan2 477 |
. . . . . . . . . . . . . 14
 
   
                   |
347 | 344, 346 | eleqtrrd 2532 |
. . . . . . . . . . . . 13
 
   
                           |
348 | 240, 285 | sylan2 477 |
. . . . . . . . . . . . . 14
 
   
           |
349 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 22470 |
. . . . . . . . . . . . . 14
 
      
                                                                                                                |
350 | 348, 349 | syldan 473 |
. . . . . . . . . . . . 13
 
   
                         
                                                                                         |
351 | 347, 350 | mpbid 214 |
. . . . . . . . . . . 12
 
   
                                                                                           |
352 | 351 | simp2d 1021 |
. . . . . . . . . . 11
 
   
                                       |
353 | 290, 241,
352 | ltled 9783 |
. . . . . . . . . 10
 
   
                                       |
354 | 239, 290,
241, 353 | fsumle 13859 |
. . . . . . . . 9
                                                     |
355 | 242, 291 | subge0d 10203 |
. . . . . . . . 9
                                                                                                           |
356 | 354, 355 | mpbird 236 |
. . . . . . . 8

 
                                                    |
357 | 242, 291 | resubcld 10047 |
. . . . . . . . 9
                                                       |
358 | 205, 357 | addge01d 10201 |
. . . . . . . 8
                                                                                   
                                
                                                      |
359 | 356, 358 | mpbid 214 |
. . . . . . 7
                              
                                
                                                     |
360 | 158, 205,
296, 311, 359 | letrd 9792 |
. . . . . 6
  
                                
                                                     |
361 | 360, 295 | breqtrrd 4429 |
. . . . 5
  
              
      |
362 | 361 | adantr 467 |
. . . 4
 
              
                
      |
363 | | fzfid 12186 |
. . . . 5
 
              
      |
364 | 170 | adantlr 721 |
. . . . 5
                      
  
      |
365 | 169 | simprd 465 |
. . . . . 6
 
       
      |
366 | 365 | adantlr 721 |
. . . . 5
                      
  
      |
367 | 24 | adantr 467 |
. . . . . . . . . . . 12
 

            |
368 | 367 | sselda 3432 |
. . . . . . . . . . 11
              
  |
369 | 368 | nnred 10624 |
. . . . . . . . . 10
              
  |
370 | 31 | ad2antlr 733 |
. . . . . . . . . 10
              
  |
371 | | ltle 9722 |
. . . . . . . . . 10
 
 
   |
372 | 369, 370,
371 | syl2anc 667 |
. . . . . . . . 9
              

   |
373 | 368, 5 | syl6eleq 2539 |
. . . . . . . . . 10
              
      |
374 | | nnz 10959 |
. . . . . . . . . . 11
   |
375 | 374 | ad2antlr 733 |
. . . . . . . . . 10
              
  |
376 | | elfz5 11792 |
. . . . . . . . . 10
           
   |
377 | 373, 375,
376 | syl2anc 667 |
. . . . . . . . 9
              
        |
378 | 372, 377 | sylibrd 238 |
. . . . . . . 8
              

       |
379 | 378 | ralimdva 2796 |
. . . . . . 7
 

 
 
                            |
380 | 379 | impr 625 |
. . . . . 6
 
              
                  |
381 | | dfss3 3422 |
. . . . . 6
              
                  |
382 | 380, 381 | sylibr 216 |
. . . . 5
 
              
 
              |
383 | 363, 364,
366, 382 | fsumless 13856 |
. . . 4
 
              
              
   
               |
384 | 185, 190,
172, 362, 383 | letrd 9792 |
. . 3
 
              
                 |
385 | | eqidd 2452 |
. . . . . 6
                      
  
      
      |
386 | | simprl 764 |
. . . . . . 7
 
              
  |
387 | 386, 5 | syl6eleq 2539 |
. . . . . 6
 
              
      |
388 | 364 | recnd 9669 |
. . . . . 6
                      
  
      |
389 | 385, 387,
388 | fsumser 13796 |
. . . . 5
 
              
                
       |
390 | 99 | fveq1i 5866 |
. . . . 5
              |
391 | 389, 390 | syl6eqr 2503 |
. . . 4
 
              
                   |
392 | 181 | adantr 467 |
. . . . 5
 
              
  |
393 | | ffn 5728 |
. . . . . . . 8
       
  |
394 | 175, 393 | syl 17 |
. . . . . . 7
   |
395 | 394 | adantr 467 |
. . . . . 6
 
              
  |
396 | | fnfvelrn 6019 |
. . . . . 6
 
       |
397 | 395, 386,
396 | syl2anc 667 |
. . . . 5
 
              
      |
398 | | supxrub 11610 |
. . . . 5
          
      |
399 | 392, 397,
398 | syl2anc 667 |
. . . 4
 
              
          |
400 | 391, 399 | eqbrtrd 4423 |
. . 3
 
              
            
      |
401 | 160, 173,
184, 384, 400 | xrletrd 11459 |
. 2
 
              
        |
402 | 157, 401 | rexlimddv 2883 |
1
  
      |