Step | Hyp | Ref
| Expression |
1 | | simprr 774 |
. . . . . . 7
                           
      |
2 | | itg1cl 22722 |
. . . . . . . 8
       |
3 | 2 | adantr 472 |
. . . . . . 7
                                  |
4 | 1, 3 | eqeltrd 2549 |
. . . . . 6
                           
  |
5 | 4 | rexlimiva 2868 |
. . . . 5
                              |
6 | 5 | abssi 3490 |
. . . 4
                              |
7 | 6 | a1i 11 |
. . 3
  
  
                          |
8 | | i1f0 22724 |
. . . . . 6
     |
9 | | 3nn 10791 |
. . . . . . . 8
 |
10 | | nnrp 11334 |
. . . . . . . 8
   |
11 | | ne0i 3728 |
. . . . . . . 8

  |
12 | 9, 10, 11 | mp2b 10 |
. . . . . . 7
 |
13 | | itg2addnc.f2 |
. . . . . . . . . . . . 13
          |
14 | 13 | ffvelrnda 6037 |
. . . . . . . . . . . 12
 

         |
15 | | elrege0 11764 |
. . . . . . . . . . . 12
       
            |
16 | 14, 15 | sylib 201 |
. . . . . . . . . . 11
 

            |
17 | 16 | simprd 470 |
. . . . . . . . . 10
 

      |
18 | 17 | ralrimiva 2809 |
. . . . . . . . 9
        |
19 | | reex 9648 |
. . . . . . . . . . 11
 |
20 | 19 | a1i 11 |
. . . . . . . . . 10
   |
21 | | c0ex 9655 |
. . . . . . . . . . 11
 |
22 | 21 | a1i 11 |
. . . . . . . . . 10
 

  |
23 | | eqidd 2472 |
. . . . . . . . . 10
       |
24 | 13 | feqmptd 5932 |
. . . . . . . . . 10
         |
25 | 20, 22, 14, 23, 24 | ofrfval2 6568 |
. . . . . . . . 9
    
        |
26 | 18, 25 | mpbird 240 |
. . . . . . . 8
      |
27 | 26 | ralrimivw 2810 |
. . . . . . 7
       |
28 | | r19.2z 3849 |
. . . . . . 7
 

   
   
  |
29 | 12, 27, 28 | sylancr 676 |
. . . . . 6
       |
30 | | fveq2 5879 |
. . . . . . . . . 10
                   |
31 | | itg10 22725 |
. . . . . . . . . 10
         |
32 | 30, 31 | syl6req 2522 |
. . . . . . . . 9
           |
33 | 32 | biantrud 515 |
. . . . . . . 8
                                                     |
34 | | fveq1 5878 |
. . . . . . . . . . . . 13
                   |
35 | 21 | fvconst2 6136 |
. . . . . . . . . . . . 13
           |
36 | 34, 35 | sylan9eq 2525 |
. . . . . . . . . . . 12
             |
37 | 36 | iftrued 3880 |
. . . . . . . . . . 11
                        |
38 | 37 | mpteq2dva 4482 |
. . . . . . . . . 10
                          |
39 | 38 | breq1d 4405 |
. . . . . . . . 9
                              |
40 | 39 | rexbidv 2892 |
. . . . . . . 8
                                |
41 | 33, 40 | bitr3d 263 |
. . . . . . 7
                              
   
   |
42 | 41 | rspcev 3136 |
. . . . . 6
         
                              |
43 | 8, 29, 42 | sylancr 676 |
. . . . 5
                              |
44 | | eqeq1 2475 |
. . . . . . . 8
     
       |
45 | 44 | anbi2d 718 |
. . . . . . 7
                          
 
                          |
46 | 45 | rexbidv 2892 |
. . . . . 6
  
                         
                     
        |
47 | 21, 46 | elab 3173 |
. . . . 5
                             
                     
       |
48 | 43, 47 | sylibr 217 |
. . . 4
                                |
49 | | ne0i 3728 |
. . . 4
                                                    
        |
50 | 48, 49 | syl 17 |
. . 3
  
  
                          |
