Proof of Theorem mbfi1fseqlem3
Step | Hyp | Ref
| Expression |
1 | | 0re 9492 |
. . . . . . . . . . . . . . . . . . . 20
 |
2 | | pnfxr 11198 |
. . . . . . . . . . . . . . . . . . . 20
 |
3 | | icossre 11482 |
. . . . . . . . . . . . . . . . . . . 20
    
   |
4 | 1, 2, 3 | mp2an 672 |
. . . . . . . . . . . . . . . . . . 19
    |
5 | | mbfi1fseq.2 |
. . . . . . . . . . . . . . . . . . . 20
          |
6 | | simpr 461 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
7 | | ffvelrn 5945 |
. . . . . . . . . . . . . . . . . . . 20
        
          |
8 | 5, 6, 7 | syl2an 477 |
. . . . . . . . . . . . . . . . . . 19
 
            |
9 | 4, 8 | sseldi 3457 |
. . . . . . . . . . . . . . . . . 18
 
         |
10 | | 2nn 10585 |
. . . . . . . . . . . . . . . . . . . . 21
 |
11 | | nnnn0 10692 |
. . . . . . . . . . . . . . . . . . . . 21
   |
12 | | nnexpcl 11990 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
13 | 10, 11, 12 | sylancr 663 |
. . . . . . . . . . . . . . . . . . . 20
       |
14 | 13 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . 19
 
         |
15 | 14 | nnred 10443 |
. . . . . . . . . . . . . . . . . 18
 
         |
16 | 9, 15 | remulcld 9520 |
. . . . . . . . . . . . . . . . 17
 
               |
17 | | reflcl 11758 |
. . . . . . . . . . . . . . . . 17
                           |
18 | 16, 17 | syl 16 |
. . . . . . . . . . . . . . . 16
 
                   |
19 | 18, 14 | nndivred 10476 |
. . . . . . . . . . . . . . 15
 
                         |
20 | 19 | ralrimivva 2908 |
. . . . . . . . . . . . . 14
                         |
21 | | mbfi1fseq.3 |
. . . . . . . . . . . . . . 15
 
                      |
22 | 21 | fmpt2 6746 |
. . . . . . . . . . . . . 14
 
                             |
23 | 20, 22 | sylib 196 |
. . . . . . . . . . . . 13
         |
24 | | fovrn 6338 |
. . . . . . . . . . . . 13
               |
25 | 23, 24 | syl3an1 1252 |
. . . . . . . . . . . 12
 
       |
26 | 25 | 3expa 1188 |
. . . . . . . . . . 11
           |
27 | | nnre 10435 |
. . . . . . . . . . . 12
   |
28 | 27 | ad2antlr 726 |
. . . . . . . . . . 11
       |
29 | | nnnn0 10692 |
. . . . . . . . . . . . . 14
   |
30 | | nnexpcl 11990 |
. . . . . . . . . . . . . 14
 
       |
31 | 10, 29, 30 | sylancr 663 |
. . . . . . . . . . . . 13
       |
32 | 31 | ad2antlr 726 |
. . . . . . . . . . . 12
           |
33 | | nnre 10435 |
. . . . . . . . . . . . 13
           |
34 | | nngt0 10457 |
. . . . . . . . . . . . 13
           |
35 | 33, 34 | jca 532 |
. . . . . . . . . . . 12
                 |
36 | 32, 35 | syl 16 |
. . . . . . . . . . 11
                 |
37 | | lemul1 10287 |
. . . . . . . . . . 11
     
                         
         |
38 | 26, 28, 36, 37 | syl3anc 1219 |
. . . . . . . . . 10
         
          
        |
39 | 38 | biimpa 484 |
. . . . . . . . 9
   

     
          
       |
40 | | simplr 754 |
. . . . . . . . . . . . . . . 16
       |
41 | 40 | adantr 465 |
. . . . . . . . . . . . . . 15
   

     
  |
42 | | simplr 754 |
. . . . . . . . . . . . . . 15
   

     
  |
43 | | simpr 461 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
44 | 43 | fveq2d 5798 |
. . . . . . . . . . . . . . . . . . 19
 
           |
45 | | simpl 457 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
46 | 45 | oveq2d 6211 |
. . . . . . . . . . . . . . . . . . 19
 
           |
47 | 44, 46 | oveq12d 6213 |
. . . . . . . . . . . . . . . . . 18
 
                       |
48 | 47 | fveq2d 5798 |
. . . . . . . . . . . . . . . . 17
 
                               |
49 | 48, 46 | oveq12d 6213 |
. . . . . . . . . . . . . . . 16
 
                                           |
