Step | Hyp | Ref
| Expression |
1 | | nfv 1769 |
. . 3
   |
2 | | sge0xaddlem2.a |
. . 3
   |
3 | | 0xr 9705 |
. . . . 5
 |
4 | 3 | a1i 11 |
. . . 4
 
   |
5 | | pnfxr 11435 |
. . . . 5
 |
6 | 5 | a1i 11 |
. . . 4
 
   |
7 | | rge0ssre 11766 |
. . . . . . 7
    |
8 | | sge0xaddlem2.b |
. . . . . . 7
 
      |
9 | 7, 8 | sseldi 3416 |
. . . . . 6
 
   |
10 | | sge0xaddlem2.c |
. . . . . . 7
 
      |
11 | 7, 10 | sseldi 3416 |
. . . . . 6
 
   |
12 | 9, 11 | readdcld 9688 |
. . . . 5
 
 
   |
13 | 12 | rexrd 9708 |
. . . 4
 
 
   |
14 | | icossicc 11746 |
. . . . . . 7
       |
15 | 14, 8 | sseldi 3416 |
. . . . . 6
 
      |
16 | | xrge0ge0 37657 |
. . . . . 6
   
  |
17 | 15, 16 | syl 17 |
. . . . 5
 
   |
18 | 14, 10 | sseldi 3416 |
. . . . . 6
 
      |
19 | | xrge0ge0 37657 |
. . . . . 6
   
  |
20 | 18, 19 | syl 17 |
. . . . 5
 
   |
21 | 9, 11, 17, 20 | addge0d 10210 |
. . . 4
 
     |
22 | 12 | ltpnfd 11446 |
. . . 4
 
 
   |
23 | 4, 6, 13, 21, 22 | elicod 11710 |
. . 3
 
 
      |
24 | 1, 2, 23 | sge0revalmpt 38334 |
. 2
 Σ^             
      |
25 | | rexadd 11548 |
. . . . 5
 
          |
26 | 9, 11, 25 | syl2anc 673 |
. . . 4
 
          |
27 | 26 | mpteq2dva 4482 |
. . 3
              |
28 | 27 | fveq2d 5883 |
. 2
 Σ^         Σ^        |
29 | | sge0xaddlem2.sb |
. . . 4
 Σ^      |
30 | | sge0xaddlem2.sc |
. . . 4
 Σ^      |
31 | | rexadd 11548 |
. . . 4
  Σ^    Σ^      Σ^       Σ^      Σ^    Σ^       |
32 | 29, 30, 31 | syl2anc 673 |
. . 3
  Σ^       Σ^      Σ^    Σ^       |
33 | 1, 2, 8 | sge0revalmpt 38334 |
. . . 4
 Σ^                |
34 | 1, 2, 10 | sge0revalmpt 38334 |
. . . 4
 Σ^                |
35 | 33, 34 | oveq12d 6326 |
. . 3
  Σ^    Σ^                             |
36 | 33 | eqcomd 2477 |
. . . . . . 7
           Σ^      |
37 | 36, 29 | eqeltrd 2549 |
. . . . . 6
             |
38 | 34, 30 | eqeltrrd 2550 |
. . . . . 6
             |
39 | 37, 38 | readdcld 9688 |
. . . . 5
                         |
40 | 39 | rexrd 9708 |
. . . 4
                         |
41 | | elinel2 3611 |
. . . . . . . . . 10
      |
42 | 41 | adantl 473 |
. . . . . . . . 9
 
      |
43 | | simpll 768 |
. . . . . . . . . . 11
          |
44 | | elpwinss 37446 |
. . . . . . . . . . . . . 14
      |
45 | 44 | adantr 472 |
. . . . . . . . . . . . 13
    

  |
46 | | simpr 468 |
. . . . . . . . . . . . 13
    

  |
47 | 45, 46 | sseldd 3419 |
. . . . . . . . . . . 12
    

  |
48 | 47 | adantll 728 |
. . . . . . . . . . 11
          |
49 | 43, 48, 9 | syl2anc 673 |
. . . . . . . . . 10
          |
50 | 43, 48, 11 | syl2anc 673 |
. . . . . . . . . 10
          |
51 | 49, 50 | readdcld 9688 |
. . . . . . . . 9
        
   |
52 | 42, 51 | fsumrecl 13877 |
. . . . . . . 8
 
    
    |
53 | 52 | rexrd 9708 |
. . . . . . 7
 
    
    |
54 | 53 | ralrimiva 2809 |
. . . . . 6
       
   |
55 | | eqid 2471 |
. . . . . . 7
    
        
   |