51 | | icossicc 11746 |
. . . . . . 7
       |
52 | | fss 5749 |
. . . . . . 7
                         |
53 | 51, 52 | mpan2 685 |
. . . . . 6
                 |
54 | | eqid 2471 |
. . . . . . 7
                             

  
                         |
55 | 54 | itg2addnclem 32057 |
. . . . . 6
                                    
          |
56 | 13, 53, 55 | 3syl 18 |
. . . . 5
       

  
                            |
57 | | itg2addnc.f3 |
. . . . 5
       |
58 | 56, 57 | eqeltrrd 2550 |
. . . 4
                                    |
59 | | ressxr 9702 |
. . . . . . 7
 |
60 | 6, 59 | sstri 3427 |
. . . . . 6
                              |
61 | | supxrub 11635 |
. . . . . 6
   
  
                                              
                                          |
62 | 60, 61 | mpan 684 |
. . . . 5
                                                                 |
63 | 62 | rgen 2766 |
. . . 4
  
  
                                                           |
64 | | breq2 4399 |
. . . . . 6
                         
            
  
                             |
65 | 64 | ralbidv 2829 |
. . . . 5
                         
           
  
                        
  
  
                                                             |
66 | 65 | rspcev 3136 |
. . . 4
                                     
  
                                                                                             |
67 | 58, 63, 66 | sylancl 675 |
. . 3
                                   |
68 | | simprr 774 |
. . . . . . 7
                           
      |
69 | | itg1cl 22722 |
. . . . . . . 8
       |
70 | 69 | adantr 472 |
. . . . . . 7
                                  |
71 | 68, 70 | eqeltrd 2549 |
. . . . . 6
                           
  |
72 | 71 | rexlimiva 2868 |
. . . . 5
                              |
73 | 72 | abssi 3490 |
. . . 4
                              |
74 | 73 | a1i 11 |
. . 3
  
  
                          |
75 | | itg2addnc.g2 |
. . . . . . . . . . . . 13
          |
76 | 75 | ffvelrnda 6037 |
. . . . . . . . . . . 12
 

         |
77 | | elrege0 11764 |
. . . . . . . . . . . 12
       
            |
78 | 76, 77 | sylib 201 |
. . . . . . . . . . 11
 

            |
79 | 78 | simprd 470 |
. . . . . . . . . 10
 

      |
80 | 79 | ralrimiva 2809 |
. . . . . . . . 9
        |
81 | 75 | feqmptd 5932 |
. . . . . . . . . 10
         |
82 | 20, 22, 76, 23, 81 | ofrfval2 6568 |
. . . . . . . . 9
    
        |
83 | 80, 82 | mpbird 240 |
. . . . . . . 8
      |
84 | 83 | ralrimivw 2810 |
. . . . . . 7
       |
85 | | r19.2z 3849 |
. . . . . . 7
 

   
   
  |
86 | 12, 84, 85 | sylancr 676 |
. . . . . 6
       |
87 | | fveq2 5879 |
. . . . . . . . . 10
                   |
88 | 87, 31 | syl6req 2522 |
. . . . . . . . 9
           |
89 | 88 | biantrud 515 |
. . . . . . . 8
                                                     |
90 | | fveq1 5878 |
. . . . . . . . . . . . 13
                   |
91 | 90, 35 | sylan9eq 2525 |
. . . . . . . . . . . 12
             |
92 | 91 | iftrued 3880 |
. . . . . . . . . . 11
                        |
93 | 92 | mpteq2dva 4482 |
. . . . . . . . . 10
                          |
94 | 93 | breq1d 4405 |
. . . . . . . . 9
                              |
95 | 94 | rexbidv 2892 |
. . . . . . . 8
                                |
96 | 89, 95 | bitr3d 263 |
. . . . . . 7
                              
   
   |
97 | 96 | rspcev 3136 |
. . . . . 6
         
                              |
98 | 8, 86, 97 | sylancr 676 |
. . . . 5
                              |
99 | | eqeq1 2475 |
. . . . . . . 8
     
       |
