Step | Hyp | Ref
| Expression |
1 | | mbff 22662 |
. . . . . . 7
 MblFn       |
2 | 1 | ad2antrr 740 |
. . . . . 6
   MblFn   
         
 
      |
3 | | ffn 5739 |
. . . . . 6
       |
4 | 2, 3 | syl 17 |
. . . . 5
   MblFn   
         
 
  |
5 | | iblmbf 22804 |
. . . . . . . 8
  MblFn |
6 | 5 | ad2antlr 741 |
. . . . . . 7
   MblFn   
         
 
MblFn |
7 | | mbff 22662 |
. . . . . . 7
 MblFn       |
8 | 6, 7 | syl 17 |
. . . . . 6
   MblFn   
         
 
      |
9 | | ffn 5739 |
. . . . . 6
       |
10 | 8, 9 | syl 17 |
. . . . 5
   MblFn   
         
 
  |
11 | | mbfdm 22663 |
. . . . . 6
 MblFn
  |
12 | 11 | ad2antrr 740 |
. . . . 5
   MblFn   
         
 
  |
13 | | mbfdm 22663 |
. . . . . 6
 MblFn
  |
14 | 6, 13 | syl 17 |
. . . . 5
   MblFn   
         
 
  |
15 | | eqid 2471 |
. . . . 5

    |
16 | | eqidd 2472 |
. . . . 5
    MblFn
 
          
 
           |
17 | | eqidd 2472 |
. . . . 5
    MblFn
 
          
 
           |
18 | 4, 10, 12, 14, 15, 16, 17 | offval 6557 |
. . . 4
   MblFn   
         
 
 
                 |
19 | | ovex 6336 |
. . . . . 6
           |
20 | 19 | a1i 11 |
. . . . 5
    MblFn
 
          
 
               |
21 | | simpll 768 |
. . . . . . 7
   MblFn   
         
 
MblFn |
22 | 21, 6 | mbfmul 22763 |
. . . . . 6
   MblFn   
         
 
 

MblFn |
23 | 18, 22 | eqeltrrd 2550 |
. . . . 5
   MblFn   
         
 
              MblFn |
24 | 23, 20 | mbfmptcl 22672 |
. . . . . . . 8
    MblFn
 
          
 
               |
25 | | eqidd 2472 |
. . . . . . . 8
   MblFn   
         
 
                              |
26 | | absf 13477 |
. . . . . . . . . 10
     |
27 | 26 | a1i 11 |
. . . . . . . . 9
   MblFn   
         
 
      |
28 | 27 | feqmptd 5932 |
. . . . . . . 8
   MblFn   
         
 
        |
29 | | fveq2 5879 |
. . . . . . . 8
                               |
30 | 24, 25, 28, 29 | fmptco 6072 |
. . . . . . 7
   MblFn   
         
 
                                    |
31 | | eqid 2471 |
. . . . . . . . 9
                             |
32 | 24, 31 | fmptd 6061 |
. . . . . . . 8
   MblFn   
         
 
                      |
33 | | ax-resscn 9614 |
. . . . . . . . . . 11
 |
34 | | ssid 3437 |
. . . . . . . . . . 11
 |
35 | | cncfss 22009 |
. . . . . . . . . . 11
 
           |
36 | 33, 34, 35 | mp2an 686 |
. . . . . . . . . 10
         |
37 | | abscncf 22011 |
. . . . . . . . . 10
     |
38 | 36, 37 | sselii 3415 |
. . . . . . . . 9
     |
39 | 38 | a1i 11 |
. . . . . . . 8
   MblFn   
         
 
      |
40 | | cncombf 22693 |
. . . . . . . 8
                MblFn                                          MblFn |
41 | 23, 32, 39, 40 | syl3anc 1292 |
. . . . . . 7
   MblFn   
         
 
                MblFn |
42 | 30, 41 | eqeltrrd 2550 |
. . . . . 6
   MblFn   
         
 
                  MblFn |
43 | 24 | abscld 13575 |
. . . . . . . . . . . 12
    MblFn
 
          
 
                   |
44 | 43 | rexrd 9708 |
. . . . . . . . . . 11
    MblFn
 
          
 
                   |
45 | 24 | absge0d 13583 |
. . . . . . . . . . 11
    MblFn
 
          
 
                   |
46 | | elxrge0 11767 |
. . . . . . . . . . 11
                 
              
                 |
47 | 44, 45, 46 | sylanbrc 677 |
. . . . . . . . . 10
    MblFn
 
          
 
                      |
48 | | 0e0iccpnf 11769 |
. . . . . . . . . . 11
    |
49 | 48 | a1i 11 |
. . . . . . . . . 10
    MblFn
 
          
 
        |
50 | 47, 49 | ifclda 3904 |
. . . . . . . . 9
   MblFn   
         
 
  
                       |
