Proof of Theorem hoidmv1lelem2
Step | Hyp | Ref
| Expression |
1 | | hoidmv1lelem2.a |
. . . . . 6
   |
2 | | hoidmv1lelem2.b |
. . . . . 6
   |
3 | | hoidmv1lelem2.m |
. . . . . . . 8
      
       |
4 | 3 | a1i 11 |
. . . . . . 7
      
         |
5 | | hoidmv1lelem2.d |
. . . . . . . . 9
       |
6 | | hoidmv1lelem2.k |
. . . . . . . . 9
   |
7 | 5, 6 | ffvelrnd 6023 |
. . . . . . . 8
       |
8 | 7, 2 | ifcld 3924 |
. . . . . . 7
       
        |
9 | 4, 8 | eqeltrd 2529 |
. . . . . 6
   |
10 | | hoidmv1lelem2.c |
. . . . . . . . . . 11
       |
11 | 10, 6 | ffvelrnd 6023 |
. . . . . . . . . 10
       |
12 | 7 | rexrd 9690 |
. . . . . . . . . 10
       |
13 | | icossre 11715 |
. . . . . . . . . 10
                         |
14 | 11, 12, 13 | syl2anc 667 |
. . . . . . . . 9
            
  |
15 | | hoidmv1lelem2.s |
. . . . . . . . 9
               |
16 | 14, 15 | sseldd 3433 |
. . . . . . . 8
   |
17 | | hoidmv1lelem2.g |
. . . . . . . 8

  |
18 | 11 | rexrd 9690 |
. . . . . . . . . . . 12
       |
19 | | icoltub 37607 |
. . . . . . . . . . . 12
                             |
20 | 18, 12, 15, 19 | syl3anc 1268 |
. . . . . . . . . . 11
       |
21 | 16, 7, 20 | ltled 9783 |
. . . . . . . . . 10

      |
22 | | hoidmv1lelem2.l |
. . . . . . . . . . 11
   |
23 | 16, 2, 22 | ltled 9783 |
. . . . . . . . . 10

  |
24 | 21, 23 | jca 535 |
. . . . . . . . 9
     
   |
25 | | lemin 11486 |
. . . . . . . . . 10
                    
    
    |
26 | 16, 7, 2, 25 | syl3anc 1268 |
. . . . . . . . 9
                   
    |
27 | 24, 26 | mpbird 236 |
. . . . . . . 8

     
         |
28 | 1, 16, 8, 17, 27 | letrd 9792 |
. . . . . . 7

     
         |
29 | 4 | eqcomd 2457 |
. . . . . . 7
       
        |
30 | 28, 29 | breqtrd 4427 |
. . . . . 6

  |
31 | | min2 11484 |
. . . . . . . 8
     
       
     
  |
32 | 7, 2, 31 | syl2anc 667 |
. . . . . . 7
       
     
  |
33 | 4, 32 | eqbrtrd 4423 |
. . . . . 6

  |
34 | 1, 2, 9, 30, 33 | eliccd 37601 |
. . . . 5
   ![[,] [,]](_icc.gif)    |
35 | 9 | recnd 9669 |
. . . . . . . 8
   |
36 | 16 | recnd 9669 |
. . . . . . . 8
   |
37 | 1 | recnd 9669 |
. . . . . . . 8
   |
38 | 35, 36, 37 | npncand 10010 |
. . . . . . 7
           |
39 | 38 | eqcomd 2457 |
. . . . . 6
           |
40 | 9, 16 | resubcld 10047 |
. . . . . . . 8
     |
41 | 16, 1 | resubcld 10047 |
. . . . . . . 8
     |
42 | 40, 41 | readdcld 9670 |
. . . . . . 7
         |
43 | | nnex 10615 |
. . . . . . . . . . . . 13
 |
44 | 43 | a1i 11 |
. . . . . . . . . . . 12
   |
45 | | volf 22483 |
. . . . . . . . . . . . . . 15
        |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
 

         |
47 | 10 | ffvelrnda 6022 |
. . . . . . . . . . . . . . 15
 

      |
48 | 5 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . 17
 

      |
49 | 16 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 

  |
50 | 48, 49 | ifcld 3924 |
. . . . . . . . . . . . . . . 16
 

     
         |