100 | 99 | anbi2d 718 |
. . . . . . 7
                          
 
                          |
101 | 100 | rexbidv 2892 |
. . . . . 6
  
                         
                     
        |
102 | 21, 101 | elab 3173 |
. . . . 5
                             
                     
       |
103 | 98, 102 | sylibr 217 |
. . . 4
                                |
104 | | ne0i 3728 |
. . . 4
                                                    
        |
105 | 103, 104 | syl 17 |
. . 3
  
  
                          |
106 | | fss 5749 |
. . . . . . 7
                         |
107 | 51, 106 | mpan2 685 |
. . . . . 6
                 |
108 | | eqid 2471 |
. . . . . . 7
                             

  
                         |
109 | 108 | itg2addnclem 32057 |
. . . . . 6
                                    
          |
110 | 75, 107, 109 | 3syl 18 |
. . . . 5
       

  
                            |
111 | | itg2addnc.g3 |
. . . . 5
       |
112 | 110, 111 | eqeltrrd 2550 |
. . . 4
                                    |
113 | 73, 59 | sstri 3427 |
. . . . . 6
                              |
114 | | supxrub 11635 |
. . . . . 6
   
  
                                              
                                          |
115 | 113, 114 | mpan 684 |
. . . . 5
                                                                 |
116 | 115 | rgen 2766 |
. . . 4
  
  
                                                           |
117 | | breq2 4399 |
. . . . . 6
                         
            
  
                             |
118 | 117 | ralbidv 2829 |
. . . . 5
                         
           
  
                        
  
  
                                                             |
119 | 118 | rspcev 3136 |
. . . 4
                                     
  
                                                                                             |
120 | 112, 116,
119 | sylancl 675 |
. . 3
                                   |
121 | | eqid 2471 |
. . 3
   
  
                         
                                  
                              
                                  |
122 | 7, 50, 67, 74, 105, 120, 121 | supadd 10597 |
. 2
                          
          

  
                         
      
  
                         
                                  
  |
123 | | supxrre 11638 |
. . . . 5
   
  
                                                                                                                                                       
  |
124 | 7, 50, 67, 123 | syl3anc 1292 |
. . . 4
                                                                  
  |
125 | 56, 124 | eqtrd 2505 |
. . 3
       

  
                         
  |
126 | | supxrre 11638 |
. . . . 5
   
  
                                                                                                                                                       
  |
127 | 74, 105, 120, 126 | syl3anc 1292 |
. . . 4
                                                                  
  |
128 | 110, 127 | eqtrd 2505 |
. . 3
       

  
                         
  |
129 | 125, 128 | oveq12d 6326 |
. 2
                                    
          

  
                         
   |
130 | | ge0addcl 11770 |
. . . . . . 7
    
           |
131 | 51, 130 | sseldi 3416 |
. . . . . 6
    
           |
132 | 131 | adantl 473 |
. . . . 5
 
                |
133 | | inidm 3632 |
. . . . 5
   |
134 | 132, 13, 75, 20, 20, 133 | off 6565 |
. . . 4
             |
135 | | eqid 2471 |
. . . . 5
                         
                               
       |
136 | 135 | itg2addnclem 32057 |
. . . 4
                     
  
                   

          |
137 | 134, 136 | syl 17 |
. . 3
           
  
                   

          |
138 | | itg2addnc.f1 |
. . . . . . . 8
 MblFn |
139 | 138, 13, 57, 75, 111 | itg2addnclem3 32059 |
. . . . . . 7
                          
    
                                    
                       
      |
140 | | simpl 464 |
. . . . . . . . . . . . . 14
     |
141 | | simpr 468 |
. . . . . . . . . . . . . 14
     |
142 | 140, 141 | i1fadd 22732 |
. . . . . . . . . . . . 13
        |
143 | 142 | ad3antlr 745 |
. . . . . . . . . . . 12
                                  
                           
 
   |
144 | | reeanv 2944 |
. . . . . . . . . . . . . . . . 17
                                                                                   |
