Step | Hyp | Ref
| Expression |
1 | | gsumzadd.g |
. . . . . 6
   |
2 | | gsumzadd.b |
. . . . . . . 8
     |
3 | | gsumzadd.0 |
. . . . . . . 8
     |
4 | 2, 3 | mndidcl 16547 |
. . . . . . 7
   |
5 | 1, 4 | syl 17 |
. . . . . 6
   |
6 | | gsumzadd.p |
. . . . . . 7
    |
7 | 2, 6, 3 | mndlid 16550 |
. . . . . 6
  
 |
8 | 1, 5, 7 | syl2anc 666 |
. . . . 5

 |
9 | 8 | adantr 467 |
. . . 4
 

 |
10 | | gsumzaddlem.f |
. . . . . . . 8
       |
11 | | gsumzadd.a |
. . . . . . . 8
   |
12 | | fvex 5873 |
. . . . . . . . . 10
     |
13 | 3, 12 | eqeltri 2524 |
. . . . . . . . 9
 |
14 | 13 | a1i 11 |
. . . . . . . 8
   |
15 | | gsumzaddlem.h |
. . . . . . . . . . 11
       |
16 | | fex 6136 |
. . . . . . . . . . 11
     
   |
17 | 15, 11, 16 | syl2anc 666 |
. . . . . . . . . 10
   |
18 | 17 | suppun 6932 |
. . . . . . . . 9
  supp    supp
  |
19 | | gsumzaddlem.w |
. . . . . . . . 9
   supp
 |
20 | 18, 19 | syl6sseqr 3478 |
. . . . . . . 8
  supp   |
21 | 10, 11, 14, 20 | gsumcllem 17535 |
. . . . . . 7
 


  |
22 | 21 | oveq2d 6304 |
. . . . . 6
 

 g   g 
   |
23 | 3 | gsumz 16614 |
. . . . . . . 8
 
  g    |
24 | 1, 11, 23 | syl2anc 666 |
. . . . . . 7
  g    |
25 | 24 | adantr 467 |
. . . . . 6
 

 g    |
26 | 22, 25 | eqtrd 2484 |
. . . . 5
 

 g   |
27 | | fex 6136 |
. . . . . . . . . . . 12
     
   |
28 | 10, 11, 27 | syl2anc 666 |
. . . . . . . . . . 11
   |
29 | 28 | suppun 6932 |
. . . . . . . . . 10
  supp    supp
  |
30 | | uncom 3577 |
. . . . . . . . . . 11
     |
31 | 30 | oveq1i 6298 |
. . . . . . . . . 10
   supp    supp
 |
32 | 29, 31 | syl6sseqr 3478 |
. . . . . . . . 9
  supp    supp
  |
33 | 32, 19 | syl6sseqr 3478 |
. . . . . . . 8
  supp   |
34 | 15, 11, 14, 33 | gsumcllem 17535 |
. . . . . . 7
 


  |
35 | 34 | oveq2d 6304 |
. . . . . 6
 

 g   g 
   |
36 | 35, 25 | eqtrd 2484 |
. . . . 5
 

 g   |
37 | 26, 36 | oveq12d 6306 |
. . . 4
 

  g   g     |
38 | 11 | adantr 467 |
. . . . . . . 8
 

  |
39 | 5 | ad2antrr 731 |
. . . . . . . 8
       |
40 | 38, 39, 39, 21, 34 | offval2 6545 |
. . . . . . 7
 

 
     |
41 | 9 | mpteq2dv 4489 |
. . . . . . 7
 


    |
42 | 40, 41 | eqtrd 2484 |
. . . . . 6
 

 
 
  |
43 | 42 | oveq2d 6304 |
. . . . 5
 

 g      g     |
44 | 43, 25 | eqtrd 2484 |
. . . 4
 

 g      |
45 | 9, 37, 44 | 3eqtr4rd 2495 |
. . 3
 

 g       g   g     |
46 | 45 | ex 436 |
. 2
   g       g   g      |
47 | 1 | adantr 467 |
. . . . . . . . 9
 
                     |
48 | 2, 6 | mndcl 16538 |
. . . . . . . . . 10
 
     |
49 | 48 | 3expb 1208 |
. . . . . . . . 9
  
  
   |
50 | 47, 49 | sylan 474 |
. . . . . . . 8
                      
  
   |