51 | 50 | rexrd 9690 |
. . . . . . . . . . . . . . 15
 

     
         |
52 | | icombl 22517 |
. . . . . . . . . . . . . . 15
                                           |
53 | 47, 51, 52 | syl2anc 667 |
. . . . . . . . . . . . . 14
 

                       |
54 | 46, 53 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
 

                              |
55 | | eqid 2451 |
. . . . . . . . . . . . 13
                                           
           |
56 | 54, 55 | fmptd 6046 |
. . . . . . . . . . . 12
                                     |
57 | 44, 56 | sge0xrcl 38227 |
. . . . . . . . . . 11
 Σ^                               |
58 | | pnfxr 11412 |
. . . . . . . . . . . 12
 |
59 | 58 | a1i 11 |
. . . . . . . . . . 11
   |
60 | | hoidmv1lelem2.r |
. . . . . . . . . . . . 13
 Σ^                      |
61 | 60 | rexrd 9690 |
. . . . . . . . . . . 12
 Σ^                      |
62 | | nfv 1761 |
. . . . . . . . . . . . 13
   |
63 | 48 | rexrd 9690 |
. . . . . . . . . . . . . . 15
 

      |
64 | | icombl 22517 |
. . . . . . . . . . . . . . 15
                         |
65 | 47, 63, 64 | syl2anc 667 |
. . . . . . . . . . . . . 14
 

              |
66 | 46, 65 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
 

                     |
67 | 47 | rexrd 9690 |
. . . . . . . . . . . . . . 15
 

      |
68 | 47 | leidd 10180 |
. . . . . . . . . . . . . . 15
 

          |
69 | | min1 11483 |
. . . . . . . . . . . . . . . 16
     
       
     
      |
70 | 48, 49, 69 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 

     
             |
71 | | icossico 11704 |
. . . . . . . . . . . . . . 15
                           
     
                   
                     |
72 | 67, 63, 68, 70, 71 | syl22anc 1269 |
. . . . . . . . . . . . . 14
 

                                   |
73 | | volss 22487 |
. . . . . . . . . . . . . 14
                                                
                   
                                           |
74 | 53, 65, 72, 73 | syl3anc 1268 |
. . . . . . . . . . . . 13
 

                                           |
75 | 62, 44, 54, 66, 74 | sge0lempt 38252 |
. . . . . . . . . . . 12
 Σ^                             Σ^                      |
76 | 60 | ltpnfd 11423 |
. . . . . . . . . . . 12
 Σ^                      |
77 | 57, 61, 59, 75, 76 | xrlelttrd 11457 |
. . . . . . . . . . 11
 Σ^                               |
78 | 57, 59, 77 | xrltned 37580 |
. . . . . . . . . 10
 Σ^                               |
79 | 78 | neneqd 2629 |
. . . . . . . . 9
 Σ^                               |
80 | 44, 56 | sge0repnf 38228 |
. . . . . . . . 9
  Σ^                            
Σ^                                |
81 | 79, 80 | mpbird 236 |
. . . . . . . 8
 Σ^                               |
82 | 40, 81 | readdcld 9670 |
. . . . . . 7
    Σ^                                |
83 | 9 | adantr 467 |
. . . . . . . . . . . . . . . 16
 

  |
84 | 48, 83 | ifcld 3924 |
. . . . . . . . . . . . . . 15
 

     
         |
85 | 84 | rexrd 9690 |
. . . . . . . . . . . . . 14
 

     
         |
86 | | icombl 22517 |
. . . . . . . . . . . . . 14
                                           |
87 | 47, 85, 86 | syl2anc 667 |
. . . . . . . . . . . . 13
 

                       |
88 | 46, 87 | ffvelrnd 6023 |
. . . . . . . . . . . 12
 

                              |
89 | | eqid 2451 |
. . . . . . . . . . . 12
                                           
           |
90 | 88, 89 | fmptd 6046 |
. . . . . . . . . . 11
                                     |
91 | 44, 90 | sge0xrcl 38227 |
. . . . . . . . . 10
 Σ^                               |
92 | | min1 11483 |
. . . . . . . . . . . . . . 15
     
       
     
      |
93 | 48, 83, 92 | syl2anc 667 |
. . . . . . . . . . . . . 14
 

     
             |
