Step | Hyp | Ref
| Expression |
1 | | nnuz 11194 |
. . 3
     |
2 | | 1zzd 10968 |
. . 3
   |
3 | | itg1climres.4 |
. . . . 5
   |
4 | | i1frn 22635 |
. . . . 5
   |
5 | 3, 4 | syl 17 |
. . . 4
   |
6 | | difss 3560 |
. . . 4

    |
7 | | ssfi 7792 |
. . . 4
     
       |
8 | 5, 6, 7 | sylancl 668 |
. . 3
       |
9 | | 1zzd 10968 |
. . . 4
 
       |
10 | | i1fima 22636 |
. . . . . . . . . . . 12
          |
11 | 3, 10 | syl 17 |
. . . . . . . . . . 11
          |
12 | 11 | ad2antrr 732 |
. . . . . . . . . 10
                  |
13 | | itg1climres.1 |
. . . . . . . . . . . 12
       |
14 | 13 | ffvelrnda 6022 |
. . . . . . . . . . 11
 

      |
15 | 14 | adantlr 721 |
. . . . . . . . . 10
               |
16 | | inmbl 22495 |
. . . . . . . . . 10
                             |
17 | 12, 15, 16 | syl2anc 667 |
. . . . . . . . 9
                        |
18 | | mblvol 22484 |
. . . . . . . . 9
             
                                     |
19 | 17, 18 | syl 17 |
. . . . . . . 8
                                              |
20 | | inss1 3652 |
. . . . . . . . . 10
            
        |
21 | 20 | a1i 11 |
. . . . . . . . 9
                               |
22 | | mblss 22485 |
. . . . . . . . . 10
                 |
23 | 12, 22 | syl 17 |
. . . . . . . . 9
                  |
24 | | mblvol 22484 |
. . . . . . . . . . 11
                                 |
25 | 12, 24 | syl 17 |
. . . . . . . . . 10
                                  |
26 | | i1fima2sn 22638 |
. . . . . . . . . . . 12
  
                 |
27 | 3, 26 | sylan 474 |
. . . . . . . . . . 11
 
                  |
28 | 27 | adantr 467 |
. . . . . . . . . 10
                      |
29 | 25, 28 | eqeltrrd 2530 |
. . . . . . . . 9
                       |
30 | | ovolsscl 22439 |
. . . . . . . . 9
                                                              |
31 | 21, 23, 29, 30 | syl3anc 1268 |
. . . . . . . 8
                             |
32 | 19, 31 | eqeltrd 2529 |
. . . . . . 7
                            |
33 | | eqid 2451 |
. . . . . . 7
                                       |
34 | 32, 33 | fmptd 6046 |
. . . . . 6
 
                              |
35 | | itg1climres.2 |
. . . . . . . . . . . . 13
 

            |
36 | 35 | adantlr 721 |
. . . . . . . . . . . 12
                     |
37 | | sslin 3658 |
. . . . . . . . . . . 12
        
                          
     |
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
                                 
     |
39 | 13 | adantr 467 |
. . . . . . . . . . . . . 14
 
           |
40 | | peano2nn 10621 |
. . . . . . . . . . . . . 14
     |
41 | | ffvelrn 6020 |
. . . . . . . . . . . . . 14
            
    |
42 | 39, 40, 41 | syl2an 480 |
. . . . . . . . . . . . 13
                 |
43 | | inmbl 22495 |
. . . . . . . . . . . . 13
                           
     |
44 | 12, 42, 43 | syl2anc 667 |
. . . . . . . . . . . 12
                    
     |
45 | | mblss 22485 |
. . . . . . . . . . . 12
            
  
              
  |
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
                    
     |
47 | | ovolss 22438 |
. . . . . . . . . . 11
                          
              
   
                                        |
48 | 38, 46, 47 | syl2anc 667 |
. . . . . . . . . 10
                                                 |
49 | | mblvol 22484 |
. . . . . . . . . . 11
            
  
              
                   
      |
