Step | Hyp | Ref
| Expression |
1 | | isummo.1 |
. . 3
        |
2 | | isummo.2 |
. . 3
 
   |
3 | | isummolem2a.dc |
. . 3
 
    
DECID
  |
4 | | summolem2.7 |
. . . 4

      |
5 | | summolem2.9 |
. . . . . . . 8

    ♯       |
6 | | 1zzd 9266 |
. . . . . . . . . . . . 13
   |
7 | | summolem2.5 |
. . . . . . . . . . . . . 14
   |
8 | 7 | nnzd 9360 |
. . . . . . . . . . . . 13
   |
9 | 6, 8 | fzfigd 10414 |
. . . . . . . . . . . 12
       |
10 | | summolem2.8 |
. . . . . . . . . . . 12
           |
11 | 9, 10 | fihasheqf1od 10750 |
. . . . . . . . . . 11
 ♯      ♯    |
12 | | nnnn0 9169 |
. . . . . . . . . . . 12
   |
13 | | hashfz1 10744 |
. . . . . . . . . . . 12

♯        |
14 | 7, 12, 13 | 3syl 17 |
. . . . . . . . . . 11
 ♯        |
15 | 11, 14 | eqtr3d 2212 |
. . . . . . . . . 10
 ♯    |
16 | 15 | oveq2d 5885 |
. . . . . . . . 9
    ♯         |
17 | | isoeq4 5799 |
. . . . . . . . 9
    ♯            ♯    
          |
18 | 16, 17 | syl 14 |
. . . . . . . 8
      ♯    
          |
19 | 5, 18 | mpbid 147 |
. . . . . . 7

         |
20 | | isof1o 5802 |
. . . . . . 7
                  |
21 | 19, 20 | syl 14 |
. . . . . 6
           |
22 | | f1of 5457 |
. . . . . 6
        
          |
23 | 21, 22 | syl 14 |
. . . . 5
           |
24 | | nnuz 9549 |
. . . . . . 7
     |
25 | 7, 24 | eleqtrdi 2270 |
. . . . . 6
       |
26 | | eluzfz2 10015 |
. . . . . 6
    
      |
27 | 25, 26 | syl 14 |
. . . . 5
       |
28 | 23, 27 | ffvelcdmd 5648 |
. . . 4
       |
29 | 4, 28 | sseldd 3156 |
. . 3
           |
30 | 4 | sselda 3155 |
. . . . . 6
 
       |
31 | | f1ocnvfv2 5773 |
. . . . . . . . 9
         
            |
32 | 21, 31 | sylan 283 |
. . . . . . . 8
 
            |
33 | | f1ocnv 5470 |
. . . . . . . . . . . 12
        
           |
34 | | f1of 5457 |
. . . . . . . . . . . 12
                     |
35 | 21, 33, 34 | 3syl 17 |
. . . . . . . . . . 11
            |
36 | 35 | ffvelcdmda 5647 |
. . . . . . . . . 10
 
            |
37 | | elfzle2 10011 |
. . . . . . . . . 10
                 |
38 | 36, 37 | syl 14 |
. . . . . . . . 9
 
        |
39 | 19 | adantr 276 |
. . . . . . . . . 10
 
          |
40 | | fzssuz 10048 |
. . . . . . . . . . . . 13
         |
41 | | uzssz 9533 |
. . . . . . . . . . . . . 14
     |
42 | | zssre 9246 |
. . . . . . . . . . . . . 14
 |
43 | 41, 42 | sstri 3164 |
. . . . . . . . . . . . 13
     |
44 | 40, 43 | sstri 3164 |
. . . . . . . . . . . 12
     |
45 | | ressxr 7988 |
. . . . . . . . . . . 12
 |
46 | 44, 45 | sstri 3164 |
. . . . . . . . . . 11
     |
47 | 46 | a1i 9 |
. . . . . . . . . 10
 
       |
48 | 4 | adantr 276 |
. . . . . . . . . . . 12
 
       |
49 | | uzssz 9533 |
. . . . . . . . . . . . 13
     |
50 | 49, 42 | sstri 3164 |
. . . . . . . . . . . 12
     |
51 | 48, 50 | sstrdi 3167 |
. . . . . . . . . . 11
 
   |
52 | 51, 45 | sstrdi 3167 |
. . . . . . . . . 10
 
   |
53 | 27 | adantr 276 |
. . . . . . . . . 10
 
       |
54 | | leisorel 10798 |
. . . . . . . . . 10
 
                                           
       |
55 | 39, 47, 52, 36, 53, 54 | syl122anc 1247 |
. . . . . . . . 9
 
               
       |
