Step | Hyp | Ref
| Expression |
1 | | sumeq1 11363 |
. . . 4


   |
2 | 1 | mpteq2dv 4095 |
. . 3

 
      |
3 | 2 | eleq1d 2246 |
. 2

     

       |
4 | | sumeq1 11363 |
. . . 4
 
   |
5 | 4 | mpteq2dv 4095 |
. . 3
     
   |
6 | 5 | eleq1d 2246 |
. 2
               |
7 | | sumeq1 11363 |
. . . 4
     
        |
8 | 7 | mpteq2dv 4095 |
. . 3
                  |
9 | 8 | eleq1d 2246 |
. 2
       
                |
10 | | sumeq1 11363 |
. . . 4
 
   |
11 | 10 | mpteq2dv 4095 |
. . 3
     
   |
12 | 11 | eleq1d 2246 |
. 2
               |
13 | | sum0 11396 |
. . . 4
  |
14 | 13 | mpteq2i 4091 |
. . 3
      |
15 | | fsumcn.4 |
. . . 4
 TopOn    |
16 | | fsumcncntop.3 |
. . . . . 6
      |
17 | 16 | cntoptopon 14035 |
. . . . 5
TopOn   |
18 | 17 | a1i 9 |
. . . 4
 TopOn    |
19 | | 0cnd 7950 |
. . . 4
   |
20 | 15, 18, 19 | cnmptc 13785 |
. . 3
       |
21 | 14, 20 | eqeltrid 2264 |
. 2
        |
22 | | simplrr 536 |
. . . . . . . . . . 11
   
 
         |
23 | 22 | eldifbd 3142 |
. . . . . . . . . 10
   
 
    
  |
24 | | disjsn 3655 |
. . . . . . . . . 10
    
  |
25 | 23, 24 | sylibr 134 |
. . . . . . . . 9
   
 
     
     |
26 | | eqidd 2178 |
. . . . . . . . 9
   
 
               |
27 | | simpllr 534 |
. . . . . . . . . 10
   
 
       |
28 | | unsnfi 6918 |
. . . . . . . . . 10
 
 
       |
29 | 27, 22, 23, 28 | syl3anc 1238 |
. . . . . . . . 9
   
 
           |
30 | | simp-4l 541 |
. . . . . . . . . 10
      
            |
31 | | simplrl 535 |
. . . . . . . . . . . 12
   
 
       |
32 | 22 | eldifad 3141 |
. . . . . . . . . . . . 13
   
 
       |
33 | 32 | snssd 3738 |
. . . . . . . . . . . 12
   
 
      
  |
34 | 31, 33 | unssd 3312 |
. . . . . . . . . . 11
   
 
           |
35 | 34 | sselda 3156 |
. . . . . . . . . 10
      
            |
36 | | simplr 528 |
. . . . . . . . . 10
      
            |
37 | 15 | adantr 276 |
. . . . . . . . . . . . . 14
 
 TopOn    |
38 | 17 | a1i 9 |
. . . . . . . . . . . . . 14
 
 TopOn    |
39 | | fsumcn.6 |
. . . . . . . . . . . . . 14
 
       |
40 | | cnf2 13708 |
. . . . . . . . . . . . . 14
  TopOn  TopOn      

       |
41 | 37, 38, 39, 40 | syl3anc 1238 |
. . . . . . . . . . . . 13
 
         |
42 | | eqid 2177 |
. . . . . . . . . . . . . 14
     |
43 | 42 | fmpt 5667 |
. . . . . . . . . . . . 13
 
        |
44 | 41, 43 | sylibr 134 |
. . . . . . . . . . . 12
 
 
  |
45 | | rsp 2524 |
. . . . . . . . . . . 12
 

   |
46 | 44, 45 | syl 14 |
. . . . . . . . . . 11
 
 
   |
47 | 46 | imp 124 |
. . . . . . . . . 10
       |
48 | 30, 35, 36, 47 | syl21anc 1237 |
. . . . . . . . 9
      
            |
49 | 25, 26, 29, 48 | fsumsplit 11415 |
. . . . . . . 8
   
 
            
       |
50 | | simplll 533 |
. . . . . . . . . . . 12
   
 
       |
51 | | simpr 110 |
. . . . . . . . . . . 12
   
 
       |
52 | 46 | impancom 260 |
. . . . . . . . . . . . 13
 
 
   |
53 | 52 | ralrimiv 2549 |
. . . . . . . . . . . 12
 
 
  |
54 | 50, 51, 53 | syl2anc 411 |
. . . . . . . . . . 11
   
 
     
  |
55 | | nfcsb1v 3091 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)  |
56 | 55 | nfel1 2330 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)
 |
57 | | csbeq1a 3067 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   |
58 | 57 | eleq1d 2246 |
. . . . . . . . . . . 12
 
  ![]_ ]_](_urbrack.gif)    |