145 | 144 | biimpri 211 |
. . . . . . . . . . . . . . . 16
                     
                                                             |
146 | 145 | ad2ant2r 761 |
. . . . . . . . . . . . . . 15
                            
                        
                                         |
147 | | ifcl 3914 |
. . . . . . . . . . . . . . . . . . 19
          |
148 | 147 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . 18
                                                        |
149 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                   
       |
150 | 149 | anbi1d 719 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     
                   
               
                  
        |
151 | 150 | imbi1d 324 |
. . . . . . . . . . . . . . . . . . . . . 22
                                     
                               
                                
                  
                               
                   |
152 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                               
       |
153 | 152 | anbi1d 719 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 
                   
               
                  
        |
154 | 153 | imbi1d 324 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                 
                               
                                
                  
                               
                   |
155 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                   
       |
156 | 155 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     
         
                       |
157 | 156 | imbi1d 324 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                      
                                    
                               
                   |
158 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                               
       |
159 | 158 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           
          
                   
        |
160 | 159 | imbi1d 324 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                  
                                    
                               
                   |
161 | | oveq12 6317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                         |
162 | | 00id 9826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
163 | 161, 162 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                       |
164 | 163 | iftrued 3880 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                             |
165 | 164 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     

    

                                            |
166 | | simpll 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
167 | 15 | simplbi 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
      |
168 | 14, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

      |
169 | 77 | simplbi 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
      |
170 | 76, 169 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

      |
171 | 168, 170,
17, 79 | addge0d 10210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

            |
172 | 166, 171 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         

            |
173 | 172 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     

    

                      |
174 | 165, 173 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     

    

                                                      |
175 | 174 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

    

                                               
                  |
176 | 172 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     

    

          
    
            |
177 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                       |
178 | | simplrr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           |
179 | | i1ff 22713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       |
180 | 179 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
         |
181 | 178, 180 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
       |
182 | 181 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
       |
183 | 182 | addid2d 9852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         
             |
184 | 177, 183 | sylan9eqr 2527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
                      |
185 | 184 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
                                    |
186 | 185 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     

    

          
                            
      |
187 | 147 | rpred 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
          |
188 | 187 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
        |
189 | 181, 188 | readdcld 9688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         
              |
190 | 189 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
      
                  |
191 | 166, 170 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         
       |
192 | 191 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
      
           |
193 | 166, 168 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
       |
194 | 193, 191 | readdcld 9688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         
             |
195 | 194 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
      
                 |
196 | | simplrr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
         
   |
197 | 196 | rpred 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
   |
198 | | rpre 11331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35

  |
199 | | rpre 11331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35

  |
200 | | min2 11507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
        |
201 | 198, 199,
200 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       
  |
202 | 201 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
        |
203 | 188, 197,
181, 202 | leadd2dd 10249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
                    |
204 | 181, 197 | readdcld 9688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
         |
205 | | letr 9745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                                                        |
206 | 189, 204,
191, 205 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
                                                 |
207 | 203, 206 | mpand 689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         
                              |
208 | 207 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
      
                      |
209 | 170, 168 | addge02d 10223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 

    
                 |
210 | 17, 209 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 

                |
211 | 166, 210 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         
    
            |
212 | 211 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
      
        
            |
213 | 190, 192,
195, 208, 212 | letrd 9809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
      
                            |
214 | 213 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     

    

          
                            |
215 | 186, 214 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     

    

          
                                  |
216 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                                                                         |
217 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             
                                   
             
   
         
                               
             |
218 | 216, 217 | ifboth 3908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
                                     
                               
            |
219 | 176, 215,
218 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     

    

          
                               
                 |
220 | 219 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
                
                               
             |
221 | 220 | adantld 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
                                                 
                  |
222 | 221 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

    

                                                     
                  |
223 | 157, 160,
175, 222 | ifbothda 3907 |
. . . . . . . . . . . . . . . . . . . . . 22
          
                          
                               
                  |
224 | 155 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           
               
                       |
225 | 224 | imbi1d 324 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                            
                                          
                               
                   |
226 | 158 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                 
          
               |