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 22669 |
. 2
       |
6 | 1, 2, 3, 4 | mbfi1fseqlem5 22670 |
. . 3
 

      
        
     |
7 | 6 | ralrimiva 2801 |
. 2
    
        
         |
8 | | simpr 463 |
. . . . . . . 8
 

  |
9 | 8 | recnd 9666 |
. . . . . . 7
 

  |
10 | 9 | abscld 13491 |
. . . . . 6
 

      |
11 | 2 | ffvelrnda 6020 |
. . . . . . . 8
 

         |
12 | | elrege0 11735 |
. . . . . . . 8
       
            |
13 | 11, 12 | sylib 200 |
. . . . . . 7
 

            |
14 | 13 | simpld 461 |
. . . . . 6
 

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

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

             |
18 | | eqid 2450 |
. . . . 5
         |
19 | | nnz 10956 |
. . . . . 6
   |
20 | 19 | ad2antrl 733 |
. . . . 5
                   |
21 | | nnuz 11191 |
. . . . . . . 8
     |
22 | | 1zzd 10965 |
. . . . . . . 8
 

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

    |
25 | | halfre 10825 |
. . . . . . . . . . . 12
   |
26 | | 0re 9640 |
. . . . . . . . . . . . 13
 |
27 | | halfgt0 10827 |
. . . . . . . . . . . . 13
   |
28 | 26, 25, 27 | ltleii 9754 |
. . . . . . . . . . . 12
   |
29 | | absid 13352 |
. . . . . . . . . . . 12
                 |
30 | 25, 28, 29 | mp2an 677 |
. . . . . . . . . . 11
         |
31 | | halflt1 10828 |
. . . . . . . . . . 11
   |
32 | 30, 31 | eqbrtri 4421 |
. . . . . . . . . 10
       |
33 | 32 | a1i 11 |
. . . . . . . . 9
 

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


         |
35 | 14 | recnd 9666 |
. . . . . . . 8
 

      |
36 | | nnex 10612 |
. . . . . . . . . 10
 |
37 | 36 | mptex 6134 |
. . . . . . . . 9
               |
38 | 37 | a1i 11 |
. . . . . . . 8
 

                |
39 | | nnnn0 10873 |
. . . . . . . . . . 11
   |
40 | 39 | adantl 468 |
. . . . . . . . . 10
       |
41 | | oveq2 6296 |
. . . . . . . . . . 11
               |
42 | | eqid 2450 |
. . . . . . . . . . 11

                |
43 | | ovex 6316 |
. . . . . . . . . . 11
       |
44 | 41, 42, 43 | fvmpt 5946 |
. . . . . . . . . 10

                    |
45 | 40, 44 | syl 17 |
. . . . . . . . 9
                         |
46 | | expcl 12287 |
. . . . . . . . . 10
   
         |
47 | 23, 40, 46 | sylancr 668 |
. . . . . . . . 9
             |
48 | 45, 47 | eqeltrd 2528 |
. . . . . . . 8
                   |
49 | 41 | oveq2d 6304 |
. . . . . . . . . . 11
                           |
50 | | eqid 2450 |
. . . . . . . . . . 11
                             |
51 | | ovex 6316 |
. . . . . . . . . . 11
             |
52 | 49, 50, 51 | fvmpt 5946 |
. . . . . . . . . 10
                                 |
53 | 52 | adantl 468 |
. . . . . . . . 9
                                     |
54 | 45 | oveq2d 6304 |
. . . . . . . . 9
                                     |
55 | 53, 54 | eqtr4d 2487 |
. . . . . . . 8
                             
             |
56 | 21, 22, 34, 35, 38, 48, 55 | climsubc2 13695 |
. . . . . . 7
 

                      |
57 | 35 | subid1d 9972 |
. . . . . . 7
 

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

                    |
59 | 58 | adantr 467 |
. . . . 5
                                     |
60 | 36 | mptex 6134 |
. . . . . 6
           |
61 | 60 | a1i 11 |
. . . . 5
                             |
62 | | simprl 763 |
. . . . . . . 8
                   |
63 | | eluznn 11226 |
. . . . . . . 8
 
       |
64 | 62, 63 | sylan 474 |
. . . . . . 7
   
                     |
65 | 64, 52 | syl 17 |
. . . . . 6
   
                                                   |