56 | 55 | rnmptss 6068 |
. . . . . 6
 
    


    
     |
57 | 54, 56 | syl 17 |
. . . . 5
      
    |
58 | | supxrcl 11625 |
. . . . 5
      
        
    
  |
59 | 57, 58 | syl 17 |
. . . 4
        
      |
60 | 35 | eqcomd 2477 |
. . . . . . 7
                        Σ^    Σ^       |
61 | 60 | adantr 472 |
. . . . . 6
 

                       Σ^    Σ^       |
62 | | nfv 1769 |
. . . . . . . 8
     |
63 | 2 | adantr 472 |
. . . . . . . 8
 

  |
64 | 15 | adantlr 729 |
. . . . . . . 8
          |
65 | | rphalfcl 11350 |
. . . . . . . . 9

    |
66 | 65 | adantl 473 |
. . . . . . . 8
 

    |
67 | 29 | adantr 472 |
. . . . . . . 8
 

Σ^      |
68 | 62, 63, 64, 66, 67 | sge0ltfirpmpt2 38382 |
. . . . . . 7
 

     Σ^     
     |
69 | 18 | adantlr 729 |
. . . . . . . . . . . 12
          |
70 | 30 | adantr 472 |
. . . . . . . . . . . 12
 

Σ^      |
71 | 62, 63, 69, 66, 70 | sge0ltfirpmpt2 38382 |
. . . . . . . . . . 11
 

     Σ^           |
72 | 71 | 3ad2ant1 1051 |
. . . . . . . . . 10
       Σ^     
   
     Σ^           |
73 | 63 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . 15
       Σ^     
   
  |
74 | 73 | 3ad2ant1 1051 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
  |
75 | | simpl1l 1081 |
. . . . . . . . . . . . . . . 16
   

   Σ^     
       |
76 | 75 | 3ad2antl1 1192 |
. . . . . . . . . . . . . . 15
     
 
 Σ^     
       Σ^             |
77 | | simpr 468 |
. . . . . . . . . . . . . . 15
     
 
 Σ^     
       Σ^             |
78 | | nfv 1769 |
. . . . . . . . . . . . . . . . 17
     |
79 | | nfcsb1v 3365 |
. . . . . . . . . . . . . . . . . 18
  
 ![]_ ]_](_urbrack.gif)  |
80 | 79 | nfel1 2626 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)
 
  |
81 | 78, 80 | nfim 2023 |
. . . . . . . . . . . . . . . 16
   
   ![]_ ]_](_urbrack.gif)
 
   |
82 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . 18
 
   |
83 | 82 | anbi2d 718 |
. . . . . . . . . . . . . . . . 17
  

     |
84 | | csbeq1a 3358 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
85 | 84 | eleq1d 2533 |
. . . . . . . . . . . . . . . . 17
 
  
  ![]_ ]_](_urbrack.gif)       |
86 | 83, 85 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
   
      
   ![]_ ]_](_urbrack.gif)
 
     |
87 | 81, 86, 8 | chvar 2119 |
. . . . . . . . . . . . . . 15
 
   ![]_ ]_](_urbrack.gif)      |
88 | 76, 77, 87 | syl2anc 673 |
. . . . . . . . . . . . . 14
     
 
 Σ^     
       Σ^             ![]_ ]_](_urbrack.gif)      |
89 | | nfcsb1v 3365 |
. . . . . . . . . . . . . . . . . 18
  
 ![]_ ]_](_urbrack.gif)  |
90 | 89 | nfel1 2626 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)
 
  |
91 | 78, 90 | nfim 2023 |
. . . . . . . . . . . . . . . 16
   
   ![]_ ]_](_urbrack.gif)
 
   |
92 | | csbeq1a 3358 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
93 | 92 | eleq1d 2533 |
. . . . . . . . . . . . . . . . 17
 
  
  ![]_ ]_](_urbrack.gif)       |
94 | 83, 93 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
   
      
   ![]_ ]_](_urbrack.gif)
 
     |
95 | 91, 94, 10 | chvar 2119 |
. . . . . . . . . . . . . . 15
 
   ![]_ ]_](_urbrack.gif)      |
96 | 76, 77, 95 | syl2anc 673 |
. . . . . . . . . . . . . 14
     
 
 Σ^     
       Σ^             ![]_ ]_](_urbrack.gif)      |
97 | | simp11r 1142 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
  |
98 | | simp12 1061 |
. . . . . . . . . . . . . . 15
   

   Σ^     
       Σ^         
     |
99 | | elpwinss 37446 |
. . . . . . . . . . . . . . 15
      |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
  |