56 | 38, 55 | mpbid 147 |
. . . . . . . 8
 
         
      |
57 | 32, 56 | eqbrtrrd 4024 |
. . . . . . 7
 
       |
58 | | eluzelz 9523 |
. . . . . . . . 9
    
  |
59 | 30, 58 | syl 14 |
. . . . . . . 8
 
   |
60 | | eluzelz 9523 |
. . . . . . . . . 10
        
      |
61 | 29, 60 | syl 14 |
. . . . . . . . 9
       |
62 | 61 | adantr 276 |
. . . . . . . 8
 
       |
63 | | eluz 9527 |
. . . . . . . 8
               
       |
64 | 59, 62, 63 | syl2anc 411 |
. . . . . . 7
 
         
       |
65 | 57, 64 | mpbird 167 |
. . . . . 6
 
           |
66 | | elfzuzb 10002 |
. . . . . 6
                         |
67 | 30, 65, 66 | sylanbrc 417 |
. . . . 5
 
           |
68 | 67 | ex 115 |
. . . 4
             |
69 | 68 | ssrdv 3161 |
. . 3

          |
70 | 1, 2, 3, 29, 69 | fsum3cvg 11367 |
. 2
                |
71 | | addid2 8083 |
. . . . 5
     |
72 | 71 | adantl 277 |
. . . 4
 

    |
73 | | addid1 8082 |
. . . . 5
     |
74 | 73 | adantl 277 |
. . . 4
 

    |
75 | | addcl 7924 |
. . . . 5
 
     |
76 | 75 | adantl 277 |
. . . 4
 
       |
77 | | 0cnd 7938 |
. . . 4
   |
78 | 27, 16 | eleqtrrd 2257 |
. . . 4
    ♯     |
79 | | iftrue 3539 |
. . . . . . . . . . . 12
        |
80 | 79 | adantl 277 |
. . . . . . . . . . 11
 
        |
81 | 80, 2 | eqeltrd 2254 |
. . . . . . . . . 10
 
        |
82 | 81 | adantlr 477 |
. . . . . . . . 9
            |
83 | 82 | adantlr 477 |
. . . . . . . 8
   

     
   
   |
84 | | iffalse 3542 |
. . . . . . . . . 10
        |
85 | | 0cn 7937 |
. . . . . . . . . 10
 |
86 | 84, 85 | eqeltrdi 2268 |
. . . . . . . . 9
        |
87 | 86 | adantl 277 |
. . . . . . . 8
   

             |
88 | 3 | adantlr 477 |
. . . . . . . . 9
        
DECID
  |
89 | | exmiddc 836 |
. . . . . . . . 9
DECID

   |
90 | 88, 89 | syl 14 |
. . . . . . . 8
        

   |
91 | 83, 87, 90 | mpjaodan 798 |
. . . . . . 7
        
   
   |
92 | | simpll 527 |
. . . . . . . . 9
   
       |
93 | | simpr 110 |
. . . . . . . . 9
   
    
      |
94 | 4 | ssneld 3157 |
. . . . . . . . 9
         |
95 | 92, 93, 94 | sylc 62 |
. . . . . . . 8
   
    
  |
96 | 95, 86 | syl 14 |
. . . . . . 7
   
            |
97 | | summolem2.6 |
. . . . . . . . 9
   |
98 | | eluzdc 9596 |
. . . . . . . . 9
 
 DECID       |
99 | 97, 98 | sylan 283 |
. . . . . . . 8
 

DECID
      |
100 | | exmiddc 836 |
. . . . . . . 8
DECID                 |
101 | 99, 100 | syl 14 |
. . . . . . 7
 

            |
102 | 91, 96, 101 | mpjaodan 798 |
. . . . . 6
 

   
   |
103 | 102, 1 | fmptd 5666 |
. . . . 5
       |
104 | | eluzelz 9523 |
. . . . 5
    
  |
105 | | ffvelcdm 5645 |
. . . . 5
     
       |
106 | 103, 104,
105 | syl2an 289 |
. . . 4
 
    
      |
107 | | elnnuz 9550 |
. . . . . . . 8

      |
108 | 107 | biimpri 133 |
. . . . . . 7
    
  |
109 | 108 | adantl 277 |
. . . . . 6
 
    
  |
110 | | isof1o 5802 |
. . . . . . . . . . . 12
     ♯          ♯       |
111 | | f1of 5457 |
. . . . . . . . . . . 12
      ♯          ♯       |
112 | 5, 110, 111 | 3syl 17 |
. . . . . . . . . . 11
      ♯       |