51 | 50 | adantr 472 |
. . . . . . . 8
    MblFn
 
          
 

  
                       |
52 | | eqid 2471 |
. . . . . . . 8
   
                      
                    |
53 | 51, 52 | fmptd 6061 |
. . . . . . 7
   MblFn   
         
 
                                |
54 | | reex 9648 |
. . . . . . . . . . . . . . 15
 |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
    MblFn
 
          
 
     |
56 | | simprl 772 |
. . . . . . . . . . . . . . 15
   MblFn   
         
 
  |
57 | 56 | ad2antrr 740 |
. . . . . . . . . . . . . 14
     MblFn
            
 
  
   |
58 | | elin 3608 |
. . . . . . . . . . . . . . . . . . . 20
  
    |
59 | 58 | simprbi 471 |
. . . . . . . . . . . . . . . . . . 19
     |
60 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . . 19
      
      |
61 | 8, 59, 60 | syl2an 485 |
. . . . . . . . . . . . . . . . . 18
    MblFn
 
          
 
         |
62 | 61 | abscld 13575 |
. . . . . . . . . . . . . . . . 17
    MblFn
 
          
 
             |
63 | 61 | absge0d 13583 |
. . . . . . . . . . . . . . . . 17
    MblFn
 
          
 
             |
64 | | elrege0 11764 |
. . . . . . . . . . . . . . . . 17
           
        
           |
65 | 62, 63, 64 | sylanbrc 677 |
. . . . . . . . . . . . . . . 16
    MblFn
 
          
 
                |
66 | | 0e0icopnf 11768 |
. . . . . . . . . . . . . . . . 17
    |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . 16
    MblFn
 
          
 
        |
68 | 65, 67 | ifclda 3904 |
. . . . . . . . . . . . . . 15
   MblFn   
         
 
  
                 |
69 | 68 | ad2antrr 740 |
. . . . . . . . . . . . . 14
     MblFn
            
 
  
                     |
70 | | fconstmpt 4883 |
. . . . . . . . . . . . . . 15
       |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . 14
    MblFn
 
          
 
           |
72 | | eqidd 2472 |
. . . . . . . . . . . . . 14
    MblFn
 
          
 
                                       |
73 | 55, 57, 69, 71, 72 | offval2 6567 |
. . . . . . . . . . . . 13
    MblFn
 
          
 
                            
                   |
74 | | ovif2 6393 |
. . . . . . . . . . . . . . 15
                   
                 |
75 | 56 | recnd 9687 |
. . . . . . . . . . . . . . . . . 18
   MblFn   
         
 
  |
76 | 75 | adantr 472 |
. . . . . . . . . . . . . . . . 17
    MblFn
 
          
 
  
  |
77 | 76 | mul01d 9850 |
. . . . . . . . . . . . . . . 16
    MblFn
 
          
 
       |
78 | 77 | ifeq2d 3891 |
. . . . . . . . . . . . . . 15
    MblFn
 
          
 
                        
                |
79 | 74, 78 | syl5eq 2517 |
. . . . . . . . . . . . . 14
    MblFn
 
          
 
                                       |
80 | 79 | mpteq2dv 4483 |
. . . . . . . . . . . . 13
    MblFn
 
          
 
    
                                      |
81 | 73, 80 | eqtrd 2505 |
. . . . . . . . . . . 12
    MblFn
 
          
 
                                                |
82 | 81 | fveq2d 5883 |
. . . . . . . . . . 11
    MblFn
 
          
 
                                                        |
83 | 68 | adantr 472 |
. . . . . . . . . . . . . 14
    MblFn
 
          
 

  
                 |
84 | | eqid 2471 |
. . . . . . . . . . . . . 14
   
                
              |
85 | 83, 84 | fmptd 6061 |
. . . . . . . . . . . . 13
   MblFn   
         
 
                          |
86 | 85 | adantr 472 |
. . . . . . . . . . . 12
    MblFn
 
          
 
                             |
87 | | inss2 3644 |
. . . . . . . . . . . . . . . . . 18


 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   MblFn   
         
 

   |
89 | 23, 20 | mbfdm2 22673 |
. . . . . . . . . . . . . . . . 17
   MblFn   
         
 

   |
90 | 8 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . 17
    MblFn
 
          
 
       |
91 | 8 | feqmptd 5932 |
. . . . . . . . . . . . . . . . . 18
   MblFn   
         
 
        |
92 | | simplr 770 |
. . . . . . . . . . . . . . . . . 18
   MblFn   
         
 
   |
93 | 91, 92 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . 17
   MblFn   
         
 
         |
94 | 88, 89, 90, 93 | iblss 22841 |
. . . . . . . . . . . . . . . 16
   MblFn   
         
 
           |