50 | | ovex 6220 |
. . . . . . . . . . . . . . . 16
                     |
51 | 49, 21, 50 | ovmpt2a 6326 |
. . . . . . . . . . . . . . 15
 
                           |
52 | 41, 42, 51 | syl2anc 661 |
. . . . . . . . . . . . . 14
   

     
                          |
53 | 52 | oveq1d 6210 |
. . . . . . . . . . . . 13
   

     
                                      |
54 | 5 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
 

         |
55 | 54 | ffvelrnda 5947 |
. . . . . . . . . . . . . . . . . . . 20
              |
56 | | elrege0 11504 |
. . . . . . . . . . . . . . . . . . . 20
       
            |
57 | 55, 56 | sylib 196 |
. . . . . . . . . . . . . . . . . . 19
                 |
58 | 57 | simpld 459 |
. . . . . . . . . . . . . . . . . 18
           |
59 | 32 | nnred 10443 |
. . . . . . . . . . . . . . . . . 18
           |
60 | 58, 59 | remulcld 9520 |
. . . . . . . . . . . . . . . . 17
                 |
61 | 32 | nnnn0d 10742 |
. . . . . . . . . . . . . . . . . . 19
           |
62 | 61 | nn0ge0d 10745 |
. . . . . . . . . . . . . . . . . 18
           |
63 | | mulge0 9963 |
. . . . . . . . . . . . . . . . . 18
      
         
     
            |
64 | 57, 59, 62, 63 | syl12anc 1217 |
. . . . . . . . . . . . . . . . 17
                 |
65 | | flge0nn0 11778 |
. . . . . . . . . . . . . . . . 17
                                       |
66 | 60, 64, 65 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
                     |
67 | 66 | adantr 465 |
. . . . . . . . . . . . . . 15
   

     
                |
68 | 67 | nn0cnd 10744 |
. . . . . . . . . . . . . 14
   

     
                |
69 | 32 | adantr 465 |
. . . . . . . . . . . . . . 15
   

     
      |
70 | 69 | nncnd 10444 |
. . . . . . . . . . . . . 14
   

     
      |
71 | 69 | nnne0d 10472 |
. . . . . . . . . . . . . 14
   

     
      |
72 | 68, 70, 71 | divcan1d 10214 |
. . . . . . . . . . . . 13
   

     
                                          |
73 | 53, 72 | eqtrd 2493 |
. . . . . . . . . . . 12
   

     
                          |
74 | 73, 67 | eqeltrd 2540 |
. . . . . . . . . . 11
   

     
            |
75 | | nn0uz 11001 |
. . . . . . . . . . 11
     |
76 | 74, 75 | syl6eleq 2550 |
. . . . . . . . . 10
   

     
                |
77 | | nnmulcl 10451 |
. . . . . . . . . . . . . 14
               |
78 | 31, 77 | mpdan 668 |
. . . . . . . . . . . . 13
 
       |
79 | 78 | ad2antlr 726 |
. . . . . . . . . . . 12
     
       |
80 | 79 | adantr 465 |
. . . . . . . . . . 11
   

     
        |
81 | 80 | nnzd 10852 |
. . . . . . . . . 10
   

     
        |
82 | | elfz5 11557 |
. . . . . . . . . 10
                
                                    
         |
83 | 76, 81, 82 | syl2anc 661 |
. . . . . . . . 9
   

     
                    
          
        |
84 | 39, 83 | mpbird 232 |
. . . . . . . 8
   

     
                      |
85 | | oveq1 6202 |
. . . . . . . . 9
                                   |
86 | | eqid 2452 |
. . . . . . . . 9
                      
              |
87 | | ovex 6220 |
. . . . . . . . 9
                 |
88 | 85, 86, 87 | fvmpt 5878 |
. . . . . . . 8
                                                                       |
89 | 84, 88 | syl 16 |
. . . . . . 7
   

     
                                                  |
90 | 26 | adantr 465 |
. . . . . . . . 9
   

     
      |
91 | 90 | recnd 9518 |
. . . . . . . 8
   

     
      |
92 | 91, 70, 71 | divcan4d 10219 |
. . . . . . 7
   

     
                      |
93 | 89, 92 | eqtrd 2493 |
. . . . . 6
   

     
                                      |
94 | | elfznn0 11593 |
. . . . . . . . . . . . 13
             |
95 | 94 | nn0red 10743 |
. . . . . . . . . . . 12
             |
96 | 31 | adantl 466 |
. . . . . . . . . . . 12
 

      |
97 | | nndivre 10463 |
. . . . . . . . . . . 12
               |
