Step | Hyp | Ref
| Expression |
1 | | iblabs.3 |
. . 3
                |
2 | | iblabs.4 |
. . . . . . . 8
          |
3 | | iblabs.5 |
. . . . . . . . 9
 
       |
4 | 3 | iblrelem 22827 |
. . . . . . . 8
        
       MblFn
                                                |
5 | 2, 4 | mpbid 215 |
. . . . . . 7
        MblFn                            
                   |
6 | 5 | simp1d 1042 |
. . . . . 6
       MblFn |
7 | 6, 3 | mbfdm2 22673 |
. . . . 5
   |
8 | | mblss 22563 |
. . . . 5
   |
9 | 7, 8 | syl 17 |
. . . 4

  |
10 | | rembl 22572 |
. . . . 5
 |
11 | 10 | a1i 11 |
. . . 4
   |
12 | | iftrue 3878 |
. . . . . 6
  
                     |
13 | 12 | adantl 473 |
. . . . 5
 
  
                     |
14 | 3 | recnd 9687 |
. . . . . 6
 
       |
15 | 14 | abscld 13575 |
. . . . 5
 
           |
16 | 13, 15 | eqeltrd 2549 |
. . . 4
 
  
             |
17 | | eldifn 3545 |
. . . . . 6
  
  |
18 | 17 | adantl 473 |
. . . . 5
 

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

 
               |
21 | | eqidd 2472 |
. . . . . . 7
               |
22 | | absf 13477 |
. . . . . . . . 9
     |
23 | 22 | a1i 11 |
. . . . . . . 8
       |
24 | 23 | feqmptd 5932 |
. . . . . . 7
         |
25 | | fveq2 5879 |
. . . . . . 7
                   |
26 | 14, 21, 24, 25 | fmptco 6072 |
. . . . . 6
                     |
27 | 12 | mpteq2ia 4478 |
. . . . . 6
                          |
28 | 26, 27 | syl6reqr 2524 |
. . . . 5
                          |
29 | | eqid 2471 |
. . . . . . 7
             |
30 | 14, 29 | fmptd 6061 |
. . . . . 6
             |
31 | | ax-resscn 9614 |
. . . . . . . . 9
 |
32 | | ssid 3437 |
. . . . . . . . 9
 |
33 | | cncfss 22009 |
. . . . . . . . 9
 
           |
34 | 31, 32, 33 | mp2an 686 |
. . . . . . . 8
         |
35 | | abscncf 22011 |
. . . . . . . 8
     |
36 | 34, 35 | sselii 3415 |
. . . . . . 7
     |
37 | 36 | a1i 11 |
. . . . . 6
       |
38 | | cncombf 22693 |
. . . . . 6
        MblFn                        MblFn |
39 | 6, 30, 37, 38 | syl3anc 1292 |
. . . . 5
         MblFn |
40 | 28, 39 | eqeltrd 2549 |
. . . 4
                MblFn |
41 | 9, 11, 16, 20, 40 | mbfss 22681 |
. . 3
                MblFn |
42 | 1, 41 | syl5eqel 2553 |
. 2
 MblFn |
43 | | reex 9648 |
. . . . . . . . 9
 |
44 | 43 | a1i 11 |
. . . . . . . 8
   |
45 | | ifan 3918 |
. . . . . . . . . 10
  
                               |
46 | | 0re 9661 |
. . . . . . . . . . . . 13
 |
47 | | ifcl 3914 |
. . . . . . . . . . . . 13
     
                |
48 | 3, 46, 47 | sylancl 675 |
. . . . . . . . . . . 12
 
                |
49 | | max1 11503 |
. . . . . . . . . . . . 13
      
 
             |
50 | 46, 3, 49 | sylancr 676 |
. . . . . . . . . . . 12
 
                |
51 | | elrege0 11764 |
. . . . . . . . . . . 12
                
                              |
52 | 48, 50, 51 | sylanbrc 677 |
. . . . . . . . . . 11
 
                   |
53 | | 0e0icopnf 11768 |
. . . . . . . . . . . 12
    |
54 | 53 | a1i 11 |
. . . . . . . . . . 11
 
      |
55 | 52, 54 | ifclda 3904 |
. . . . . . . . . 10
     
                  |
56 | 45, 55 | syl5eqel 2553 |
. . . . . . . . 9
                     |
57 | 56 | adantr 472 |
. . . . . . . 8
 

  
                 |
58 | | ifan 3918 |
. . . . . . . . . 10
  
                  
                |
59 | 3 | renegcld 10067 |
. . . . . . . . . . . . 13
 
        |
60 | | ifcl 3914 |
. . . . . . . . . . . . 13
                         |
61 | 59, 46, 60 | sylancl 675 |
. . . . . . . . . . . 12
 
                  |
62 | | max1 11503 |
. . . . . . . . . . . . 13
                         |
63 | 46, 59, 62 | sylancr 676 |
. . . . . . . . . . . 12
 
                  |
64 | | elrege0 11764 |
. . . . . . . . . . . 12
                  
                                  |
65 | 61, 63, 64 | sylanbrc 677 |
. . . . . . . . . . 11
 
                     |
