Step | Hyp | Ref
| Expression |
1 | | eqid 2450 |
. . 3
           

          |
2 | 1 | itg2val 22679 |
. 2
                  
          |
3 | | itg2addnclem.1 |
. . . 4
 
  
                         |
4 | 3 | supeq1i 7958 |
. . 3
  
                         
         |
5 | | xrltso 11437 |
. . . . 5
 |
6 | 5 | a1i 11 |
. . . 4
          |
7 | | simprr 765 |
. . . . . . . 8
         
      |
8 | | itg1cl 22636 |
. . . . . . . . . 10
       |
9 | 8 | rexrd 9687 |
. . . . . . . . 9
       |
10 | 9 | adantr 467 |
. . . . . . . 8
                |
11 | 7, 10 | eqeltrd 2528 |
. . . . . . 7
         
  |
12 | 11 | rexlimiva 2874 |
. . . . . 6
            |
13 | 12 | abssi 3503 |
. . . . 5
            |
14 | | supxrcl 11597 |
. . . . 5
     
     
  

             |
15 | 13, 14 | mp1i 13 |
. . . 4
                         |
16 | | fveq1 5862 |
. . . . . . . . . . . . . . . 16
           |
17 | 16 | eqeq1d 2452 |
. . . . . . . . . . . . . . 15
             |
18 | 16 | oveq1d 6303 |
. . . . . . . . . . . . . . 15
               |
19 | 17, 18 | ifbieq2d 3905 |
. . . . . . . . . . . . . 14
                                 |
20 | 19 | mpteq2dv 4489 |
. . . . . . . . . . . . 13
                                     |
21 | 20 | breq1d 4411 |
. . . . . . . . . . . 12
                   
                     |
22 | 21 | rexbidv 2900 |
. . . . . . . . . . 11
  
                 
                      |
23 | | fveq2 5863 |
. . . . . . . . . . . 12
           |
24 | 23 | eqeq2d 2460 |
. . . . . . . . . . 11
     
       |
25 | 22, 24 | anbi12d 716 |
. . . . . . . . . 10
                          
 
                          |
26 | 25 | cbvrexv 3019 |
. . . . . . . . 9
                           
                     
       |
27 | | breq2 4405 |
. . . . . . . . . . . . . . . . 17
                                           |
28 | | breq2 4405 |
. . . . . . . . . . . . . . . . 17
                                    
                  |
29 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
           |
30 | | 0le0 10696 |
. . . . . . . . . . . . . . . . . . 19
 |
31 | 29, 30 | syl6eqbr 4439 |
. . . . . . . . . . . . . . . . . 18
           |
32 | 31 | adantl 468 |
. . . . . . . . . . . . . . . . 17
    
         
  |
33 | | rpge0 11311 |
. . . . . . . . . . . . . . . . . . . 20

  |
34 | 33 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . 19
       |
35 | | i1ff 22627 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
36 | 35 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . . . . . . 21
         |
37 | 36 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . 20
           |
38 | | rpre 11305 |
. . . . . . . . . . . . . . . . . . . . 21

  |
39 | 38 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . 20
       |
40 | 37, 39 | addge01d 10198 |
. . . . . . . . . . . . . . . . . . 19
                   |
41 | 34, 40 | mpbid 214 |
. . . . . . . . . . . . . . . . . 18
                 |
42 | 41 | adantr 467 |
. . . . . . . . . . . . . . . . 17
    
                  |
43 | 27, 28, 32, 42 | ifbothda 3915 |
. . . . . . . . . . . . . . . 16
                          |
44 | 43 | adantlll 723 |
. . . . . . . . . . . . . . 15
            
                      |
45 | 35 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . 18
           
      |
46 | 45 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . . 17
            
       |
47 | 46 | rexrd 9687 |
. . . . . . . . . . . . . . . 16
            
       |
48 | | 0re 9640 |
. . . . . . . . . . . . . . . . . 18
 |
49 | 38 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . 19
            
   |
