Step | Hyp | Ref
| Expression |
1 | | iblabsnclem.1 |
. . 3
                |
2 | | iblabsnclem.2 |
. . . . . . . 8
          |
3 | | iblabsnclem.3 |
. . . . . . . . 9
 
       |
4 | 3 | iblrelem 22804 |
. . . . . . . 8
        
       MblFn
                                                |
5 | 2, 4 | mpbid 215 |
. . . . . . 7
        MblFn                            
                   |
6 | 5 | simp1d 1026 |
. . . . . 6
       MblFn |
7 | 6, 3 | mbfdm2 22650 |
. . . . 5
   |
8 | | mblss 22540 |
. . . . 5
   |
9 | 7, 8 | syl 17 |
. . . 4

  |
10 | | rembl 22549 |
. . . . 5
 |
11 | 10 | a1i 11 |
. . . 4
   |
12 | 3 | recnd 9700 |
. . . . . 6
 
       |
13 | 12 | abscld 13553 |
. . . . 5
 
           |
14 | | 0re 9674 |
. . . . 5
 |
15 | | ifcl 3935 |
. . . . 5
         
                |
16 | 13, 14, 15 | sylancl 673 |
. . . 4
 
  
             |
17 | | eldifn 3568 |
. . . . . 6
  
  |
18 | 17 | adantl 472 |
. . . . 5
 

 
  |
19 | | iffalse 3902 |
. . . . 5
                |
20 | 18, 19 | syl 17 |
. . . 4
 

 
               |
21 | | iftrue 3899 |
. . . . . 6
  
                     |
22 | 21 | mpteq2ia 4501 |
. . . . 5
                          |
23 | | eqid 2462 |
. . . . . . 7
                     |
24 | 13, 23 | fmptd 6074 |
. . . . . 6
                 |
25 | 13 | adantlr 726 |
. . . . . . . . . . 11
               |
26 | 25 | biantrurd 515 |
. . . . . . . . . 10
     
       
                     |
27 | 3 | adantlr 726 |
. . . . . . . . . . . . 13
           |
28 | | simplr 767 |
. . . . . . . . . . . . 13
       |
29 | 27, 28 | absled 13547 |
. . . . . . . . . . . 12
             
     
        |
30 | 29 | notbid 300 |
. . . . . . . . . . 11
             
 
            |
31 | 28, 25 | ltnled 9813 |
. . . . . . . . . . 11
     
       
           |
32 | | renegcl 9968 |
. . . . . . . . . . . . . . . . 17
    |
33 | 32 | rexrd 9721 |
. . . . . . . . . . . . . . . 16
    |
34 | 33 | ad2antlr 738 |
. . . . . . . . . . . . . . 15
        |
35 | | elioomnf 11763 |
. . . . . . . . . . . . . . 15
 
        
              |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . 14
             
              |
37 | 27 | biantrurd 515 |
. . . . . . . . . . . . . 14
         

              |
38 | 28 | renegcld 10079 |
. . . . . . . . . . . . . . 15
        |
39 | 27, 38 | ltnled 9813 |
. . . . . . . . . . . . . 14
         

        |
40 | 36, 37, 39 | 3bitr2d 289 |
. . . . . . . . . . . . 13
             
        |
41 | | rexr 9717 |
. . . . . . . . . . . . . . . 16
   |
42 | 41 | ad2antlr 738 |
. . . . . . . . . . . . . . 15
       |
43 | | elioopnf 11762 |
. . . . . . . . . . . . . . 15

       
             |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . 14
            
             |
45 | 27 | biantrurd 515 |
. . . . . . . . . . . . . 14
     
   
             |
46 | 28, 27 | ltnled 9813 |
. . . . . . . . . . . . . 14
     
   
       |
47 | 44, 45, 46 | 3bitr2d 289 |
. . . . . . . . . . . . 13
            
       |
48 | 40, 47 | orbi12d 721 |
. . . . . . . . . . . 12
                      
 
            |
49 | | ianor 495 |
. . . . . . . . . . . 12
      
                  |
50 | 48, 49 | syl6bbr 271 |
. . . . . . . . . . 11
                      
 
            |
51 | 30, 31, 50 | 3bitr4rd 294 |
. . . . . . . . . 10
                      
           |
52 | | elioopnf 11762 |
. . . . . . . . . . 11

           
                     |
53 | 42, 52 | syl 17 |
. . . . . . . . . 10
                
                     |
54 | 26, 51, 53 | 3bitr4rd 294 |
. . . . . . . . 9
                
    
               |
55 | 54 | rabbidva 3047 |
. . . . . . . 8
 


           
                     |
56 | 23 | mptpreima 5351 |
. . . . . . . 8
               
  
             |
57 | | eqid 2462 |
. . . . . . . . . . 11
             |
58 | 57 | mptpreima 5351 |
. . . . . . . . . 10
                          |
59 | 57 | mptpreima 5351 |
. . . . . . . . . 10
           
  
         |