94 | | icossico 11704 |
. . . . . . . . . . . . . 14
                           
     
                   
                     |
95 | 67, 63, 68, 93, 94 | syl22anc 1269 |
. . . . . . . . . . . . 13
 

                                   |
96 | | volss 22487 |
. . . . . . . . . . . . 13
                                                
                   
                                           |
97 | 87, 65, 95, 96 | syl3anc 1268 |
. . . . . . . . . . . 12
 

                                           |
98 | 62, 44, 88, 66, 97 | sge0lempt 38252 |
. . . . . . . . . . 11
 Σ^                             Σ^                      |
99 | 91, 61, 59, 98, 76 | xrlelttrd 11457 |
. . . . . . . . . 10
 Σ^                               |
100 | 91, 59, 99 | xrltned 37580 |
. . . . . . . . 9
 Σ^                               |
101 | 100 | neneqd 2629 |
. . . . . . . 8
 Σ^                               |
102 | 44, 90 | sge0repnf 38228 |
. . . . . . . 8
  Σ^                            
Σ^                                |
103 | 101, 102 | mpbird 236 |
. . . . . . 7
 Σ^                               |
104 | | hoidmv1lelem2.e |
. . . . . . . . . . 11
   |
105 | | hoidmv1lelem2.u |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    Σ^                               |
106 | 104, 105 | syl6eleq 2539 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    Σ^                                |
107 | | oveq1 6297 |
. . . . . . . . . . . 12
       |
108 | | simpl 459 |
. . . . . . . . . . . . . . . . . 18
 
   |
109 | 108 | breq2d 4414 |
. . . . . . . . . . . . . . . . 17
 
             |
110 | 109, 108 | ifbieq2d 3906 |
. . . . . . . . . . . . . . . 16
 
                             |
111 | 110 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
 
                                  
          |
112 | 111 | fveq2d 5869 |
. . . . . . . . . . . . . 14
 
                
                                    |
113 | 112 | mpteq2dva 4489 |
. . . . . . . . . . . . 13
                                                         |
114 | 113 | fveq2d 5869 |
. . . . . . . . . . . 12
 Σ^                             Σ^                               |
115 | 107, 114 | breq12d 4415 |
. . . . . . . . . . 11
   
Σ^                            
  Σ^                                |
116 | 115 | elrab 3196 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    Σ^                                 ![[,] [,]](_icc.gif)    Σ^                                |
117 | 106, 116 | sylib 200 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)    Σ^                                |
118 | 117 | simprd 465 |
. . . . . . . 8
  
Σ^                               |
119 | 41, 81, 40, 118 | leadd2dd 10228 |
. . . . . . 7
      
 
 Σ^                                |
120 | | difssd 3561 |
. . . . . . . . . 10
       |
121 | 62, 44, 54, 81, 120 | sge0ssrempt 38247 |
. . . . . . . . 9
 Σ^                                   |
122 | | difexg 4551 |
. . . . . . . . . . . . . . 15
       |
123 | 43, 122 | ax-mp 5 |
. . . . . . . . . . . . . 14
     |
124 | 123 | a1i 11 |
. . . . . . . . . . . . 13
       |
125 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
 

             |
126 | | simpl 459 |
. . . . . . . . . . . . . . . 16
 

      |
127 | | eldifi 3555 |
. . . . . . . . . . . . . . . . 17
       |
128 | 127 | adantl 468 |
. . . . . . . . . . . . . . . 16
 

      |
129 | 126, 128,
47 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 

          |
130 | 128, 85 | syldan 473 |
. . . . . . . . . . . . . . 15
 

                   |
131 | 129, 130,
86 | syl2anc 667 |
. . . . . . . . . . . . . 14
 

                           |
132 | 125, 131 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
 

                   
              |
133 | 62, 124, 132 | sge0xrclmpt 38270 |
. . . . . . . . . . . 12
 Σ^                                   |
134 | 44, 88, 120 | sge0lessmpt 38241 |
. . . . . . . . . . . . 13
 Σ^                                
Σ^                               |
135 | 133, 91, 59, 134, 99 | xrlelttrd 11457 |
. . . . . . . . . . . 12
 Σ^                                   |
136 | 133, 59, 135 | xrltned 37580 |
. . . . . . . . . . 11
 Σ^                                   |
