Step | Hyp | Ref
| Expression |
1 | | eqid 2451 |
. . . 4
       g              g      
 |
2 | 1 | a1i 11 |
. . 3
        g      
       g      
  |
3 | | xrltso 11440 |
. . . . . 6
 |
4 | 3 | supex 7977 |
. . . . 5
       g        |
5 | 4 | a1i 11 |
. . . 4
        g      
  |
6 | | elsncg 3991 |
. . . 4
        g 
             g               g               g      
       g      
   |
7 | 5, 6 | syl 17 |
. . 3
         g               g               g      
       g      
   |
8 | 2, 7 | mpbird 236 |
. 2
        g      
        g          |
9 | | sge0tsms.x |
. . . . . . 7
   |
10 | 9 | adantr 467 |
. . . . . 6
 

  |
11 | | sge0tsms.f |
. . . . . . 7
          |
12 | 11 | adantr 467 |
. . . . . 6
 

         |
13 | | simpr 463 |
. . . . . 6
 

  |
14 | 10, 12, 13 | sge0pnfval 38215 |
. . . . 5
 

Σ^    |
15 | | ffn 5728 |
. . . . . . . . . 10
       
  |
16 | 11, 15 | syl 17 |
. . . . . . . . 9
   |
17 | 16 | adantr 467 |
. . . . . . . 8
 

  |
18 | | fvelrnb 5912 |
. . . . . . . 8


       |
19 | 17, 18 | syl 17 |
. . . . . . 7
 


       |
20 | 13, 19 | mpbid 214 |
. . . . . 6
 


      |
21 | | iccssxr 11717 |
. . . . . . . . . . . . . 14
    |
22 | | sge0tsms.g |
. . . . . . . . . . . . . . 15
  ↾s      |
23 | | simpr 463 |
. . . . . . . . . . . . . . 15
 
         |
24 | 11 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
             |
25 | | elinel1 3619 |
. . . . . . . . . . . . . . . . . 18
       |
26 | | elpwi 3960 |
. . . . . . . . . . . . . . . . . 18
    |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . 17
      |
28 | 27 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
      |
29 | | fssres 5749 |
. . . . . . . . . . . . . . . 16
                     |
30 | 24, 28, 29 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
               |
31 | | elinel2 3620 |
. . . . . . . . . . . . . . . . 17
      |
32 | 31 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
      |
33 | | 0red 9644 |
. . . . . . . . . . . . . . . 16
 
      |
34 | 30, 32, 33 | fdmfifsupp 7893 |
. . . . . . . . . . . . . . 15
 
      finSupp   |
35 | 22, 23, 30, 34 | gsumge0cl 38213 |
. . . . . . . . . . . . . 14
 
     g         |
36 | 21, 35 | sseldi 3430 |
. . . . . . . . . . . . 13
 
     g      |
37 | 36 | ralrimiva 2802 |
. . . . . . . . . . . 12
       g      |
38 | 37 | 3ad2ant1 1029 |
. . . . . . . . . . 11
 
           g      |
39 | | eqid 2451 |
. . . . . . . . . . . 12
     g 
        g      |
40 | 39 | rnmptss 6052 |
. . . . . . . . . . 11
 
     g         g       |
41 | 38, 40 | syl 17 |
. . . . . . . . . 10
 
    
     g       |
42 | | snelpwi 4645 |
. . . . . . . . . . . . . 14
      |
43 | | snfi 7650 |
. . . . . . . . . . . . . . 15
   |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
     |
45 | 42, 44 | elind 3618 |
. . . . . . . . . . . . 13
        |
46 | 45 | 3ad2ant2 1030 |
. . . . . . . . . . . 12
 
            |
47 | 11 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
          |
48 | | snssi 4116 |
. . . . . . . . . . . . . . . . . . 19
  
  |
49 | 48 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
  
  |
50 | 47, 49 | fssresd 5750 |
. . . . . . . . . . . . . . . . 17
 
                |