66 | 14 | ad2antrr 731 |
. . . . . . 7
   
                         |
67 | 64, 39 | syl 17 |
. . . . . . . 8
   
                     |
68 | | reexpcl 12286 |
. . . . . . . 8
   
         |
69 | 25, 67, 68 | sylancr 668 |
. . . . . . 7
   
                           |
70 | 66, 69 | resubcld 10044 |
. . . . . 6
   
                                 |
71 | 65, 70 | eqeltrd 2528 |
. . . . 5
   
                                       |
72 | | fveq2 5863 |
. . . . . . . . 9
           |
73 | 72 | fveq1d 5865 |
. . . . . . . 8
                   |
74 | | eqid 2450 |
. . . . . . . 8
                     |
75 | | fvex 5873 |
. . . . . . . 8
         |
76 | 73, 74, 75 | fvmpt 5946 |
. . . . . . 7
                         |
77 | 64, 76 | syl 17 |
. . . . . 6
   
                                           |
78 | 5 | ad3antrrr 735 |
. . . . . . . . 9
   
                         |
79 | 78, 64 | ffvelrnd 6021 |
. . . . . . . 8
   
                         |
80 | | i1ff 22627 |
. . . . . . . 8
               |
81 | 79, 80 | syl 17 |
. . . . . . 7
   
                             |
82 | 8 | ad2antrr 731 |
. . . . . . 7
   
                     |
83 | 81, 82 | ffvelrnd 6021 |
. . . . . 6
   
                             |
84 | 77, 83 | eqeltrd 2528 |
. . . . 5
   
                                   |
85 | 35 | ad2antrr 731 |
. . . . . . . . . . 11
   
                         |
86 | | 2nn 10764 |
. . . . . . . . . . . . . 14
 |
87 | | nnexpcl 12282 |
. . . . . . . . . . . . . 14
 
       |
88 | 86, 67, 87 | sylancr 668 |
. . . . . . . . . . . . 13
   
                         |
89 | 88 | nnred 10621 |
. . . . . . . . . . . 12
   
                         |
90 | 89 | recnd 9666 |
. . . . . . . . . . 11
   
                         |
91 | 88 | nnne0d 10651 |
. . . . . . . . . . 11
   
                         |
92 | 85, 90, 91 | divcan4d 10386 |
. . . . . . . . . 10
   
                                         |
93 | 92 | eqcomd 2456 |
. . . . . . . . 9
   
                                         |
94 | | 2cnd 10679 |
. . . . . . . . . 10
   
                     |
95 | | 2ne0 10699 |
. . . . . . . . . . 11
 |
96 | 95 | a1i 11 |
. . . . . . . . . 10
   
                     |
97 | | eluzelz 11165 |
. . . . . . . . . . 11
    
  |
98 | 97 | adantl 468 |
. . . . . . . . . 10
   
                     |
99 | 94, 96, 98 | exprecd 12421 |
. . . . . . . . 9
   
                                 |
100 | 93, 99 | oveq12d 6306 |
. . . . . . . 8
   
                                                         |
101 | 66, 89 | remulcld 9668 |
. . . . . . . . . 10
   
                               |
102 | 101 | recnd 9666 |
. . . . . . . . 9
   
                               |
103 | | 1cnd 9656 |
. . . . . . . . 9
   
                     |
104 | 102, 103,
90, 91 | divsubdird 10419 |
. . . . . . . 8
   
                                                               |
105 | 100, 104 | eqtr4d 2487 |
. . . . . . 7
   
                                                   |
106 | | fllep1 12034 |
. . . . . . . . . 10
                                       |
107 | 101, 106 | syl 17 |
. . . . . . . . 9
   
                                               |
108 | | 1red 9655 |
. . . . . . . . . 10
   
                     |
109 | | reflcl 12029 |
. . . . . . . . . . 11
                           |
110 | 101, 109 | syl 17 |
. . . . . . . . . 10
   
                                   |
111 | 101, 108,
110 | lesubaddd 10207 |
. . . . . . . . 9
   
                                                                           |
112 | 107, 111 | mpbird 236 |
. . . . . . . 8
   
                                               |
113 | | peano2rem 9938 |
. . . . . . . . . 10
                         |
114 | 101, 113 | syl 17 |
. . . . . . . . 9
   
                                 |