60 | 58, 59 | uneq12i 3598 |
. . . . . . . . 9
                                                     |
61 | | unrab 3726 |
. . . . . . . . 9
                                         |
62 | 60, 61 | eqtri 2484 |
. . . . . . . 8
                                                   |
63 | 55, 56, 62 | 3eqtr4g 2521 |
. . . . . . 7
 

               
                                   |
64 | | iblmbf 22781 |
. . . . . . . . . 10
              MblFn |
65 | 2, 64 | syl 17 |
. . . . . . . . 9
       MblFn |
66 | 3, 57 | fmptd 6074 |
. . . . . . . . 9
             |
67 | | mbfima 22644 |
. . . . . . . . . 10
        MblFn                             |
68 | | mbfima 22644 |
. . . . . . . . . 10
        MblFn                            |
69 | | unmbl 22546 |
. . . . . . . . . 10
                            
                                    |
70 | 67, 68, 69 | syl2anc 671 |
. . . . . . . . 9
        MblFn                                             |
71 | 65, 66, 70 | syl2anc 671 |
. . . . . . . 8
                                  |
72 | 71 | adantr 471 |
. . . . . . 7
 

                                 |
73 | 63, 72 | eqeltrd 2540 |
. . . . . 6
 

               
    |
74 | | elioomnf 11763 |
. . . . . . . . . . . . . 14

           
                     |
75 | 42, 74 | syl 17 |
. . . . . . . . . . . . 13
                
                     |
76 | 25 | biantrurd 515 |
. . . . . . . . . . . . 13
             
                     |
77 | 27, 28 | absltd 13546 |
. . . . . . . . . . . . 13
             
     
        |
78 | 75, 76, 77 | 3bitr2d 289 |
. . . . . . . . . . . 12
                
     
        |
79 | 27 | biantrurd 515 |
. . . . . . . . . . . 12
               
               
     |
80 | 78, 79 | bitrd 261 |
. . . . . . . . . . 11
                
                    |
81 | | 3anass 995 |
. . . . . . . . . . 11
               
                   |
82 | 80, 81 | syl6bbr 271 |
. . . . . . . . . 10
                
         
        |
83 | | elioo2 11711 |
. . . . . . . . . . . 12
                       
        |
84 | 33, 41, 83 | syl2anc 671 |
. . . . . . . . . . 11
          
         
        |
85 | 84 | ad2antlr 738 |
. . . . . . . . . 10
              
         
        |
86 | 82, 85 | bitr4d 264 |
. . . . . . . . 9
                
            |
87 | 86 | rabbidva 3047 |
. . . . . . . 8
 


                         |
88 | 23 | mptpreima 5351 |
. . . . . . . 8
                                |
89 | 57 | mptpreima 5351 |
. . . . . . . 8
                
           |
90 | 87, 88, 89 | 3eqtr4g 2521 |
. . . . . . 7
 

                                    |
91 | | mbfima 22644 |
. . . . . . . . 9
        MblFn                              |
92 | 65, 66, 91 | syl2anc 671 |
. . . . . . . 8
                   |
93 | 92 | adantr 471 |
. . . . . . 7
 

                  |
94 | 90, 93 | eqeltrd 2540 |
. . . . . 6
 

                    |
95 | 24, 7, 73, 94 | ismbf2d 22653 |
. . . . 5
           MblFn |
96 | 22, 95 | syl5eqel 2544 |
. . . 4
                MblFn |
97 | 9, 11, 16, 20, 96 | mbfss 22658 |
. . 3
                MblFn |
98 | 1, 97 | syl5eqel 2544 |
. 2
 MblFn |
99 | | reex 9661 |
. . . . . . . . 9
 |
100 | 99 | a1i 11 |
. . . . . . . 8
   |
101 | | ifan 3939 |
. . . . . . . . . 10
  
                               |
102 | | ifcl 3935 |
. . . . . . . . . . . . 13
     
                |
103 | 3, 14, 102 | sylancl 673 |
. . . . . . . . . . . 12
 
                |
104 | | max1 11514 |
. . . . . . . . . . . . 13
      
 
             |
105 | 14, 3, 104 | sylancr 674 |
. . . . . . . . . . . 12
 
                |
106 | | elrege0 11773 |
. . . . . . . . . . . 12
                
                              |
107 | 103, 105,
106 | sylanbrc 675 |
. . . . . . . . . . 11
 
                   |
108 | | 0e0icopnf 11777 |
. . . . . . . . . . . 12
    |
109 | 108 | a1i 11 |
. . . . . . . . . . 11
 
      |
110 | 107, 109 | ifclda 3925 |
. . . . . . . . . 10
     
                  |
111 | 101, 110 | syl5eqel 2544 |
. . . . . . . . 9
                     |
112 | 111 | adantr 471 |
. . . . . . . 8
 

  
                 |
113 | | ifan 3939 |
. . . . . . . . . 10
  
                  
                |