51 | 50 | feqmptd 5918 |
. . . . . . . . . . . . . . . 16
 
                   |
52 | | fvres 5879 |
. . . . . . . . . . . . . . . . . 18
                 |
53 | 52 | mpteq2ia 4485 |
. . . . . . . . . . . . . . . . 17
                     |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
                       |
55 | 51, 54 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
 
               |
56 | 55 | oveq2d 6306 |
. . . . . . . . . . . . . 14
 
  g       g            |
57 | 56 | 3adant3 1028 |
. . . . . . . . . . . . 13
 
      g       g 
          |
58 | | xrge0cmn 19010 |
. . . . . . . . . . . . . . . . 17
  ↾s     CMnd |
59 | 22, 58 | eqeltri 2525 |
. . . . . . . . . . . . . . . 16
CMnd |
60 | | cmnmnd 17445 |
. . . . . . . . . . . . . . . 16
 CMnd   |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . . . 15
 |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
 
       |
63 | | simp2 1009 |
. . . . . . . . . . . . . 14
 
       |
64 | 11 | ffvelrnda 6022 |
. . . . . . . . . . . . . . 15
 
          |
65 | 64 | 3adant3 1028 |
. . . . . . . . . . . . . 14
 
              |
66 | | df-ss 3418 |
. . . . . . . . . . . . . . . . . 18
       
      |
67 | 21, 66 | mpbi 212 |
. . . . . . . . . . . . . . . . 17
         |
68 | 67 | eqcomi 2460 |
. . . . . . . . . . . . . . . 16
      
  |
69 | | ovex 6318 |
. . . . . . . . . . . . . . . . 17
    |
70 | | xrsbas 18984 |
. . . . . . . . . . . . . . . . . 18
      |
71 | 22, 70 | ressbas 15179 |
. . . . . . . . . . . . . . . . 17
   
  
        |
72 | 69, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
          |
73 | 68, 72 | eqtri 2473 |
. . . . . . . . . . . . . . 15
        |
74 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
75 | 73, 74 | gsumsn 17587 |
. . . . . . . . . . . . . 14
 
         g                |
76 | 62, 63, 65, 75 | syl3anc 1268 |
. . . . . . . . . . . . 13
 
      g                |
77 | | simp3 1010 |
. . . . . . . . . . . . 13
 
           |
78 | 57, 76, 77 | 3eqtrrd 2490 |
. . . . . . . . . . . 12
 
    
 g        |
79 | | reseq2 5100 |
. . . . . . . . . . . . . . 15
     
     |
80 | 79 | oveq2d 6306 |
. . . . . . . . . . . . . 14
    g     g        |
81 | 80 | eqeq2d 2461 |
. . . . . . . . . . . . 13
   
g   
 g         |
82 | 81 | rspcev 3150 |
. . . . . . . . . . . 12
        g            g 
    |
83 | 46, 78, 82 | syl2anc 667 |
. . . . . . . . . . 11
 
          g 
    |
84 | | pnfxr 11412 |
. . . . . . . . . . . . 13
 |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
 
    
  |
86 | 39 | elrnmpt 5081 |
. . . . . . . . . . . 12
     g     
 

 g 
     |
87 | 85, 86 | syl 17 |
. . . . . . . . . . 11
 
          g     
 

 g 
     |
88 | 83, 87 | mpbird 236 |
. . . . . . . . . 10
 
    

 
  g       |
89 | | supxrpnf 11604 |
. . . . . . . . . 10
       g          g     
       g         |
90 | 41, 88, 89 | syl2anc 667 |
. . . . . . . . 9
 
            g      
  |
91 | 90 | 3exp 1207 |
. . . . . . . 8
              g      
    |
92 | 91 | adantr 467 |
. . . . . . 7
 


            g           |
93 | 92 | rexlimdv 2877 |
. . . . . 6
 

 
   
       g          |
94 | 20, 93 | mpd 15 |
. . . . 5
 

       g         |
