Step | Hyp | Ref
| Expression |
1 | | mbfi1fseq.1 |
. . 3
 MblFn |
2 | | mbfi1fseq.2 |
. . 3
          |
3 | | mbfi1fseq.3 |
. . 3
 
                      |
4 | | mbfi1fseq.4 |
. . 3
 
     ![[,] [,]](_icc.gif)        
            |
5 | 1, 2, 3, 4 | mbfi1fseqlem4 22755 |
. 2
       |
6 | 1, 2, 3, 4 | mbfi1fseqlem5 22756 |
. . 3
 

      
        
     |
7 | 6 | ralrimiva 2809 |
. 2
    
        
         |
8 | | simpr 468 |
. . . . . . . 8
 

  |
9 | 8 | recnd 9687 |
. . . . . . 7
 

  |
10 | 9 | abscld 13575 |
. . . . . 6
 

      |
11 | 2 | ffvelrnda 6037 |
. . . . . . . 8
 

         |
12 | | elrege0 11764 |
. . . . . . . 8
       
            |
13 | 11, 12 | sylib 201 |
. . . . . . 7
 

            |
14 | 13 | simpld 466 |
. . . . . 6
 

      |
15 | 10, 14 | readdcld 9688 |
. . . . 5
 

            |
16 | | arch 10890 |
. . . . 5
                        |
17 | 15, 16 | syl 17 |
. . . 4
 

             |
18 | | eqid 2471 |
. . . . 5
         |
19 | | nnz 10983 |
. . . . . 6
   |
20 | 19 | ad2antrl 742 |
. . . . 5
                   |
21 | | nnuz 11218 |
. . . . . . . 8
     |
22 | | 1zzd 10992 |
. . . . . . . 8
 

  |
23 | | halfcn 10852 |
. . . . . . . . . 10
   |
24 | 23 | a1i 11 |
. . . . . . . . 9
 

    |
25 | | halfre 10851 |
. . . . . . . . . . . 12
   |
26 | | 0re 9661 |
. . . . . . . . . . . . 13
 |
27 | | halfgt0 10853 |
. . . . . . . . . . . . 13
   |
28 | 26, 25, 27 | ltleii 9775 |
. . . . . . . . . . . 12
   |
29 | | absid 13436 |
. . . . . . . . . . . 12
                 |
30 | 25, 28, 29 | mp2an 686 |
. . . . . . . . . . 11
         |
31 | | halflt1 10854 |
. . . . . . . . . . 11
   |
32 | 30, 31 | eqbrtri 4415 |
. . . . . . . . . 10
       |
33 | 32 | a1i 11 |
. . . . . . . . 9
 

        |
34 | 24, 33 | expcnv 13999 |
. . . . . . . 8
 


         |
35 | 14 | recnd 9687 |
. . . . . . . 8
 

      |
36 | | nnex 10637 |
. . . . . . . . . 10
 |
37 | 36 | mptex 6152 |
. . . . . . . . 9
               |
38 | 37 | a1i 11 |
. . . . . . . 8
 

                |
39 | | nnnn0 10900 |
. . . . . . . . . . 11
   |
40 | 39 | adantl 473 |
. . . . . . . . . 10
       |
41 | | oveq2 6316 |
. . . . . . . . . . 11
               |
42 | | eqid 2471 |
. . . . . . . . . . 11

                |
43 | | ovex 6336 |
. . . . . . . . . . 11
       |
44 | 41, 42, 43 | fvmpt 5963 |
. . . . . . . . . 10

                    |
45 | 40, 44 | syl 17 |
. . . . . . . . 9
                         |
46 | | expcl 12328 |
. . . . . . . . . 10
   
         |
47 | 23, 40, 46 | sylancr 676 |
. . . . . . . . 9
             |
48 | 45, 47 | eqeltrd 2549 |
. . . . . . . 8
                   |
49 | 41 | oveq2d 6324 |
. . . . . . . . . . 11
                           |
50 | | eqid 2471 |
. . . . . . . . . . 11
                             |
51 | | ovex 6336 |
. . . . . . . . . . 11
             |
52 | 49, 50, 51 | fvmpt 5963 |
. . . . . . . . . 10
                                 |
53 | 52 | adantl 473 |
. . . . . . . . 9
                                     |
54 | 45 | oveq2d 6324 |
. . . . . . . . 9
                                     |
55 | 53, 54 | eqtr4d 2508 |
. . . . . . . 8
                             
             |
56 | 21, 22, 34, 35, 38, 48, 55 | climsubc2 13779 |
. . . . . . 7
 

                      |
