Proof of Theorem itgmulc2nclem2
Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.4 |
. . . . . . 7
   |
2 | | max0sub 11270 |
. . . . . . 7
            
    |
3 | 1, 2 | syl 16 |
. . . . . 6
                 |
4 | 3 | oveq1d 6208 |
. . . . 5
    
 
      
       |
5 | 4 | adantr 465 |
. . . 4
 
                     |
6 | | 0re 9490 |
. . . . . . . 8
 |
7 | | ifcl 3932 |
. . . . . . . 8
 
   
    |
8 | 1, 6, 7 | sylancl 662 |
. . . . . . 7
   
    |
9 | 8 | recnd 9516 |
. . . . . 6
   
    |
10 | 9 | adantr 465 |
. . . . 5
 
        |
11 | 1 | renegcld 9879 |
. . . . . . . 8
    |
12 | | ifcl 3932 |
. . . . . . . 8
         
   |
13 | 11, 6, 12 | sylancl 662 |
. . . . . . 7
          |
14 | 13 | recnd 9516 |
. . . . . 6
          |
15 | 14 | adantr 465 |
. . . . 5
 
          |
16 | | itgmulc2nc.5 |
. . . . . 6
 
   |
17 | 16 | recnd 9516 |
. . . . 5
 
   |
18 | 10, 15, 17 | subdird 9905 |
. . . 4
 
                     
               |
19 | 5, 18 | eqtr3d 2494 |
. . 3
 
 
                     |
20 | 19 | itgeq2dv 21385 |
. 2
           
 
               |
21 | | ovex 6218 |
. . . 4
        |
22 | 21 | a1i 11 |
. . 3
 
          |
23 | | itgmulc2nc.3 |
. . . 4
      |
24 | | itgmulc2nc.m |
. . . . . . 7
     MblFn |
25 | | ovex 6218 |
. . . . . . . 8
   |
26 | 25 | a1i 11 |
. . . . . . 7
 
 
   |
27 | 24, 26 | mbfdm2 21242 |
. . . . . 6
   |
28 | 8 | adantr 465 |
. . . . . 6
 
        |
29 | | fconstmpt 4983 |
. . . . . . 7
   
 
           |
30 | 29 | a1i 11 |
. . . . . 6
                   |
31 | | eqidd 2452 |
. . . . . 6
       |
32 | 27, 28, 16, 30, 31 | offval2 6439 |
. . . . 5
      
            
      |
33 | | iblmbf 21371 |
. . . . . . 7
      MblFn |
34 | 23, 33 | syl 16 |
. . . . . 6
   MblFn |
35 | | eqid 2451 |
. . . . . . 7
     |
36 | 17, 35 | fmptd 5969 |
. . . . . 6
         |
37 | 34, 8, 36 | mbfmulc2re 21252 |
. . . . 5
      
        MblFn |
38 | 32, 37 | eqeltrrd 2540 |
. . . 4
          MblFn |
39 | 9, 16, 23, 38 | iblmulc2nc 28598 |
. . 3
             |
40 | | ovex 6218 |
. . . 4
          |
41 | 40 | a1i 11 |
. . 3
 
            |
42 | 13 | adantr 465 |
. . . . . 6
 
          |
43 | | fconstmpt 4983 |
. . . . . . 7
   
                 |
44 | 43 | a1i 11 |
. . . . . 6
                       |
45 | 27, 42, 16, 44, 31 | offval2 6439 |
. . . . 5
                        
     |
46 | 34, 13, 36 | mbfmulc2re 21252 |
. . . . 5
                 MblFn |
47 | 45, 46 | eqeltrrd 2540 |
. . . 4
        
   MblFn |
48 | 14, 16, 23, 47 | iblmulc2nc 28598 |
. . 3
        
      |
49 | 19 | mpteq2dva 4479 |
. . . 4
                           |
50 | 49, 24 | eqeltrrd 2540 |
. . 3
     
 
             MblFn |
51 | 22, 39, 41, 48, 50 | itgsubnc 28595 |
. 2
       
                    
        
          |
52 | | ovex 6218 |
. . . . . . 7
             |
53 | 52 | a1i 11 |
. . . . . 6
 
               |
54 | | ifcl 3932 |
. . . . . . . 8
 
   
    |
55 | 16, 6, 54 | sylancl 662 |
. . . . . . 7
 
        |
