Step | Hyp | Ref
| Expression |
1 | | sge0f1o.4 |
. . . . . 6
   |
2 | | sge0f1o.5 |
. . . . . . 7
       |
3 | | f1ofo 5821 |
. . . . . . 7
    
      |
4 | 2, 3 | syl 17 |
. . . . . 6
       |
5 | | fornex 6762 |
. . . . . 6
     
   |
6 | 1, 4, 5 | sylc 62 |
. . . . 5
   |
7 | 6 | adantr 467 |
. . . 4
 

 
  |
8 | | sge0f1o.1 |
. . . . . 6
   |
9 | | sge0f1o.7 |
. . . . . 6
 
      |
10 | | eqid 2451 |
. . . . . 6
     |
11 | 8, 9, 10 | fmptdf 6048 |
. . . . 5
            |
12 | 11 | adantr 467 |
. . . 4
 

             |
13 | | pnfex 11413 |
. . . . . . . 8
 |
14 | | eqid 2451 |
. . . . . . . . 9
     |
15 | 14 | elrnmpt 5081 |
. . . . . . . 8
 

   |
16 | 13, 15 | ax-mp 5 |
. . . . . . 7
 

  |
17 | 16 | biimpi 198 |
. . . . . 6
  
  |
18 | 17 | adantl 468 |
. . . . 5
 

  
  |
19 | | sge0f1o.2 |
. . . . . . 7
   |
20 | | nfv 1761 |
. . . . . . 7
    |
21 | | simp3 1010 |
. . . . . . . . . 10
 

  |
22 | | f1of 5814 |
. . . . . . . . . . . . . . 15
    
      |
23 | 2, 22 | syl 17 |
. . . . . . . . . . . . . 14
       |
24 | 23 | ffvelrnda 6022 |
. . . . . . . . . . . . 13
 
       |
25 | | sge0f1o.6 |
. . . . . . . . . . . . 13
 
       |
26 | | nfcv 2592 |
. . . . . . . . . . . . . 14
       |
27 | | nfv 1761 |
. . . . . . . . . . . . . . 15
       |
28 | 26 | nfcsb1 3378 |
. . . . . . . . . . . . . . . 16
        ![]_ ]_](_urbrack.gif)  |
29 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
   |
30 | 28, 29 | nfeq 2603 |
. . . . . . . . . . . . . . 15
        ![]_ ]_](_urbrack.gif)
 |
31 | 27, 30 | nfim 2003 |
. . . . . . . . . . . . . 14
             ![]_ ]_](_urbrack.gif)
  |
32 | | eqeq1 2455 |
. . . . . . . . . . . . . . 15
     
       |
33 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . 16
           ![]_ ]_](_urbrack.gif)   |
34 | 33 | eqeq1d 2453 |
. . . . . . . . . . . . . . 15
     
      ![]_ ]_](_urbrack.gif)    |
35 | 32, 34 | imbi12d 322 |
. . . . . . . . . . . . . 14
            
      ![]_ ]_](_urbrack.gif)     |
36 | | sge0f1o.3 |
. . . . . . . . . . . . . 14
   |
37 | 26, 31, 35, 36 | vtoclgf 3105 |
. . . . . . . . . . . . 13
                ![]_ ]_](_urbrack.gif)
   |
38 | 24, 25, 37 | sylc 62 |
. . . . . . . . . . . 12
 
       ![]_ ]_](_urbrack.gif)   |
39 | 38 | eqcomd 2457 |
. . . . . . . . . . 11
 
       ![]_ ]_](_urbrack.gif)   |
40 | 39 | 3adant3 1028 |
. . . . . . . . . 10
 

      ![]_ ]_](_urbrack.gif)   |
41 | 21, 40 | eqtrd 2485 |
. . . . . . . . 9
 

      ![]_ ]_](_urbrack.gif)   |
42 | | simpl 459 |
. . . . . . . . . . . . 13
 
   |
43 | 42, 24 | jca 535 |
. . . . . . . . . . . 12
 
         |
44 | | nfv 1761 |
. . . . . . . . . . . . . . 15
       |
45 | 8, 44 | nfan 2011 |
. . . . . . . . . . . . . 14
         |
46 | 28 | nfel1 2606 |
. . . . . . . . . . . . . 14
        ![]_ ]_](_urbrack.gif)
 
  |
47 | 45, 46 | nfim 2003 |
. . . . . . . . . . . . 13
               ![]_ ]_](_urbrack.gif)
     |
48 | | eleq1 2517 |
. . . . . . . . . . . . . . 15
     
       |
49 | 48 | anbi2d 710 |
. . . . . . . . . . . . . 14
      

         |