95 | 61, 94 | iblabs 22865 |
. . . . . . . . . . . . . . 15
   MblFn   
         
 
               |
96 | 62, 63 | iblpos 22829 |
. . . . . . . . . . . . . . 15
   MblFn   
         
 
  
                        MblFn                          |
97 | 95, 96 | mpbid 215 |
. . . . . . . . . . . . . 14
   MblFn   
         
 
  
          MblFn                         |
98 | 97 | simprd 470 |
. . . . . . . . . . . . 13
   MblFn   
         
 
                       |
99 | 98 | adantr 472 |
. . . . . . . . . . . 12
    MblFn
 
          
 
         
                |
100 | | simplrl 778 |
. . . . . . . . . . . . 13
    MblFn
 
          
 
  
  |
101 | | neq0 3733 |
. . . . . . . . . . . . . . 15
   
    |
102 | | 0re 9661 |
. . . . . . . . . . . . . . . . . . 19
 |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
    MblFn
 
          
 
     |
104 | 58 | simplbi 467 |
. . . . . . . . . . . . . . . . . . . 20
     |
105 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . . . 20
      
      |
106 | 2, 104, 105 | syl2an 485 |
. . . . . . . . . . . . . . . . . . 19
    MblFn
 
          
 
         |
107 | 106 | abscld 13575 |
. . . . . . . . . . . . . . . . . 18
    MblFn
 
          
 
             |
108 | | simplrl 778 |
. . . . . . . . . . . . . . . . . 18
    MblFn
 
          
 
     |
109 | 106 | absge0d 13583 |
. . . . . . . . . . . . . . . . . 18
    MblFn
 
          
 
             |
110 | | simprr 774 |
. . . . . . . . . . . . . . . . . . 19
   MblFn   
         
 
            |
111 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
112 | 111 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
113 | 112 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . 20
         
           |
114 | 113 | rspccva 3135 |
. . . . . . . . . . . . . . . . . . 19
           
        
  |
115 | 110, 104,
114 | syl2an 485 |
. . . . . . . . . . . . . . . . . 18
    MblFn
 
          
 
             |
116 | 103, 107,
108, 109, 115 | letrd 9809 |
. . . . . . . . . . . . . . . . 17
    MblFn
 
          
 
     |
117 | 116 | ex 441 |
. . . . . . . . . . . . . . . 16
   MblFn   
         
 
      |
118 | 117 | exlimdv 1787 |
. . . . . . . . . . . . . . 15
   MblFn   
         
 
 
 
   |
119 | 101, 118 | syl5bi 225 |
. . . . . . . . . . . . . 14
   MblFn   
         
 
      |
120 | 119 | imp 436 |
. . . . . . . . . . . . 13
    MblFn
 
          
 
  
  |
121 | | elrege0 11764 |
. . . . . . . . . . . . 13
   
    |
122 | 100, 120,
121 | sylanbrc 677 |
. . . . . . . . . . . 12
    MblFn
 
          
 
  
     |
123 | 86, 99, 122 | itg2mulc 22784 |
. . . . . . . . . . 11
    MblFn
 
          
 
                                                        |
124 | 82, 123 | eqtr3d 2507 |
. . . . . . . . . 10
    MblFn
 
          
 
         
                                         |
125 | 100, 99 | remulcld 9689 |
. . . . . . . . . 10
    MblFn
 
          
 
                            |
126 | 124, 125 | eqeltrd 2549 |
. . . . . . . . 9
    MblFn
 
          
 
         
                  |
127 | 126 | ex 441 |
. . . . . . . 8
   MblFn   
         
 
                             |
128 | | noel 3726 |
. . . . . . . . . . . . . 14
 |
129 | | eleq2 2538 |
. . . . . . . . . . . . . 14
    
    |
130 | 128, 129 | mtbiri 310 |
. . . . . . . . . . . . 13
  

   |
131 | | iffalse 3881 |
. . . . . . . . . . . . 13
 
                    |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . 12
                      |
133 | 132 | mpteq2dv 4483 |
. . . . . . . . . . 11
                          |
134 | | fconstmpt 4883 |
. . . . . . . . . . 11
       |
135 | 133, 134 | syl6eqr 2523 |
. . . . . . . . . 10
                            |
136 | 135 | fveq2d 5883 |
. . . . . . . . 9
                                    |
137 | | itg20 22774 |
. . . . . . . . . 10
         |
138 | 137, 102 | eqeltri 2545 |
. . . . . . . . 9
         |
139 | 136, 138 | syl6eqel 2557 |
. . . . . . . 8
                            |
140 | 127, 139 | pm2.61d2 165 |
. . . . . . 7
   MblFn   
         
 
                         |
141 | 108, 62 | remulcld 9689 |
. . . . . . . . . . . . 13
    MblFn
 
          
 
               |