114 | 3 | renegcld 10079 |
. . . . . . . . . . . . 13
 
        |
115 | | ifcl 3935 |
. . . . . . . . . . . . 13
                         |
116 | 114, 14, 115 | sylancl 673 |
. . . . . . . . . . . 12
 
                  |
117 | | max1 11514 |
. . . . . . . . . . . . 13
                         |
118 | 14, 114, 117 | sylancr 674 |
. . . . . . . . . . . 12
 
                  |
119 | | elrege0 11773 |
. . . . . . . . . . . 12
                  
                                  |
120 | 116, 118,
119 | sylanbrc 675 |
. . . . . . . . . . 11
 
                     |
121 | 120, 109 | ifclda 3925 |
. . . . . . . . . 10
     
                    |
122 | 113, 121 | syl5eqel 2544 |
. . . . . . . . 9
                       |
123 | 122 | adantr 471 |
. . . . . . . 8
 

  
                   |
124 | | eqidd 2463 |
. . . . . . . 8
                                     |
125 | | eqidd 2463 |
. . . . . . . 8
                                         |
126 | 100, 112,
123, 124, 125 | offval2 6580 |
. . . . . . 7
                    
                                                         |
127 | 101, 113 | oveq12i 6332 |
. . . . . . . . 9
                                       
              
                    |
128 | | max0add 13428 |
. . . . . . . . . . . . 13
                    
                        |
129 | 3, 128 | syl 17 |
. . . . . . . . . . . 12
 
                
                        |
130 | | iftrue 3899 |
. . . . . . . . . . . . . 14
  
                 
             |
131 | 130 | adantl 472 |
. . . . . . . . . . . . 13
 
  
                 
             |
132 | | iftrue 3899 |
. . . . . . . . . . . . . 14
  
                                   |
133 | 132 | adantl 472 |
. . . . . . . . . . . . 13
 
  
                                   |
134 | 131, 133 | oveq12d 6338 |
. . . . . . . . . . . 12
 
                                                        
                |
135 | 21 | adantl 472 |
. . . . . . . . . . . 12
 
  
                     |
136 | 129, 134,
135 | 3eqtr4d 2506 |
. . . . . . . . . . 11
 
                                                        |
137 | 136 | ex 440 |
. . . . . . . . . 10
                                                          |
138 | | 00id 9839 |
. . . . . . . . . . 11
   |
139 | | iffalse 3902 |
. . . . . . . . . . . 12
                     |
140 | | iffalse 3902 |
. . . . . . . . . . . 12
                       |
141 | 139, 140 | oveq12d 6338 |
. . . . . . . . . . 11
                                             |
142 | 138, 141,
19 | 3eqtr4a 2522 |
. . . . . . . . . 10
                                                        |
143 | 137, 142 | pm2.61d1 164 |
. . . . . . . . 9
                                                        |
144 | 127, 143 | syl5eq 2508 |
. . . . . . . 8
                                                  |
145 | 144 | mpteq2dv 4506 |
. . . . . . 7
                                                      |
146 | 126, 145 | eqtrd 2496 |
. . . . . 6
                    
                                    |
147 | 146, 1 | syl6reqr 2515 |
. . . . 5
                                          |
148 | 147 | fveq2d 5896 |
. . . 4
                           
                      |
149 | 111 | adantr 471 |
. . . . . 6
 
                     |
150 | 101, 139 | syl5eq 2508 |
. . . . . . 7
                  |
151 | 18, 150 | syl 17 |
. . . . . 6
 

 
  
              |
152 | | ibar 511 |
. . . . . . . . 9
 
   

        |
153 | 152 | ifbid 3915 |
. . . . . . . 8
                
              |
154 | 153 | mpteq2ia 4501 |
. . . . . . 7
  
                              |
155 | 3, 6 | mbfpos 22663 |
. . . . . . 7
                MblFn |
156 | 154, 155 | syl5eqelr 2545 |
. . . . . 6
                  MblFn |
157 | 9, 11, 149, 151, 156 | mbfss 22658 |
. . . . 5
                  MblFn |
158 | | eqid 2462 |
. . . . . 6
   
                               |
159 | 112, 158 | fmptd 6074 |
. . . . 5
                           |
160 | 5 | simp2d 1027 |
. . . . 5
                        |
161 | | eqid 2462 |
. . . . . 6
   
                                   |
162 | 123, 161 | fmptd 6074 |
. . . . 5
                             |
163 | 5 | simp3d 1028 |
. . . . 5
                          |
164 | 157, 159,
160, 162, 163 | itg2addnc 32042 |
. . . 4
                                                                                            |
165 | 148, 164 | eqtrd 2496 |
. . 3
            
                                        |
166 | 160, 163 | readdcld 9701 |
. . 3
                                                 |
167 | 165, 166 | eqeltrd 2540 |
. 2
       |
168 | 98, 167 | jca 539 |
1
  MblFn        |