50 | 33 | eleq1d 2513 |
. . . . . . . . . . . . . 14
     
  
      ![]_ ]_](_urbrack.gif)       |
51 | 49, 50 | imbi12d 322 |
. . . . . . . . . . . . 13
       
                  ![]_ ]_](_urbrack.gif)
       |
52 | 26, 47, 51, 9 | vtoclgf 3105 |
. . . . . . . . . . . 12
      
           ![]_ ]_](_urbrack.gif)       |
53 | 24, 43, 52 | sylc 62 |
. . . . . . . . . . 11
 
       ![]_ ]_](_urbrack.gif)      |
54 | 28, 10, 33 | elrnmpt1sf 37464 |
. . . . . . . . . . 11
            ![]_ ]_](_urbrack.gif)
          ![]_ ]_](_urbrack.gif)
    |
55 | 24, 53, 54 | syl2anc 667 |
. . . . . . . . . 10
 
       ![]_ ]_](_urbrack.gif)     |
56 | 55 | 3adant3 1028 |
. . . . . . . . 9
 

      ![]_ ]_](_urbrack.gif)     |
57 | 41, 56 | eqeltrd 2529 |
. . . . . . . 8
 

    |
58 | 57 | 3exp 1207 |
. . . . . . 7
 
      |
59 | 19, 20, 58 | rexlimd 2871 |
. . . . . 6
  
     |
60 | 59 | adantr 467 |
. . . . 5
 

   
     |
61 | 18, 60 | mpd 15 |
. . . 4
 

      |
62 | 7, 12, 61 | sge0pnfval 38215 |
. . 3
 

  Σ^      |
63 | 1 | adantr 467 |
. . . 4
 

 
  |
64 | 39, 53 | eqeltrd 2529 |
. . . . . 6
 
      |
65 | 19, 64, 14 | fmptdf 6048 |
. . . . 5
            |
66 | 65 | adantr 467 |
. . . 4
 

             |
67 | | simpr 463 |
. . . 4
 

      |
68 | 63, 66, 67 | sge0pnfval 38215 |
. . 3
 

  Σ^      |
69 | 62, 68 | eqtr4d 2488 |
. 2
 

  Σ^    Σ^      |
70 | | sumex 13754 |
. . . . . . 7

 |
71 | 70 | a1i 11 |
. . . . . 6
          
  |
72 | | cnvimass 5188 |
. . . . . . . . . . . . 13
    
 |
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
        |
74 | | fdm 5733 |
. . . . . . . . . . . . 13
       |
75 | 23, 74 | syl 17 |
. . . . . . . . . . . 12
   |
76 | 73, 75 | sseqtrd 3468 |
. . . . . . . . . . 11
        |
77 | | fex 6138 |
. . . . . . . . . . . . . . 15
     
   |
78 | 23, 1, 77 | syl2anc 667 |
. . . . . . . . . . . . . 14
   |
79 | | cnvexg 6739 |
. . . . . . . . . . . . . 14
 
  |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . 13
 
  |
81 | | imaexg 6730 |
. . . . . . . . . . . . 13
         |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . 12
        |
83 | | elpwg 3959 |
. . . . . . . . . . . 12
                     |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
                |
85 | 76, 84 | mpbird 236 |
. . . . . . . . . 10
         |
86 | 85 | adantr 467 |
. . . . . . . . 9
 
            |
87 | | f1ocnv 5826 |
. . . . . . . . . . . . 13
    
       |
88 | 2, 87 | syl 17 |
. . . . . . . . . . . 12
        |
89 | | f1ofun 5816 |
. . . . . . . . . . . 12
         |
90 | 88, 89 | syl 17 |
. . . . . . . . . . 11
    |
91 | 90 | adantr 467 |
. . . . . . . . . 10
 
       |
92 | | elinel2 3620 |
. . . . . . . . . . 11
      |
93 | 92 | adantl 468 |
. . . . . . . . . 10
 
      |
94 | | imafi 7867 |
. . . . . . . . . 10
  
        |
95 | 91, 93, 94 | syl2anc 667 |
. . . . . . . . 9
 
           |
96 | 86, 95 | elind 3618 |
. . . . . . . 8
 
              |
97 | 96 | adantlr 721 |
. . . . . . 7
                    |
98 | | nfv 1761 |
. . . . . . . . . 10
 
  |
99 | 8, 98 | nfan 2011 |
. . . . . . . . 9
       |
100 | | nfv 1761 |
. . . . . . . . 9
     |
101 | 99, 100 | nfan 2011 |
. . . . . . . 8
            |