98 | 95, 96, 97 | syl2anr 478 |
. . . . . . . . . . 11
       
               |
99 | 98, 86 | fmptd 5971 |
. . . . . . . . . 10
 

                                  |
100 | | ffn 5662 |
. . . . . . . . . 10
                                                               |
101 | 99, 100 | syl 16 |
. . . . . . . . 9
 

                              |
102 | 101 | adantr 465 |
. . . . . . . 8
                                   |
103 | 102 | adantr 465 |
. . . . . . 7
   

     
    
                
        |
104 | | fnfvelrn 5944 |
. . . . . . 7
                                                                                       
               |
105 | 103, 84, 104 | syl2anc 661 |
. . . . . 6
   

     
                                                    |
106 | 93, 105 | eqeltrrd 2541 |
. . . . 5
   

     
        
               |
107 | 79 | nnnn0d 10742 |
. . . . . . . . . . 11
     
       |
108 | 107, 75 | syl6eleq 2550 |
. . . . . . . . . 10
     
           |
109 | | eluzfz2 11571 |
. . . . . . . . . 10
          
                  |
110 | 108, 109 | syl 16 |
. . . . . . . . 9
     
                 |
111 | | oveq1 6202 |
. . . . . . . . . 10
                           |
112 | | ovex 6220 |
. . . . . . . . . 10
             |
113 | 111, 86, 112 | fvmpt 5878 |
. . . . . . . . 9
                                      
                    |
114 | 110, 113 | syl 16 |
. . . . . . . 8
                          
                    |
115 | 28 | recnd 9518 |
. . . . . . . . 9
       |
116 | 32 | nncnd 10444 |
. . . . . . . . 9
           |
117 | 32 | nnne0d 10472 |
. . . . . . . . 9
           |
118 | 115, 116,
117 | divcan4d 10219 |
. . . . . . . 8
                   |
119 | 114, 118 | eqtrd 2493 |
. . . . . . 7
                          
        |
120 | | fnfvelrn 5944 |
. . . . . . . 8
                              
                                                
               |
121 | 102, 110,
120 | syl2anc 661 |
. . . . . . 7
                          
                          |
122 | 119, 121 | eqeltrrd 2541 |
. . . . . 6
         
               |
123 | 122 | adantr 465 |
. . . . 5
   

          
               |
124 | 106, 123 | ifclda 3924 |
. . . 4
                                      |
125 | | eluzfz1 11570 |
. . . . . . . 8
          
   
        |
126 | 108, 125 | syl 16 |
. . . . . . 7
        
        |
127 | | oveq1 6202 |
. . . . . . . 8
               |
128 | | ovex 6220 |
. . . . . . . 8
       |
129 | 127, 86, 128 | fvmpt 5878 |
. . . . . . 7
                                         |
130 | 126, 129 | syl 16 |
. . . . . 6
                                   |
131 | | nncn 10436 |
. . . . . . . 8
           |
132 | | nnne0 10460 |
. . . . . . . 8
           |
133 | 131, 132 | div0d 10212 |
. . . . . . 7
             |
134 | 32, 133 | syl 16 |
. . . . . 6
             |
135 | 130, 134 | eqtrd 2493 |
. . . . 5
                             |
136 | | fnfvelrn 5944 |
. . . . . 6
                             
                                     
               |
137 | 102, 126,
136 | syl2anc 661 |
. . . . 5
                                               |
138 | 135, 137 | eqeltrrd 2541 |
. . . 4
         
               |
139 | | ifcl 3934 |
. . . 4
        
      
                     
                   ![[,] [,]](_icc.gif)                                      |
140 | 124, 138,
139 | syl2anc 661 |
. . 3
      
   ![[,] [,]](_icc.gif)                  
                   |
141 | | eqid 2452 |
. . 3
      ![[,] [,]](_icc.gif)         
               ![[,] [,]](_icc.gif)        
           |
142 | 140, 141 | fmptd 5971 |
. 2
 

      ![[,] [,]](_icc.gif)         
                                 |
143 | | mbfi1fseq.1 |
. . . . 5
 MblFn |
144 | | mbfi1fseq.4 |
. . . . 5
 
     ![[,] [,]](_icc.gif)        
            |
145 | 143, 5, 21, 144 | mbfi1fseqlem2 21322 |
. . . 4
           ![[,] [,]](_icc.gif)                     |
146 | 145 | adantl 466 |
. . 3
 

          ![[,] [,]](_icc.gif)        
            |
147 | 146 | feq1d 5649 |
. 2
 

                                 ![[,] [,]](_icc.gif)                                            |
148 | 142, 147 | mpbird 232 |
1
 

       
    
               |