113 | 112 | ad2antrr 488 |
. . . . . . . . . 10
       

     ♯       |
114 | | 1zzd 9266 |
. . . . . . . . . . . 12
       

  |
115 | 15, 8 | eqeltrd 2254 |
. . . . . . . . . . . . 13
 ♯    |
116 | 115 | ad2antrr 488 |
. . . . . . . . . . . 12
       

♯    |
117 | | eluzelz 9523 |
. . . . . . . . . . . . 13
    
  |
118 | 117 | ad2antlr 489 |
. . . . . . . . . . . 12
       

  |
119 | 114, 116,
118 | 3jca 1177 |
. . . . . . . . . . 11
       

 ♯     |
120 | | eluzle 9526 |
. . . . . . . . . . . . 13
    
  |
121 | 120 | ad2antlr 489 |
. . . . . . . . . . . 12
       

  |
122 | | simpr 110 |
. . . . . . . . . . . . 13
       

  |
123 | 15 | breq2d 4012 |
. . . . . . . . . . . . . 14
  ♯ 
   |
124 | 123 | ad2antrr 488 |
. . . . . . . . . . . . 13
       

 ♯     |
125 | 122, 124 | mpbird 167 |
. . . . . . . . . . . 12
       

♯    |
126 | 121, 125 | jca 306 |
. . . . . . . . . . 11
       

 ♯     |
127 | | elfz2 9999 |
. . . . . . . . . . 11
    ♯     ♯    ♯      |
128 | 119, 126,
127 | sylanbrc 417 |
. . . . . . . . . 10
       

   ♯     |
129 | 113, 128 | ffvelcdmd 5648 |
. . . . . . . . 9
       

      |
130 | 129 | iftrued 3541 |
. . . . . . . 8
       

             ![]_ ]_](_urbrack.gif) 
       ![]_ ]_](_urbrack.gif)   |
131 | 4 | ad2antrr 488 |
. . . . . . . . . . 11
       

      |
132 | 23 | ad2antrr 488 |
. . . . . . . . . . . 12
       

          |
133 | 16 | eleq2d 2247 |
. . . . . . . . . . . . . 14
     ♯  
       |
134 | 133 | ad2antrr 488 |
. . . . . . . . . . . . 13
       

    ♯  
       |
135 | 128, 134 | mpbid 147 |
. . . . . . . . . . . 12
       

      |
136 | 132, 135 | ffvelcdmd 5648 |
. . . . . . . . . . 11
       

      |
137 | 131, 136 | sseldd 3156 |
. . . . . . . . . 10
       

          |
138 | 49, 137 | sselid 3153 |
. . . . . . . . 9
       

      |
139 | 102 | ralrimiva 2550 |
. . . . . . . . . 10
         |
140 | 139 | ad2antrr 488 |
. . . . . . . . 9
       

        |
141 | | nfv 1528 |
. . . . . . . . . . . 12
       |
142 | | nfcsb1v 3090 |
. . . . . . . . . . . 12
        ![]_ ]_](_urbrack.gif)  |
143 | | nfcv 2319 |
. . . . . . . . . . . 12
   |
144 | 141, 142,
143 | nfif 3562 |
. . . . . . . . . . 11
               ![]_ ]_](_urbrack.gif)    |
145 | 144 | nfel1 2330 |
. . . . . . . . . 10
               ![]_ ]_](_urbrack.gif)    |
146 | | eleq1 2240 |
. . . . . . . . . . . 12
     
       |
147 | | csbeq1a 3066 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif)   |
148 | 146, 147 | ifbieq1d 3556 |
. . . . . . . . . . 11
                       ![]_ ]_](_urbrack.gif)     |
149 | 148 | eleq1d 2246 |
. . . . . . . . . 10
          
             ![]_ ]_](_urbrack.gif) 
    |
150 | 145, 149 | rspc 2835 |
. . . . . . . . 9
      
                  ![]_ ]_](_urbrack.gif)      |
151 | 138, 140,
150 | sylc 62 |
. . . . . . . 8
       

             ![]_ ]_](_urbrack.gif) 
   |
152 | 130, 151 | eqeltrrd 2255 |
. . . . . . 7
       

      ![]_ ]_](_urbrack.gif)   |
153 | | 0cnd 7938 |
. . . . . . 7
       
   |
154 | 109 | nnzd 9360 |
. . . . . . . 8
 
    
  |
155 | 8 | adantr 276 |
. . . . . . . 8
 
    
  |
156 | | zdcle 9315 |
. . . . . . . 8
 
 DECID   |