56 | 16 | iblre 21397 |
. . . . . . . . 9
    
               
       |
57 | 23, 56 | mpbid 210 |
. . . . . . . 8
          
            |
58 | 57 | simpld 459 |
. . . . . . 7
    
      |
59 | | eqidd 2452 |
. . . . . . . . 9
    
      
     |
60 | 27, 28, 55, 30, 59 | offval2 6439 |
. . . . . . . 8
      
                 
           |
61 | 16, 34 | mbfpos 21255 |
. . . . . . . . 9
    
   MblFn |
62 | 55 | recnd 9516 |
. . . . . . . . . 10
 
        |
63 | | eqid 2451 |
. . . . . . . . . 10
  
 
    
 
   |
64 | 62, 63 | fmptd 5969 |
. . . . . . . . 9
    
         |
65 | 61, 8, 64 | mbfmulc2re 21252 |
. . . . . . . 8
      
             MblFn |
66 | 60, 65 | eqeltrrd 2540 |
. . . . . . 7
          
    MblFn |
67 | 9, 55, 58, 66 | iblmulc2nc 28598 |
. . . . . 6
          
       |
68 | | ovex 6218 |
. . . . . . 7
           
   |
69 | 68 | a1i 11 |
. . . . . 6
 
            
    |
70 | 16 | renegcld 9879 |
. . . . . . . 8
 
    |
71 | | ifcl 3932 |
. . . . . . . 8
         
   |
72 | 70, 6, 71 | sylancl 662 |
. . . . . . 7
 
          |
73 | 57 | simprd 463 |
. . . . . . 7
             |
74 | | eqidd 2452 |
. . . . . . . . 9
                
    |
75 | 27, 28, 72, 30, 74 | offval2 6439 |
. . . . . . . 8
      
                                 |
76 | 16, 34 | mbfneg 21254 |
. . . . . . . . . 10
    MblFn |
77 | 70, 76 | mbfpos 21255 |
. . . . . . . . 9
          MblFn |
78 | 72 | recnd 9516 |
. . . . . . . . . 10
 
          |
79 | | eqid 2451 |
. . . . . . . . . 10
  
        
       |
80 | 78, 79 | fmptd 5969 |
. . . . . . . . 9
                |
81 | 77, 8, 80 | mbfmulc2re 21252 |
. . . . . . . 8
      
               MblFn |
82 | 75, 81 | eqeltrrd 2540 |
. . . . . . 7
                 MblFn |
83 | 9, 72, 73, 82 | iblmulc2nc 28598 |
. . . . . 6
                    |
84 | | max0sub 11270 |
. . . . . . . . . . . 12
            
    |
85 | 16, 84 | syl 16 |
. . . . . . . . . . 11
 
            
    |
86 | 85 | oveq2d 6209 |
. . . . . . . . . 10
 
         
 
      
      
     |
87 | 10, 62, 78 | subdid 9904 |
. . . . . . . . . 10
 
         
 
      
            
      
             |
88 | 86, 87 | eqtr3d 2494 |
. . . . . . . . 9
 
           
 
         
 
      
     |
89 | 88 | mpteq2dva 4479 |
. . . . . . . 8
              
 
         
 
      
      |
90 | 32, 89 | eqtrd 2492 |
. . . . . . 7
      
                  
      
              |
91 | 90, 37 | eqeltrrd 2540 |
. . . . . 6
     
 
         
 
      
    MblFn |
92 | 53, 67, 69, 83, 91 | itgsubnc 28595 |
. . . . 5
       
                   
               
                        |
93 | 88 | itgeq2dv 21385 |
. . . . 5
                
 
         
 
      
      |
94 | 16, 23 | itgreval 21400 |
. . . . . . 7
                          |
95 | 94 | oveq2d 6209 |
. . . . . 6
              
                         |
96 | 55, 58 | itgcl 21387 |
. . . . . . 7
    
 
    |
97 | 72, 73 | itgcl 21387 |
. . . . . . 7
    
        |
98 | 9, 96, 97 | subdid 9904 |
. . . . . 6
                               
 
             
                |
99 | | max1 11261 |
. . . . . . . . 9
 

 
 
   |
100 | 6, 1, 99 | sylancr 663 |
. . . . . . . 8

 
 
   |
101 | | max1 11261 |
. . . . . . . . 9
 

 
 
   |
102 | 6, 16, 101 | sylancr 663 |
. . . . . . . 8
 
   
    |
