Proof of Theorem iblabsnc
Step | Hyp | Ref
| Expression |
1 | | iblabsnc.m |
. 2
       MblFn |
2 | | iblabsnc.2 |
. . . . . . . . . . 11
      |
3 | | iblmbf 22804 |
. . . . . . . . . . 11
      MblFn |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
   MblFn |
5 | | iblabsnc.1 |
. . . . . . . . . 10
 
   |
6 | 4, 5 | mbfmptcl 22672 |
. . . . . . . . 9
 
   |
7 | 6 | abscld 13575 |
. . . . . . . 8
 
       |
8 | 7 | rexrd 9708 |
. . . . . . 7
 
       |
9 | 6 | absge0d 13583 |
. . . . . . 7
 
       |
10 | | elxrge0 11767 |
. . . . . . 7
       
    
       |
11 | 8, 9, 10 | sylanbrc 677 |
. . . . . 6
 
          |
12 | | 0e0iccpnf 11769 |
. . . . . . 7
    |
13 | 12 | a1i 11 |
. . . . . 6
 
      |
14 | 11, 13 | ifclda 3904 |
. . . . 5
               |
15 | 14 | adantr 472 |
. . . 4
 

              |
16 | | eqid 2471 |
. . . 4
                       |
17 | 15, 16 | fmptd 6061 |
. . 3
                     |
18 | | reex 9648 |
. . . . . . . . 9
 |
19 | 18 | a1i 11 |
. . . . . . . 8
   |
20 | 6 | recld 13334 |
. . . . . . . . . . . . 13
 
       |
21 | 20 | recnd 9687 |
. . . . . . . . . . . 12
 
       |
22 | 21 | abscld 13575 |
. . . . . . . . . . 11
 
           |
23 | 21 | absge0d 13583 |
. . . . . . . . . . 11
 
           |
24 | | elrege0 11764 |
. . . . . . . . . . 11
           
        
           |
25 | 22, 23, 24 | sylanbrc 677 |
. . . . . . . . . 10
 
              |
26 | | 0e0icopnf 11768 |
. . . . . . . . . . 11
    |
27 | 26 | a1i 11 |
. . . . . . . . . 10
 
      |
28 | 25, 27 | ifclda 3904 |
. . . . . . . . 9
                   |
29 | 28 | adantr 472 |
. . . . . . . 8
 

                  |
30 | 6 | imcld 13335 |
. . . . . . . . . . . . 13
 
       |
31 | 30 | recnd 9687 |
. . . . . . . . . . . 12
 
       |
32 | 31 | abscld 13575 |
. . . . . . . . . . 11
 
           |
33 | 31 | absge0d 13583 |
. . . . . . . . . . 11
 
           |
34 | | elrege0 11764 |
. . . . . . . . . . 11
           
        
           |
35 | 32, 33, 34 | sylanbrc 677 |
. . . . . . . . . 10
 
              |
36 | 35, 27 | ifclda 3904 |
. . . . . . . . 9
                   |
37 | 36 | adantr 472 |
. . . . . . . 8
 

                  |
38 | | eqidd 2472 |
. . . . . . . 8
                                 |
39 | | eqidd 2472 |
. . . . . . . 8
                                 |
40 | 19, 29, 37, 38, 39 | offval2 6567 |
. . . . . . 7
                                                                  |
41 | | iftrue 3878 |
. . . . . . . . . . 11
  
                     |
42 | | iftrue 3878 |
. . . . . . . . . . 11
  
                     |
43 | 41, 42 | oveq12d 6326 |
. . . . . . . . . 10
                                                 |
44 | | iftrue 3878 |
. . . . . . . . . 10
  
                                         |
45 | 43, 44 | eqtr4d 2508 |
. . . . . . . . 9
                                                      |
46 | | 00id 9826 |
. . . . . . . . . 10
   |
47 | | iffalse 3881 |
. . . . . . . . . . 11
                |
48 | | iffalse 3881 |
. . . . . . . . . . 11
                |
49 | 47, 48 | oveq12d 6326 |
. . . . . . . . . 10
                                 |
50 | | iffalse 3881 |
. . . . . . . . . 10
                          |
51 | 46, 49, 50 | 3eqtr4a 2531 |
. . . . . . . . 9
                                                      |
52 | 45, 51 | pm2.61i 169 |
. . . . . . . 8
                                                    |
53 | 52 | mpteq2i 4479 |
. . . . . . 7
                                                        |
54 | 40, 53 | syl6req 2522 |
. . . . . 6
                                           
                 |
55 | 54 | fveq2d 5883 |
. . . . 5
                                                  
                  |
56 | | eqid 2471 |
. . . . . . . 8
                               |
57 | 6 | iblcn 22835 |
. . . . . . . . . 10
    
                   |
58 | 2, 57 | mpbid 215 |
. . . . . . . . 9
                   |
59 | 58 | simpld 466 |
. . . . . . . 8
          |
60 | 5, 2, 56, 59, 20 | iblabsnclem 32069 |
. . . . . . 7
                 MblFn
                      |
