Step | Hyp | Ref
| Expression |
1 | | sge0split.a |
. . . . 5
   |
2 | 1 | adantr 472 |
. . . 4
 
Σ^     |
3 | | sge0split.b |
. . . . 5
   |
4 | 3 | adantr 472 |
. . . 4
 
Σ^     |
5 | | sge0split.u |
. . . 4
   |
6 | | sge0split.in0 |
. . . . 5
     |
7 | 6 | adantr 472 |
. . . 4
 
Σ^       |
8 | | sge0split.f |
. . . . 5
          |
9 | 8 | adantr 472 |
. . . 4
 
Σ^            |
10 | | simpr 468 |
. . . 4
 
Σ^   Σ^    |
11 | 2, 4, 5, 7, 9, 10 | sge0resplit 38362 |
. . 3
 
Σ^   Σ^   Σ^    Σ^       |
12 | | unexg 6611 |
. . . . . . . . 9
 
     |
13 | 1, 3, 12 | syl2anc 673 |
. . . . . . . 8
     |
14 | 5, 13 | syl5eqel 2553 |
. . . . . . 7
   |
15 | 14 | adantr 472 |
. . . . . 6
 
Σ^     |
16 | 15, 9, 10 | sge0ssre 38353 |
. . . . 5
 
Σ^   Σ^      |
17 | 15, 9, 10 | sge0ssre 38353 |
. . . . 5
 
Σ^   Σ^      |
18 | | rexadd 11548 |
. . . . 5
  Σ^    Σ^ 
    Σ^       Σ^      Σ^    Σ^       |
19 | 16, 17, 18 | syl2anc 673 |
. . . 4
 
Σ^    Σ^       Σ^      Σ^    Σ^       |
20 | 19 | eqcomd 2477 |
. . 3
 
Σ^    Σ^    Σ^      Σ^       Σ^       |
21 | 11, 20 | eqtrd 2505 |
. 2
 
Σ^   Σ^   Σ^       Σ^       |
22 | | simpl 464 |
. . 3
 
Σ^     |
23 | | simpr 468 |
. . . . 5
 
Σ^  
Σ^    |
24 | 14, 8 | sge0repnf 38342 |
. . . . . 6
  Σ^  Σ^     |
25 | 24 | adantr 472 |
. . . . 5
 
Σ^    Σ^  Σ^     |
26 | 23, 25 | mtbid 307 |
. . . 4
 
Σ^  
Σ^    |
27 | 26 | notnotrd 117 |
. . 3
 
Σ^   Σ^    |
28 | 14, 8 | sge0xrcl 38341 |
. . . . 5
 Σ^    |
29 | 28 | adantr 472 |
. . . 4
 
Σ^   Σ^    |
30 | | ssun1 3588 |
. . . . . . . . . 10

  |
31 | 30, 5 | sseqtr4i 3451 |
. . . . . . . . 9
 |
32 | 31 | a1i 11 |
. . . . . . . 8

  |
33 | 8, 32 | fssresd 5762 |
. . . . . . 7
            |
34 | 1, 33 | sge0xrcl 38341 |
. . . . . 6
 Σ^      |
35 | | iccssxr 11742 |
. . . . . . 7
    |
36 | | ssun2 3589 |
. . . . . . . . . . 11

  |
37 | 36, 5 | sseqtr4i 3451 |
. . . . . . . . . 10
 |
38 | 37 | a1i 11 |
. . . . . . . . 9

  |
39 | 8, 38 | fssresd 5762 |
. . . . . . . 8
            |
40 | 3, 39 | sge0cl 38337 |
. . . . . . 7
 Σ^         |
41 | 35, 40 | sseldi 3416 |
. . . . . 6
 Σ^      |
42 | 34, 41 | xaddcld 11612 |
. . . . 5
  Σ^       Σ^       |
43 | 42 | adantr 472 |
. . . 4
 
Σ^    Σ^       Σ^       |
44 | | pnfxr 11435 |
. . . . . . . . 9
 |
45 | | eqid 2471 |
. . . . . . . . 9
 |
