Step | Hyp | Ref
| Expression |
1 | | iblabs.2 |
. . . . . 6
      |
2 | | iblmbf 22718 |
. . . . . 6
      MblFn |
3 | 1, 2 | syl 17 |
. . . . 5
   MblFn |
4 | | iblabs.1 |
. . . . 5
 
   |
5 | 3, 4 | mbfmptcl 22586 |
. . . 4
 
   |
6 | | eqidd 2451 |
. . . 4
       |
7 | | absf 13393 |
. . . . . 6
     |
8 | 7 | a1i 11 |
. . . . 5
       |
9 | 8 | feqmptd 5916 |
. . . 4
         |
10 | | fveq2 5863 |
. . . 4
           |
11 | 5, 6, 9, 10 | fmptco 6054 |
. . 3
             |
12 | | eqid 2450 |
. . . . 5
     |
13 | 5, 12 | fmptd 6044 |
. . . 4
         |
14 | | ax-resscn 9593 |
. . . . . . 7
 |
15 | | ssid 3450 |
. . . . . . 7
 |
16 | | cncfss 21924 |
. . . . . . 7
 
           |
17 | 14, 15, 16 | mp2an 677 |
. . . . . 6
         |
18 | | abscncf 21926 |
. . . . . 6
     |
19 | 17, 18 | sselii 3428 |
. . . . 5
     |
20 | 19 | a1i 11 |
. . . 4
       |
21 | | cncombf 22607 |
. . . 4
    MblFn                MblFn |
22 | 3, 13, 20, 21 | syl3anc 1267 |
. . 3
     MblFn |
23 | 11, 22 | eqeltrrd 2529 |
. 2
       MblFn |
24 | 5 | abscld 13491 |
. . . . . . . 8
 
       |
25 | 24 | rexrd 9687 |
. . . . . . 7
 
       |
26 | 5 | absge0d 13499 |
. . . . . . 7
 
       |
27 | | elxrge0 11738 |
. . . . . . 7
       
    
       |
28 | 25, 26, 27 | sylanbrc 669 |
. . . . . 6
 
          |
29 | | 0e0iccpnf 11740 |
. . . . . . 7
    |
30 | 29 | a1i 11 |
. . . . . 6
 
      |
31 | 28, 30 | ifclda 3912 |
. . . . 5
               |
32 | 31 | adantr 467 |
. . . 4
 

              |
33 | | eqid 2450 |
. . . 4
                       |
34 | 32, 33 | fmptd 6044 |
. . 3
                     |
35 | | reex 9627 |
. . . . . . . . 9
 |
36 | 35 | a1i 11 |
. . . . . . . 8
   |
37 | 5 | recld 13250 |
. . . . . . . . . . . . 13
 
       |
38 | 37 | recnd 9666 |
. . . . . . . . . . . 12
 
       |
39 | 38 | abscld 13491 |
. . . . . . . . . . 11
 
           |
40 | 38 | absge0d 13499 |
. . . . . . . . . . 11
 
           |
41 | | elrege0 11735 |
. . . . . . . . . . 11
           
        
           |
42 | 39, 40, 41 | sylanbrc 669 |
. . . . . . . . . 10
 
              |
43 | | 0e0icopnf 11739 |
. . . . . . . . . . 11
    |
44 | 43 | a1i 11 |
. . . . . . . . . 10
 
      |
45 | 42, 44 | ifclda 3912 |
. . . . . . . . 9
                   |
46 | 45 | adantr 467 |
. . . . . . . 8
 

                  |
47 | 5 | imcld 13251 |
. . . . . . . . . . . . 13
 
       |
48 | 47 | recnd 9666 |
. . . . . . . . . . . 12
 
       |
49 | 48 | abscld 13491 |
. . . . . . . . . . 11
 
           |
50 | 48 | absge0d 13499 |
. . . . . . . . . . 11
 
           |
51 | | elrege0 11735 |
. . . . . . . . . . 11
           
        
           |
52 | 49, 50, 51 | sylanbrc 669 |
. . . . . . . . . 10
 
              |
53 | 52, 44 | ifclda 3912 |
. . . . . . . . 9
                   |
54 | 53 | adantr 467 |
. . . . . . . 8
 

                  |
55 | | eqidd 2451 |
. . . . . . . 8
                                 |
56 | | eqidd 2451 |
. . . . . . . 8
                                 |
57 | 36, 46, 54, 55, 56 | offval2 6545 |
. . . . . . 7
                                                                  |
58 | | iftrue 3886 |
. . . . . . . . . . 11
  
                     |
59 | | iftrue 3886 |
. . . . . . . . . . 11
  
                     |
60 | 58, 59 | oveq12d 6306 |
. . . . . . . . . 10
                                                 |
61 | | iftrue 3886 |
. . . . . . . . . 10
  
                                         |
62 | 60, 61 | eqtr4d 2487 |
. . . . . . . . 9
                                                      |
63 | | 00id 9805 |
. . . . . . . . . 10
   |
64 | | iffalse 3889 |
. . . . . . . . . . 11
                |
65 | | iffalse 3889 |
. . . . . . . . . . 11
                |
66 | 64, 65 | oveq12d 6306 |
. . . . . . . . . 10
                                 |
67 | | iffalse 3889 |
. . . . . . . . . 10
                          |
68 | 63, 66, 67 | 3eqtr4a 2510 |
. . . . . . . . 9
                                                      |
69 | 62, 68 | pm2.61i 168 |
. . . . . . . 8
                                                    |
70 | 69 | mpteq2i 4485 |
. . . . . . 7
                                                        |