95 | 14, 94 | eqtr4d 2488 |
. . . 4
 

Σ^         g         |
96 | 9 | adantr 467 |
. . . . . 6
 
   |
97 | 11 | adantr 467 |
. . . . . . 7
 
          |
98 | | simpr 463 |
. . . . . . 7
 
   |
99 | 97, 98 | fge0iccico 38212 |
. . . . . 6
 
          |
100 | 96, 99 | sge0reval 38214 |
. . . . 5
 
 Σ^                  |
101 | 24, 28 | feqresmpt 5919 |
. . . . . . . . . . 11
 
              |
102 | 101 | adantlr 721 |
. . . . . . . . . 10
                  |
103 | 102 | oveq2d 6306 |
. . . . . . . . 9
         g     g          |
104 | 22 | fveq2i 5868 |
. . . . . . . . . . 11
       ↾s       |
105 | | eqid 2451 |
. . . . . . . . . . . . . 14
  ↾s      
↾s      |
106 | | xrsadd 18985 |
. . . . . . . . . . . . . 14
      |
107 | 105, 106 | ressplusg 15239 |
. . . . . . . . . . . . 13
   
    
↾s        |
108 | 69, 107 | ax-mp 5 |
. . . . . . . . . . . 12
    
↾s       |
109 | 108 | eqcomi 2460 |
. . . . . . . . . . 11
    ↾s        |
110 | 104, 109 | eqtr2i 2474 |
. . . . . . . . . 10
     |
111 | 22 | oveq1i 6300 |
. . . . . . . . . . 11
 ↾s       
↾s    
↾s      |
112 | | icossicc 11721 |
. . . . . . . . . . . . 13
       |
113 | 69, 112 | pm3.2i 457 |
. . . . . . . . . . . 12
            |
114 | | ressabs 15188 |
. . . . . . . . . . . 12
    
 
       
↾s    
↾s      
↾s       |
115 | 113, 114 | ax-mp 5 |
. . . . . . . . . . 11
  
↾s    
↾s      
↾s      |
116 | 111, 115 | eqtr2i 2474 |
. . . . . . . . . 10
  ↾s      ↾s      |
117 | 59 | elexi 3055 |
. . . . . . . . . . 11
 |
118 | 117 | a1i 11 |
. . . . . . . . . 10
          |
119 | | simpr 463 |
. . . . . . . . . 10
             |
120 | 112 | a1i 11 |
. . . . . . . . . 10
         
      |
121 | | 0xr 9687 |
. . . . . . . . . . . . 13
 |
122 | 121 | a1i 11 |
. . . . . . . . . . . 12
    
       |
123 | 84 | a1i 11 |
. . . . . . . . . . . 12
    
       |
124 | 97 | ad2antrr 732 |
. . . . . . . . . . . . . 14
    
              |
125 | 27 | sselda 3432 |
. . . . . . . . . . . . . . 15
    

  |
126 | 125 | adantll 720 |
. . . . . . . . . . . . . 14
    
       |
127 | 124, 126 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
    
              |
128 | 21, 127 | sseldi 3430 |
. . . . . . . . . . . 12
    
           |
129 | | iccgelb 11691 |
. . . . . . . . . . . . 13
                |
130 | 122, 123,
127, 129 | syl3anc 1268 |
. . . . . . . . . . . 12
    
           |
131 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
           |
132 | 131 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . 19
           |
133 | 132 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
   
    
    
      |
134 | | ffun 5731 |
. . . . . . . . . . . . . . . . . . . . . 22
          |
135 | 11, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
   |
136 | 135 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
          |
137 | 23, 125 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . 21
          |
138 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          |
139 | 11, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
140 | 139 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
141 | 140 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . 21
          |
142 | 137, 141 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . 20
          |
143 | | fvelrn 6015 |
. . . . . . . . . . . . . . . . . . . 20
         |
144 | 136, 142,
143 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
              |