102 | | nfcv 2592 |
. . . . . . . . . . . 12
  |
103 | | nfmpt1 4492 |
. . . . . . . . . . . . 13
     |
104 | 103 | nfrn 5077 |
. . . . . . . . . . . 12
     |
105 | 102, 104 | nfel 2604 |
. . . . . . . . . . 11
    |
106 | 105 | nfn 1983 |
. . . . . . . . . 10
    |
107 | 19, 106 | nfan 2011 |
. . . . . . . . 9
  
    |
108 | | nfv 1761 |
. . . . . . . . 9

    |
109 | 107, 108 | nfan 2011 |
. . . . . . . 8
            |
110 | 95 | adantlr 721 |
. . . . . . . 8
                 |
111 | | f1of1 5813 |
. . . . . . . . . . . . 13
    
      |
112 | 2, 111 | syl 17 |
. . . . . . . . . . . 12
       |
113 | 112 | adantr 467 |
. . . . . . . . . . 11
 
          |
114 | 84 | adantr 467 |
. . . . . . . . . . . 12
 
                   |
115 | 86, 114 | mpbid 214 |
. . . . . . . . . . 11
 
           |
116 | | f1ores 5828 |
. . . . . . . . . . 11
           
                           |
117 | 113, 115,
116 | syl2anc 667 |
. . . . . . . . . 10
 
                               |
118 | 4 | adantr 467 |
. . . . . . . . . . . 12
 
          |
119 | | elpwinss 37387 |
. . . . . . . . . . . . 13
      |
120 | 119 | adantl 468 |
. . . . . . . . . . . 12
 
      |
121 | | foimacnv 5831 |
. . . . . . . . . . . 12
     
            |
122 | 118, 120,
121 | syl2anc 667 |
. . . . . . . . . . 11
 
               |
123 | 122 | f1oeq3d 37442 |
. . . . . . . . . 10
 
                                                 |
124 | 117, 123 | mpbid 214 |
. . . . . . . . 9
 
                      |
125 | 124 | adantlr 721 |
. . . . . . . 8
                            |
126 | 82 | ad2antrr 732 |
. . . . . . . . . 10
                    |
127 | | simpll 760 |
. . . . . . . . . . 11
               |
128 | 96 | adantr 467 |
. . . . . . . . . . 11
                       |
129 | | simpr 463 |
. . . . . . . . . . 11
            
       |
130 | 127, 128,
129 | jca31 537 |
. . . . . . . . . 10
                       
        |
131 | | eleq1 2517 |
. . . . . . . . . . . . . 14
                     |
132 | 131 | anbi2d 710 |
. . . . . . . . . . . . 13
       
   
             |
133 | | eleq2 2518 |
. . . . . . . . . . . . 13
      
        |
134 | 132, 133 | anbi12d 717 |
. . . . . . . . . . . 12
        
                         |
135 | | reseq2 5100 |
. . . . . . . . . . . . . 14
                 |
136 | 135 | fveq1d 5867 |
. . . . . . . . . . . . 13
                         |
137 | 136 | eqeq1d 2453 |
. . . . . . . . . . . 12
            
              |
138 | 134, 137 | imbi12d 322 |
. . . . . . . . . . 11
             
       
  
        
                     |
139 | | fvres 5879 |
. . . . . . . . . . . . 13
             |
140 | 139 | adantl 468 |
. . . . . . . . . . . 12
                    |
141 | | simpll 760 |
. . . . . . . . . . . . 13
          |
142 | | elpwinss 37387 |
. . . . . . . . . . . . . . 15
      |
143 | 142 | adantl 468 |
. . . . . . . . . . . . . 14
 
      |
144 | 143 | sselda 3432 |
. . . . . . . . . . . . 13
          |
145 | 141, 144,
25 | syl2anc 667 |
. . . . . . . . . . . 12
              |
146 | 140, 145 | eqtrd 2485 |
. . . . . . . . . . 11
                |
147 | 138, 146 | vtoclg 3107 |
. . . . . . . . . 10
                 
                    |
148 | 126, 130,
147 | sylc 62 |
. . . . . . . . 9
                          |
149 | 148 | adantllr 725 |
. . . . . . . 8
                              |
150 | 82 | ad3antrrr 736 |
. . . . . . . . 9
                   |
151 | | simpll 760 |
. . . . . . . . . 10
                  |
152 | 85 | ad3antrrr 736 |
. . . . . . . . . . 11
                    |
153 | 110 | adantr 467 |
. . . . . . . . . . 11
                   |
154 | 152, 153 | elind 3618 |
. . . . . . . . . 10
                      |
155 | | simpr 463 |
. . . . . . . . . . . 12
          |