142 | 141 | rexrd 9708 |
. . . . . . . . . . . 12
    MblFn
 
          
 
               |
143 | 108, 62, 116, 63 | mulge0d 10211 |
. . . . . . . . . . . 12
    MblFn
 
          
 
               |
144 | | elxrge0 11767 |
. . . . . . . . . . . 12
                        
             |
145 | 142, 143,
144 | sylanbrc 677 |
. . . . . . . . . . 11
    MblFn
 
          
 
                  |
146 | 145, 49 | ifclda 3904 |
. . . . . . . . . 10
   MblFn   
         
 
  
                   |
147 | 146 | adantr 472 |
. . . . . . . . 9
    MblFn
 
          
 

  
                   |
148 | | eqid 2471 |
. . . . . . . . 9
   
                                   |
149 | 147, 148 | fmptd 6061 |
. . . . . . . 8
   MblFn   
         
 
                            |
150 | 106, 61 | absmuld 13593 |
. . . . . . . . . . . . 13
    MblFn
 
          
 
                                     |
151 | | abscl 13418 |
. . . . . . . . . . . . . . . 16
               |
152 | | absge0 13427 |
. . . . . . . . . . . . . . . 16
               |
153 | 151, 152 | jca 541 |
. . . . . . . . . . . . . . 15
                         |
154 | 61, 153 | syl 17 |
. . . . . . . . . . . . . 14
    MblFn
 
          
 
                       |
155 | | lemul1a 10481 |
. . . . . . . . . . . . . 14
          
                                                          |
156 | 107, 108,
154, 115, 155 | syl31anc 1295 |
. . . . . . . . . . . . 13
    MblFn
 
          
 
                                 |
157 | 150, 156 | eqbrtrd 4416 |
. . . . . . . . . . . 12
    MblFn
 
          
 
                             |
158 | | iftrue 3878 |
. . . . . . . . . . . . 13
                                        |
159 | 158 | adantl 473 |
. . . . . . . . . . . 12
    MblFn
 
          
 
                                        |
160 | | iftrue 3878 |
. . . . . . . . . . . . 13
                                |
161 | 160 | adantl 473 |
. . . . . . . . . . . 12
    MblFn
 
          
 
                                |
162 | 157, 159,
161 | 3brtr4d 4426 |
. . . . . . . . . . 11
    MblFn
 
          
 
                       
  
                |
163 | | 0le0 10721 |
. . . . . . . . . . . . . 14
 |
164 | 163 | a1i 11 |
. . . . . . . . . . . . 13
 
   |
165 | | iffalse 3881 |
. . . . . . . . . . . . 13
 
                        |
166 | 164, 165,
131 | 3brtr4d 4426 |
. . . . . . . . . . . 12
 
                                         |
167 | 166 | adantl 473 |
. . . . . . . . . . 11
    MblFn
 
          
 
                       
  
                |
168 | 162, 167 | pm2.61dan 808 |
. . . . . . . . . 10
   MblFn   
         
 
  
                                     |
169 | 168 | ralrimivw 2810 |
. . . . . . . . 9
   MblFn   
         
 
                                         |
170 | 54 | a1i 11 |
. . . . . . . . . 10
   MblFn   
         
 
  |
171 | | eqidd 2472 |
. . . . . . . . . 10
   MblFn   
         
 
                          
                     |
172 | | eqidd 2472 |
. . . . . . . . . 10
   MblFn   
         
 
                                        |
173 | 170, 51, 147, 171, 172 | ofrfval2 6568 |
. . . . . . . . 9
   MblFn   
         
 
                                            
                    
  
                 |
174 | 169, 173 | mpbird 240 |
. . . . . . . 8
   MblFn   
         
 
                                             |
175 | | itg2le 22776 |
. . . . . . . 8
                                                                                                     
                                 
                  |
176 | 53, 149, 174, 175 | syl3anc 1292 |
. . . . . . 7
   MblFn   
         
 
                                 
                  |
177 | | itg2lecl 22775 |
. . . . . . 7
                                                                                        
                                              |
178 | 53, 140, 176, 177 | syl3anc 1292 |
. . . . . 6
   MblFn   
         
 
                             |
179 | 43, 45 | iblpos 22829 |
. . . . . 6
   MblFn   
         
 
  
                                    MblFn                                |
180 | 42, 178, 179 | mpbir2and 936 |
. . . . 5
   MblFn   
         
 
                     |
181 | 20, 23, 180 | iblabsr 22866 |
. . . 4
   MblFn   
         
 
                 |
182 | 18, 181 | eqeltrd 2549 |
. . 3
   MblFn   
         
 
 
    |
183 | 182 | rexlimdvaa 2872 |
. 2
  MblFn
                     |
184 | 183 | 3impia 1228 |
1
  MblFn
 
          
 
    |