59 | 56, 58 | rspc 2836 |
. . . . . . . . . . 11
  
  ![]_ ]_](_urbrack.gif)
   |
60 | 32, 54, 59 | sylc 62 |
. . . . . . . . . 10
   
 
       ![]_ ]_](_urbrack.gif)   |
61 | | sumsns 11423 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)   |
62 | 22, 60, 61 | syl2anc 411 |
. . . . . . . . 9
   
 
           ![]_ ]_](_urbrack.gif)   |
63 | 62 | oveq2d 5891 |
. . . . . . . 8
   
 
             
  ![]_ ]_](_urbrack.gif)    |
64 | 49, 63 | eqtrd 2210 |
. . . . . . 7
   
 
            
  ![]_ ]_](_urbrack.gif)    |
65 | 64 | mpteq2dva 4094 |
. . . . . 6
    
              
  ![]_ ]_](_urbrack.gif)     |
66 | 65 | adantr 276 |
. . . . 5
   
 
     
                 ![]_ ]_](_urbrack.gif)     |
67 | | nfcv 2319 |
. . . . . 6
      ![]_ ]_](_urbrack.gif)   |
68 | | nfcv 2319 |
. . . . . . . 8
   |
69 | | nfcsb1v 3091 |
. . . . . . . 8
  
 ![]_ ]_](_urbrack.gif)  |
70 | 68, 69 | nfsum 11365 |
. . . . . . 7
     ![]_ ]_](_urbrack.gif)  |
71 | | nfcv 2319 |
. . . . . . 7
  |
72 | | nfcv 2319 |
. . . . . . . 8
   |
73 | 72, 69 | nfcsb 3095 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
74 | 70, 71, 73 | nfov 5905 |
. . . . . 6
      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
75 | | csbeq1a 3067 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)   |
76 | 75 | sumeq2ad 11377 |
. . . . . . 7
 
   ![]_ ]_](_urbrack.gif)   |
77 | 75 | csbeq2dv 3084 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
78 | 76, 77 | oveq12d 5893 |
. . . . . 6
     ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
79 | 67, 74, 78 | cbvmpt 4099 |
. . . . 5
  
  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
80 | 66, 79 | eqtrdi 2226 |
. . . 4
   
 
     
                 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
81 | 15 | ad3antrrr 492 |
. . . . 5
   
 
     
    TopOn    |
82 | | nfcv 2319 |
. . . . . . 7
    |
83 | 82, 70, 76 | cbvmpt 4099 |
. . . . . 6
 
     ![]_ ]_](_urbrack.gif)   |
84 | | simpr 110 |
. . . . . 6
   
 
     
           |
85 | 83, 84 | eqeltrrid 2265 |
. . . . 5
   
 
     
        ![]_ ]_](_urbrack.gif)      |
86 | | nfcv 2319 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)  |
87 | 86, 73, 77 | cbvmpt 4099 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
88 | | simprr 531 |
. . . . . . . . 9
    
        |
89 | 88 | eldifad 3141 |
. . . . . . . 8
    
      |
90 | 89 | adantr 276 |
. . . . . . 7
   
 
     
      |
91 | 39 | ralrimiva 2550 |
. . . . . . . 8
  
     |
92 | 91 | ad3antrrr 492 |
. . . . . . 7
   
 
     
    

     |
93 | | nfcv 2319 |
. . . . . . . . . 10
   |
94 | 93, 55 | nfmpt 4096 |
. . . . . . . . 9
     ![]_ ]_](_urbrack.gif)   |
95 | 94 | nfel1 2330 |
. . . . . . . 8
     ![]_ ]_](_urbrack.gif)     |
96 | 57 | mpteq2dv 4095 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)    |
97 | 96 | eleq1d 2246 |
. . . . . . . 8
         ![]_ ]_](_urbrack.gif)       |
98 | 95, 97 | rspc 2836 |
. . . . . . 7
  

      ![]_ ]_](_urbrack.gif)       |
99 | 90, 92, 98 | sylc 62 |
. . . . . 6
   
 
     
       ![]_ ]_](_urbrack.gif)      |
100 | 87, 99 | eqeltrrid 2265 |
. . . . 5
   
 
     
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      |
101 | 16 | addcncntop 14055 |
. . . . . 6
     |
102 | 101 | a1i 9 |
. . . . 5
   
 
     
          |
103 | 81, 85, 100, 102 | cnmpt12f 13789 |
. . . 4
   
 
     
         ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)       |
104 | 80, 103 | eqeltrd 2254 |
. . 3
   
 
     
                |
105 | 104 | ex 115 |
. 2
    
      
  

            |
106 | | fsumcn.5 |
. 2
   |
107 | 3, 6, 9, 12, 21, 105, 106 | findcard2sd 6892 |
1
        |