Step | Hyp | Ref
| Expression |
1 | | iccssxr 11742 |
. . . . . . 7
    |
2 | | xrge0gsumle.g |
. . . . . . . . . 10
  ↾s      |
3 | | xrsbas 19061 |
. . . . . . . . . 10
      |
4 | 2, 3 | ressbas2 15258 |
. . . . . . . . 9
      
      |
5 | 1, 4 | ax-mp 5 |
. . . . . . . 8
        |
6 | | eqid 2471 |
. . . . . . . . . 10
  ↾s      
↾s      |
7 | 6 | xrge0subm 19086 |
. . . . . . . . 9
   SubMnd   ↾s       |
8 | | xrex 11322 |
. . . . . . . . . . . . 13
 |
9 | | difexg 4545 |
. . . . . . . . . . . . 13

     |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . 12
    |
11 | | simpl 464 |
. . . . . . . . . . . . . . 15
     |
12 | | ge0nemnf 11491 |
. . . . . . . . . . . . . . 15
     |
13 | 11, 12 | jca 541 |
. . . . . . . . . . . . . 14
       |
14 | | elxrge0 11767 |
. . . . . . . . . . . . . 14
   

   |
15 | | eldifsn 4088 |
. . . . . . . . . . . . . 14
   
    |
16 | 13, 14, 15 | 3imtr4i 274 |
. . . . . . . . . . . . 13
   

    |
17 | 16 | ssriv 3422 |
. . . . . . . . . . . 12
       |
18 | | ressabs 15266 |
. . . . . . . . . . . 12
  
            ↾s    
↾s      
↾s       |
19 | 10, 17, 18 | mp2an 686 |
. . . . . . . . . . 11
  
↾s     ↾s       ↾s  
   |
20 | 2, 19 | eqtr4i 2496 |
. . . . . . . . . 10
   ↾s    
↾s      |
21 | 6 | xrs10 19084 |
. . . . . . . . . 10
    
↾s       |
22 | 20, 21 | subm0 16681 |
. . . . . . . . 9
    SubMnd   ↾s            |
23 | 7, 22 | ax-mp 5 |
. . . . . . . 8
     |
24 | | xrge0cmn 19087 |
. . . . . . . . . 10
  ↾s     CMnd |
25 | 2, 24 | eqeltri 2545 |
. . . . . . . . 9
CMnd |
26 | 25 | a1i 11 |
. . . . . . . 8
 
    CMnd |
27 | | elfpw 7894 |
. . . . . . . . . 10
   
    |
28 | 27 | simprbi 471 |
. . . . . . . . 9
      |
29 | 28 | adantl 473 |
. . . . . . . 8
 
      |
30 | | xrge0gsumle.f |
. . . . . . . . 9
          |
31 | 27 | simplbi 467 |
. . . . . . . . 9
      |
32 | | fssres 5761 |
. . . . . . . . 9
                     |
33 | 30, 31, 32 | syl2an 485 |
. . . . . . . 8
 
               |
34 | | c0ex 9655 |
. . . . . . . . . 10
 |
35 | 34 | a1i 11 |
. . . . . . . . 9
 
      |
36 | 33, 29, 35 | fdmfifsupp 7911 |
. . . . . . . 8
 
      finSupp   |
37 | 5, 23, 26, 29, 33, 36 | gsumcl 17627 |
. . . . . . 7
 
     g         |
38 | 1, 37 | sseldi 3416 |
. . . . . 6
 
     g      |
39 | | eqid 2471 |
. . . . . 6
     g 
        g      |
40 | 38, 39 | fmptd 6061 |
. . . . 5
      g              |
41 | | frn 5747 |
. . . . 5
      g           
     g 
     |
42 | 40, 41 | syl 17 |
. . . 4
      g       |
43 | | 0ss 3766 |
. . . . . . 7
 |
44 | | 0fin 7817 |
. . . . . . 7
 |
45 | | elfpw 7894 |
. . . . . . 7
        |
46 | 43, 44, 45 | mpbir2an 934 |
. . . . . 6
    |
47 | | 0cn 9653 |
. . . . . 6
 |
48 | | reseq2 5106 |
. . . . . . . . . 10

  
   |
49 | | res0 5115 |
. . . . . . . . . 10
   |
50 | 48, 49 | syl6eq 2521 |
. . . . . . . . 9

    |
51 | 50 | oveq2d 6324 |
. . . . . . . 8

 g 
   g    |
52 | 23 | gsum0 16599 |
. . . . . . . 8
 g   |