156 | 122 | eqcomd 2457 |
. . . . . . . . . . . . 13
 
               |
157 | 156 | adantr 467 |
. . . . . . . . . . . 12
                   |
158 | 155, 157 | eleqtrd 2531 |
. . . . . . . . . . 11
                   |
159 | 158 | adantllr 725 |
. . . . . . . . . 10
                       |
160 | 151, 154,
159 | jca31 537 |
. . . . . . . . 9
                          
            |
161 | 131 | anbi2d 710 |
. . . . . . . . . . . 12
               
                 |
162 | | imaeq2 5164 |
. . . . . . . . . . . . 13
                     |
163 | 162 | eleq2d 2514 |
. . . . . . . . . . . 12
          
            |
164 | 161, 163 | anbi12d 717 |
. . . . . . . . . . 11
         

 
           
           
             |
165 | 164 | imbi1d 319 |
. . . . . . . . . 10
          
  
        

               
              |
166 | | rge0ssre 11740 |
. . . . . . . . . . . . 13
    |
167 | | ax-resscn 9596 |
. . . . . . . . . . . . 13
 |
168 | 166, 167 | sstri 3441 |
. . . . . . . . . . . 12
    |
169 | | simplll 768 |
. . . . . . . . . . . . 13
                  |
170 | | simpllr 769 |
. . . . . . . . . . . . 13
                    |
171 | | fimass 37443 |
. . . . . . . . . . . . . . . . 17
        
  |
172 | 23, 171 | syl 17 |
. . . . . . . . . . . . . . . 16
    
  |
173 | 172 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
                  |
174 | | simpr 463 |
. . . . . . . . . . . . . . 15
                  |
175 | 173, 174 | sseldd 3433 |
. . . . . . . . . . . . . 14
              |
176 | 175 | adantllr 725 |
. . . . . . . . . . . . 13
                  |
177 | | foelrni 5913 |
. . . . . . . . . . . . . . . 16
     


      |
178 | 4, 177 | sylan 474 |
. . . . . . . . . . . . . . 15
 
 
      |
179 | 178 | adantlr 721 |
. . . . . . . . . . . . . 14
       
      |
180 | | nfv 1761 |
. . . . . . . . . . . . . . . 16

 |
181 | 107, 180 | nfan 2011 |
. . . . . . . . . . . . . . 15
         |
182 | | nfv 1761 |
. . . . . . . . . . . . . . 15

    |
183 | | csbid 3371 |
. . . . . . . . . . . . . . . . . . . . . 22
  ![]_ ]_](_urbrack.gif)  |
184 | 183 | eqcomi 2460 |
. . . . . . . . . . . . . . . . . . . . 21
  ![]_ ]_](_urbrack.gif)  |
185 | 184 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
    
  ![]_ ]_](_urbrack.gif)   |
186 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
187 | 186 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
188 | 187 | csbeq1d 3370 |
. . . . . . . . . . . . . . . . . . . . 21
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
189 | 188 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . . . . . 20
 
    
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
190 | 38 | idi 2 |
. . . . . . . . . . . . . . . . . . . . 21
 
       ![]_ ]_](_urbrack.gif)   |
191 | 190 | 3adant3 1028 |
. . . . . . . . . . . . . . . . . . . 20
 
    
      ![]_ ]_](_urbrack.gif)   |
192 | 185, 189,
191 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
193 | 192 | 3adant1r 1261 |
. . . . . . . . . . . . . . . . . 18
             |
194 | | 0xr 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
195 | 194 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      |
196 | | pnfxr 11412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
197 | 196 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
   
  |
198 | 64 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
         |
199 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
   
     |
200 | 195, 197,
198, 199 | eliccnelico 37631 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      |
201 | 200 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   
  |
202 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
203 | 64 | idi 2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
      |
204 | 14 | elrnmpt1 5083 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
   |
205 | 202, 203,
204 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
206 | 205 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
   |
207 | 201, 206 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . 21
   
   

   |
208 | 207 | adantllr 725 |
. . . . . . . . . . . . . . . . . . . 20
       
   

   |
209 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . . 20
       
   

   |
210 | 208, 209 | condan 803 |
. . . . . . . . . . . . . . . . . . 19
            |
211 | 210 | 3adant3 1028 |
. . . . . . . . . . . . . . . . . 18
                |
212 | 193, 211 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . 17
                |
213 | 212 | 3exp 1207 |
. . . . . . . . . . . . . . . 16
 
                |
214 | 213 | adantr 467 |
. . . . . . . . . . . . . . 15
                    |
215 | 181, 182,
214 | rexlimd 2871 |
. . . . . . . . . . . . . 14
        
          |