101 | | elinel2 3611 |
. . . . . . . . . . . . . . . 16
      |
102 | 101 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . 15
       Σ^     
   
  |
103 | 102 | 3ad2ant1 1051 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
  |
104 | | simp2 1031 |
. . . . . . . . . . . . . . 15
   

   Σ^     
       Σ^         
     |
105 | | elpwinss 37446 |
. . . . . . . . . . . . . . 15
      |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
  |
107 | | elinel2 3611 |
. . . . . . . . . . . . . . 15
      |
108 | 107 | 3ad2ant2 1052 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
  |
109 | | simp13 1062 |
. . . . . . . . . . . . . . 15
   

   Σ^     
       Σ^         
Σ^     
     |
110 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
   |
111 | 110, 79, 84 | cbvmpt 4487 |
. . . . . . . . . . . . . . . . . 18
     ![]_ ]_](_urbrack.gif)   |
112 | 111 | fveq2i 5882 |
. . . . . . . . . . . . . . . . 17
Σ^    Σ^    ![]_ ]_](_urbrack.gif)    |
113 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
   |
114 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
   |
115 | 84, 113, 114, 110, 79 | cbvsum 13838 |
. . . . . . . . . . . . . . . . . 18

   ![]_ ]_](_urbrack.gif)  |
116 | 115 | oveq1i 6318 |
. . . . . . . . . . . . . . . . 17
 
       ![]_ ]_](_urbrack.gif)
    |
117 | 112, 116 | breq12i 4404 |
. . . . . . . . . . . . . . . 16
 Σ^        
Σ^    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
     |
118 | 117 | biimpi 199 |
. . . . . . . . . . . . . . 15
 Σ^         Σ^    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
     |
119 | 109, 118 | syl 17 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
Σ^    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
     |
120 | | simp3 1032 |
. . . . . . . . . . . . . . 15
   

   Σ^     
       Σ^         
Σ^           |
121 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
   |
122 | 121, 89, 92 | cbvmpt 4487 |
. . . . . . . . . . . . . . . . . 18
     ![]_ ]_](_urbrack.gif)   |
123 | 122 | fveq2i 5882 |
. . . . . . . . . . . . . . . . 17
Σ^    Σ^    ![]_ ]_](_urbrack.gif)    |
124 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
   |
125 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
   |
126 | 92, 124, 125, 121, 89 | cbvsum 13838 |
. . . . . . . . . . . . . . . . . 18

   ![]_ ]_](_urbrack.gif)  |
127 | 126 | oveq1i 6318 |
. . . . . . . . . . . . . . . . 17
 
       ![]_ ]_](_urbrack.gif)
    |
128 | 123, 127 | breq12i 4404 |
. . . . . . . . . . . . . . . 16
 Σ^        
Σ^    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
     |
129 | 128 | biimpi 199 |
. . . . . . . . . . . . . . 15
 Σ^         Σ^    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
     |
130 | 120, 129 | syl 17 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
Σ^    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
     |
131 | | simp11l 1141 |
. . . . . . . . . . . . . . 15
   

   Σ^     
       Σ^         
  |
132 | 84, 92 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
133 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
134 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
135 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
136 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  |
137 | 79, 136, 89 | nfov 6334 |
. . . . . . . . . . . . . . . . . . . . . . 23
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
138 | 132, 133,
134, 135, 137 | cbvsum 13838 |
. . . . . . . . . . . . . . . . . . . . . 22

  
 
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
139 | 138 | mpteq2i 4479 |
. . . . . . . . . . . . . . . . . . . . 21
    
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
140 | 139 | rneqi 5067 |
. . . . . . . . . . . . . . . . . . . 20
     
  
 
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
141 | 140 | supeq1i 7979 |
. . . . . . . . . . . . . . . . . . 19
       
              ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
142 | 141 | eqcomi 2480 |
. . . . . . . . . . . . . . . . . 18
          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)            
     |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . . . . 17
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)            
      |
144 | 143, 24 | eqtr4d 2508 |
. . . . . . . . . . . . . . . 16
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     Σ^        |
145 | | ge0xaddcl 11772 |
. . . . . . . . . . . . . . . . . . 19
    
              |
146 | 15, 18, 145 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
 
           |
147 | 26, 146 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . 17
 
 
      |
148 | 1, 2, 147 | sge0clmpt 38381 |
. . . . . . . . . . . . . . . 16
 Σ^           |
149 | 144, 148 | eqeltrd 2549 |
. . . . . . . . . . . . . . 15
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)          |
150 | 131, 149 | syl 17 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)          |
151 | 112, 29 | syl5eqelr 2554 |
. . . . . . . . . . . . . . 15
 Σ^    ![]_ ]_](_urbrack.gif)     |