137 | 136 | neneqd 2629 |
. . . . . . . . . 10
 Σ^                                   |
138 | 62, 124, 132 | sge0repnfmpt 38281 |
. . . . . . . . . 10
  Σ^                                
Σ^                     
              |
139 | 137, 138 | mpbird 236 |
. . . . . . . . 9
 Σ^                                   |
140 | 9, 11 | resubcld 10047 |
. . . . . . . . 9
         |
141 | 128, 54 | syldan 473 |
. . . . . . . . . 10
 

                   
              |
142 | 128, 53 | syldan 473 |
. . . . . . . . . . 11
 

                           |
143 | 128, 67 | syldan 473 |
. . . . . . . . . . . 12
 

          |
144 | 128, 68 | syldan 473 |
. . . . . . . . . . . 12
 

       
      |
145 | | iftrue 3887 |
. . . . . . . . . . . . . . . 16
                        |
146 | 145 | adantl 468 |
. . . . . . . . . . . . . . 15
                            |
147 | 48 | leidd 10180 |
. . . . . . . . . . . . . . . . . 18
 

          |
148 | 147 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                   |
149 | 48 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
               |
150 | 83 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
           |
151 | 49 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
           |
152 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
               |
153 | 20, 22 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . 22
     
   |
154 | | ltmin 11488 |
. . . . . . . . . . . . . . . . . . . . . . 23
                    
    
    |
155 | 16, 7, 2, 154 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
    |
156 | 153, 155 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . 21
      
         |
157 | 156, 29 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . . 20
   |
158 | 157 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
           |
159 | 149, 151,
150, 152, 158 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . 18
               |
160 | 149, 150,
159 | ltled 9783 |
. . . . . . . . . . . . . . . . 17
               |
161 | 148, 160 | jca 535 |
. . . . . . . . . . . . . . . 16
             
           |
162 | | lemin 11486 |
. . . . . . . . . . . . . . . . 17
               
     
                   
    |
163 | 149, 149,
150, 162 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
             
     
                   
    |
164 | 161, 163 | mpbird 236 |
. . . . . . . . . . . . . . 15
                   
        |
165 | 146, 164 | eqbrtrd 4423 |
. . . . . . . . . . . . . 14
                     
     
         |
166 | | iffalse 3890 |
. . . . . . . . . . . . . . . 16
    
               |
167 | 166 | adantl 468 |
. . . . . . . . . . . . . . 15
                        |
168 | 49 | adantr 467 |
. . . . . . . . . . . . . . . 16
        
  |
169 | 84 | adantr 467 |
. . . . . . . . . . . . . . . 16
                        |
170 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
            
  |
171 | 48 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
               |
172 | 168, 171 | ltnled 9782 |
. . . . . . . . . . . . . . . . . . 19
                 
   |
173 | 170, 172 | mpbird 236 |
. . . . . . . . . . . . . . . . . 18
               |
174 | 157 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
           |
175 | 173, 174 | jca 535 |
. . . . . . . . . . . . . . . . 17
             
   |
176 | 83 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
        
  |
177 | | ltmin 11488 |
. . . . . . . . . . . . . . . . . 18
                    
    
    |
178 | 168, 171,
176, 177 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
                           
    |
179 | 175, 178 | mpbird 236 |
. . . . . . . . . . . . . . . 16
                        |
180 | 168, 169,
179 | ltled 9783 |
. . . . . . . . . . . . . . 15
                        |
181 | 167, 180 | eqbrtrd 4423 |
. . . . . . . . . . . . . 14
                     
     
         |
182 | 165, 181 | pm2.61dan 800 |
. . . . . . . . . . . . 13
 

     
                      |
183 | 128, 182 | syldan 473 |
. . . . . . . . . . . 12
 

                
     
         |
184 | | icossico 11704 |
. . . . . . . . . . . 12
             
                      
     
     
                     
       
             
         |
185 | 143, 130,
144, 183, 184 | syl22anc 1269 |
. . . . . . . . . . 11
 

                                     
          |
186 | | volss 22487 |
. . . . . . . . . . 11
                                    
                    
                   
                         
                       
           |
187 | 142, 131,
185, 186 | syl3anc 1268 |
. . . . . . . . . 10
 

                   
                         
          |