157 | 154, 155,
156 | syl2anc 411 |
. . . . . . 7
 
    
DECID
  |
158 | 152, 153,
157 | ifcldadc 3563 |
. . . . . 6
 
    
 
       ![]_ ]_](_urbrack.gif) 
   |
159 | | breq1 4003 |
. . . . . . . 8
 
   |
160 | | fveq2 5511 |
. . . . . . . . 9
           |
161 | 160 | csbeq1d 3064 |
. . . . . . . 8
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
162 | 159, 161 | ifbieq1d 3556 |
. . . . . . 7
  
       ![]_ ]_](_urbrack.gif) 
          ![]_ ]_](_urbrack.gif)     |
163 | | isummolem2a.h |
. . . . . . 7
          ![]_ ]_](_urbrack.gif)     |
164 | 162, 163 | fvmptg 5588 |
. . . . . 6
           ![]_ ]_](_urbrack.gif)         
       ![]_ ]_](_urbrack.gif) 
   |
165 | 109, 158,
164 | syl2anc 411 |
. . . . 5
 
    
             ![]_ ]_](_urbrack.gif)     |
166 | 165, 158 | eqeltrd 2254 |
. . . 4
 
    
      |
167 | | fveqeq2 5520 |
. . . . . 6
             |
168 | | eldifi 3257 |
. . . . . . . . 9
        ♯           ♯      |
169 | | elfzelz 10008 |
. . . . . . . . 9
       ♯      |
170 | 168, 169 | syl 14 |
. . . . . . . 8
        ♯       |
171 | | eldifn 3258 |
. . . . . . . . . 10
        ♯    
  |
172 | 171, 84 | syl 14 |
. . . . . . . . 9
        ♯            |
173 | 172, 85 | eqeltrdi 2268 |
. . . . . . . 8
        ♯            |
174 | 1 | fvmpt2 5595 |
. . . . . . . 8
               
   |
175 | 170, 173,
174 | syl2anc 411 |
. . . . . . 7
        ♯                |
176 | 175, 172 | eqtrd 2210 |
. . . . . 6
        ♯           |
177 | 167, 176 | vtoclga 2803 |
. . . . 5
        ♯           |
178 | 177 | adantl 277 |
. . . 4
 
       ♯            |
179 | 112 | ffvelcdmda 5647 |
. . . . . 6
 
   ♯          |
180 | 179 | iftrued 3541 |
. . . . 5
 
   ♯                 ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
181 | 4 | adantr 276 |
. . . . . . . 8
 
   ♯          |
182 | 181, 179 | sseldd 3156 |
. . . . . . 7
 
   ♯              |
183 | | eluzelz 9523 |
. . . . . . 7
        
      |
184 | 182, 183 | syl 14 |
. . . . . 6
 
   ♯          |
185 | | simpl 109 |
. . . . . . . 8
 
   ♯      |
186 | 185, 184 | jca 306 |
. . . . . . 7
 
   ♯            |
187 | | nfv 1528 |
. . . . . . . . 9
         |
188 | | nfv 1528 |
. . . . . . . . . . 11
       |
189 | | nfcsb1v 3090 |
. . . . . . . . . . 11
        ![]_ ]_](_urbrack.gif)  |
190 | 188, 189,
143 | nfif 3562 |
. . . . . . . . . 10
               ![]_ ]_](_urbrack.gif)    |
191 | 190 | nfel1 2330 |
. . . . . . . . 9
               ![]_ ]_](_urbrack.gif)    |
192 | 187, 191 | nfim 1572 |
. . . . . . . 8
                      ![]_ ]_](_urbrack.gif)     |
193 | | eleq1 2240 |
. . . . . . . . . 10
     
       |
194 | 193 | anbi2d 464 |
. . . . . . . . 9
      

         |
195 | | eleq1 2240 |
. . . . . . . . . . 11
     
       |
196 | | csbeq1a 3066 |
. . . . . . . . . . 11
           ![]_ ]_](_urbrack.gif)   |
197 | 195, 196 | ifbieq1d 3556 |
. . . . . . . . . 10
                       ![]_ ]_](_urbrack.gif)     |
198 | 197 | eleq1d 2246 |
. . . . . . . . 9
          
             ![]_ ]_](_urbrack.gif) 
    |
199 | 194, 198 | imbi12d 234 |
. . . . . . . 8
       
                           ![]_ ]_](_urbrack.gif)       |
200 | 192, 199,
102 | vtoclg1f 2796 |
. . . . . . 7
      
                  ![]_ ]_](_urbrack.gif)      |