50 | 46, 49 | readdcld 9667 |
. . . . . . . . . . . . . . . . . 18
            
         |
51 | | ifcl 3922 |
. . . . . . . . . . . . . . . . . 18
                          |
52 | 48, 50, 51 | sylancr 668 |
. . . . . . . . . . . . . . . . 17
            
                  |
53 | 52 | rexrd 9687 |
. . . . . . . . . . . . . . . 16
            
                  |
54 | | iccssxr 11714 |
. . . . . . . . . . . . . . . . . . 19
    |
55 | | fss 5735 |
. . . . . . . . . . . . . . . . . . 19
                   |
56 | 54, 55 | mpan2 676 |
. . . . . . . . . . . . . . . . . 18
              |
57 | 56 | ad2antrr 731 |
. . . . . . . . . . . . . . . . 17
           
      |
58 | 57 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . 16
            
       |
59 | | xrletr 11452 |
. . . . . . . . . . . . . . . 16
                                                                      
       |
60 | 47, 53, 58, 59 | syl3anc 1267 |
. . . . . . . . . . . . . . 15
            
                                             
       |
61 | 44, 60 | mpand 680 |
. . . . . . . . . . . . . 14
            
                
               |
62 | 61 | ralimdva 2795 |
. . . . . . . . . . . . 13
           
 
              
                |
63 | | reex 9627 |
. . . . . . . . . . . . . . 15
 |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . 14
           
  |
65 | | eqidd 2451 |
. . . . . . . . . . . . . 14
           
                                    |
66 | | id 22 |
. . . . . . . . . . . . . . . 16
                 |
67 | 66 | feqmptd 5916 |
. . . . . . . . . . . . . . 15
       
        |
68 | 67 | ad2antrr 731 |
. . . . . . . . . . . . . 14
           
        |
69 | 64, 52, 58, 65, 68 | ofrfval2 6546 |
. . . . . . . . . . . . 13
           
                  
                       |
70 | 35 | feqmptd 5916 |
. . . . . . . . . . . . . . 15
         |
71 | 70 | ad2antlr 732 |
. . . . . . . . . . . . . 14
           
        |
72 | 64, 46, 58, 71, 68 | ofrfval2 6546 |
. . . . . . . . . . . . 13
           
              |
73 | 62, 69, 72 | 3imtr4d 272 |
. . . . . . . . . . . 12
           
                   
   |
74 | 73 | rexlimdva 2878 |
. . . . . . . . . . 11
        
                     
   |
75 | 74 | anim1d 567 |
. . . . . . . . . 10
        
                     
      
        |
76 | 75 | reximdva 2861 |
. . . . . . . . 9
                              
                 |
77 | 26, 76 | syl5bi 221 |
. . . . . . . 8
                              
                 |
78 | 77 | ss2abdv 3501 |
. . . . . . 7
        

  
                            
        |
79 | 78 | sseld 3430 |
. . . . . 6
                               
     
    
         |
80 | | simp3r 1036 |
. . . . . . . . . . 11
        
       
      |
81 | 9 | 3ad2ant2 1029 |
. . . . . . . . . . 11
        
              |
82 | 80, 81 | eqeltrd 2528 |
. . . . . . . . . 10
        
       
  |
83 | 82 | rexlimdv3a 2880 |
. . . . . . . . 9
            
    
   |
84 | 83 | abssdv 3502 |
. . . . . . . 8
        

           |
85 | | xrsupss 11591 |
. . . . . . . 8
     
     
    
          
  
              |
86 | 84, 85 | syl 17 |
. . . . . . 7
        
 
           
   
              |
87 | 6, 86 | supub 7970 |
. . . . . 6
             
     
  

              |
88 | 79, 87 | syld 45 |
. . . . 5
                               
     
  

              |
89 | 88 | imp 431 |
. . . 4
        
                             
  

             |
90 | | supxrlub 11608 |
. . . . . . . 8
   
          
  

          
  
             |
91 | 13, 90 | mpan 675 |
. . . . . . 7

               
  
             |
92 | 91 | adantl 468 |
. . . . . 6
        
     
          
  
             |
