Step | Hyp | Ref
| Expression |
1 | | snex 4641 |
. . . . 5
 
 |
2 | 1 | a1i 11 |
. . . 4
 
         |
3 | | sge0sn.2 |
. . . . 5
            |
4 | 3 | adantr 467 |
. . . 4
 
                |
5 | | id 22 |
. . . . . . 7
           |
6 | 5 | eqcomd 2457 |
. . . . . 6
           |
7 | 6 | adantl 468 |
. . . . 5
 
    
      |
8 | | ffun 5731 |
. . . . . . . 8
         
  |
9 | 3, 8 | syl 17 |
. . . . . . 7
   |
10 | 9 | adantr 467 |
. . . . . 6
 
    
  |
11 | | sge0sn.1 |
. . . . . . . . 9
   |
12 | | snidg 3994 |
. . . . . . . . 9
     |
13 | 11, 12 | syl 17 |
. . . . . . . 8
     |
14 | | fdm 5733 |
. . . . . . . . . 10
         
    |
15 | 3, 14 | syl 17 |
. . . . . . . . 9
     |
16 | 15 | eqcomd 2457 |
. . . . . . . 8
     |
17 | 13, 16 | eleqtrd 2531 |
. . . . . . 7
   |
18 | 17 | adantr 467 |
. . . . . 6
 
       |
19 | | fvelrn 6015 |
. . . . . 6
         |
20 | 10, 18, 19 | syl2anc 667 |
. . . . 5
 
           |
21 | 7, 20 | eqeltrd 2529 |
. . . 4
 
    
  |
22 | 2, 4, 21 | sge0pnfval 38215 |
. . 3
 
     Σ^    |
23 | | simpr 463 |
. . 3
 
           |
24 | 22, 23 | eqtr4d 2488 |
. 2
 
     Σ^        |
25 | 1 | a1i 11 |
. . . 4
 
      
  |
26 | 3 | adantr 467 |
. . . . 5
 
                |
27 | | elsni 3993 |
. . . . . . . . 9
            |
28 | 27 | eqcomd 2457 |
. . . . . . . 8
            |
29 | 28 | con3i 141 |
. . . . . . 7
             |
30 | 29 | adantl 468 |
. . . . . 6
 
             |
31 | 11, 3 | rnsnf 37458 |
. . . . . . . 8
         |
32 | 31 | eqcomd 2457 |
. . . . . . 7
         |
33 | 32 | adantr 467 |
. . . . . 6
 
             |
34 | 30, 33 | neleqtrd 2550 |
. . . . 5
 
       |
35 | 26, 34 | fge0iccico 38212 |
. . . 4
 
                |
36 | 25, 35 | sge0reval 38214 |
. . 3
 
     Σ^          
      
  |
37 | | sum0 13787 |
. . . . . . . 8
      |
38 | 37 | eqcomi 2460 |
. . . . . . 7
      |
39 | 38 | a1i 11 |
. . . . . 6
 
            |
40 | | nfcvd 2593 |
. . . . . . . 8
 
             |
41 | | nfv 1761 |
. . . . . . . 8
         |
42 | | fveq2 5865 |
. . . . . . . . 9
           |
43 | 42 | adantl 468 |
. . . . . . . 8
       
           |
44 | 11 | adantr 467 |
. . . . . . . 8
 
       |
45 | | rge0ssre 11740 |
. . . . . . . . . 10
    |
46 | | ax-resscn 9596 |
. . . . . . . . . 10
 |
47 | 45, 46 | sstri 3441 |
. . . . . . . . 9
    |
48 | 44, 12 | syl 17 |
. . . . . . . . . 10
 
         |
49 | 35, 48 | ffvelrnd 6023 |
. . . . . . . . 9
 
              |
50 | 47, 49 | sseldi 3430 |
. . . . . . . 8
 
           |
51 | 40, 41, 43, 44, 50 | sumsnd 37347 |
. . . . . . 7
 
                  |
52 | 51 | eqcomd 2457 |
. . . . . 6
 
           
      |
53 | 39, 52 | preq12d 4059 |
. . . . 5
 
                     
       |
54 | 53 | supeq1d 7960 |
. . . 4
 
                           
         |
55 | | xrltso 11440 |
. . . . . . . 8
 |
56 | 55 | a1i 11 |
. . . . . . 7
   |
57 | | 0xr 9687 |
. . . . . . . 8
 |