201 | 179, 186,
200 | sylc 62 |
. . . . . 6
 
   ♯                 ![]_ ]_](_urbrack.gif)     |
202 | | eleq1 2240 |
. . . . . . . 8
     
       |
203 | | csbeq1 3060 |
. . . . . . . 8
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
204 | 202, 203 | ifbieq1d 3556 |
. . . . . . 7
      
   ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)     |
205 | | nfcv 2319 |
. . . . . . . . 9
        |
206 | | nfv 1528 |
. . . . . . . . . 10
  |
207 | | nfcsb1v 3090 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)  |
208 | 206, 207,
143 | nfif 3562 |
. . . . . . . . 9
       ![]_ ]_](_urbrack.gif)    |
209 | | eleq1 2240 |
. . . . . . . . . 10
 
   |
210 | | csbeq1a 3066 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)   |
211 | 209, 210 | ifbieq1d 3556 |
. . . . . . . . 9
           ![]_ ]_](_urbrack.gif)     |
212 | 205, 208,
211 | cbvmpt 4095 |
. . . . . . . 8
    
      
 ![]_ ]_](_urbrack.gif)     |
213 | 1, 212 | eqtri 2198 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)     |
214 | 204, 213 | fvmptg 5588 |
. . . . . 6
                   ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif) 
   |
215 | 184, 201,
214 | syl2anc 411 |
. . . . 5
 
   ♯                         ![]_ ]_](_urbrack.gif) 
   |
216 | | elfznn 10037 |
. . . . . . . 8
    ♯  
  |
217 | 216 | adantl 277 |
. . . . . . 7
 
   ♯      |
218 | | elfzle2 10011 |
. . . . . . . . . . 11
    ♯  
♯    |
219 | 218 | adantl 277 |
. . . . . . . . . 10
 
   ♯    ♯    |
220 | 15 | breq2d 4012 |
. . . . . . . . . . 11
  ♯ 
   |
221 | 220 | adantr 276 |
. . . . . . . . . 10
 
   ♯     ♯ 
   |
222 | 219, 221 | mpbid 147 |
. . . . . . . . 9
 
   ♯      |
223 | 222 | iftrued 3541 |
. . . . . . . 8
 
   ♯             ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
224 | 180, 201 | eqeltrrd 2255 |
. . . . . . . 8
 
   ♯          ![]_ ]_](_urbrack.gif)
  |
225 | 223, 224 | eqeltrd 2254 |
. . . . . . 7
 
   ♯             ![]_ ]_](_urbrack.gif)     |
226 | | breq1 4003 |
. . . . . . . . 9
 
   |
227 | | fveq2 5511 |
. . . . . . . . . 10
           |
228 | 227 | csbeq1d 3064 |
. . . . . . . . 9
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
229 | 226, 228 | ifbieq1d 3556 |
. . . . . . . 8
  
       ![]_ ]_](_urbrack.gif) 
          ![]_ ]_](_urbrack.gif)     |
230 | 229, 163 | fvmptg 5588 |
. . . . . . 7
           ![]_ ]_](_urbrack.gif)         
       ![]_ ]_](_urbrack.gif) 
   |
231 | 217, 225,
230 | syl2anc 411 |
. . . . . 6
 
   ♯                 ![]_ ]_](_urbrack.gif)     |
232 | 231, 223 | eqtrd 2210 |
. . . . 5
 
   ♯              ![]_ ]_](_urbrack.gif)   |
233 | 180, 215,
232 | 3eqtr4rd 2221 |
. . . 4
 
   ♯                  |
234 | 72, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233 | seq3coll 10803 |
. . 3
                   |
235 | 15, 7 | eqeltrd 2254 |
. . . . 5
 ♯    |
236 | 235, 7 | jca 306 |
. . . 4
  ♯ 
   |
237 | 16 | eqcomd 2183 |
. . . . . 6
        ♯     |
238 | | f1oeq2 5446 |
. . . . . 6
        ♯  
              ♯        |
239 | 237, 238 | syl 14 |
. . . . 5
               ♯        |
240 | 10, 239 | mpbid 147 |
. . . 4
      ♯       |
241 | | isummolem2a.g |
. . . 4
   ♯         ![]_ ]_](_urbrack.gif) 
   |
242 | 1, 2, 236, 240, 21, 241, 163 | summodclem3 11369 |
. . 3
      ♯           |
243 | 15 | fveq2d 5515 |
. . 3
      ♯           |
244 | 234, 242,
243 | 3eqtr2d 2216 |
. 2
                   |
245 | 70, 244 | breqtrd 4026 |
1
            |