93 | | simprrr 774 |
. . . . . . . . . . . . . . 15
             
             |
94 | 93 | breq2d 4413 |
. . . . . . . . . . . . . 14
             
       
       |
95 | | simplll 767 |
. . . . . . . . . . . . . . . . 17
              
                     |
96 | | i1f0 22638 |
. . . . . . . . . . . . . . . . . . 19
     |
97 | | 2rp 11304 |
. . . . . . . . . . . . . . . . . . . . 21
 |
98 | 97 | ne0ii 3737 |
. . . . . . . . . . . . . . . . . . . 20
 |
99 | | ffvelrn 6018 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
          |
100 | | elxrge0 11738 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
    
       |
101 | 99, 100 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
     
       |
102 | 101 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . 23
        

      |
103 | 102 | ralrimiva 2801 |
. . . . . . . . . . . . . . . . . . . . . 22
        
      |
104 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
          |
105 | | c0ex 9634 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
   |
107 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . . . . . . 23
              |
108 | 104, 106,
99, 107, 67 | ofrfval2 6546 |
. . . . . . . . . . . . . . . . . . . . . 22
           
        |
109 | 103, 108 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . 21
             |
110 | 109 | ralrimivw 2802 |
. . . . . . . . . . . . . . . . . . . 20
        
     |
111 | | r19.2z 3857 |
. . . . . . . . . . . . . . . . . . . 20
 

   
   
  |
112 | 98, 110, 111 | sylancr 668 |
. . . . . . . . . . . . . . . . . . 19
        
     |
113 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
114 | | itg10 22639 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
115 | 113, 114 | syl6req 2501 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
116 | 115 | biantrud 510 |
. . . . . . . . . . . . . . . . . . . . 21
                                                     |
117 | | fveq1 5862 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
118 | 105 | fvconst2 6118 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
119 | 117, 118 | sylan9eq 2504 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
120 | | iftrue 3886 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                      |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                        |
122 | 121 | mpteq2dva 4488 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          |
123 | 122 | breq1d 4411 |
. . . . . . . . . . . . . . . . . . . . . 22
                              |
124 | 123 | rexbidv 2900 |
. . . . . . . . . . . . . . . . . . . . 21
                                |
125 | 116, 124 | bitr3d 259 |
. . . . . . . . . . . . . . . . . . . 20
                              
   
   |
126 | 125 | rspcev 3149 |
. . . . . . . . . . . . . . . . . . 19
         
                              |
127 | 96, 112, 126 | sylancr 668 |
. . . . . . . . . . . . . . . . . 18
        
                            |
128 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
   |
129 | | mnflt 11422 |
. . . . . . . . . . . . . . . . . . . 20
   |
130 | 48, 129 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
   |
131 | 128, 130 | eqbrtrd 4422 |
. . . . . . . . . . . . . . . . . 18
   |
132 | | eqeq1 2454 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
133 | 132 | anbi2d 709 |
. . . . . . . . . . . . . . . . . . . . 21
                          
 
                          |
134 | 133 | rexbidv 2900 |
. . . . . . . . . . . . . . . . . . . 20
  
                         
                     
        |
135 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
136 | 134, 135 | anbi12d 716 |
. . . . . . . . . . . . . . . . . . 19
                        
                            
         |
137 | 105, 136 | spcev 3140 |
. . . . . . . . . . . . . . . . . 18
                                                      
        |
138 | 127, 131,
137 | syl2an 480 |
. . . . . . . . . . . . . . . . 17
        
                                  |
139 | 95, 138 | sylan 474 |
. . . . . . . . . . . . . . . 16
           
   
                                     
        |
140 | | simp-4r 776 |
. . . . . . . . . . . . . . . . . 18
           
   
            
  |
141 | 8 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
                |
142 | 141 | ad3antlr 736 |
. . . . . . . . . . . . . . . . . 18
           
   
            
      |
143 | | simpllr 768 |
. . . . . . . . . . . . . . . . . . 19
              
              |