216 | 179, 215 | mpd 15 |
. . . . . . . . . . . . 13
            |
217 | 169, 170,
176, 216 | syl21anc 1267 |
. . . . . . . . . . . 12
                     |
218 | 168, 217 | sseldi 3430 |
. . . . . . . . . . 11
                  |
219 | 218 | idi 2 |
. . . . . . . . . 10
                  |
220 | 165, 219 | vtoclg 3107 |
. . . . . . . . 9
         

          
             |
221 | 150, 160,
220 | sylc 62 |
. . . . . . . 8
              |
222 | 101, 109,
36, 110, 125, 149, 221 | fsumf1of 37653 |
. . . . . . 7
          
         |
223 | | sumeq1 13755 |
. . . . . . . . 9
      
         |
224 | 223 | eqeq2d 2461 |
. . . . . . . 8
                    |
225 | 224 | rspcev 3150 |
. . . . . . 7
                         
  |
226 | 97, 222, 225 | syl2anc 667 |
. . . . . 6
                
  |
227 | 71, 226 | rnmptssrn 37456 |
. . . . 5
 
         
 
 
   |
228 | | sumex 13754 |
. . . . . . 7

 |
229 | 228 | a1i 11 |
. . . . . 6
          
  |
230 | 6, 172 | ssexd 4550 |
. . . . . . . . . . . 12
       |
231 | | elpwg 3959 |
. . . . . . . . . . . 12
                  |
232 | 230, 231 | syl 17 |
. . . . . . . . . . 11
          
   |
233 | 172, 232 | mpbird 236 |
. . . . . . . . . 10
        |
234 | 233 | adantr 467 |
. . . . . . . . 9
 
           |
235 | | ffun 5731 |
. . . . . . . . . . . 12
       |
236 | 23, 235 | syl 17 |
. . . . . . . . . . 11
   |
237 | 236 | adantr 467 |
. . . . . . . . . 10
 
      |
238 | | elinel2 3620 |
. . . . . . . . . . 11
      |
239 | 238 | adantl 468 |
. . . . . . . . . 10
 
      |
240 | | imafi 7867 |
. . . . . . . . . 10
         |
241 | 237, 239,
240 | syl2anc 667 |
. . . . . . . . 9
 
          |
242 | 234, 241 | elind 3618 |
. . . . . . . 8
 
             |
243 | 242 | adantlr 721 |
. . . . . . 7
                   |
244 | | nfv 1761 |
. . . . . . . . . 10
     |
245 | 99, 244 | nfan 2011 |
. . . . . . . . 9
            |
246 | | nfv 1761 |
. . . . . . . . . 10

    |
247 | 107, 246 | nfan 2011 |
. . . . . . . . 9
            |
248 | 238 | adantl 468 |
. . . . . . . . 9
            |
249 | 112 | adantr 467 |
. . . . . . . . . . 11
 
          |
250 | | f1ores 5828 |
. . . . . . . . . . 11
     
             |
251 | 249, 143,
250 | syl2anc 667 |
. . . . . . . . . 10
 
                |
252 | 251 | adantlr 721 |
. . . . . . . . 9
                      |
253 | 146 | adantllr 725 |
. . . . . . . . 9
                    |
254 | 245, 247,
36, 248, 252, 253, 218 | fsumf1of 37653 |
. . . . . . . 8
                   |
255 | 254 | eqcomd 2457 |
. . . . . . 7
          
        |
256 | | sumeq1 13755 |
. . . . . . . . 9
     
        |
257 | 256 | eqeq2d 2461 |
. . . . . . . 8
        
         |
258 | 257 | rspcev 3150 |
. . . . . . 7
         
       
 
      |
259 | 243, 255,
258 | syl2anc 667 |
. . . . . 6
               
   |
260 | 229, 259 | rnmptssrn 37456 |
. . . . 5
 
                 |
261 | 227, 260 | eqssd 3449 |
. . . 4
 
         
 
 
   |
262 | 261 | supeq1d 7960 |
. . 3
 
         
         
     |
263 | 6 | adantr 467 |
. . . 4
 
  
  |
264 | 99, 263, 216 | sge0revalmpt 38220 |
. . 3
 
   Σ^                |
265 | 1 | adantr 467 |
. . . 4
 
  
  |
266 | 107, 265,
210 | sge0revalmpt 38220 |
. . 3
 
   Σ^          
     |
267 | 262, 264,
266 | 3eqtr4d 2495 |
. 2
 
   Σ^    Σ^      |
268 | 69, 267 | pm2.61dan 800 |
1
 Σ^    Σ^      |