188 | 62, 124, 141, 132, 187 | sge0lempt 38252 |
. . . . . . . . 9
 Σ^                                
Σ^                                   |
189 | 121, 139,
140, 188 | leadd2dd 10228 |
. . . . . . . 8
        Σ^                                         Σ^                                    |
190 | | difsnid 4118 |
. . . . . . . . . . . . . . . 16
           |
191 | 6, 190 | syl 17 |
. . . . . . . . . . . . . . 15
           |
192 | 191 | eqcomd 2457 |
. . . . . . . . . . . . . 14
           |
193 | 192 | mpteq1d 4484 |
. . . . . . . . . . . . 13
                                                                 |
194 | 193 | fveq2d 5869 |
. . . . . . . . . . . 12
 Σ^                             Σ^                                       |
195 | | neldifsnd 4100 |
. . . . . . . . . . . . 13
       |
196 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
197 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
198 | 197 | breq1d 4412 |
. . . . . . . . . . . . . . . 16
     
       |
199 | 198, 197 | ifbieq1d 3904 |
. . . . . . . . . . . . . . 15
                   
         |
200 | 196, 199 | oveq12d 6308 |
. . . . . . . . . . . . . 14
             
                               |
201 | 200 | fveq2d 5869 |
. . . . . . . . . . . . 13
                 
                       
           |
202 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
          |
203 | 7, 16 | ifcld 3924 |
. . . . . . . . . . . . . . . 16
       
        |
204 | 203 | rexrd 9690 |
. . . . . . . . . . . . . . 15
       
        |
205 | | icombl 22517 |
. . . . . . . . . . . . . . 15
                                           |
206 | 11, 204, 205 | syl2anc 667 |
. . . . . . . . . . . . . 14
                        |
207 | 202, 206 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
                
              |
208 | 62, 124, 6, 195, 141, 201, 207 | sge0splitsn 38283 |
. . . . . . . . . . . 12
 Σ^                                      Σ^                     
                                          |
209 | | volicore 38403 |
. . . . . . . . . . . . . . 15
                                   
           |
210 | 11, 203, 209 | syl2anc 667 |
. . . . . . . . . . . . . 14
                
           |
211 | | rexadd 11525 |
. . . . . . . . . . . . . 14
  Σ^                                                            Σ^                                                               Σ^                                                             |
212 | 121, 210,
211 | syl2anc 667 |
. . . . . . . . . . . . 13
  Σ^                                                               Σ^                                                             |
213 | | volico 38363 |
. . . . . . . . . . . . . . . 16
                                   
                                                    |
214 | 11, 203, 213 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                
                                                    |
215 | 16, 7 | ltnled 9782 |
. . . . . . . . . . . . . . . . . . 19
         
   |
216 | 20, 215 | mpbid 214 |
. . . . . . . . . . . . . . . . . 18
       |
217 | 216 | iffalsed 3892 |
. . . . . . . . . . . . . . . . 17
       
        |
218 | 217 | breq2d 4414 |
. . . . . . . . . . . . . . . 16
                          |
219 | 218 | ifbid 3903 |
. . . . . . . . . . . . . . 15
             
                                                          |
220 | 217 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
                            |
221 | 220 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
                           |
222 | 217, 204 | eqeltrrd 2530 |
. . . . . . . . . . . . . . . . . . . 20
   |
223 | 222 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
       |
224 | 18 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
           |
225 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
226 | 16 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
227 | 11 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
228 | 226, 227 | lenltd 9781 |
. . . . . . . . . . . . . . . . . . . 20
 
         
       |
229 | 225, 228 | mpbird 236 |
. . . . . . . . . . . . . . . . . . 19
 
           |
230 | | icogelb 11686 |
. . . . . . . . . . . . . . . . . . . . 21
                             |
231 | 18, 12, 15, 230 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . 20
    
  |
232 | 231 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
           |
233 | 223, 224,
229, 232 | xrletrid 11452 |
. . . . . . . . . . . . . . . . . 18
 
           |
234 | 233 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
 
     
                 |
235 | 227 | recnd 9669 |
. . . . . . . . . . . . . . . . . 18
 
           |
236 | 235 | subidd 9974 |
. . . . . . . . . . . . . . . . 17
 
                 |