144 | | ngtmnft 11459 |
. . . . . . . . . . . . . . . . . . . . . 22


   |
145 | 144 | biimprd 227 |
. . . . . . . . . . . . . . . . . . . . 21

    |
146 | 145 | necon1ad 2640 |
. . . . . . . . . . . . . . . . . . . 20


   |
147 | 146 | imp 431 |
. . . . . . . . . . . . . . . . . . 19
     |
148 | 143, 147 | sylan 474 |
. . . . . . . . . . . . . . . . . 18
           
   
            
  |
149 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
        
   |
150 | 9 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
                |
151 | 149, 150 | anim12i 569 |
. . . . . . . . . . . . . . . . . . . 20
             
               |
152 | | xrltle 11445 |
. . . . . . . . . . . . . . . . . . . . 21
       
           |
153 | 152 | imp 431 |
. . . . . . . . . . . . . . . . . . . 20
       
    
      |
154 | 151, 153 | sylan 474 |
. . . . . . . . . . . . . . . . . . 19
              
                  |
155 | 154 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
           
   
            
      |
156 | | xrre 11461 |
. . . . . . . . . . . . . . . . . 18
             
  |
157 | 140, 142,
148, 155, 156 | syl22anc 1268 |
. . . . . . . . . . . . . . . . 17
           
   
            
  |
158 | 127 | ad3antrrr 735 |
. . . . . . . . . . . . . . . . . . . . . 22
             
       
              
      
                            |
159 | | simplrl 769 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
       
              
     
      |
160 | | simplrl 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
       
        |
161 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
        |
162 | | cnvimass 5187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          |
163 | | fdm 5731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
164 | 35, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
165 | 162, 164 | syl5sseq 3479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
      |
166 | 165 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
          
   
  |
167 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
              
       |
168 | 163 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
169 | | ffun 5729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
170 | | difpreima 6006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

                         |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
        
           |
172 | | cnvimarndm 5188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      |
173 | 172 | difeq1i 3546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                        |
174 | 171, 173 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
               |
175 | 168, 174 | difeq12d 3551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                             |
176 | | cnvimass 5187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
        |
177 | | dfss4 3676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       
                    |
178 | 176, 177 | mpbi 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                   |
179 | 175, 178 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                         |
180 | 179 | eleq2d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                
          |
181 | | ffn 5726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
182 | | fniniseg 6001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        
         |
183 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
184 | 182, 183 | syl6bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                |
185 | 181, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                    |
186 | 180, 185 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                        |
187 | 35, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                    |
188 | 187 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                    |
189 | 188 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
           
     
      |
190 | 161, 166,
167, 189 | itg10a 22661 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
            |
191 | 160, 190 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
       
              
            |
192 | 159, 191 | breqtrd 4426 |
. . . . . . . . . . . . . . . . . . . . . 22
             
       
              
     
  |
193 | 158, 192,
137 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . 21
             
       
              
                              
        |
194 | | simprl 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
      
  |
195 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
196 | 194, 195 | anim12i 569 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
       
          |
197 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            
     
  |
198 | | fvex 5873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
199 | 198 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   
       |
200 | | ovex 6316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                
        |
201 | 200, 105 | ifex 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                            
          |
202 | 201 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   
       
                     
           |
203 | 35 | feqmptd 5916 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
204 | 203 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            
     

       |
205 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            
     
                             
                 
                     
            |
206 | 197, 199,
202, 204, 205 | offval2 6545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            
     
 
       
                     
                                             
             |
207 | | ovif2 6371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                                 
                
                          
                 |
208 | 172, 163 | syl5eq 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
            |
209 | 208 | difeq1d 3549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                              |
210 | 171, 209 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
         
               |
211 | 210 | eleq2d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
              

           |
212 | 35, 211 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
          

           |
213 | 212 | ad3antrrr 735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                   
      
   

           |
214 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                   
   |
215 | 214 | biantrurd 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                   
                     |
216 | | eldif 3413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                     |
217 | 215, 216 | syl6bbr 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                   
                     |