115 | 88 | nngt0d 10650 |
. . . . . . . . 9
   
                         |
116 | | lediv1 10467 |
. . . . . . . . 9
                                                                                                           |
117 | 114, 110,
89, 115, 116 | syl112anc 1271 |
. . . . . . . 8
   
                                                                                       |
118 | 112, 117 | mpbid 214 |
. . . . . . 7
   
                                                           |
119 | 105, 118 | eqbrtrd 4422 |
. . . . . 6
   
                                                     |
120 | 1, 2, 3, 4 | mbfi1fseqlem2 22667 |
. . . . . . . . . 10
           ![[,] [,]](_icc.gif)                     |
121 | 64, 120 | syl 17 |
. . . . . . . . 9
   
                             ![[,] [,]](_icc.gif)        
            |
122 | 121 | fveq1d 5865 |
. . . . . . . 8
   
                                  ![[,] [,]](_icc.gif)        
               |
123 | | ovex 6316 |
. . . . . . . . . . 11
     |
124 | | vex 3047 |
. . . . . . . . . . 11
 |
125 | 123, 124 | ifex 3948 |
. . . . . . . . . 10
     
        |
126 | | c0ex 9634 |
. . . . . . . . . 10
 |
127 | 125, 126 | ifex 3948 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)                   |
128 | | eqid 2450 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)                         ![[,] [,]](_icc.gif)        
           |
129 | 128 | fvmpt2 5955 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)        
                 ![[,] [,]](_icc.gif)        
                  ![[,] [,]](_icc.gif)                    |
130 | 82, 127, 129 | sylancl 667 |
. . . . . . . 8
   
                          ![[,] [,]](_icc.gif)                           ![[,] [,]](_icc.gif)                    |
131 | 77, 122, 130 | 3eqtrd 2488 |
. . . . . . 7
   
                                      ![[,] [,]](_icc.gif)                    |
132 | 10 | ad2antrr 731 |
. . . . . . . . . . . 12
   
                         |
133 | 15 | ad2antrr 731 |
. . . . . . . . . . . 12
   
                               |
134 | 64 | nnred 10621 |
. . . . . . . . . . . 12
   
                     |
135 | 11 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
   
                            |
136 | 135, 12 | sylib 200 |
. . . . . . . . . . . . . 14
   
                               |
137 | 136 | simprd 465 |
. . . . . . . . . . . . 13
   
                         |
138 | 132, 66 | addge01d 10198 |
. . . . . . . . . . . . 13
   
                           
             |
139 | 137, 138 | mpbid 214 |
. . . . . . . . . . . 12
   
                      
            |
140 | 62 | adantr 467 |
. . . . . . . . . . . . . 14
   
                     |
141 | 140 | nnred 10621 |
. . . . . . . . . . . . 13
   
                     |
142 | | simplrr 770 |
. . . . . . . . . . . . . 14
   
                               |
143 | 133, 141,
142 | ltled 9780 |
. . . . . . . . . . . . 13
   
                            
  |
144 | | eluzle 11168 |
. . . . . . . . . . . . . 14
    
  |
145 | 144 | adantl 468 |
. . . . . . . . . . . . 13
   
                     |
146 | 133, 141,
134, 143, 145 | letrd 9789 |
. . . . . . . . . . . 12
   
                            
  |
147 | 132, 133,
134, 139, 146 | letrd 9789 |
. . . . . . . . . . 11
   
                      
  |
148 | 82, 134 | absled 13485 |
. . . . . . . . . . 11
   
                         
    |
149 | 147, 148 | mpbid 214 |
. . . . . . . . . 10
   
                        |
150 | 149 | simpld 461 |
. . . . . . . . 9
   
                      |
151 | 149 | simprd 465 |
. . . . . . . . 9
   
                     |
152 | 134 | renegcld 10043 |
. . . . . . . . . 10
   
                      |
153 | | elicc2 11696 |
. . . . . . . . . 10
        ![[,] [,]](_icc.gif) 
      |
154 | 152, 134,
153 | syl2anc 666 |
. . . . . . . . 9
   
                       ![[,] [,]](_icc.gif) 
      |
155 | 82, 150, 151, 154 | mpbir3and 1190 |
. . . . . . . 8
   
                      ![[,] [,]](_icc.gif)    |
156 | 155 | iftrued 3888 |
. . . . . . 7
   
                        ![[,] [,]](_icc.gif)                                 |