58 | 57 | a1i 11 |
. . . . . . 7
   |
59 | | iccssxr 11717 |
. . . . . . . 8
    |
60 | 3, 13 | ffvelrnd 6023 |
. . . . . . . 8
          |
61 | 59, 60 | sseldi 3430 |
. . . . . . 7
       |
62 | | suppr 7987 |
. . . . . . 7
                                |
63 | 56, 58, 61, 62 | syl3anc 1268 |
. . . . . 6
                           |
64 | | pnfxr 11412 |
. . . . . . . . . . 11
 |
65 | 64 | a1i 11 |
. . . . . . . . . 10
   |
66 | 58, 65, 60 | 3jca 1188 |
. . . . . . . . 9
 
          |
67 | | iccgelb 11691 |
. . . . . . . . 9
                |
68 | 66, 67 | syl 17 |
. . . . . . . 8

      |
69 | 58, 61 | xrlenltd 9700 |
. . . . . . . 8
         
   |
70 | 68, 69 | mpbid 214 |
. . . . . . 7
       |
71 | 70 | iffalsed 3892 |
. . . . . 6
                    |
72 | 63, 71 | eqtr2d 2486 |
. . . . 5
                  |
73 | 72 | adantr 467 |
. . . 4
 
                      |
74 | | pwsn 4192 |
. . . . . . . . . . . 12
  
      |
75 | 74 | ineq1i 3630 |
. . . . . . . . . . 11
       
  
  |
76 | | 0fin 7799 |
. . . . . . . . . . . . 13
 |
77 | | snfi 7650 |
. . . . . . . . . . . . 13
 
 |
78 | | prssi 4128 |
. . . . . . . . . . . . 13
 
 
        |
79 | 76, 77, 78 | mp2an 678 |
. . . . . . . . . . . 12
      |
80 | | df-ss 3418 |
. . . . . . . . . . . . 13
  
  
              |
81 | 80 | biimpi 198 |
. . . . . . . . . . . 12
  
  
     
        |
82 | 79, 81 | ax-mp 5 |
. . . . . . . . . . 11
  
  
       |
83 | 75, 82 | eqtri 2473 |
. . . . . . . . . 10
           |
84 | | mpteq1 4483 |
. . . . . . . . . 10
                             
       |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . 9
    
             
      |
86 | | 0ex 4535 |
. . . . . . . . . . . . 13
 |
87 | 86 | a1i 11 |
. . . . . . . . . . . 12
  |
88 | 1 | a1i 11 |
. . . . . . . . . . . 12
    |
89 | | sumex 13754 |
. . . . . . . . . . . . 13
      |
90 | 89 | a1i 11 |
. . . . . . . . . . . 12
       |
91 | | sumex 13754 |
. . . . . . . . . . . . 13
        |
92 | 91 | a1i 11 |
. . . . . . . . . . . 12
  
      |
93 | | sumeq1 13755 |
. . . . . . . . . . . . 13


    
      |
94 | 93 | adantl 468 |
. . . . . . . . . . . 12
 

    
      |
95 | | sumeq1 13755 |
. . . . . . . . . . . . 13
          
      |
96 | 95 | adantl 468 |
. . . . . . . . . . . 12
           
      |
97 | 87, 88, 90, 92, 94, 96 | fmptpr 6089 |
. . . . . . . . . . 11
              
        
             |
98 | 97 | trud 1453 |
. . . . . . . . . 10
         
   
               
      |
99 | 98 | eqcomi 2460 |
. . . . . . . . 9
      
                   
         |
100 | 85, 99 | eqtri 2473 |
. . . . . . . 8
    
                
   
          |
101 | 100 | rneqi 5061 |
. . . . . . 7
              
          
          |
102 | | rnpropg 5316 |
. . . . . . . 8
 
 

   
            
               
       |
103 | 86, 1, 102 | mp2an 678 |
. . . . . . 7
  
          
          
       
      |
104 | 101, 103 | eqtri 2473 |
. . . . . 6
             
       
      |
105 | 104 | supeq1i 7961 |
. . . . 5
        
      
   
       
        |
106 | 105 | a1i 11 |
. . . 4
 
                                
         |
107 | 54, 73, 106 | 3eqtr4d 2495 |
. . 3
 
                           |
108 | 36, 107 | eqtr4d 2488 |
. 2
 
     Σ^        |
109 | 24, 108 | pm2.61dan 800 |
1
 Σ^        |