218 | 213, 217 | bitr4d 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                   
      
   
          |
219 | 218 | con2bid 331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                   
        
    
       |
220 | | fniniseg 6001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
        
         |
221 | 35, 181, 220 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
        
         |
222 | 221 | ad3antrrr 735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                   
        
         |
223 | 219, 222 | bitr3d 259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                   
      
             |
224 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
               |
225 | | 0m0e0 10716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
226 | 224, 225 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
             |
227 | 226 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
               |
228 | 223, 227 | syl6bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                   
      
   
         |
229 | 228 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
         
     
     
             |
230 | 229 | ifeq2da 3911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   
       
                                                 
                          
            |
231 | 207, 230 | syl5eq 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   
       
    
                     
                                                        |
232 | 231 | mpteq2dva 4488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            
     
            
                     
                                             
             |
233 | 206, 232 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            
     
 
       
                     
                                             
             |
234 | | simpll 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            
     
  |
235 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   
                 
         |
236 | | 1ex 9635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
237 | 236, 105 | ifex 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
               |
238 | 237 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   
       
         |
239 | | fconstmpt 4877 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                  
                                    |
240 | 239 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            
     
                                                        |
241 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            
     
                       
          |
242 | 197, 235,
238, 240, 241 | offval2 6545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            
     
                   
                 
                           
                         |
243 | | ovif2 6371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                 
        
    
                                                                
          |
244 | | resubcl 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     
         |
245 | 8, 244 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           |
246 | 245 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
            
     
        |
247 | | 2re 10676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 |
248 | | i1fima 22629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     
      |
249 | | mblvol 22477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     
   
       
             
       |
250 | 248, 249 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                      
       |
251 | | neldifsn 4098 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     |
252 | | i1fima2 22630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
              
       |
253 | 251, 252 | mpan2 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                |
254 | 250, 253 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
         
       |
255 | | remulcl 9621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
          
                        |
256 | 247, 254,
255 | sylancr 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                   |
257 | 256 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
            
     
         
        |
258 | | 2cnd 10679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
            
     
  |
259 | 254 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
            
     
                |
260 | 259 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
            
     
                |
261 | | 2ne0 10699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 |
262 | 261 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
            
     
  |
263 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
            
     
                |
264 | 258, 260,
262, 263 | mulne0d 10261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
            
     
         
        |
265 | 246, 257,
264 | redivcld 10432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
            
     
                          |
266 | 265 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
            
     
                          |
267 | 266 | mulid1d 9657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
            
     
                 
                        
         |
268 | 266 | mul01d 9829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
            
     
                 
          |
269 | 267, 268 | ifeq12d 3900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            
     
                                                        
               
                     
           |
270 | 243, 269 | syl5eq 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            
     
                 
        
    
                                    
           |
271 | 270 | mpteq2dv 4489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            
     
                  
        
    
                
                     
            |
272 | 242, 271 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            
     
                   
                 
                
                     
            |
273 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                 |
274 | 273 | i1f1 22641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      
           
             
          |
275 | 248, 253,
274 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        
          |
276 | 275 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            
     
                  |
277 | 276, 265 | i1fmulc 22654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            
     
                   
                 
           |
278 | 272, 277 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            
     
                             
            |
279 | | i1fsub 22659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
                     
                                          
             |
280 | 234, 278,
279 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            
     
 
       
                     
             |
281 | 233, 280 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
     
                                                |
282 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
          
    
       |
283 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           |
284 | 283 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                      
                             
          |
285 | 282, 284 | ifbieq1d 3903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  
    
                          
                
                          
            |
286 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                  
                  
                          
            |
287 | | ovex 6316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                               |
288 | 287, 105 | ifex 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                 
           |
289 | 285, 286,
288 | fvmpt 5946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
                          
                    
                          
            |
290 | 289 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
        
                          
             
      
                          
             |
291 | 290, 289 | ifbieq1d 3903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
                          
                       
                          
                 
                                 
                 
                          
              |
292 | | iftrue 3886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
                            |