157 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
   |
158 | 157 | fveq2d 5867 |
. . . . . . . . . . . . . . 15
 
           |
159 | | simpl 459 |
. . . . . . . . . . . . . . . 16
 
   |
160 | 159 | oveq2d 6304 |
. . . . . . . . . . . . . . 15
 
           |
161 | 158, 160 | oveq12d 6306 |
. . . . . . . . . . . . . 14
 
                       |
162 | 161 | fveq2d 5867 |
. . . . . . . . . . . . 13
 
                               |
163 | 162, 160 | oveq12d 6306 |
. . . . . . . . . . . 12
 
                                           |
164 | | ovex 6316 |
. . . . . . . . . . . 12
                     |
165 | 163, 3, 164 | ovmpt2a 6424 |
. . . . . . . . . . 11
 
                           |
166 | 64, 82, 165 | syl2anc 666 |
. . . . . . . . . 10
   
                                             |
167 | 110, 88 | nndivred 10655 |
. . . . . . . . . . 11
   
                                         |
168 | | flle 12032 |
. . . . . . . . . . . . 13
                                     |
169 | 101, 168 | syl 17 |
. . . . . . . . . . . 12
   
                                             |
170 | | ledivmul2 10481 |
. . . . . . . . . . . . 13
                                                                                   |
171 | 110, 66, 89, 115, 170 | syl112anc 1271 |
. . . . . . . . . . . 12
   
                                                                       |
172 | 169, 171 | mpbird 236 |
. . . . . . . . . . 11
   
                                             |
173 | 9 | ad2antrr 731 |
. . . . . . . . . . . . . 14
   
                     |
174 | 173 | absge0d 13499 |
. . . . . . . . . . . . 13
   
                         |
175 | 66, 132 | addge02d 10199 |
. . . . . . . . . . . . 13
   
                                         |
176 | 174, 175 | mpbid 214 |
. . . . . . . . . . . 12
   
                                   |
177 | 66, 133, 134, 176, 146 | letrd 9789 |
. . . . . . . . . . 11
   
                         |
178 | 167, 66, 134, 172, 177 | letrd 9789 |
. . . . . . . . . 10
   
                                         |
179 | 166, 178 | eqbrtrd 4422 |
. . . . . . . . 9
   
                         |
180 | 179 | iftrued 3888 |
. . . . . . . 8
   
                                      |
181 | 180, 166 | eqtrd 2484 |
. . . . . . 7
   
                                                      |
182 | 131, 156,
181 | 3eqtrd 2488 |
. . . . . 6
   
                                                       |
183 | 119, 65, 182 | 3brtr4d 4432 |
. . . . 5
   
                                                     |
184 | 182, 172 | eqbrtrd 4422 |
. . . . 5
   
                                       |
185 | 18, 20, 59, 61, 71, 84, 183, 184 | climsqz 13697 |
. . . 4
                                 |
186 | 17, 185 | rexlimddv 2882 |
. . 3
 

                |
187 | 186 | ralrimiva 2801 |
. 2
  
               |
188 | 36 | mptex 6134 |
. . . 4
       ![[,] [,]](_icc.gif)         
           |
189 | 4, 188 | eqeltri 2524 |
. . 3
 |
190 | | feq1 5708 |
. . . 4
         
   |
191 | | fveq1 5862 |
. . . . . . 7
           |
192 | 191 | breq2d 4413 |
. . . . . 6
       
 
       |
193 | | fveq1 5862 |
. . . . . . 7
          
    |
194 | 191, 193 | breq12d 4414 |
. . . . . 6
                     
     |
195 | 192, 194 | anbi12d 716 |
. . . . 5
    
        
         
        
          |
196 | 195 | ralbidv 2826 |
. . . 4
  
  
        
       
  
        
          |
197 | 191 | fveq1d 5865 |
. . . . . . 7
                   |
198 | 197 | mpteq2dv 4489 |
. . . . . 6
                       |
199 | 198 | breq1d 4411 |
. . . . 5
               
                 |
200 | 199 | ralbidv 2826 |
. . . 4
  

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

           
                          |
202 | 189, 201 | spcev 3140 |
. 2
         
        
                                 
        
                         |
203 | 5, 7, 187, 202 | syl3anc 1267 |
1
           
        
                         |