50 | 44, 49 | syl 17 |
. . . . . . . . . 10
                                           
      |
51 | 48, 19, 50 | 3brtr4d 4433 |
. . . . . . . . 9
                                               |
52 | 51 | ralrimiva 2802 |
. . . . . . . 8
 
                                            |
53 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
54 | 53 | ineq2d 3634 |
. . . . . . . . . . . . 13
                             |
55 | 54 | fveq2d 5869 |
. . . . . . . . . . . 12
                                     |
56 | | fvex 5875 |
. . . . . . . . . . . 12
                  |
57 | 55, 33, 56 | fvmpt 5948 |
. . . . . . . . . . 11
                                           |
58 | | peano2nn 10621 |
. . . . . . . . . . . 12
     |
59 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
               |
60 | 59 | ineq2d 3634 |
. . . . . . . . . . . . . 14
                                 |
61 | 60 | fveq2d 5869 |
. . . . . . . . . . . . 13
                                         |
62 | | fvex 5875 |
. . . . . . . . . . . . 13
                    |
63 | 61, 33, 62 | fvmpt 5948 |
. . . . . . . . . . . 12
                                                 |
64 | 58, 63 | syl 17 |
. . . . . . . . . . 11
                                               |
65 | 57, 64 | breq12d 4415 |
. . . . . . . . . 10
                                                                                         |
66 | 65 | ralbiia 2818 |
. . . . . . . . 9
 
                                               
                                       |
67 | | oveq1 6297 |
. . . . . . . . . . . . . 14
       |
68 | 67 | fveq2d 5869 |
. . . . . . . . . . . . 13
               |
69 | 68 | ineq2d 3634 |
. . . . . . . . . . . 12
            
                    |
70 | 69 | fveq2d 5869 |
. . . . . . . . . . 11
                                         |
71 | 55, 70 | breq12d 4415 |
. . . . . . . . . 10
                                 
                                           |
72 | 71 | cbvralv 3019 |
. . . . . . . . 9
 
                                   
                                       |
73 | 66, 72 | bitr4i 256 |
. . . . . . . 8
 
                                               
                                
      |
74 | 52, 73 | sylibr 216 |
. . . . . . 7
 
                                                        |
75 | 74 | r19.21bi 2757 |
. . . . . 6
                                                           |
76 | | ovolss 22438 |
. . . . . . . . . . 11
                                                              |
77 | 20, 23, 76 | sylancr 669 |
. . . . . . . . . 10
                                         |
78 | 77, 19, 25 | 3brtr4d 4433 |
. . . . . . . . 9
                                       |
79 | 78 | ralrimiva 2802 |
. . . . . . . 8
 
                                    |
80 | 57 | breq1d 4412 |
. . . . . . . . . 10
                                   
                               |
81 | 80 | ralbiia 2818 |
. . . . . . . . 9
 
                                                                 |
82 | 55 | breq1d 4412 |
. . . . . . . . . 10
                             
                               |
83 | 82 | cbvralv 3019 |
. . . . . . . . 9
 
                                                           |
84 | 81, 83 | bitr4i 256 |
. . . . . . . 8
 
                                                                 |
85 | 79, 84 | sylibr 216 |
. . . . . . 7
 
                                          |
86 | | breq2 4406 |
. . . . . . . . 9
                                   
                                     |
87 | 86 | ralbidv 2827 |
. . . . . . . 8
                                    
                                      |
88 | 87 | rspcev 3150 |
. . . . . . 7
                                                                            |
89 | 27, 85, 88 | syl2anc 667 |
. . . . . 6
 
                                |
90 | 1, 9, 34, 75, 89 | climsup 13733 |
. . . . 5
 
                                                 |
91 | | eqid 2451 |
. . . . . . . 8
                               |
92 | 17, 91 | fmptd 6046 |
. . . . . . 7
 
                          |
93 | 38 | ralrimiva 2802 |
. . . . . . . 8
 
                              
     |