145 | 144 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   
    
           |
146 | 133, 145 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . 17
   
    
    
  |
147 | 146 | adantlllr 37361 |
. . . . . . . . . . . . . . . 16
    
             |
148 | 98 | ad3antrrr 736 |
. . . . . . . . . . . . . . . 16
    
             |
149 | 147, 148 | pm2.65da 580 |
. . . . . . . . . . . . . . 15
    
           |
150 | 149 | neqned 2631 |
. . . . . . . . . . . . . 14
    
           |
151 | | ge0xrre 37633 |
. . . . . . . . . . . . . 14
                    |
152 | 127, 150,
151 | syl2anc 667 |
. . . . . . . . . . . . 13
    
           |
153 | 152 | ltpnfd 11423 |
. . . . . . . . . . . 12
    
           |
154 | 122, 123,
128, 130, 153 | elicod 11685 |
. . . . . . . . . . 11
    
              |
155 | | eqid 2451 |
. . . . . . . . . . 11
             |
156 | 154, 155 | fmptd 6046 |
. . . . . . . . . 10
                       |
157 | | 0e0icopnf 11742 |
. . . . . . . . . . 11
    |
158 | 157 | a1i 11 |
. . . . . . . . . 10
             |
159 | 21 | sseli 3428 |
. . . . . . . . . . . 12
   
  |
160 | | xaddid2 11533 |
. . . . . . . . . . . . 13

       |
161 | | xaddid1 11532 |
. . . . . . . . . . . . 13

       |
162 | 160, 161 | jca 535 |
. . . . . . . . . . . 12

              |
163 | 159, 162 | syl 17 |
. . . . . . . . . . 11
   
              |
164 | 163 | adantl 468 |
. . . . . . . . . 10
    
                      |
165 | 73, 110, 116, 118, 119, 120, 156, 158, 164 | gsumress 16519 |
. . . . . . . . 9
         g           ↾s  
  g          |
166 | | rege0subm 19024 |
. . . . . . . . . . . . 13
   SubMnd ℂfld |
167 | 166 | a1i 11 |
. . . . . . . . . . . 12
         
 SubMnd ℂfld  |
168 | | eqid 2451 |
. . . . . . . . . . . 12
ℂfld
↾s     ℂfld ↾s      |
169 | 119, 167,
156, 168 | gsumsubm 16620 |
. . . . . . . . . . 11
        ℂfld g         ℂfld ↾s     g          |
170 | | eqidd 2452 |
. . . . . . . . . . 11
         ℂfld ↾s  
  g         ℂfld ↾s     g          |
171 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
172 | 171 | mptex 6136 |
. . . . . . . . . . . . 13
       |
173 | 172 | a1i 11 |
. . . . . . . . . . . 12
                |
174 | | ovex 6318 |
. . . . . . . . . . . . 13
ℂfld
↾s      |
175 | 174 | a1i 11 |
. . . . . . . . . . . 12
        ℂfld ↾s
      |
176 | | ovex 6318 |
. . . . . . . . . . . . 13
  ↾s      |
177 | 176 | a1i 11 |
. . . . . . . . . . . 12
         
↾s       |
178 | | rge0ssre 11740 |
. . . . . . . . . . . . . . . . 17
    |
179 | | ax-resscn 9596 |
. . . . . . . . . . . . . . . . 17
 |
180 | 178, 179 | sstri 3441 |
. . . . . . . . . . . . . . . 16
    |
181 | | cnfldbas 18974 |
. . . . . . . . . . . . . . . . 17
  ℂfld |
182 | 168, 181 | ressbas2 15180 |
. . . . . . . . . . . . . . . 16
   
      ℂfld ↾s
       |
183 | 180, 182 | ax-mp 5 |
. . . . . . . . . . . . . . 15
      ℂfld ↾s
      |
184 | 183 | eqcomi 2460 |
. . . . . . . . . . . . . 14
   ℂfld ↾s          |