51 | 50 | caovclg 6458 |
. . . . . . 7
                      
  
   |
52 | | simprl 763 |
. . . . . . . 8
 
                         |
53 | | nnuz 11191 |
. . . . . . . 8
     |
54 | 52, 53 | syl6eleq 2538 |
. . . . . . 7
 
                             |
55 | 10 | adantr 467 |
. . . . . . . . 9
 
                         |
56 | | f1of1 5811 |
. . . . . . . . . . . 12
            
              |
57 | 56 | ad2antll 734 |
. . . . . . . . . . 11
 
                                 |
58 | | suppssdm 6924 |
. . . . . . . . . . . . . 14
   supp 
  |
59 | 58 | a1i 11 |
. . . . . . . . . . . . 13
    supp
    |
60 | 19 | a1i 11 |
. . . . . . . . . . . . 13
    supp   |
61 | | dmun 5040 |
. . . . . . . . . . . . . 14

    |
62 | | fdm 5731 |
. . . . . . . . . . . . . . . . 17
       |
63 | 10, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
64 | | fdm 5731 |
. . . . . . . . . . . . . . . . 17
       |
65 | 15, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
66 | 63, 65 | uneq12d 3588 |
. . . . . . . . . . . . . . 15
       |
67 | | unidm 3576 |
. . . . . . . . . . . . . . 15
   |
68 | 66, 67 | syl6eq 2500 |
. . . . . . . . . . . . . 14
     |
69 | 61, 68 | syl5req 2497 |
. . . . . . . . . . . . 13
 
   |
70 | 59, 60, 69 | 3sstr4d 3474 |
. . . . . . . . . . . 12

  |
71 | 70 | adantr 467 |
. . . . . . . . . . 11
 
                     |
72 | | f1ss 5782 |
. . . . . . . . . . 11
                             |
73 | 57, 71, 72 | syl2anc 666 |
. . . . . . . . . 10
 
                                 |
74 | | f1f 5777 |
. . . . . . . . . 10
                           |
75 | 73, 74 | syl 17 |
. . . . . . . . 9
 
                                 |
76 | | fco 5737 |
. . . . . . . . 9
                                   |
77 | 55, 75, 76 | syl2anc 666 |
. . . . . . . 8
 
                   
               |
78 | 77 | ffvelrnda 6020 |
. . . . . . 7
                     
                 |
79 | 15 | adantr 467 |
. . . . . . . . 9
 
                         |
80 | | fco 5737 |
. . . . . . . . 9
                                   |
81 | 79, 75, 80 | syl2anc 666 |
. . . . . . . 8
 
                   
               |
82 | 81 | ffvelrnda 6020 |
. . . . . . 7
                     
                 |
83 | | ffn 5726 |
. . . . . . . . . . . 12
    
  |
84 | 55, 83 | syl 17 |
. . . . . . . . . . 11
 
                     |
85 | | ffn 5726 |
. . . . . . . . . . . 12
    
  |
86 | 79, 85 | syl 17 |
. . . . . . . . . . 11
 
                     |
87 | 11 | adantr 467 |
. . . . . . . . . . 11
 
                     |
88 | | ovex 6316 |
. . . . . . . . . . . 12
         |
89 | 88 | a1i 11 |
. . . . . . . . . . 11
 
                             |
90 | | inidm 3640 |
. . . . . . . . . . 11
   |
91 | 84, 86, 75, 87, 87, 89, 90 | ofco 6548 |
. . . . . . . . . 10
 
                            
    |
92 | 91 | fveq1d 5865 |
. . . . . . . . 9
 
                                 
       |
93 | 92 | adantr 467 |
. . . . . . . 8
                     
                               |
94 | | fnfco 5746 |
. . . . . . . . . 10
                           |
95 | 84, 75, 94 | syl2anc 666 |
. . . . . . . . 9
 
                   
           |
96 | | fnfco 5746 |
. . . . . . . . . 10
                           |
97 | 86, 75, 96 | syl2anc 666 |
. . . . . . . . 9
 
                   
           |
98 | | inidm 3640 |
. . . . . . . . 9
                           |
99 | | eqidd 2451 |
. . . . . . . . 9
                     
                       |
100 | | eqidd 2451 |
. . . . . . . . 9
                     
                       |