53 | 51, 52 | syl6eq 2521 |
. . . . . . 7

 g 
    |
54 | 39, 53 | elrnmpt1s 5088 |
. . . . . 6
 
  
      g       |
55 | 46, 47, 54 | mp2an 686 |
. . . . 5
     g      |
56 | 55 | a1i 11 |
. . . 4
      g       |
57 | 42, 56 | sseldd 3419 |
. . 3
   |
58 | 25 | a1i 11 |
. . . . 5
 CMnd |
59 | | xrge0gsumle.b |
. . . . . . 7
      |
60 | | elfpw 7894 |
. . . . . . . 8
   
    |
61 | 60 | simprbi 471 |
. . . . . . 7
      |
62 | 59, 61 | syl 17 |
. . . . . 6
   |
63 | | diffi 7821 |
. . . . . 6
     |
64 | 62, 63 | syl 17 |
. . . . 5
     |
65 | 60 | simplbi 467 |
. . . . . . . 8
      |
66 | 59, 65 | syl 17 |
. . . . . . 7

  |
67 | 66 | ssdifssd 3560 |
. . . . . 6
  
  |
68 | 30, 67 | fssresd 5762 |
. . . . 5
                |
69 | 34 | a1i 11 |
. . . . . 6
   |
70 | 68, 64, 69 | fdmfifsupp 7911 |
. . . . 5
     finSupp   |
71 | 5, 23, 58, 64, 68, 70 | gsumcl 17627 |
. . . 4
  g           |
72 | 1, 71 | sseldi 3416 |
. . 3
  g        |
73 | | xrge0gsumle.c |
. . . . . 6

  |
74 | | ssfi 7810 |
. . . . . 6
  
  |
75 | 62, 73, 74 | syl2anc 673 |
. . . . 5
   |
76 | 73, 66 | sstrd 3428 |
. . . . . 6

  |
77 | 30, 76 | fssresd 5762 |
. . . . 5
            |
78 | 77, 75, 69 | fdmfifsupp 7911 |
. . . . 5
   finSupp   |
79 | 5, 23, 58, 75, 77, 78 | gsumcl 17627 |
. . . 4
  g         |
80 | 1, 79 | sseldi 3416 |
. . 3
  g      |
81 | | elxrge0 11767 |
. . . . 5
  g        
  g       g         |
82 | 81 | simprbi 471 |
. . . 4
  g        
 g 
      |
83 | 71, 82 | syl 17 |
. . 3

 g 
      |
84 | | xleadd2a 11565 |
. . 3
    g       g    
 g 
       g       
  g        g         |
85 | 57, 72, 80, 83, 84 | syl31anc 1295 |
. 2
   g          g        g         |
86 | | xaddid1 11556 |
. . 3
  g      g         g 
    |
87 | 80, 86 | syl 17 |
. 2
   g         g      |
88 | | ovex 6336 |
. . . . 5
    |
89 | | xrsadd 19062 |
. . . . . 6
      |
90 | 2, 89 | ressplusg 15317 |
. . . . 5
   
      |
91 | 88, 90 | ax-mp 5 |
. . . 4
     |
92 | 30, 66 | fssresd 5762 |
. . . 4
            |
93 | 92, 62, 69 | fdmfifsupp 7911 |
. . . 4
   finSupp   |
94 | | disjdif 3830 |
. . . . 5
     |
95 | 94 | a1i 11 |
. . . 4
       |
96 | | undif2 3834 |
. . . . 5
       |
97 | | ssequn1 3595 |
. . . . . 6

    |
98 | 73, 97 | sylib 201 |
. . . . 5
     |
99 | 96, 98 | syl5req 2518 |
. . . 4
       |
100 | 5, 23, 91, 58, 59, 92, 93, 95, 99 | gsumsplit 17639 |
. . 3
  g      g          g           |
101 | 73 | resabs1d 5140 |
. . . . 5
         |
102 | 101 | oveq2d 6324 |
. . . 4
  g       g 
    |
103 | | difss 3549 |
. . . . . 6
   |
104 | | resabs1 5139 |
. . . . . 6
         
     |
105 | 103, 104 | mp1i 13 |
. . . . 5
        
    |
106 | 105 | oveq2d 6324 |
. . . 4
  g         g 
      |
107 | 102, 106 | oveq12d 6326 |
. . 3
   g  
       g  
        g 
      g         |
108 | 100, 107 | eqtr2d 2506 |
. 2
   g        g        g      |
109 | 85, 87, 108 | 3brtr3d 4425 |
1
  g   
 g 
    |