46 | | xreqle 37628 |
. . . . . . . . 9
    |
47 | 44, 45, 46 | mp2an 686 |
. . . . . . . 8
 |
48 | 47 | a1i 11 |
. . . . . . 7
 

 
  |
49 | 14 | adantr 472 |
. . . . . . . . 9
 

 
  |
50 | 8 | adantr 472 |
. . . . . . . . 9
 

 
         |
51 | | rnresss 37522 |
. . . . . . . . . . 11
   |
52 | 51 | sseli 3414 |
. . . . . . . . . 10
    |
53 | 52 | adantl 473 |
. . . . . . . . 9
 

 
  |
54 | 49, 50, 53 | sge0pnfval 38329 |
. . . . . . . 8
 

 
Σ^    |
55 | | ge0nemnf2 37726 |
. . . . . . . . . . . . . 14
 Σ^      
Σ^      |
56 | 40, 55 | syl 17 |
. . . . . . . . . . . . 13
 Σ^      |
57 | | xaddpnf2 11543 |
. . . . . . . . . . . . 13
  Σ^    Σ^        Σ^       |
58 | 41, 56, 57 | syl2anc 673 |
. . . . . . . . . . . 12
    Σ^       |
59 | 58 | eqcomd 2477 |
. . . . . . . . . . 11
    Σ^       |
60 | 59 | adantr 472 |
. . . . . . . . . 10
 

 
   Σ^       |
61 | 1 | adantr 472 |
. . . . . . . . . . . 12
 

 
  |
62 | 33 | adantr 472 |
. . . . . . . . . . . 12
 

 
           |
63 | | simpr 468 |
. . . . . . . . . . . 12
 

 

   |
64 | 61, 62, 63 | sge0pnfval 38329 |
. . . . . . . . . . 11
 

 
Σ^      |
65 | 64 | oveq1d 6323 |
. . . . . . . . . 10
 

 
 Σ^       Σ^        Σ^       |
66 | 60, 54, 65 | 3eqtr4d 2515 |
. . . . . . . . 9
 

 
Σ^   Σ^       Σ^       |
67 | 66, 54 | eqtr3d 2507 |
. . . . . . . 8
 

 
 Σ^       Σ^       |
68 | 54, 67 | breq12d 4408 |
. . . . . . 7
 

 
 Σ^ 
 Σ^       Σ^    
   |
69 | 48, 68 | mpbird 240 |
. . . . . 6
 

 
Σ^   Σ^       Σ^       |
70 | 47 | a1i 11 |
. . . . . . . . 9
 

 
  |
71 | 14 | adantr 472 |
. . . . . . . . . . 11
 

 
  |
72 | 8 | adantr 472 |
. . . . . . . . . . 11
 

 
         |
73 | | rnresss 37522 |
. . . . . . . . . . . . 13
   |
74 | 73 | sseli 3414 |
. . . . . . . . . . . 12
    |
75 | 74 | adantl 473 |
. . . . . . . . . . 11
 

 
  |
76 | 71, 72, 75 | sge0pnfval 38329 |
. . . . . . . . . 10
 

 
Σ^    |
77 | 3 | adantr 472 |
. . . . . . . . . . . . 13
 

 
  |
78 | 39 | adantr 472 |
. . . . . . . . . . . . 13
 

 
           |
79 | | simpr 468 |
. . . . . . . . . . . . 13
 

 

   |
80 | 77, 78, 79 | sge0pnfval 38329 |
. . . . . . . . . . . 12
 

 
Σ^      |
81 | 80 | oveq2d 6324 |
. . . . . . . . . . 11
 

 
 Σ^       Σ^      Σ^         |
82 | 1, 33 | sge0cl 38337 |
. . . . . . . . . . . . . 14
 Σ^         |
83 | | ge0nemnf2 37726 |
. . . . . . . . . . . . . 14
 Σ^      
Σ^      |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . 13
 Σ^      |
85 | | xaddpnf1 11542 |
. . . . . . . . . . . . 13
  Σ^    Σ^      Σ^      
  |