101 | 95, 97, 89, 89, 98, 99, 100 | ofval 6537 |
. . . . . . . 8
                     
                                    |
102 | 93, 101 | eqtrd 2484 |
. . . . . . 7
                     
                                  |
103 | 1 | ad2antrr 731 |
. . . . . . . 8
                     
 ..^     
  |
104 | | elfzouz 11921 |
. . . . . . . . . 10
  ..^    
      |
105 | 104 | adantl 468 |
. . . . . . . . 9
                     
 ..^     
      |
106 | | elfzouz2 11931 |
. . . . . . . . . . . . 13
  ..^    
          |
107 | 106 | adantl 468 |
. . . . . . . . . . . 12
                     
 ..^                |
108 | | fzss2 11835 |
. . . . . . . . . . . 12
            
          |
109 | 107, 108 | syl 17 |
. . . . . . . . . . 11
                     
 ..^         
          |
110 | 109 | sselda 3431 |
. . . . . . . . . 10
                      
 ..^     
               |
111 | 78 | adantlr 720 |
. . . . . . . . . 10
                      
 ..^     
                 |
112 | 110, 111 | syldan 473 |
. . . . . . . . 9
                      
 ..^     
             |
113 | 2, 6 | mndcl 16538 |
. . . . . . . . . . 11
 
     |
114 | 113 | 3expb 1208 |
. . . . . . . . . 10
  
  
   |
115 | 103, 114 | sylan 474 |
. . . . . . . . 9
                      
 ..^      
  
   |
116 | 105, 112,
115 | seqcl 12230 |
. . . . . . . 8
                     
 ..^                |
117 | 82 | adantlr 720 |
. . . . . . . . . 10
                      
 ..^     
                 |
118 | 110, 117 | syldan 473 |
. . . . . . . . 9
                      
 ..^     
             |
119 | 105, 118,
115 | seqcl 12230 |
. . . . . . . 8
                     
 ..^                |
120 | | fzofzp1 12005 |
. . . . . . . . 9
  ..^    
            |
121 | | ffvelrn 6018 |
. . . . . . . . 9
                
                    |
122 | 77, 120, 121 | syl2an 480 |
. . . . . . . 8
                     
 ..^                |
123 | | ffvelrn 6018 |
. . . . . . . . 9
                
                    |
124 | 81, 120, 123 | syl2an 480 |
. . . . . . . 8
                     
 ..^                |
125 | | fvco3 5940 |
. . . . . . . . . . . 12
              
                        
     |
126 | 75, 120, 125 | syl2an 480 |
. . . . . . . . . . 11
                     
 ..^                    
     |
127 | | ffvelrn 6018 |
. . . . . . . . . . . . . 14
              
                  |
128 | 75, 120, 127 | syl2an 480 |
. . . . . . . . . . . . 13
                     
 ..^              |
129 | | fzp1disj 11851 |
. . . . . . . . . . . . . . 15
           |
130 | | disjsn 4031 |
. . . . . . . . . . . . . . 15
     
     
       |
131 | 129, 130 | mpbi 212 |
. . . . . . . . . . . . . 14
       |
132 | 73 | adantr 467 |
. . . . . . . . . . . . . . 15
                     
 ..^                    |
133 | 120 | adantl 468 |
. . . . . . . . . . . . . . 15
                     
 ..^                  |
134 | | f1elima 6162 |
. . . . . . . . . . . . . . 15
              
                     
              
         |
135 | 132, 133,
109, 134 | syl3anc 1267 |
. . . . . . . . . . . . . 14
                     
 ..^          
                   |
136 | 131, 135 | mtbiri 305 |
. . . . . . . . . . . . 13
                     
 ..^                      |
137 | 128, 136 | eldifd 3414 |
. . . . . . . . . . . 12
                     
 ..^                        |
138 | | gsumzaddlem.4 |
. . . . . . . . . . . . . . . . . 18
 
              g 
      |
139 | 138 | expr 619 |
. . . . . . . . . . . . . . . . 17
 

  
         g         |
140 | 139 | ralrimiv 2799 |
. . . . . . . . . . . . . . . 16
 

             g        |
141 | 140 | ex 436 |
. . . . . . . . . . . . . . 15
               g 
       |
142 | 141 | alrimiv 1772 |
. . . . . . . . . . . . . 14
                 g         |