57 | 35 | subid1d 9994 |
. . . . . . 7
 

            |
58 | 56, 57 | breqtrd 4420 |
. . . . . 6
 

                    |
59 | 58 | adantr 472 |
. . . . 5
                                     |
60 | 36 | mptex 6152 |
. . . . . 6
           |
61 | 60 | a1i 11 |
. . . . 5
                             |
62 | | simprl 772 |
. . . . . . . 8
                   |
63 | | eluznn 11252 |
. . . . . . . 8
 
       |
64 | 62, 63 | sylan 479 |
. . . . . . 7
   
                     |
65 | 64, 52 | syl 17 |
. . . . . 6
   
                                                   |
66 | 14 | ad2antrr 740 |
. . . . . . 7
   
                         |
67 | 64, 39 | syl 17 |
. . . . . . . 8
   
                     |
68 | | reexpcl 12327 |
. . . . . . . 8
   
         |
69 | 25, 67, 68 | sylancr 676 |
. . . . . . 7
   
                           |
70 | 66, 69 | resubcld 10068 |
. . . . . 6
   
                                 |
71 | 65, 70 | eqeltrd 2549 |
. . . . 5
   
                                       |
72 | | fveq2 5879 |
. . . . . . . . 9
           |
73 | 72 | fveq1d 5881 |
. . . . . . . 8
                   |
74 | | eqid 2471 |
. . . . . . . 8
                     |
75 | | fvex 5889 |
. . . . . . . 8
         |
76 | 73, 74, 75 | fvmpt 5963 |
. . . . . . 7
                         |
77 | 64, 76 | syl 17 |
. . . . . 6
   
                                           |
78 | 5 | ad3antrrr 744 |
. . . . . . . . 9
   
                         |
79 | 78, 64 | ffvelrnd 6038 |
. . . . . . . 8
   
                         |
80 | | i1ff 22713 |
. . . . . . . 8
               |
81 | 79, 80 | syl 17 |
. . . . . . 7
   
                             |
82 | 8 | ad2antrr 740 |
. . . . . . 7
   
                     |
83 | 81, 82 | ffvelrnd 6038 |
. . . . . 6
   
                             |
84 | 77, 83 | eqeltrd 2549 |
. . . . 5
   
                                   |
85 | 35 | ad2antrr 740 |
. . . . . . . . . . 11
   
                         |
86 | | 2nn 10790 |
. . . . . . . . . . . . . 14
 |
87 | | nnexpcl 12323 |
. . . . . . . . . . . . . 14
 
       |
88 | 86, 67, 87 | sylancr 676 |
. . . . . . . . . . . . 13
   
                         |
89 | 88 | nnred 10646 |
. . . . . . . . . . . 12
   
                         |
90 | 89 | recnd 9687 |
. . . . . . . . . . 11
   
                         |
91 | 88 | nnne0d 10676 |
. . . . . . . . . . 11
   
                         |
92 | 85, 90, 91 | divcan4d 10411 |
. . . . . . . . . 10
   
                                         |
93 | 92 | eqcomd 2477 |
. . . . . . . . 9
   
                                         |
94 | | 2cnd 10704 |
. . . . . . . . . 10
   
                     |
95 | | 2ne0 10724 |
. . . . . . . . . . 11
 |
96 | 95 | a1i 11 |
. . . . . . . . . 10
   
                     |
97 | | eluzelz 11192 |
. . . . . . . . . . 11
    
  |
98 | 97 | adantl 473 |
. . . . . . . . . 10
   
                     |
99 | 94, 96, 98 | exprecd 12462 |
. . . . . . . . 9
   
                                 |
100 | 93, 99 | oveq12d 6326 |
. . . . . . . 8
   
                                                         |
101 | 66, 89 | remulcld 9689 |
. . . . . . . . . 10
   
                               |
102 | 101 | recnd 9687 |
. . . . . . . . 9
   
                               |
103 | | 1cnd 9677 |
. . . . . . . . 9
   
                     |
104 | 102, 103,
90, 91 | divsubdird 10444 |
. . . . . . . 8
   
                                                               |
105 | 100, 104 | eqtr4d 2508 |
. . . . . . 7
   
                                                   |
106 | | fllep1 12070 |
. . . . . . . . . 10
                                       |
107 | 101, 106 | syl 17 |
. . . . . . . . 9
   
                                               |
108 | | 1red 9676 |
. . . . . . . . . 10
   
                     |
109 | | reflcl 12065 |
. . . . . . . . . . 11
                           |
110 | 101, 109 | syl 17 |
. . . . . . . . . 10
   
                                   |