185 | 112, 21 | sstri 3441 |
. . . . . . . . . . . . . . 15
    |
186 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
  ↾s      
↾s      |
187 | 186, 70 | ressbas2 15180 |
. . . . . . . . . . . . . . 15
      
     ↾s  
     |
188 | 185, 187 | ax-mp 5 |
. . . . . . . . . . . . . 14
       
↾s       |
189 | 184, 188 | eqtri 2473 |
. . . . . . . . . . . . 13
   ℂfld ↾s           ↾s       |
190 | 189 | a1i 11 |
. . . . . . . . . . . 12
           ℂfld ↾s           ↾s        |
191 | | rge0srg 19038 |
. . . . . . . . . . . . . . 15
ℂfld
↾s     SRing |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . 14
     ℂfld ↾s         ℂfld ↾s
      ℂfld ↾s
    SRing |
193 | | simpl 459 |
. . . . . . . . . . . . . 14
     ℂfld ↾s         ℂfld ↾s
         ℂfld ↾s
       |
194 | | simpr 463 |
. . . . . . . . . . . . . 14
     ℂfld ↾s         ℂfld ↾s
         ℂfld ↾s
       |
195 | | eqid 2451 |
. . . . . . . . . . . . . . 15
   ℂfld ↾s         ℂfld
↾s       |
196 | | eqid 2451 |
. . . . . . . . . . . . . . 15
  ℂfld ↾s        ℂfld
↾s       |
197 | 195, 196 | srgacl 17757 |
. . . . . . . . . . . . . 14
  ℂfld ↾s     SRing
   ℂfld ↾s
        ℂfld ↾s
          ℂfld ↾s
          ℂfld ↾s
       |
198 | 192, 193,
194, 197 | syl3anc 1268 |
. . . . . . . . . . . . 13
     ℂfld ↾s         ℂfld ↾s
          ℂfld ↾s
          ℂfld ↾s
       |
199 | 198 | adantl 468 |
. . . . . . . . . . . 12
    
        ℂfld ↾s         ℂfld ↾s
           ℂfld ↾s           ℂfld ↾s
       |
200 | 178 | a1i 11 |
. . . . . . . . . . . . . . . 16
    ℂfld ↾s
    
     |
201 | | id 22 |
. . . . . . . . . . . . . . . . 17
    ℂfld ↾s
    
   ℂfld
↾s        |
202 | 201, 184 | syl6eleq 2539 |
. . . . . . . . . . . . . . . 16
    ℂfld ↾s
    
     |
203 | 200, 202 | sseldd 3433 |
. . . . . . . . . . . . . . 15
    ℂfld ↾s
    
  |
204 | 203 | adantr 467 |
. . . . . . . . . . . . . 14
     ℂfld ↾s         ℂfld ↾s
        |
205 | 178 | a1i 11 |
. . . . . . . . . . . . . . . 16
    ℂfld ↾s
    
     |
206 | | id 22 |
. . . . . . . . . . . . . . . . 17
    ℂfld ↾s
    
   ℂfld
↾s        |
207 | 206, 184 | syl6eleq 2539 |
. . . . . . . . . . . . . . . 16
    ℂfld ↾s
    
     |
208 | 205, 207 | sseldd 3433 |
. . . . . . . . . . . . . . 15
    ℂfld ↾s
    
  |
209 | 208 | adantl 468 |
. . . . . . . . . . . . . 14
     ℂfld ↾s         ℂfld ↾s
        |
210 | | rexadd 11525 |
. . . . . . . . . . . . . . . 16
 
          |
211 | 210 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
 
          |
212 | 166 | elexi 3055 |
. . . . . . . . . . . . . . . . . . . 20
    |
213 | | cnfldadd 18975 |
. . . . . . . . . . . . . . . . . . . . 21
 ℂfld |
214 | 168, 213 | ressplusg 15239 |
. . . . . . . . . . . . . . . . . . . 20
   
  ℂfld