86 | 34, 84, 85 | syl2anc 673 |
. . . . . . . . . . . 12
  Σ^      
  |
87 | 86 | adantr 472 |
. . . . . . . . . . 11
 

 
 Σ^         |
88 | 81, 87 | eqtrd 2505 |
. . . . . . . . . 10
 

 
 Σ^       Σ^       |
89 | 76, 88 | breq12d 4408 |
. . . . . . . . 9
 

 
 Σ^ 
 Σ^       Σ^    
   |
90 | 70, 89 | mpbird 240 |
. . . . . . . 8
 

 
Σ^   Σ^       Σ^       |
91 | 90 | adantlr 729 |
. . . . . . 7
         Σ^   Σ^       Σ^       |
92 | | simpr 468 |
. . . . . . . . . . . 12
                                 |
93 | | vex 3034 |
. . . . . . . . . . . . 13
 |
94 | | eqid 2471 |
. . . . . . . . . . . . . 14
    
                |
95 | 94 | elrnmpt 5087 |
. . . . . . . . . . . . 13
                 
       |
96 | 93, 95 | ax-mp 5 |
. . . . . . . . . . . 12
     
    
     
      |
97 | 92, 96 | sylib 201 |
. . . . . . . . . . 11
                          
      |
98 | | simp3 1032 |
. . . . . . . . . . . . . . 15
                  
       |
99 | | inss1 3643 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  |
100 | | inss2 3644 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
101 | 99, 100 | sstri 3427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
102 | | inss2 3644 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  |
103 | | inss2 3644 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
104 | 102, 103 | sstri 3427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
105 | 101, 104 | ssini 3646 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
  |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
    |
107 | 106, 6 | sseqtrd 3454 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
  |
108 | | ss0 3768 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
    |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
110 | 109 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . 19
                
     |
111 | | indi 3680 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
   |
112 | 111 | eqcomi 2480 |
. . . . . . . . . . . . . . . . . . . . . 22
       
   |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
                |
114 | 5 | eqcomi 2480 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
115 | 114 | ineq2i 3622 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
    
       |
117 | | elinel1 3610 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
118 | | elpwi 3951 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
      |
120 | | df-ss 3404 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
121 | 120 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
122 | 119, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
    
   |
123 | 113, 116,
122 | 3eqtrrd 2510 |
. . . . . . . . . . . . . . . . . . . 20
            |
124 | 123 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
                      |
125 | | elinel2 3611 |
. . . . . . . . . . . . . . . . . . . 20
      |
126 | 125 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
                |
127 | | rge0ssre 11766 |
. . . . . . . . . . . . . . . . . . . . 21
    |
128 | 8 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                  |
129 | | pm4.56 503 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
   
       |
130 | 129 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
   
       |
131 | | elun 3565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
    
    |
132 | 130, 131 | sylnibr 312 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
   
   
    |
133 | 132 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
   
    |
134 | | rnresun 37519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
   |
135 | 134 | eqcomi 2480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
   |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
        |
137 | 114 | reseq2i 5108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
  |
138 | 137 | rneqi 5067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
139 | 138 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
  
   |
140 | | ffn 5739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
  |
141 | | fnresdm 5695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
142 | 8, 140, 141 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
143 | 142 | rneqd 5068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
144 | 136, 139,
143 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
    |
145 | 144 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
146 | 133, 145 | neleqtrd 2570 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
  |
147 | 128, 146 | fge0iccico 38326 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  |
148 | 147 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . 22
    

    
    
         |
149 | 119 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    

  |
150 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    

  |
151 | 149, 150 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . . . . . 23
    

  |
152 | 151 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . 22
    

    
    
  |
153 | 148, 152 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . 21
    

    
    
         |
154 | 127, 153 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . 20
    

    
    
      |
155 | 154 | recnd 9687 |
. . . . . . . . . . . . . . . . . . 19
    

    
    
      |
156 | 110, 124,
126, 155 | fsumsplit 13883 |
. . . . . . . . . . . . . . . . . 18
              
                        |
157 | | infi 7813 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
158 | 125, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   |
159 | 158 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
              
   |