143 | 142 | ad2antrr 731 |
. . . . . . . . . . . . 13
                     
 ..^                      g 
       |
144 | | imassrn 5178 |
. . . . . . . . . . . . . 14
         |
145 | 75 | adantr 467 |
. . . . . . . . . . . . . . 15
                     
 ..^                    |
146 | | frn 5733 |
. . . . . . . . . . . . . . 15
            
  |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . 14
                     
 ..^     
  |
148 | 144, 147 | syl5ss 3442 |
. . . . . . . . . . . . 13
                     
 ..^                |
149 | | vex 3047 |
. . . . . . . . . . . . . . 15
 |
150 | | imaexg 6727 |
. . . . . . . . . . . . . . 15
           |
151 | 149, 150 | ax-mp 5 |
. . . . . . . . . . . . . 14
         |
152 | | sseq1 3452 |
. . . . . . . . . . . . . . 15
         
           |
153 | | difeq2 3544 |
. . . . . . . . . . . . . . . 16
                       |
154 | | reseq2 5099 |
. . . . . . . . . . . . . . . . . . . 20
                       |
155 | 154 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . 19
          g     g              |
156 | 155 | sneqd 3979 |
. . . . . . . . . . . . . . . . . 18
           g       g               |
157 | 156 | fveq2d 5867 |
. . . . . . . . . . . . . . . . 17
              g           g                |
158 | 157 | eleq2d 2513 |
. . . . . . . . . . . . . . . 16
                   g 
   
         g                 |
159 | 153, 158 | raleqbidv 3000 |
. . . . . . . . . . . . . . 15
          
            g                           g 
               |
160 | 152, 159 | imbi12d 322 |
. . . . . . . . . . . . . 14
                        g 
                                   g 
                |
161 | 151, 160 | spcv 3139 |
. . . . . . . . . . . . 13
                 g 
                                   g 
               |
162 | 143, 148,
161 | sylc 62 |
. . . . . . . . . . . 12
                     
 ..^      
                    g                |
163 | | fveq2 5863 |
. . . . . . . . . . . . . 14
    
                  |
164 | 163 | eleq1d 2512 |
. . . . . . . . . . . . 13
    
            g 
           
               g                 |
165 | 164 | rspcv 3145 |
. . . . . . . . . . . 12
                
 
                    g                             g                 |
166 | 137, 162,
165 | sylc 62 |
. . . . . . . . . . 11
                     
 ..^                     g 
              |
167 | 126, 166 | eqeltrd 2528 |
. . . . . . . . . 10
                     
 ..^                   g 
              |
168 | | gsumzadd.z |
. . . . . . . . . . . . 13
Cntz   |
169 | 151 | a1i 11 |
. . . . . . . . . . . . 13
                     
 ..^                |
170 | 15 | ad2antrr 731 |
. . . . . . . . . . . . . 14
                     
 ..^            |
171 | 170, 148 | fssresd 5748 |
. . . . . . . . . . . . 13
                     
 ..^                              |
172 | | gsumzaddlem.2 |
. . . . . . . . . . . . . . 15
       |
173 | 172 | ad2antrr 731 |
. . . . . . . . . . . . . 14
                     
 ..^     
      |
174 | | resss 5127 |
. . . . . . . . . . . . . . 15
         
 |
175 | | rnss 5062 |
. . . . . . . . . . . . . . 15
 
         
        
  |
176 | 174, 175 | ax-mp 5 |
. . . . . . . . . . . . . 14
           |
177 | 168 | cntzidss 16984 |
. . . . . . . . . . . . . 14
               

         
                |
178 | 173, 176,
177 | sylancl 667 |
. . . . . . . . . . . . 13
                     
 ..^               
                |
179 | 105, 53 | syl6eleqr 2539 |
. . . . . . . . . . . . 13
                     
 ..^     
  |
180 | | f1ores 5826 |
. . . . . . . . . . . . . . 15
                 
                                 |
181 | 132, 109,
180 | syl2anc 666 |
. . . . . . . . . . . . . 14
                     
 ..^                              |
182 | | f1of1 5811 |
. . . . . . . . . . . . . 14
 
                                             |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . . 13
                     
 ..^                              |
184 | | suppssdm 6924 |
. . . . . . . . . . . . . . 15
 
         supp 
          |