↾s        |
215 | 212, 214 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
  ℂfld
↾s       |
216 | 215, 213 | eqtr3i 2475 |
. . . . . . . . . . . . . . . . . 18
  ℂfld ↾s       ℂfld |
217 | 216, 213 | eqtr4i 2476 |
. . . . . . . . . . . . . . . . 17
  ℂfld ↾s       |
218 | 217 | oveqi 6303 |
. . . . . . . . . . . . . . . 16
    ℂfld ↾s
          |
219 | 218 | a1i 11 |
. . . . . . . . . . . . . . 15
 
     ℂfld ↾s            |
220 | 186, 106 | ressplusg 15239 |
. . . . . . . . . . . . . . . . . . 19
   
    
↾s        |
221 | 212, 220 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
    
↾s       |
222 | 221 | eqcomi 2460 |
. . . . . . . . . . . . . . . . 17
    ↾s        |
223 | 222 | oveqi 6303 |
. . . . . . . . . . . . . . . 16
     
↾s              |
224 | 223 | a1i 11 |
. . . . . . . . . . . . . . 15
 
       ↾s               |
225 | 211, 219,
224 | 3eqtr4d 2495 |
. . . . . . . . . . . . . 14
 
     ℂfld ↾s              ↾s          |
226 | 204, 209,
225 | syl2anc 667 |
. . . . . . . . . . . . 13
     ℂfld ↾s         ℂfld ↾s
          ℂfld ↾s
             ↾s          |
227 | 226 | adantl 468 |
. . . . . . . . . . . 12
    
        ℂfld ↾s         ℂfld ↾s
           ℂfld ↾s              ↾s          |
228 | | funmpt 5618 |
. . . . . . . . . . . . 13
       |
229 | 228 | a1i 11 |
. . . . . . . . . . . 12
                |
230 | 154, 183 | syl6eleq 2539 |
. . . . . . . . . . . . . 14
    
            ℂfld ↾s
       |
231 | 230 | ralrimiva 2802 |
. . . . . . . . . . . . 13
        
       ℂfld
↾s        |
232 | 155 | rnmptss 6052 |
. . . . . . . . . . . . 13
 
       ℂfld ↾s
    
         ℂfld ↾s
       |
233 | 231, 232 | syl 17 |
. . . . . . . . . . . 12
                 ℂfld ↾s        |
234 | 173, 175,
177, 190, 199, 227, 229, 233 | gsumpropd2 16517 |
. . . . . . . . . . 11
         ℂfld ↾s  
  g           ↾s  
  g          |
235 | 169, 170,
234 | 3eqtrd 2489 |
. . . . . . . . . 10
        ℂfld g           ↾s  
  g          |
236 | 31 | adantl 468 |
. . . . . . . . . . 11
          |
237 | 152 | recnd 9669 |
. . . . . . . . . . 11
    
           |
238 | 236, 237 | gsumfsum 19034 |
. . . . . . . . . 10
        ℂfld g               |
239 | 235, 238 | eqtr3d 2487 |
. . . . . . . . 9
          
↾s     g               |
240 | 103, 165,
239 | 3eqtrrd 2490 |
. . . . . . . 8
        
     g      |
241 | 240 | mpteq2dva 4489 |
. . . . . . 7
 
                g 
     |
242 | 241 | rneqd 5062 |
. . . . . 6
 
 
 
            g       |
243 | 242 | supeq1d 7960 |
. . . . 5
 
                      g         |
244 | 100, 243 | eqtrd 2485 |
. . . 4
 
 Σ^         g         |
245 | 95, 244 | pm2.61dan 800 |
. . 3
 Σ^         g         |
246 | 22, 9, 11, 1 | xrge0tsms 21852 |
. . 3
  tsums          g          |
247 | 245, 246 | eleq12d 2523 |
. 2
  Σ^   tsums 
       g               g           |
248 | 8, 247 | mpbird 236 |
1
 Σ^   tsums    |