71 | 57, 70 | syl6req 2501 |
. . . . . 6
                                           
                 |
72 | 71 | fveq2d 5867 |
. . . . 5
                                                  
                  |
73 | | eqid 2450 |
. . . . . . . 8
                               |
74 | 5 | iblcn 22749 |
. . . . . . . . . 10
    
                   |
75 | 1, 74 | mpbid 214 |
. . . . . . . . 9
                   |
76 | 75 | simpld 461 |
. . . . . . . 8
          |
77 | 4, 1, 73, 76, 37 | iblabslem 22778 |
. . . . . . 7
                 MblFn
                      |
78 | 77 | simpld 461 |
. . . . . 6
                MblFn |
79 | 46, 73 | fmptd 6044 |
. . . . . 6
                         |
80 | 77 | simprd 465 |
. . . . . 6
                      |
81 | | eqid 2450 |
. . . . . . . 8
                               |
82 | 75 | simprd 465 |
. . . . . . . 8
          |
83 | 4, 1, 81, 82, 47 | iblabslem 22778 |
. . . . . . 7
                 MblFn
                      |
84 | 83 | simpld 461 |
. . . . . 6
                MblFn |
85 | 54, 81 | fmptd 6044 |
. . . . . 6
                         |
86 | 83 | simprd 465 |
. . . . . 6
                      |
87 | 78, 79, 80, 84, 85, 86 | itg2add 22710 |
. . . . 5
                     
                                                          |
88 | 72, 87 | eqtrd 2484 |
. . . 4
                                                                        |
89 | 80, 86 | readdcld 9667 |
. . . 4
                                           |
90 | 88, 89 | eqeltrd 2528 |
. . 3
                                |
91 | 39, 49 | readdcld 9667 |
. . . . . . . . 9
 
                     |
92 | 91 | rexrd 9687 |
. . . . . . . 8
 
                     |
93 | 39, 49, 40, 50 | addge0d 10186 |
. . . . . . . 8
 
                     |
94 | | elxrge0 11738 |
. . . . . . . 8
                                                              |
95 | 92, 93, 94 | sylanbrc 669 |
. . . . . . 7
 
                        |
96 | 95, 30 | ifclda 3912 |
. . . . . 6
                             |
97 | 96 | adantr 467 |
. . . . 5
 

                            |
98 | | eqid 2450 |
. . . . 5
                                                   |
99 | 97, 98 | fmptd 6044 |
. . . 4
                                   |
100 | | ax-icn 9595 |
. . . . . . . . . . . 12
 |
101 | | mulcl 9620 |
. . . . . . . . . . . 12
               |
102 | 100, 48, 101 | sylancr 668 |
. . . . . . . . . . 11
 
 
       |
103 | 38, 102 | abstrid 13511 |
. . . . . . . . . 10
 
                                       |
104 | 5 | replimd 13253 |
. . . . . . . . . . 11
 
               |
105 | 104 | fveq2d 5867 |
. . . . . . . . . 10
 
                       |
106 | | absmul 13350 |
. . . . . . . . . . . . 13
          
                      |
107 | 100, 48, 106 | sylancr 668 |
. . . . . . . . . . . 12
 
               
           |
108 | | absi 13342 |
. . . . . . . . . . . . . 14
     |
109 | 108 | oveq1i 6298 |
. . . . . . . . . . . . 13
                         |
110 | 49 | recnd 9666 |
. . . . . . . . . . . . . 14
 
           |
111 | 110 | mulid2d 9658 |
. . . . . . . . . . . . 13
 
                     |
112 | 109, 111 | syl5eq 2496 |
. . . . . . . . . . . 12
 
     
                   |
113 | 107, 112 | eqtr2d 2485 |
. . . . . . . . . . 11
 
            
        |
114 | 113 | oveq2d 6304 |
. . . . . . . . . 10
 
                                         |
115 | 103, 105,
114 | 3brtr4d 4432 |
. . . . . . . . 9
 
                         |
116 | | iftrue 3886 |
. . . . . . . . . 10
  
             |
117 | 116 | adantl 468 |
. . . . . . . . 9
 
  
             |
118 | 61 | adantl 468 |
. . . . . . . . 9
 
  
                                         |
119 | 115, 117,
118 | 3brtr4d 4432 |
. . . . . . . 8
 
  
                                |
120 | 119 | ex 436 |
. . . . . . 7
          
                          |
121 | | 0le0 10696 |
. . . . . . . . 9
 |
122 | 121 | a1i 11 |
. . . . . . . 8

  |
123 | | iffalse 3889 |
. . . . . . . 8
            |
124 | 122, 123,
67 | 3brtr4d 4432 |
. . . . . . 7
                                   |
125 | 120, 124 | pm2.61d1 163 |
. . . . . 6
         
                         |
126 | 125 | ralrimivw 2802 |
. . . . 5
                                    |
127 | | eqidd 2451 |
. . . . . 6
                         |
128 | | eqidd 2451 |
. . . . . 6
                                                     |
129 | 36, 32, 97, 127, 128 | ofrfval2 6546 |
. . . . 5
                                                                           |
130 | 126, 129 | mpbird 236 |
. . . 4
                                        |
131 | | itg2le 22690 |
. . . 4
                    
                               
                                                   
                               |
132 | 34, 99, 130, 131 | syl3anc 1267 |
. . 3
                                               |
133 | | itg2lecl 22689 |
. . 3
                                                               
                                               |
134 | 34, 90, 132, 133 | syl3anc 1267 |
. 2
                  |
135 | 24, 26 | iblpos 22743 |
. 2
                MblFn                    |
136 | 23, 134, 135 | mpbir2and 932 |
1
          |