152 | 131, 151 | syl 17 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
Σ^    ![]_ ]_](_urbrack.gif)     |
153 | 123, 30 | syl5eqelr 2554 |
. . . . . . . . . . . . . . 15
 Σ^    ![]_ ]_](_urbrack.gif)     |
154 | 131, 153 | syl 17 |
. . . . . . . . . . . . . 14
   

   Σ^     
       Σ^         
Σ^    ![]_ ]_](_urbrack.gif)     |
155 | 74, 88, 96, 97, 100, 103, 106, 108, 119, 130, 150, 152, 154 | sge0xaddlem1 38389 |
. . . . . . . . . . . . 13
   

   Σ^     
       Σ^         
 Σ^    ![]_ ]_](_urbrack.gif)   Σ^    ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)           |
156 | 112, 123 | oveq12i 6320 |
. . . . . . . . . . . . . 14
 Σ^    Σ^      Σ^    ![]_ ]_](_urbrack.gif)   Σ^    ![]_ ]_](_urbrack.gif)     |
157 | 141 | oveq1i 6318 |
. . . . . . . . . . . . . 14
       
    
               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)          |
158 | 156, 157 | breq12i 4404 |
. . . . . . . . . . . . 13
  Σ^    Σ^             
       
 Σ^    ![]_ ]_](_urbrack.gif)   Σ^    ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)           |
159 | 155, 158 | sylibr 217 |
. . . . . . . . . . . 12
   

   Σ^     
       Σ^         
 Σ^    Σ^             
          |
160 | 159 | 3exp 1230 |
. . . . . . . . . . 11
       Σ^     
   
   
 Σ^          Σ^    Σ^             
            |
161 | 160 | rexlimdv 2870 |
. . . . . . . . . 10
       Σ^     
   
 
    Σ^          Σ^    Σ^             
           |
162 | 72, 161 | mpd 15 |
. . . . . . . . 9
       Σ^     
   
 Σ^    Σ^             
          |
163 | 162 | 3exp 1230 |
. . . . . . . 8
 

   
 Σ^          Σ^    Σ^             
            |
164 | 163 | rexlimdv 2870 |
. . . . . . 7
 

 
    Σ^          Σ^    Σ^             
           |
165 | 68, 164 | mpd 15 |
. . . . . 6
 

 Σ^    Σ^             
          |
166 | 61, 165 | eqbrtrd 4416 |
. . . . 5
 

                              
          |
167 | 40, 59, 166 | xrlexaddrp 37662 |
. . . 4
                             
    
  |
168 | 24 | eqcomd 2477 |
. . . . 5
        
    Σ^        |
169 | 43, 48, 23 | syl2anc 673 |
. . . . . . . . . 10
        
      |
170 | 42, 169 | sge0fsummpt 38346 |
. . . . . . . . 9
 
    Σ^      

   |
171 | 49 | recnd 9687 |
. . . . . . . . . 10
          |
172 | 50 | recnd 9687 |
. . . . . . . . . 10
          |
173 | 42, 171, 172 | fsumadd 13882 |
. . . . . . . . 9
 
    
   
    |
174 | 170, 173 | eqtrd 2505 |
. . . . . . . 8
 
    Σ^       
    |
175 | 42, 49 | fsumrecl 13877 |
. . . . . . . . 9
 
    
  |
176 | 42, 50 | fsumrecl 13877 |
. . . . . . . . 9
 
    
  |
177 | 37 | adantr 472 |
. . . . . . . . 9
 
                |
178 | 38 | adantr 472 |
. . . . . . . . 9
 
                |
179 | | elinel2 3611 |
. . . . . . . . . . . . . . . 16
      |
180 | 179 | adantl 473 |
. . . . . . . . . . . . . . 15
 
      |
181 | | simpll 768 |
. . . . . . . . . . . . . . . 16
          |
182 | | elpwinss 37446 |
. . . . . . . . . . . . . . . . . . 19
      |
183 | 182 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
    

  |
184 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
    

  |
185 | 183, 184 | sseldd 3419 |
. . . . . . . . . . . . . . . . 17
    

  |
186 | 185 | adantll 728 |
. . . . . . . . . . . . . . . 16
          |
187 | 181, 186,
9 | syl2anc 673 |
. . . . . . . . . . . . . . 15
          |
188 | 180, 187 | fsumrecl 13877 |
. . . . . . . . . . . . . 14
 
    
  |
189 | 188 | rexrd 9708 |
. . . . . . . . . . . . 13
 
    
  |