237 | 234, 236 | eqtr2d 2486 |
. . . . . . . . . . . . . . . 16
 
             |
238 | 221, 237 | ifeqda 3914 |
. . . . . . . . . . . . . . 15
                                     |
239 | 214, 219,
238 | 3eqtrd 2489 |
. . . . . . . . . . . . . 14
                
                 |
240 | 239 | oveq2d 6306 |
. . . . . . . . . . . . 13
  Σ^                                                            Σ^                                          |
241 | 121 | recnd 9669 |
. . . . . . . . . . . . . 14
 Σ^                                   |
242 | 11 | recnd 9669 |
. . . . . . . . . . . . . . 15
       |
243 | 36, 242 | subcld 9986 |
. . . . . . . . . . . . . 14
         |
244 | 241, 243 | addcomd 9835 |
. . . . . . . . . . . . 13
  Σ^                                               Σ^                                    |
245 | 212, 240,
244 | 3eqtrd 2489 |
. . . . . . . . . . . 12
  Σ^                                                                     Σ^                                    |
246 | 194, 208,
245 | 3eqtrd 2489 |
. . . . . . . . . . 11
 Σ^                                    Σ^                                    |
247 | 246 | oveq2d 6306 |
. . . . . . . . . 10
    Σ^                                        Σ^                                     |
248 | 40 | recnd 9669 |
. . . . . . . . . . . 12
     |
249 | 248, 243,
241 | addassd 9665 |
. . . . . . . . . . 11
            Σ^                     
                      Σ^                                     |
250 | 249 | eqcomd 2457 |
. . . . . . . . . 10
           Σ^                                              Σ^                     
              |
251 | 35, 36, 242 | npncand 10010 |
. . . . . . . . . . 11
                   |
252 | 251 | oveq1d 6305 |
. . . . . . . . . 10
            Σ^                     
                   Σ^                                    |
253 | 247, 250,
252 | 3eqtrd 2489 |
. . . . . . . . 9
    Σ^                                     Σ^                                    |
254 | 192 | mpteq1d 4484 |
. . . . . . . . . . 11
                                                                 |
255 | 254 | fveq2d 5869 |
. . . . . . . . . 10
 Σ^                             Σ^                                       |
256 | 197 | breq1d 4412 |
. . . . . . . . . . . . . 14
     
       |
257 | 256, 197 | ifbieq1d 3904 |
. . . . . . . . . . . . 13
                   
         |
258 | 196, 257 | oveq12d 6308 |
. . . . . . . . . . . 12
             
                               |
259 | 258 | fveq2d 5869 |
. . . . . . . . . . 11
                 
                       
           |
260 | 7, 9 | ifcld 3924 |
. . . . . . . . . . . . . 14
       
        |
261 | 260 | rexrd 9690 |
. . . . . . . . . . . . 13
       
        |
262 | | icombl 22517 |
. . . . . . . . . . . . 13
                                           |
263 | 11, 261, 262 | syl2anc 667 |
. . . . . . . . . . . 12
                        |
264 | 202, 263 | ffvelrnd 6023 |
. . . . . . . . . . 11
                
              |
265 | 62, 124, 6, 195, 132, 259, 264 | sge0splitsn 38283 |
. . . . . . . . . 10
 Σ^                                      Σ^                     
                                          |
266 | | volicore 38403 |
. . . . . . . . . . . . 13
                                   
           |
267 | 11, 260, 266 | syl2anc 667 |
. . . . . . . . . . . 12
                
           |
268 | | rexadd 11525 |
. . . . . . . . . . . 12
  Σ^                                                            Σ^                                                               Σ^                                                             |
269 | 139, 267,
268 | syl2anc 667 |
. . . . . . . . . . 11
  Σ^                                                               Σ^                                                             |
270 | | volico 38363 |
. . . . . . . . . . . . . 14
                                   
                                                    |
271 | 11, 260, 270 | syl2anc 667 |
. . . . . . . . . . . . 13
                
                                                    |
272 | 20, 157 | jca 535 |
. . . . . . . . . . . . . . . 16
     
   |
273 | | ltmin 11488 |
. . . . . . . . . . . . . . . . 17
                    
    
    |
274 | 16, 7, 9, 273 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
                   
    |