111 | 101, 108,
110 | lesubaddd 10231 |
. . . . . . . . 9
   
                                                                           |
112 | 107, 111 | mpbird 240 |
. . . . . . . 8
   
                                               |
113 | | peano2rem 9961 |
. . . . . . . . . 10
                         |
114 | 101, 113 | syl 17 |
. . . . . . . . 9
   
                                 |
115 | 88 | nngt0d 10675 |
. . . . . . . . 9
   
                         |
116 | | lediv1 10492 |
. . . . . . . . 9
                                                                                                           |
117 | 114, 110,
89, 115, 116 | syl112anc 1296 |
. . . . . . . 8
   
                                                                                       |
118 | 112, 117 | mpbid 215 |
. . . . . . 7
   
                                                           |
119 | 105, 118 | eqbrtrd 4416 |
. . . . . 6
   
                                                     |
120 | 1, 2, 3, 4 | mbfi1fseqlem2 22753 |
. . . . . . . . . 10
           ![[,] [,]](_icc.gif)                     |
121 | 64, 120 | syl 17 |
. . . . . . . . 9
   
                             ![[,] [,]](_icc.gif)        
            |
122 | 121 | fveq1d 5881 |
. . . . . . . 8
   
                                  ![[,] [,]](_icc.gif)        
               |
123 | | ovex 6336 |
. . . . . . . . . . 11
     |
124 | | vex 3034 |
. . . . . . . . . . 11
 |
125 | 123, 124 | ifex 3940 |
. . . . . . . . . 10
     
        |
126 | | c0ex 9655 |
. . . . . . . . . 10
 |
127 | 125, 126 | ifex 3940 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)                   |
128 | | eqid 2471 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)                         ![[,] [,]](_icc.gif)        
           |
129 | 128 | fvmpt2 5972 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)        
                 ![[,] [,]](_icc.gif)        
                  ![[,] [,]](_icc.gif)                    |
130 | 82, 127, 129 | sylancl 675 |
. . . . . . . 8
   
                          ![[,] [,]](_icc.gif)                           ![[,] [,]](_icc.gif)                    |
131 | 77, 122, 130 | 3eqtrd 2509 |
. . . . . . 7
   
                                      ![[,] [,]](_icc.gif)                    |
132 | 10 | ad2antrr 740 |
. . . . . . . . . . . 12
   
                         |
133 | 15 | ad2antrr 740 |
. . . . . . . . . . . 12
   
                               |
134 | 64 | nnred 10646 |
. . . . . . . . . . . 12
   
                     |
135 | 11 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
   
                            |
136 | 135, 12 | sylib 201 |
. . . . . . . . . . . . . 14
   
                               |
137 | 136 | simprd 470 |
. . . . . . . . . . . . 13
   
                         |
138 | 132, 66 | addge01d 10222 |
. . . . . . . . . . . . 13
   
                           
             |
139 | 137, 138 | mpbid 215 |
. . . . . . . . . . . 12
   
                      
            |
140 | 62 | adantr 472 |
. . . . . . . . . . . . . 14
   
                     |
141 | 140 | nnred 10646 |
. . . . . . . . . . . . 13
   
                     |
142 | | simplrr 779 |
. . . . . . . . . . . . . 14
   
                               |
143 | 133, 141,
142 | ltled 9800 |
. . . . . . . . . . . . 13
   
                            
  |
144 | | eluzle 11195 |
. . . . . . . . . . . . . 14
    
  |
145 | 144 | adantl 473 |
. . . . . . . . . . . . 13
   
                     |
146 | 133, 141,
134, 143, 145 | letrd 9809 |
. . . . . . . . . . . 12
   
                            
  |
147 | 132, 133,
134, 139, 146 | letrd 9809 |
. . . . . . . . . . 11
   
                      
  |
148 | 82, 134 | absled 13569 |
. . . . . . . . . . 11
   
                         
    |
149 | 147, 148 | mpbid 215 |
. . . . . . . . . 10
   
                        |
150 | 149 | simpld 466 |
. . . . . . . . 9
   
                      |
151 | 149 | simprd 470 |
. . . . . . . . 9
   
                     |
152 | 134 | renegcld 10067 |
. . . . . . . . . 10
   
                      |
153 | | elicc2 11724 |
. . . . . . . . . 10
        ![[,] [,]](_icc.gif) 
      |
154 | 152, 134,
153 | syl2anc 673 |
. . . . . . . . 9
   
                       ![[,] [,]](_icc.gif) 
      |