103 | 9, 55, 58, 66, 8, 55, 100, 102 | itgmulc2nclem1 28599 |
. . . . . . 7
          
 
                    |
104 | | max1 11261 |
. . . . . . . . 9
             |
105 | 6, 70, 104 | sylancr 663 |
. . . . . . . 8
 
          |
106 | 9, 72, 73, 82, 8, 72, 100, 105 | itgmulc2nclem1 28599 |
. . . . . . 7
          
                    
     |
107 | 103, 106 | oveq12d 6211 |
. . . . . 6
    
 
             
                    
             
 
      
      |
108 | 95, 98, 107 | 3eqtrd 2496 |
. . . . 5
                               
 
      
      |
109 | 92, 93, 108 | 3eqtr4d 2502 |
. . . 4
                       |
110 | | ovex 6218 |
. . . . . . 7
         
 
   |
111 | 110 | a1i 11 |
. . . . . 6
 
          
 
    |
112 | 27, 42, 55, 44, 59 | offval2 6439 |
. . . . . . . 8
                 
       
              |
113 | 61, 13, 64 | mbfmulc2re 21252 |
. . . . . . . 8
                 
    MblFn |
114 | 112, 113 | eqeltrrd 2540 |
. . . . . . 7
        
        MblFn |
115 | 14, 55, 58, 114 | iblmulc2nc 28598 |
. . . . . 6
        
           |
116 | | ovex 6218 |
. . . . . . 7
         
       |
117 | 116 | a1i 11 |
. . . . . 6
 
          
        |
118 | 27, 42, 72, 44, 74 | offval2 6439 |
. . . . . . . 8
                                  
         |
119 | 77, 13, 80 | mbfmulc2re 21252 |
. . . . . . . 8
                        MblFn |
120 | 118, 119 | eqeltrrd 2540 |
. . . . . . 7
        
      
   MblFn |
121 | 14, 72, 73, 120 | iblmulc2nc 28598 |
. . . . . 6
        
      
      |
122 | 85 | oveq2d 6209 |
. . . . . . . . . 10
 
                    
              |
123 | 15, 62, 78 | subdid 9904 |
. . . . . . . . . 10
 
                    
          
         
          
     |
124 | 122, 123 | eqtr3d 2494 |
. . . . . . . . 9
 
                    
 
           
         |
125 | 124 | mpteq2dva 4479 |
. . . . . . . 8
        
              
 
           
          |
126 | 45, 125 | eqtrd 2492 |
. . . . . . 7
                     
             
          
      |
127 | 126, 46 | eqeltrrd 2540 |
. . . . . 6
     
             
          
    MblFn |
128 | 111, 115,
117, 121, 127 | itgsubnc 28595 |
. . . . 5
              
                                  
            
      
      |
129 | 124 | itgeq2dv 21385 |
. . . . 5
                         
 
           
          |
130 | 94 | oveq2d 6209 |
. . . . . 6
       
           
                        |
131 | 14, 96, 97 | subdid 9904 |
. . . . . 6
       
                         
                         
          |
132 | | max1 11261 |
. . . . . . . . 9
             |
133 | 6, 11, 132 | sylancr 663 |
. . . . . . . 8

 
       |
134 | 14, 55, 58, 114, 13, 55, 133, 102 | itgmulc2nclem1 28599 |
. . . . . . 7
       
                     
 
     |
135 | 14, 72, 73, 120, 13, 72, 133, 105 | itgmulc2nclem1 28599 |
. . . . . . 7
       
                                 |
136 | 134, 135 | oveq12d 6211 |
. . . . . 6
    
                         
                 
            
          
      |
137 | 130, 131,
136 | 3eqtrd 2496 |
. . . . 5
       
                  
            
      
      |
138 | 128, 129,
137 | 3eqtr4d 2502 |
. . . 4
                           |
139 | 109, 138 | oveq12d 6211 |
. . 3
       
        
                                  |
140 | 16, 23 | itgcl 21387 |
. . . 4
      |
141 | 9, 14, 140 | subdird 9905 |
. . 3
    
 
      
         
 
                    |
142 | 3 | oveq1d 6208 |
. . 3
    
 
      
        
    |
143 | 139, 141,
142 | 3eqtr2d 2498 |
. 2
       
        
               |
144 | 20, 51, 143 | 3eqtrrd 2497 |
1
   
         |