160 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . 22
    

    
      
  
            |
161 | | elinel1 3610 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
162 | 161 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
    

    
      
  |
163 | 160, 162,
154 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
    

    
      
      |
164 | 159, 163 | fsumrecl 13877 |
. . . . . . . . . . . . . . . . . . . 20
                        |
165 | | infi 7813 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
166 | 125, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   |
167 | 166 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
              
   |
168 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . 22
    

    
      
  
            |
169 | | elinel1 3610 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
170 | 169 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
    

    
      
  |
171 | 168, 170,
154 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
    

    
      
      |
172 | 167, 171 | fsumrecl 13877 |
. . . . . . . . . . . . . . . . . . . 20
                        |
173 | | rexadd 11548 |
. . . . . . . . . . . . . . . . . . . 20
                               
                 
          |
174 | 164, 172,
173 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
                                                       |
175 | 174 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . 18
                                            
          |
176 | 156, 175 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
              
                
          |
177 | | ressxr 9702 |
. . . . . . . . . . . . . . . . . . . 20
 |
178 | 177, 164 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . 19
                        |
179 | 177, 172 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . 19
                        |
180 | 1 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  
  |
181 | 33 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
           |
182 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
    |
183 | 181, 182 | fge0iccico 38326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  
           |
184 | 180, 183 | sge0reval 38328 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  
Σ^                      |
185 | 184 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  
                Σ^      |
186 | 34 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  
Σ^      |
187 | 185, 186 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
                  |
188 | 187 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
189 | 3 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  
  |
190 | 39 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
           |
191 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
    |
192 | 190, 191 | fge0iccico 38326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  
           |
193 | 189, 192 | sge0reval 38328 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  
Σ^                      |
194 | 193 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  
                Σ^      |
195 | 41 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  
Σ^      |
196 | 194, 195 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
                  |
197 | 196 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
198 | 188, 197 | jca 541 |
. . . . . . . . . . . . . . . . . . . 20
                                             |
199 | 198 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
                     
        
                   |
200 | 178, 179,
199 | jca31 543 |
. . . . . . . . . . . . . . . . . 18
                        
               
        
                    |
201 | 180 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
     
      |
202 | 181 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
               |
203 | 182 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
   

   |
204 | 202, 203 | fge0iccico 38326 |
. . . . . . . . . . . . . . . . . . . . . 22
     
               |
205 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
     
        |
206 | 158 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
     
        |
207 | 201, 204,
205, 206 | fsumlesge0 38333 |
. . . . . . . . . . . . . . . . . . . . 21
     
             
Σ^      |
208 | 100 | sseli 3414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
209 | | fvres 5893 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
210 | 208, 209 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
211 | 210 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          |
212 | 211 | sumeq2dv 13846 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                        |
213 | 184 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
     
    Σ^                      |
214 | 212, 213 | breq12d 4408 |
. . . . . . . . . . . . . . . . . . . . 21
     
              
Σ^           
                   |
215 | 207, 214 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . 20
     
           
                  |
216 | 215 | adantlr 729 |
. . . . . . . . . . . . . . . . . . 19
                                        |
217 | 189 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
     
      |
218 | 190 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
               |
219 | 191 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
   

   |
220 | 218, 219 | fge0iccico 38326 |
. . . . . . . . . . . . . . . . . . . . . 22
     
               |
221 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
     
        |
222 | 166 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
     
        |
223 | 217, 220,
221, 222 | fsumlesge0 38333 |
. . . . . . . . . . . . . . . . . . . . 21
     
             
Σ^      |
224 | 103 | sseli 3414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
225 | | fvres 5893 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
227 | 226 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          |
228 | 227 | sumeq2dv 13846 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                        |
229 | 193 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
     
    Σ^                      |
230 | 228, 229 | breq12d 4408 |
. . . . . . . . . . . . . . . . . . . . 21
     
              
Σ^           
                   |
231 | 223, 230 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . 20
     
           
                  |
232 | 231 | adantllr 733 |
. . . . . . . . . . . . . . . . . . 19
                                        |