94 | | fvex 5875 |
. . . . . . . . . . . . 13
     |
95 | 94 | inex2 4545 |
. . . . . . . . . . . 12
              |
96 | 54, 91, 95 | fvmpt 5948 |
. . . . . . . . . . 11
                                   |
97 | | fvex 5875 |
. . . . . . . . . . . . . 14
       |
98 | 97 | inex2 4545 |
. . . . . . . . . . . . 13
                |
99 | 60, 91, 98 | fvmpt 5948 |
. . . . . . . . . . . 12
                                         |
100 | 58, 99 | syl 17 |
. . . . . . . . . . 11
                                       |
101 | 96, 100 | sseq12d 3461 |
. . . . . . . . . 10
                    
                    
            
                  |
102 | 101 | ralbiia 2818 |
. . . . . . . . 9
 
                                                                       |
103 | 54, 69 | sseq12d 3461 |
. . . . . . . . . 10
                          
  
            
                  |
104 | 103 | cbvralv 3019 |
. . . . . . . . 9
 
                        
  
             
                 |
105 | 102, 104 | bitr4i 256 |
. . . . . . . 8
 
                                                                 
     |
106 | 93, 105 | sylibr 216 |
. . . . . . 7
 
                        
                       |
107 | | volsup 22509 |
. . . . . . 7
                                        
                                               
                   |
108 | 92, 106, 107 | syl2anc 667 |
. . . . . 6
 
                              
                   |
109 | 96 | iuneq2i 4297 |
. . . . . . . . . 10
                                   |
110 | 54 | cbviunv 4317 |
. . . . . . . . . 10
                             |
111 | | iunin2 4342 |
. . . . . . . . . 10
                      
      |
112 | 109, 110,
111 | 3eqtr2i 2479 |
. . . . . . . . 9
                            
      |
113 | | ffn 5728 |
. . . . . . . . . . . . . 14
       |
114 | | fniunfv 6152 |
. . . . . . . . . . . . . 14
         |
115 | 13, 113, 114 | 3syl 18 |
. . . . . . . . . . . . 13
         |
116 | | itg1climres.3 |
. . . . . . . . . . . . 13
    |
117 | 115, 116 | eqtrd 2485 |
. . . . . . . . . . . 12
        |
118 | 117 | adantr 467 |
. . . . . . . . . . 11
 
            |
119 | 118 | ineq2d 3634 |
. . . . . . . . . 10
 
             
                |
120 | 11 | adantr 467 |
. . . . . . . . . . . 12
 
              |
121 | 120, 22 | syl 17 |
. . . . . . . . . . 11
 
              |
122 | | df-ss 3418 |
. . . . . . . . . . 11
                          |
123 | 121, 122 | sylib 200 |
. . . . . . . . . 10
 
             
         |
124 | 119, 123 | eqtrd 2485 |
. . . . . . . . 9
 
             
              |
125 | 112, 124 | syl5eq 2497 |
. . . . . . . 8
 
                                  |
126 | | ffn 5728 |
. . . . . . . . 9
                                     |
127 | | fniunfv 6152 |
. . . . . . . . 9
                                     
                |
128 | 92, 126, 127 | 3syl 18 |
. . . . . . . 8
 
                          
                |
129 | 125, 128 | eqtr3d 2487 |
. . . . . . 7
 
                              |
130 | 129 | fveq2d 5869 |
. . . . . 6
 
                                      |
131 | | frn 5735 |
. . . . . . . . 9
                        
                    |
132 | 34, 131 | syl 17 |
. . . . . . . 8
 
    
                  
  |
133 | | fdm 5733 |
. . . . . . . . . . 11
                        
                    |
134 | 34, 133 | syl 17 |
. . . . . . . . . 10
 
    
                     |
135 | | 1nn 10620 |
. . . . . . . . . . 11
 |
136 | | ne0i 3737 |
. . . . . . . . . . 11
   |
137 | 135, 136 | mp1i 13 |
. . . . . . . . . 10
 
       |