61 | 60 | simpld 466 |
. . . . . 6
                MblFn |
62 | 29, 56 | fmptd 6061 |
. . . . . 6
                         |
63 | 60 | simprd 470 |
. . . . . 6
                      |
64 | | eqid 2471 |
. . . . . . 7
                               |
65 | 37, 64 | fmptd 6061 |
. . . . . 6
                         |
66 | 58 | simprd 470 |
. . . . . . . 8
          |
67 | 5, 2, 64, 66, 30 | iblabsnclem 32069 |
. . . . . . 7
                 MblFn
                      |
68 | 67 | simprd 470 |
. . . . . 6
                      |
69 | 61, 62, 63, 65, 68 | itg2addnc 32060 |
. . . . 5
                     
                                                          |
70 | 55, 69 | eqtrd 2505 |
. . . 4
                                                                        |
71 | 63, 68 | readdcld 9688 |
. . . 4
                                           |
72 | 70, 71 | eqeltrd 2549 |
. . 3
                                |
73 | 22, 32 | readdcld 9688 |
. . . . . . . . 9
 
                     |
74 | 73 | rexrd 9708 |
. . . . . . . 8
 
                     |
75 | 22, 32, 23, 33 | addge0d 10210 |
. . . . . . . 8
 
                     |
76 | | elxrge0 11767 |
. . . . . . . 8
                                                              |
77 | 74, 75, 76 | sylanbrc 677 |
. . . . . . 7
 
                        |
78 | 77, 13 | ifclda 3904 |
. . . . . 6
                             |
79 | 78 | adantr 472 |
. . . . 5
 

                            |
80 | | eqid 2471 |
. . . . 5
                                                   |
81 | 79, 80 | fmptd 6061 |
. . . 4
                                   |
82 | | ax-icn 9616 |
. . . . . . . . . . 11
 |
83 | | mulcl 9641 |
. . . . . . . . . . 11
               |
84 | 82, 31, 83 | sylancr 676 |
. . . . . . . . . 10
 
 
       |
85 | 21, 84 | abstrid 13595 |
. . . . . . . . 9
 
                                       |
86 | | iftrue 3878 |
. . . . . . . . . . 11
  
             |
87 | 86 | adantl 473 |
. . . . . . . . . 10
 
  
             |
88 | 6 | replimd 13337 |
. . . . . . . . . . 11
 
               |
89 | 88 | fveq2d 5883 |
. . . . . . . . . 10
 
                       |
90 | 87, 89 | eqtrd 2505 |
. . . . . . . . 9
 
  
                         |
91 | 44 | adantl 473 |
. . . . . . . . . 10
 
  
                                         |
92 | | absmul 13434 |
. . . . . . . . . . . . 13
          
                      |
93 | 82, 31, 92 | sylancr 676 |
. . . . . . . . . . . 12
 
               
           |
94 | | absi 13426 |
. . . . . . . . . . . . . 14
     |
95 | 94 | oveq1i 6318 |
. . . . . . . . . . . . 13
                         |
96 | 32 | recnd 9687 |
. . . . . . . . . . . . . 14
 
           |
97 | 96 | mulid2d 9679 |
. . . . . . . . . . . . 13
 
                     |
98 | 95, 97 | syl5eq 2517 |
. . . . . . . . . . . 12
 
     
                   |
99 | 93, 98 | eqtr2d 2506 |
. . . . . . . . . . 11
 
            
        |
100 | 99 | oveq2d 6324 |
. . . . . . . . . 10
 
                                         |
101 | 91, 100 | eqtrd 2505 |
. . . . . . . . 9
 
  
                                           |
102 | 85, 90, 101 | 3brtr4d 4426 |
. . . . . . . 8
 
  
                                |
103 | 102 | ex 441 |
. . . . . . 7
          
                          |
104 | | 0le0 10721 |
. . . . . . . . 9
 |
105 | 104 | a1i 11 |
. . . . . . . 8

  |
106 | | iffalse 3881 |
. . . . . . . 8
            |
107 | 105, 106,
50 | 3brtr4d 4426 |
. . . . . . 7
                                   |
108 | 103, 107 | pm2.61d1 164 |
. . . . . 6
         
                         |
109 | 108 | ralrimivw 2810 |
. . . . 5
                                    |
110 | | eqidd 2472 |
. . . . . 6
                         |
111 | | eqidd 2472 |
. . . . . 6
                                                     |
112 | 19, 15, 79, 110, 111 | ofrfval2 6568 |
. . . . 5
                                                                           |
113 | 109, 112 | mpbird 240 |
. . . 4
                                        |
114 | | itg2le 22776 |
. . . 4
                    
                               
                                                   
                               |
115 | 17, 81, 113, 114 | syl3anc 1292 |
. . 3
                                               |
116 | | itg2lecl 22775 |
. . 3
                                                               
                                               |
117 | 17, 72, 115, 116 | syl3anc 1292 |
. 2
                  |
118 | 7, 9 | iblpos 22829 |
. 2
                MblFn                    |
119 | 1, 117, 118 | mpbir2and 936 |
1
          |