233 | 216, 232 | jca 541 |
. . . . . . . . . . . . . . . . . 18
                                       
             
        
   |
234 | | xle2add 11570 |
. . . . . . . . . . . . . . . . . 18
           
               
        
                           
                
             
        
                     
                          
        
    |
235 | 200, 233,
234 | sylc 61 |
. . . . . . . . . . . . . . . . 17
                                                             
        
   |
236 | 176, 235 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . 16
              
           
        
                      |
237 | 236 | 3adant3 1050 |
. . . . . . . . . . . . . . 15
                  
            
        
                      |
238 | 98, 237 | eqbrtrd 4416 |
. . . . . . . . . . . . . 14
                  
                          
        
   |
239 | 238 | 3exp 1230 |
. . . . . . . . . . . . 13
            
             
        
                        |
240 | 239 | rexlimdv 2870 |
. . . . . . . . . . . 12
               
   
                          
        
    |
241 | 240 | adantr 472 |
. . . . . . . . . . 11
                      
 
  
                              
        
    |
242 | 97, 241 | mpd 15 |
. . . . . . . . . 10
                                               
        
   |
243 | 242 | ralrimiva 2809 |
. . . . . . . . 9
          
 
               
        
                      |
244 | 147 | sge0rnre 38320 |
. . . . . . . . . . 11
        
         
  |
245 | 177 | a1i 11 |
. . . . . . . . . . 11
           |
246 | 244, 245 | sstrd 3428 |
. . . . . . . . . 10
        
         
  |
247 | 188, 197 | xaddcld 11612 |
. . . . . . . . . 10
                                   
        
   |
248 | | supxrleub 11637 |
. . . . . . . . . 10
           
       
        
                            
      
                          
        
 

 
               
        
                       |
249 | 246, 247,
248 | syl2anc 673 |
. . . . . . . . 9
                                                  
        
 

 
               
        
                       |
250 | 243, 249 | mpbird 240 |
. . . . . . . 8
                                                 
        
   |
251 | 14 | ad2antrr 740 |
. . . . . . . . 9
           |
252 | 251, 147 | sge0reval 38328 |
. . . . . . . 8
         Σ^                  |
253 | 184 | adantr 472 |
. . . . . . . . 9
         Σ^                      |
254 | 193 | adantlr 729 |
. . . . . . . . 9
         Σ^                      |
255 | 253, 254 | oveq12d 6326 |
. . . . . . . 8
          Σ^       Σ^            
        
                      |
256 | 250, 252,
255 | 3brtr4d 4426 |
. . . . . . 7
         Σ^   Σ^       Σ^       |
257 | 91, 256 | pm2.61dan 808 |
. . . . . 6
 
  
Σ^   Σ^       Σ^       |
258 | 69, 257 | pm2.61dan 808 |
. . . . 5
 Σ^   Σ^       Σ^       |
259 | 258 | adantr 472 |
. . . 4
 
Σ^   Σ^   Σ^       Σ^       |
260 | | pnfge 11455 |
. . . . . . 7
  Σ^       Σ^      Σ^       Σ^    
  |
261 | 42, 260 | syl 17 |
. . . . . 6
  Σ^       Σ^    
  |
262 | 261 | adantr 472 |
. . . . 5
 
Σ^    Σ^       Σ^    
  |
263 | | id 22 |
. . . . . . 7
 Σ^  Σ^    |
264 | 263 | eqcomd 2477 |
. . . . . 6
 Σ^  Σ^    |
265 | 264 | adantl 473 |
. . . . 5
 
Σ^  
Σ^    |
266 | 262, 265 | breqtrd 4420 |
. . . 4
 
Σ^    Σ^       Σ^    
Σ^    |
267 | 29, 43, 259, 266 | xrletrid 11475 |
. . 3
 
Σ^   Σ^   Σ^       Σ^       |
268 | 22, 27, 267 | syl2anc 673 |
. 2
 
Σ^   Σ^   Σ^       Σ^       |
269 | 21, 268 | pm2.61dan 808 |
1
 Σ^   Σ^       Σ^       |