138 | 134, 137 | eqnetrd 2691 |
. . . . . . . . 9
 
    
                     |
139 | | dm0rn0 5051 |
. . . . . . . . . 10
                                         |
140 | 139 | necon3bii 2676 |
. . . . . . . . 9
                                         |
141 | 138, 140 | sylib 200 |
. . . . . . . 8
 
    
                     |
142 | | ffn 5728 |
. . . . . . . . . . 11
                                             |
143 | | breq1 4405 |
. . . . . . . . . . . 12
                                                   |
144 | 143 | ralrn 6025 |
. . . . . . . . . . 11
                   
 
                                               |
145 | 34, 142, 144 | 3syl 18 |
. . . . . . . . . 10
 
                                                      |
146 | 145 | rexbidv 2901 |
. . . . . . . . 9
 
                             
                          |
147 | 89, 146 | mpbird 236 |
. . . . . . . 8
 
                             |
148 | | supxrre 11613 |
. . . . . . . 8
                    

                                        
                      
                         |
149 | 132, 141,
147, 148 | syl3anc 1268 |
. . . . . . 7
 
                           
                         |
150 | | rnco2 5342 |
. . . . . . . . 9
                    
                |
151 | | eqidd 2452 |
. . . . . . . . . . 11
 
                                     |
152 | | volf 22483 |
. . . . . . . . . . . . 13
        |
153 | 152 | a1i 11 |
. . . . . . . . . . . 12
 
              |
154 | 153 | feqmptd 5918 |
. . . . . . . . . . 11
 
    
        |
155 | | fveq2 5865 |
. . . . . . . . . . 11
             
                       |
156 | 17, 151, 154, 155 | fmptco 6056 |
. . . . . . . . . 10
 
      
                                    |
157 | 156 | rneqd 5062 |
. . . . . . . . 9
 
    
                                      |
158 | 150, 157 | syl5reqr 2500 |
. . . . . . . 8
 
    
                                        |
159 | 158 | supeq1d 7960 |
. . . . . . 7
 
                           
                      
  |
160 | 149, 159 | eqtr3d 2487 |
. . . . . 6
 
                                                  
  |
161 | 108, 130,
160 | 3eqtr4d 2495 |
. . . . 5
 
                                         |
162 | 90, 161 | breqtrrd 4429 |
. . . 4
 
                                     |
163 | | i1ff 22634 |
. . . . . . . 8
       |
164 | | frn 5735 |
. . . . . . . 8
    
  |
165 | 3, 163, 164 | 3syl 18 |
. . . . . . 7
   |
166 | 165 | ssdifssd 3571 |
. . . . . 6
       |
167 | 166 | sselda 3432 |
. . . . 5
 
       |
168 | 167 | recnd 9669 |
. . . 4
 
       |
169 | | nnex 10615 |
. . . . . 6
 |
170 | 169 | mptex 6136 |
. . . . 5
                      |
171 | 170 | a1i 11 |
. . . 4
 
                            |
172 | 34 | ffvelrnda 6022 |
. . . . 5
                                  |
173 | 172 | recnd 9669 |
. . . 4
                                  |
174 | 55 | oveq2d 6306 |
. . . . . . 7
                                         |
175 | | eqid 2451 |
. . . . . . 7
                                           |
176 | | ovex 6318 |
. . . . . . 7
                    |
177 | 174, 175,
176 | fvmpt 5948 |
. . . . . 6
                                               |
178 | 57 | oveq2d 6306 |
. . . . . 6
                                               |
179 | 177, 178 | eqtr4d 2488 |
. . . . 5
                                                     |
180 | 179 | adantl 468 |
. . . 4
                                                             |
181 | 1, 9, 162, 168, 171, 173, 180 | climmulc2 13700 |
. . 3
 
                                         |
182 | 169 | mptex 6136 |
. . . 4
       |
183 | 182 | a1i 11 |
. . 3
         |
184 | 167 | adantr 467 |
. . . . . . . 8
           |