66 | 65, 54 | ifclda 3904 |
. . . . . . . . . 10
     
                    |
67 | 58, 66 | syl5eqel 2553 |
. . . . . . . . 9
                       |
68 | 67 | adantr 472 |
. . . . . . . 8
 

  
                   |
69 | | eqidd 2472 |
. . . . . . . 8
                                     |
70 | | eqidd 2472 |
. . . . . . . 8
                                         |
71 | 44, 57, 68, 69, 70 | offval2 6567 |
. . . . . . 7
                    
                                                         |
72 | 45, 58 | oveq12i 6320 |
. . . . . . . . 9
                                       
              
                    |
73 | | max0add 13450 |
. . . . . . . . . . . . 13
                    
                        |
74 | 3, 73 | syl 17 |
. . . . . . . . . . . 12
 
                
                        |
75 | | iftrue 3878 |
. . . . . . . . . . . . . 14
  
                 
             |
76 | 75 | adantl 473 |
. . . . . . . . . . . . 13
 
  
                 
             |
77 | | iftrue 3878 |
. . . . . . . . . . . . . 14
  
                                   |
78 | 77 | adantl 473 |
. . . . . . . . . . . . 13
 
  
                                   |
79 | 76, 78 | oveq12d 6326 |
. . . . . . . . . . . 12
 
                                                        
                |
80 | 74, 79, 13 | 3eqtr4d 2515 |
. . . . . . . . . . 11
 
                                                        |
81 | 80 | ex 441 |
. . . . . . . . . 10
                                                          |
82 | | 00id 9826 |
. . . . . . . . . . 11
   |
83 | | iffalse 3881 |
. . . . . . . . . . . 12
                     |
84 | | iffalse 3881 |
. . . . . . . . . . . 12
                       |
85 | 83, 84 | oveq12d 6326 |
. . . . . . . . . . 11
                                             |
86 | 82, 85, 19 | 3eqtr4a 2531 |
. . . . . . . . . 10
                                                        |
87 | 81, 86 | pm2.61d1 164 |
. . . . . . . . 9
                                                        |
88 | 72, 87 | syl5eq 2517 |
. . . . . . . 8
                                                  |
89 | 88 | mpteq2dv 4483 |
. . . . . . 7
                                                      |
90 | 71, 89 | eqtrd 2505 |
. . . . . 6
                    
                                    |
91 | 90, 1 | syl6reqr 2524 |
. . . . 5
                                          |
92 | 91 | fveq2d 5883 |
. . . 4
                           
                      |
93 | 56 | adantr 472 |
. . . . . 6
 
                     |
94 | 45, 83 | syl5eq 2517 |
. . . . . . 7
                  |
95 | 18, 94 | syl 17 |
. . . . . 6
 

 
  
              |
96 | | ibar 512 |
. . . . . . . . 9
 
   

        |
97 | 96 | ifbid 3894 |
. . . . . . . 8
                
              |
98 | 97 | mpteq2ia 4478 |
. . . . . . 7
  
                              |
99 | 3, 6 | mbfpos 22686 |
. . . . . . 7
                MblFn |
100 | 98, 99 | syl5eqelr 2554 |
. . . . . 6
                  MblFn |
101 | 9, 11, 93, 95, 100 | mbfss 22681 |
. . . . 5
                  MblFn |
102 | | eqid 2471 |
. . . . . 6
   
                               |
103 | 57, 102 | fmptd 6061 |
. . . . 5
                           |
104 | 5 | simp2d 1043 |
. . . . 5
                        |
105 | 67 | adantr 472 |
. . . . . 6
 
                       |
106 | 58, 84 | syl5eq 2517 |
. . . . . . 7
                    |
107 | 18, 106 | syl 17 |
. . . . . 6
 

 
  
                |
108 | | ibar 512 |
. . . . . . . . 9
 
    

         |
109 | 108 | ifbid 3894 |
. . . . . . . 8
                  
                |
110 | 109 | mpteq2ia 4478 |
. . . . . . 7
  
                                  |
111 | 3, 6 | mbfneg 22685 |
. . . . . . . 8
        MblFn |
112 | 59, 111 | mbfpos 22686 |
. . . . . . 7
                  MblFn |
113 | 110, 112 | syl5eqelr 2554 |
. . . . . 6
                    MblFn |
114 | 9, 11, 105, 107, 113 | mbfss 22681 |
. . . . 5
                    MblFn |
115 | | eqid 2471 |
. . . . . 6
   
                                   |
116 | 68, 115 | fmptd 6061 |
. . . . 5
                             |
117 | 5 | simp3d 1044 |
. . . . 5
                          |
118 | 101, 103,
104, 114, 116, 117 | itg2add 22796 |
. . . 4
                                                                                            |
119 | 92, 118 | eqtrd 2505 |
. . 3
            
                                        |
120 | 104, 117 | readdcld 9688 |
. . 3
                                                 |
121 | 119, 120 | eqeltrd 2549 |
. 2
       |
122 | 42, 121 | jca 541 |
1
  MblFn        |