155 | 82, 150, 151, 154 | mpbir3and 1213 |
. . . . . . . 8
   
                      ![[,] [,]](_icc.gif)    |
156 | 155 | iftrued 3880 |
. . . . . . 7
   
                        ![[,] [,]](_icc.gif)                                 |
157 | | simpr 468 |
. . . . . . . . . . . . . . . 16
 
   |
158 | 157 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
 
           |
159 | | simpl 464 |
. . . . . . . . . . . . . . . 16
 
   |
160 | 159 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
 
           |
161 | 158, 160 | oveq12d 6326 |
. . . . . . . . . . . . . 14
 
                       |
162 | 161 | fveq2d 5883 |
. . . . . . . . . . . . 13
 
                               |
163 | 162, 160 | oveq12d 6326 |
. . . . . . . . . . . 12
 
                                           |
164 | | ovex 6336 |
. . . . . . . . . . . 12
                     |
165 | 163, 3, 164 | ovmpt2a 6446 |
. . . . . . . . . . 11
 
                           |
166 | 64, 82, 165 | syl2anc 673 |
. . . . . . . . . 10
   
                                             |
167 | 110, 88 | nndivred 10680 |
. . . . . . . . . . 11
   
                                         |
168 | | flle 12068 |
. . . . . . . . . . . . 13
                                     |
169 | 101, 168 | syl 17 |
. . . . . . . . . . . 12
   
                                             |
170 | | ledivmul2 10506 |
. . . . . . . . . . . . 13
                                                                                   |
171 | 110, 66, 89, 115, 170 | syl112anc 1296 |
. . . . . . . . . . . 12
   
                                                                       |
172 | 169, 171 | mpbird 240 |
. . . . . . . . . . 11
   
                                             |
173 | 9 | ad2antrr 740 |
. . . . . . . . . . . . . 14
   
                     |
174 | 173 | absge0d 13583 |
. . . . . . . . . . . . 13
   
                         |
175 | 66, 132 | addge02d 10223 |
. . . . . . . . . . . . 13
   
                                         |
176 | 174, 175 | mpbid 215 |
. . . . . . . . . . . 12
   
                                   |
177 | 66, 133, 134, 176, 146 | letrd 9809 |
. . . . . . . . . . 11
   
                         |
178 | 167, 66, 134, 172, 177 | letrd 9809 |
. . . . . . . . . 10
   
                                         |
179 | 166, 178 | eqbrtrd 4416 |
. . . . . . . . 9
   
                         |
180 | 179 | iftrued 3880 |
. . . . . . . 8
   
                                      |
181 | 180, 166 | eqtrd 2505 |
. . . . . . 7
   
                                                      |
182 | 131, 156,
181 | 3eqtrd 2509 |
. . . . . 6
   
                                                       |
183 | 119, 65, 182 | 3brtr4d 4426 |
. . . . 5
   
                                                     |
184 | 182, 172 | eqbrtrd 4416 |
. . . . 5
   
                                       |
185 | 18, 20, 59, 61, 71, 84, 183, 184 | climsqz 13781 |
. . . 4
                                 |
186 | 17, 185 | rexlimddv 2875 |
. . 3
 

                |
187 | 186 | ralrimiva 2809 |
. 2
  
               |
188 | 36 | mptex 6152 |
. . . 4
       ![[,] [,]](_icc.gif)         
           |
189 | 4, 188 | eqeltri 2545 |
. . 3
 |
190 | | feq1 5720 |
. . . 4
         
   |
191 | | fveq1 5878 |
. . . . . . 7
           |
192 | 191 | breq2d 4407 |
. . . . . 6
       
 
       |
193 | | fveq1 5878 |
. . . . . . 7
          
    |
194 | 191, 193 | breq12d 4408 |
. . . . . 6
                     
     |
195 | 192, 194 | anbi12d 725 |
. . . . 5
    
        
         
        
          |
196 | 195 | ralbidv 2829 |
. . . 4
  
  
        
       
  
        
          |
197 | 191 | fveq1d 5881 |
. . . . . . 7
                   |
198 | 197 | mpteq2dv 4483 |
. . . . . 6
                       |
199 | 198 | breq1d 4405 |
. . . . 5
               
                 |
200 | 199 | ralbidv 2829 |
. . . 4
  

            
                  |
201 | 190, 196,
200 | 3anbi123d 1365 |
. . 3
                           
              
    

           
                          |
202 | 189, 201 | spcev 3127 |
. 2
         
        
                                 
        
                         |
203 | 5, 7, 187, 202 | syl3anc 1292 |
1
           
        
                         |