185 | 184, 32 | remulcld 9671 |
. . . . . . 7
                              |
186 | 185, 175 | fmptd 6046 |
. . . . . 6
 
                                |
187 | 186 | ffvelrnda 6022 |
. . . . 5
                                    |
188 | 187 | recnd 9669 |
. . . 4
                                    |
189 | 188 | anasss 653 |
. . 3
 
                                  |
190 | 3 | adantr 467 |
. . . . . . . . 9
 

  |
191 | | itg1climres.5 |
. . . . . . . . . 10
                |
192 | 191 | i1fres 22663 |
. . . . . . . . 9
         |
193 | 190, 14, 192 | syl2anc 667 |
. . . . . . . 8
 

  |
194 | 8 | adantr 467 |
. . . . . . . 8
 


     |
195 | | ffn 5728 |
. . . . . . . . . . . . . 14
       |
196 | 3, 163, 195 | 3syl 18 |
. . . . . . . . . . . . 13
   |
197 | 196 | adantr 467 |
. . . . . . . . . . . 12
 

  |
198 | | fnfvelrn 6019 |
. . . . . . . . . . . 12
 
       |
199 | 197, 198 | sylan 474 |
. . . . . . . . . . 11
           |
200 | | i1f0rn 22640 |
. . . . . . . . . . . . 13
   |
201 | 3, 200 | syl 17 |
. . . . . . . . . . . 12
   |
202 | 201 | ad2antrr 732 |
. . . . . . . . . . 11
       |
203 | 199, 202 | ifcld 3924 |
. . . . . . . . . 10
      
             |
204 | 203, 191 | fmptd 6046 |
. . . . . . . . 9
 

      |
205 | | frn 5735 |
. . . . . . . . 9
       |
206 | | ssdif 3568 |
. . . . . . . . 9


         |
207 | 204, 205,
206 | 3syl 18 |
. . . . . . . 8
 


         |
208 | 165 | adantr 467 |
. . . . . . . . 9
 

  |
209 | 208 | ssdifd 3569 |
. . . . . . . 8
 


         |
210 | | itg1val2 22642 |
. . . . . . . 8
                                                  |
211 | 193, 194,
207, 209, 210 | syl13anc 1270 |
. . . . . . 7
 

    
                    |
212 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . 21
     |
213 | | c0ex 9637 |
. . . . . . . . . . . . . . . . . . . . 21
 |
214 | 212, 213 | ifex 3949 |
. . . . . . . . . . . . . . . . . . . 20
              |
215 | 191 | fvmpt2 5957 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
216 | 214, 215 | mpan2 677 |
. . . . . . . . . . . . . . . . . . 19
                    |
217 | 216 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
   

    
                    |
218 | 217 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . 17
   

    
                      |
219 | | eldifsni 4098 |
. . . . . . . . . . . . . . . . . . . . 21
       |
220 | 219 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . 20
   

    
   |
221 | | neeq1 2686 |
. . . . . . . . . . . . . . . . . . . 20
                               |
222 | 220, 221 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . . . . 19
   

    
              
                |
223 | | iffalse 3890 |
. . . . . . . . . . . . . . . . . . . 20
                    |
224 | 223 | necon1ai 2651 |
. . . . . . . . . . . . . . . . . . 19
             
      |
225 | 222, 224 | syl6 34 |
. . . . . . . . . . . . . . . . . 18
   

    
              
       |
226 | 225 | pm4.71rd 641 |
. . . . . . . . . . . . . . . . 17
   

    
                   
                 |
227 | 218, 226 | bitrd 257 |
. . . . . . . . . . . . . . . 16
   

    
                            |
228 | | iftrue 3887 |
. . . . . . . . . . . . . . . . . . 19
      
                 |
229 | 228 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . 18
                  
       |
230 | 229 | pm5.32i 643 |
. . . . . . . . . . . . . . . . 17
                                |
231 | | ancom 452 |
. . . . . . . . . . . . . . . . 17
          
    
       |