185 | | dmres 5124 |
. . . . . . . . . . . . . . . 16
                     |
186 | 185 | a1i 11 |
. . . . . . . . . . . . . . 15
                     
 ..^                        
   |
187 | 184, 186 | syl5sseq 3479 |
. . . . . . . . . . . . . 14
                     
 ..^                 supp
            |
188 | | inss1 3651 |
. . . . . . . . . . . . . . 15
        
          |
189 | | df-ima 4846 |
. . . . . . . . . . . . . . . 16
               |
190 | 189 | a1i 11 |
. . . . . . . . . . . . . . 15
                     
 ..^                      |
191 | 188, 190 | syl5sseq 3479 |
. . . . . . . . . . . . . 14
                     
 ..^               
        |
192 | 187, 191 | sstrd 3441 |
. . . . . . . . . . . . 13
                     
 ..^                 supp
        |
193 | | eqid 2450 |
. . . . . . . . . . . . 13
                   supp
                   supp  |
194 | 2, 3, 6, 168, 103, 169, 171, 178, 179, 183, 192, 193 | gsumval3 17534 |
. . . . . . . . . . . 12
                     
 ..^       g                                      |
195 | 189 | eqimss2i 3486 |
. . . . . . . . . . . . . . . . . 18
               |
196 | | cores 5337 |
. . . . . . . . . . . . . . . . . 18
                                           |
197 | 195, 196 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 
                         |
198 | | resco 5338 |
. . . . . . . . . . . . . . . . 17
                 |
199 | 197, 198 | eqtr4i 2475 |
. . . . . . . . . . . . . . . 16
 
                         |
200 | 199 | fveq1i 5864 |
. . . . . . . . . . . . . . 15
                                   |
201 | | fvres 5877 |
. . . . . . . . . . . . . . 15
                         |
202 | 200, 201 | syl5eq 2496 |
. . . . . . . . . . . . . 14
                                   |
203 | 202 | adantl 468 |
. . . . . . . . . . . . 13
                      
 ..^     
       
                           |
204 | 105, 203 | seqfveq 12234 |
. . . . . . . . . . . 12
                     
 ..^                                        |
205 | 194, 204 | eqtr2d 2485 |
. . . . . . . . . . 11
                     
 ..^               g              |
206 | | fvex 5873 |
. . . . . . . . . . . 12
         |
207 | 206 | elsnc 3991 |
. . . . . . . . . . 11
           g            
         g 
            |
208 | 205, 207 | sylibr 216 |
. . . . . . . . . 10
                     
 ..^                g               |
209 | 6, 168 | cntzi 16976 |
. . . . . . . . . 10
               g 
                      g                                  

                |
210 | 167, 208,
209 | syl2anc 666 |
. . . . . . . . 9
                     
 ..^            
                               |
211 | 210 | eqcomd 2456 |
. . . . . . . 8
                     
 ..^        

                                  |
212 | 2, 6, 103, 116, 119, 122, 124, 211 | mnd4g 16546 |
. . . . . . 7
                     
 ..^               
                                                                    |
213 | 51, 51, 54, 78, 82, 102, 212 | seqcaopr3 12245 |
. . . . . 6
 
                                                              |
214 | 50, 55, 79, 87, 87, 90 | off 6543 |
. . . . . . 7
 
                            |
215 | | gsumzaddlem.3 |
. . . . . . . 8
             |
216 | 215 | adantr 467 |
. . . . . . 7
 
                   
           |
217 | 47, 114 | sylan 474 |
. . . . . . . . 9
                      
  
   |
218 | 217, 55, 79, 87, 87, 90 | off 6543 |
. . . . . . . 8
 
                            |
219 | | eldifi 3554 |
. . . . . . . . . 10
     |
220 | | eqidd 2451 |
. . . . . . . . . . 11
                     
           |
221 | | eqidd 2451 |
. . . . . . . . . . 11
                     
           |
222 | 84, 86, 87, 87, 90, 220, 221 | ofval 6537 |
. . . . . . . . . 10
                     
            
       |
223 | 219, 222 | sylan2 477 |
. . . . . . . . 9
                     
                      |
224 | 18 | adantr 467 |
. . . . . . . . . . . 12
 
                    supp    supp
  |
225 | | f1ofo 5819 |
. . . . . . . . . . . . . . . 16
            
              |