190 | 189 | ralrimiva 2809 |
. . . . . . . . . . . 12
         |
191 | | eqid 2471 |
. . . . . . . . . . . . 13
    
        |
192 | 191 | rnmptss 6068 |
. . . . . . . . . . . 12
 
    
    
   |
193 | 190, 192 | syl 17 |
. . . . . . . . . . 11
         |
194 | 193 | adantr 472 |
. . . . . . . . . 10
 
            |
195 | | simpr 468 |
. . . . . . . . . . . 12
 
         |
196 | | eqidd 2472 |
. . . . . . . . . . . 12
 
    
   |
197 | | sumeq1 13832 |
. . . . . . . . . . . . . 14
 
   |
198 | 197 | eqeq2d 2481 |
. . . . . . . . . . . . 13
    
    |
199 | 198 | rspcev 3136 |
. . . . . . . . . . . 12
     
  
 
      |
200 | 195, 196,
199 | syl2anc 673 |
. . . . . . . . . . 11
 
         
   |
201 | 175 | elexd 3042 |
. . . . . . . . . . 11
 
    
  |
202 | 191, 200,
201 | elrnmptd 37524 |
. . . . . . . . . 10
 
    
        |
203 | | supxrub 11635 |
. . . . . . . . . 10
        
                    |
204 | 194, 202,
203 | syl2anc 673 |
. . . . . . . . 9
 
    
      
     |
205 | | nfv 1769 |
. . . . . . . . . . . 12
   |
206 | | eqid 2471 |
. . . . . . . . . . . 12
    
        |
207 | | elinel2 3611 |
. . . . . . . . . . . . . . 15
      |
208 | 207 | adantl 473 |
. . . . . . . . . . . . . 14
 
      |
209 | | simpll 768 |
. . . . . . . . . . . . . . 15
          |
210 | | elpwinss 37446 |
. . . . . . . . . . . . . . . . . 18
      |
211 | 210 | adantr 472 |
. . . . . . . . . . . . . . . . 17
    

  |
212 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
    

  |
213 | 211, 212 | sseldd 3419 |
. . . . . . . . . . . . . . . 16
    

  |
214 | 213 | adantll 728 |
. . . . . . . . . . . . . . 15
          |
215 | 209, 214,
11 | syl2anc 673 |
. . . . . . . . . . . . . 14
          |
216 | 208, 215 | fsumrecl 13877 |
. . . . . . . . . . . . 13
 
    
  |
217 | 216 | rexrd 9708 |
. . . . . . . . . . . 12
 
    
  |
218 | 205, 206,
217 | rnmptssd 37544 |
. . . . . . . . . . 11
         |
219 | 218 | adantr 472 |
. . . . . . . . . 10
 
            |
220 | | eqidd 2472 |
. . . . . . . . . . . 12
 
    
   |
221 | | sumeq1 13832 |
. . . . . . . . . . . . . 14
 
   |
222 | 221 | eqeq2d 2481 |
. . . . . . . . . . . . 13
    
    |
223 | 222 | rspcev 3136 |
. . . . . . . . . . . 12
     
  
 
      |
224 | 195, 220,
223 | syl2anc 673 |
. . . . . . . . . . 11
 
         
   |
225 | 176 | elexd 3042 |
. . . . . . . . . . 11
 
    
  |
226 | 206, 224,
225 | elrnmptd 37524 |
. . . . . . . . . 10
 
    
        |
227 | | supxrub 11635 |
. . . . . . . . . 10
        
                    |
228 | 219, 226,
227 | syl2anc 673 |
. . . . . . . . 9
 
    
      
     |
229 | 175, 176,
177, 178, 204, 228 | le2addd 10253 |
. . . . . . . 8
 
               
                |
230 | 174, 229 | eqbrtrd 4416 |
. . . . . . 7
 
    Σ^             
                |
231 | 230 | ralrimiva 2809 |
. . . . . 6
      Σ^                              |
232 | 1, 2, 147, 40 | sge0lefimpt 38379 |
. . . . . 6
  Σ^                           
     Σ^                               |
233 | 231, 232 | mpbird 240 |
. . . . 5
 Σ^                              |
234 | 168, 233 | eqbrtrd 4416 |
. . . 4
        
           
                |
235 | 40, 59, 167, 234 | xrletrid 11475 |
. . 3
                              
      |
236 | 32, 35, 235 | 3eqtrd 2509 |
. 2
  Σ^       Σ^            
      |
237 | 24, 28, 236 | 3eqtr4d 2515 |
1
 Σ^          Σ^       Σ^       |