275 | 272, 274 | mpbird 236 |
. . . . . . . . . . . . . . 15
      
         |
276 | 11, 16, 260, 231, 275 | lelttrd 9793 |
. . . . . . . . . . . . . 14
    
     
         |
277 | 276 | iftrued 3889 |
. . . . . . . . . . . . 13
             
                                                 |
278 | | iftrue 3887 |
. . . . . . . . . . . . . . . . 17
                        |
279 | 278 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
    
     
             |
280 | 12 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
      |
281 | 9 | rexrd 9690 |
. . . . . . . . . . . . . . . . . 18
   |
282 | 281 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
  |
283 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
    
      |
284 | | min1 11483 |
. . . . . . . . . . . . . . . . . . . 20
     
       
     
      |
285 | 7, 2, 284 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
       
     
      |
286 | 4, 285 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . . 18

      |
287 | 286 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
      |
288 | 280, 282,
283, 287 | xrletrid 11452 |
. . . . . . . . . . . . . . . 16
 
    
      |
289 | 279, 288 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
 
    
     
         |
290 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
           |
291 | 290 | iffalsed 3892 |
. . . . . . . . . . . . . . 15
 
                    |
292 | 289, 291 | pm2.61dan 800 |
. . . . . . . . . . . . . 14
       
        |
293 | 292 | oveq1d 6305 |
. . . . . . . . . . . . 13
                            |
294 | 271, 277,
293 | 3eqtrd 2489 |
. . . . . . . . . . . 12
                
                 |
295 | 294 | oveq2d 6306 |
. . . . . . . . . . 11
  Σ^                                                            Σ^                                          |
296 | 139 | recnd 9669 |
. . . . . . . . . . . 12
 Σ^                                   |
297 | 35, 242 | subcld 9986 |
. . . . . . . . . . . 12
         |
298 | 296, 297 | addcomd 9835 |
. . . . . . . . . . 11
  Σ^                                               Σ^                                    |
299 | 269, 295,
298 | 3eqtrd 2489 |
. . . . . . . . . 10
  Σ^                                                                     Σ^                                    |
300 | 255, 265,
299 | 3eqtrd 2489 |
. . . . . . . . 9
 Σ^                                    Σ^                                    |
301 | 253, 300 | breq12d 4415 |
. . . . . . . 8
     Σ^                              Σ^                            
 
     Σ^                                         Σ^                                     |
302 | 189, 301 | mpbird 236 |
. . . . . . 7
    Σ^                              Σ^                               |
303 | 42, 82, 103, 119, 302 | letrd 9792 |
. . . . . 6
      
Σ^                               |
304 | 39, 303 | eqbrtrd 4423 |
. . . . 5
  
Σ^                               |
305 | 34, 304 | jca 535 |
. . . 4
    ![[,] [,]](_icc.gif)    Σ^                                |
306 | | oveq1 6297 |
. . . . . 6
       |
307 | | breq2 4406 |
. . . . . . . . . . 11
     
       |
308 | | id 22 |
. . . . . . . . . . 11
   |
309 | 307, 308 | ifbieq2d 3906 |
. . . . . . . . . 10
                   
         |
310 | 309 | oveq2d 6306 |
. . . . . . . . 9
             
                               |
311 | 310 | fveq2d 5869 |
. . . . . . . 8
                                         
           |
312 | 311 | mpteq2dv 4490 |
. . . . . . 7
                                                         |
313 | 312 | fveq2d 5869 |
. . . . . 6
 Σ^                             Σ^                               |
314 | 306, 313 | breq12d 4415 |
. . . . 5
   
Σ^                            
  Σ^                                |
315 | 314 | elrab 3196 |
. . . 4
    ![[,] [,]](_icc.gif)    Σ^                                 ![[,] [,]](_icc.gif)    Σ^                                |
316 | 305, 315 | sylibr 216 |
. . 3
    ![[,] [,]](_icc.gif)    Σ^                                |
317 | 316, 105 | syl6eleqr 2540 |
. 2
   |
318 | 272 | simprd 465 |
. 2
   |
319 | | breq2 4406 |
. . 3
 
   |
320 | 319 | rspcev 3150 |
. 2
   
  |
321 | 317, 318,
320 | syl2anc 667 |
1
    |