226 | | forn 5794 |
. . . . . . . . . . . . . . . 16
            
  |
227 | 225, 226 | syl 17 |
. . . . . . . . . . . . . . 15
            
  |
228 | 227, 19 | syl6eq 2500 |
. . . . . . . . . . . . . 14
            
   supp
  |
229 | 228 | sseq2d 3459 |
. . . . . . . . . . . . 13
            
  supp  supp    supp
   |
230 | 229 | ad2antll 734 |
. . . . . . . . . . . 12
 
                     supp
 supp
 
 supp    |
231 | 224, 230 | mpbird 236 |
. . . . . . . . . . 11
 
                    supp   |
232 | 13 | a1i 11 |
. . . . . . . . . . 11
 
                     |
233 | 55, 231, 87, 232 | suppssr 6943 |
. . . . . . . . . 10
                     
        |
234 | 29 | adantr 467 |
. . . . . . . . . . . . 13
 
                    supp    supp
  |
235 | 234, 31 | syl6sseqr 3478 |
. . . . . . . . . . . 12
 
                    supp    supp
  |
236 | 228 | sseq2d 3459 |
. . . . . . . . . . . . 13
            
  supp  supp    supp
   |
237 | 236 | ad2antll 734 |
. . . . . . . . . . . 12
 
                     supp
 supp
 
 supp    |
238 | 235, 237 | mpbird 236 |
. . . . . . . . . . 11
 
                    supp   |
239 | 79, 238, 87, 232 | suppssr 6943 |
. . . . . . . . . 10
                     
        |
240 | 233, 239 | oveq12d 6306 |
. . . . . . . . 9
                     
               |
241 | 8 | ad2antrr 731 |
. . . . . . . . 9
                     
  
 |
242 | 223, 240,
241 | 3eqtrd 2488 |
. . . . . . . 8
                     
           |
243 | 218, 242 | suppss 6942 |
. . . . . . 7
 
                       supp   |
244 | | ovex 6316 |
. . . . . . . . 9
    |
245 | 244, 149 | coex 6742 |
. . . . . . . 8
      |
246 | | suppimacnv 6922 |
. . . . . . . . 9
              supp               |
247 | 246 | eqcomd 2456 |
. . . . . . . 8
                          supp   |
248 | 245, 13, 247 | mp2an 677 |
. . . . . . 7
                  supp  |
249 | 2, 3, 6, 168, 47, 87, 214, 216, 52, 73, 243, 248 | gsumval3 17534 |
. . . . . 6
 
                    g      
               |
250 | | gsumzaddlem.1 |
. . . . . . . . 9
       |
251 | 250 | adantr 467 |
. . . . . . . 8
 
                         |
252 | | eqid 2450 |
. . . . . . . 8
   supp    supp
 |
253 | 2, 3, 6, 168, 47, 87, 55, 251, 52, 73, 231, 252 | gsumval3 17534 |
. . . . . . 7
 
                    g                |
254 | 172 | adantr 467 |
. . . . . . . 8
 
                         |
255 | | eqid 2450 |
. . . . . . . 8
   supp    supp
 |
256 | 2, 3, 6, 168, 47, 87, 79, 254, 52, 73, 238, 255 | gsumval3 17534 |
. . . . . . 7
 
                    g                |
257 | 253, 256 | oveq12d 6306 |
. . . . . 6
 
                     g   g     

                        |
258 | 213, 249,
257 | 3eqtr4d 2494 |
. . . . 5
 
                    g       g   g     |
259 | 258 | expr 619 |
. . . 4
 
                   g       g   g      |
260 | 259 | exlimdv 1778 |
. . 3
 
                  
 g       g   g      |
261 | 260 | expimpd 607 |
. 2
                    
 g       g   g      |
262 | | gsumzadd.fn |
. . . . 5
 finSupp
 |
263 | | gsumzadd.hn |
. . . . 5
 finSupp
 |
264 | 262, 263 | fsuppun 7899 |
. . . 4
    supp
  |
265 | 19, 264 | syl5eqel 2532 |
. . 3
   |
266 | | fz1f1o 13769 |
. . 3
 
                      |
267 | 265, 266 | syl 17 |
. 2
                        |
268 | 46, 261, 267 | mpjaod 383 |
1
  g       g   g     |