232 | 230, 231 | bitri 253 |
. . . . . . . . . . . . . . . 16
                                |
233 | 227, 232 | syl6bb 265 |
. . . . . . . . . . . . . . 15
   

    
                   |
234 | 233 | pm5.32da 647 |
. . . . . . . . . . . . . 14
        
      
               |
235 | | anass 655 |
. . . . . . . . . . . . . 14
                           |
236 | 234, 235 | syl6bbr 267 |
. . . . . . . . . . . . 13
        
      
      
        |
237 | | i1ff 22634 |
. . . . . . . . . . . . . . . 16
       |
238 | | ffn 5728 |
. . . . . . . . . . . . . . . 16
       |
239 | 193, 237,
238 | 3syl 18 |
. . . . . . . . . . . . . . 15
 

  |
240 | 239 | adantr 467 |
. . . . . . . . . . . . . 14
        
  |
241 | | fniniseg 6003 |
. . . . . . . . . . . . . 14
        
         |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . . 13
        
                 |
243 | | elin 3617 |
. . . . . . . . . . . . . 14
                             |
244 | 197 | adantr 467 |
. . . . . . . . . . . . . . . 16
        
  |
245 | | fniniseg 6003 |
. . . . . . . . . . . . . . . 16
        
         |
246 | 244, 245 | syl 17 |
. . . . . . . . . . . . . . 15
        
                 |
247 | 246 | anbi1d 711 |
. . . . . . . . . . . . . 14
        
             
      
        |
248 | 243, 247 | syl5bb 261 |
. . . . . . . . . . . . 13
        
             
      
        |
249 | 236, 242,
248 | 3bitr4d 289 |
. . . . . . . . . . . 12
        
                        |
250 | 249 | alrimiv 1773 |
. . . . . . . . . . 11
        
         
                |
251 | | nfmpt1 4492 |
. . . . . . . . . . . . . . 15
                  |
252 | 191, 251 | nfcxfr 2590 |
. . . . . . . . . . . . . 14
   |
253 | 252 | nfcnv 5013 |
. . . . . . . . . . . . 13
    |
254 | | nfcv 2592 |
. . . . . . . . . . . . 13
     |
255 | 253, 254 | nfima 5176 |
. . . . . . . . . . . 12
          |
256 | | nfcv 2592 |
. . . . . . . . . . . 12
                |
257 | 255, 256 | cleqf 2617 |
. . . . . . . . . . 11
                    
         
                |
258 | 250, 257 | sylibr 216 |
. . . . . . . . . 10
        
                      |
259 | 258 | fveq2d 5869 |
. . . . . . . . 9
        
                              |
260 | 259 | oveq2d 6306 |
. . . . . . . 8
        
                                  |
261 | 260 | sumeq2dv 13769 |
. . . . . . 7
 

                   
                          |
262 | 211, 261 | eqtrd 2485 |
. . . . . 6
 

    
                          |
263 | 262 | mpteq2dva 4489 |
. . . . 5
                                    |
264 | 263 | fveq1d 5867 |
. . . 4
              
                             |
265 | 174 | sumeq2sdv 13770 |
. . . . . 6
                                                     |
266 | | eqid 2451 |
. . . . . 6
                                                       |
267 | | sumex 13754 |
. . . . . 6
                          |
268 | 265, 266,
267 | fvmpt 5948 |
. . . . 5
    
                                                      |
269 | 177 | sumeq2sdv 13770 |
. . . . 5
                                                           |
270 | 268, 269 | eqtr4d 2488 |
. . . 4
    
                                                            |
271 | 264, 270 | sylan9eq 2505 |
. . 3
 

                                           |
272 | 1, 2, 8, 181, 183, 189, 271 | climfsum 13880 |
. 2
                            |
273 | | itg1val 22641 |
. . 3
                          |
274 | 3, 273 | syl 17 |
. 2
                          |
275 | 272, 274 | breqtrrd 4429 |
1
             |