Step | Hyp | Ref
| Expression |
1 | | ssid 3451 |
. 2
 |
2 | | fsumcn.5 |
. . 3
   |
3 | | sseq1 3453 |
. . . . . 6


   |
4 | | sumeq1 13755 |
. . . . . . . 8


   |
5 | 4 | mpteq2dv 4490 |
. . . . . . 7

 
      |
6 | 5 | eleq1d 2513 |
. . . . . 6

     

       |
7 | 3, 6 | imbi12d 322 |
. . . . 5

 
      
         |
8 | 7 | imbi2d 318 |
. . . 4

         
 
          |
9 | | sseq1 3453 |
. . . . . 6
 
   |
10 | | sumeq1 13755 |
. . . . . . . 8
 
   |
11 | 10 | mpteq2dv 4490 |
. . . . . . 7
     
   |
12 | 11 | eleq1d 2513 |
. . . . . 6
               |
13 | 9, 12 | imbi12d 322 |
. . . . 5
                   |
14 | 13 | imbi2d 318 |
. . . 4
  
         
          |
15 | | sseq1 3453 |
. . . . . 6
             |
16 | | sumeq1 13755 |
. . . . . . . 8
     
        |
17 | 16 | mpteq2dv 4490 |
. . . . . . 7
                  |
18 | 17 | eleq1d 2513 |
. . . . . 6
       
                |
19 | 15, 18 | imbi12d 322 |
. . . . 5
                                |
20 | 19 | imbi2d 318 |
. . . 4
              
                     |
21 | | sseq1 3453 |
. . . . . 6
 
   |
22 | | sumeq1 13755 |
. . . . . . . 8
 
   |
23 | 22 | mpteq2dv 4490 |
. . . . . . 7
     
   |
24 | 23 | eleq1d 2513 |
. . . . . 6
               |
25 | 21, 24 | imbi12d 322 |
. . . . 5
                   |
26 | 25 | imbi2d 318 |
. . . 4
  
         
          |
27 | | sum0 13787 |
. . . . . . 7
  |
28 | 27 | mpteq2i 4486 |
. . . . . 6
      |
29 | | fsumcn.4 |
. . . . . . 7
 TopOn    |
30 | | fsumcn.3 |
. . . . . . . . 9
  ℂfld |
31 | 30 | cnfldtopon 21803 |
. . . . . . . 8
TopOn   |
32 | 31 | a1i 11 |
. . . . . . 7
 TopOn    |
33 | | 0cnd 9636 |
. . . . . . 7
   |
34 | 29, 32, 33 | cnmptc 20677 |
. . . . . 6
       |
35 | 28, 34 | syl5eqel 2533 |
. . . . 5
        |
36 | 35 | a1d 26 |
. . . 4
 
        |
37 | | ssun1 3597 |
. . . . . . . . . 10
     |
38 | | sstr 3440 |
. . . . . . . . . 10
 
        
  |
39 | 37, 38 | mpan 676 |
. . . . . . . . 9
    
  |
40 | 39 | imim1i 60 |
. . . . . . . 8
 
          
        |
41 | | simplr 762 |
. . . . . . . . . . . . . . . . . 18
  
       
  |
42 | | disjsn 4032 |
. . . . . . . . . . . . . . . . . 18
    
  |
43 | 41, 42 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
  
              |
44 | | eqidd 2452 |
. . . . . . . . . . . . . . . . 17
  
                  |
45 | 2 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
  
       
  |
46 | | simprl 764 |
. . . . . . . . . . . . . . . . . 18
  
              |
47 | | ssfi 7792 |
. . . . . . . . . . . . . . . . . 18
             |
48 | 45, 46, 47 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
  
              |
49 | | simplll 768 |
. . . . . . . . . . . . . . . . . 18
   

    
         |
50 | 46 | sselda 3432 |
. . . . . . . . . . . . . . . . . 18
   

    
         |
51 | | simplrr 771 |
. . . . . . . . . . . . . . . . . 18
   

    
         |
52 | 29 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 TopOn    |
53 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 TopOn    |
54 | | fsumcn.6 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
55 | | cnf2 20265 |
. . . . . . . . . . . . . . . . . . . . . 22
  TopOn  TopOn      

       |
56 | 52, 53, 54, 55 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . 21
 
         |
57 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
58 | 57 | fmpt 6043 |
. . . . . . . . . . . . . . . . . . . . 21
 
        |
59 | 56, 58 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . 20
 
 
  |
60 | | rsp 2754 |
. . . . . . . . . . . . . . . . . . . 20
 

   |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
 
   |
62 | 61 | imp 431 |
. . . . . . . . . . . . . . . . . 18
       |
63 | 49, 50, 51, 62 | syl21anc 1267 |
. . . . . . . . . . . . . . . . 17
   

    
         |
64 | 43, 44, 48, 63 | fsumsplit 13806 |
. . . . . . . . . . . . . . . 16
  
                       |
65 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
  
            |
66 | 65 | unssbd 3612 |
. . . . . . . . . . . . . . . . . . . 20
  
       
  |
67 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . 21
 |
68 | 67 | snss 4096 |
. . . . . . . . . . . . . . . . . . . 20

    |
69 | 66, 68 | sylibr 216 |
. . . . . . . . . . . . . . . . . . 19
  
        |
70 | 69 | adantrr 723 |
. . . . . . . . . . . . . . . . . 18
  
          |
71 | 61 | impancom 442 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
   |
72 | 71 | ralrimiv 2800 |
. . . . . . . . . . . . . . . . . . . 20
 
 
  |
73 | 72 | ad2ant2rl 755 |
. . . . . . . . . . . . . . . . . . 19
  
        
  |
74 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . . . . . . 21
  
 ![]_ ]_](_urbrack.gif)  |
75 | 74 | nfel1 2606 |
. . . . . . . . . . . . . . . . . . . 20
    ![]_ ]_](_urbrack.gif)
 |
76 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . . . . . . 21
   ![]_ ]_](_urbrack.gif)   |
77 | 76 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . 20
 
  ![]_ ]_](_urbrack.gif)    |
78 | 75, 77 | rspc 3144 |
. . . . . . . . . . . . . . . . . . 19
  
  ![]_ ]_](_urbrack.gif)
   |
79 | 70, 73, 78 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
  
        
 ![]_ ]_](_urbrack.gif)
  |
80 | | sumsns 13811 |
. . . . . . . . . . . . . . . . . 18
    ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)   |
81 | 70, 79, 80 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
  
              ![]_ ]_](_urbrack.gif)   |
82 | 81 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
  
                
  ![]_ ]_](_urbrack.gif)    |
83 | 64, 82 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
  
                  ![]_ ]_](_urbrack.gif)    |
84 | 83 | anassrs 654 |
. . . . . . . . . . . . . 14
   

    
           ![]_ ]_](_urbrack.gif)    |
85 | 84 | mpteq2dva 4489 |
. . . . . . . . . . . . 13
  
                   ![]_ ]_](_urbrack.gif)     |
86 | 85 | adantrr 723 |
. . . . . . . . . . . 12
  
            

         
  ![]_ ]_](_urbrack.gif)     |
87 | | nfcv 2592 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)   |
88 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
   |
89 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . 15
  
 ![]_ ]_](_urbrack.gif)  |
90 | 88, 89 | nfsum 13757 |
. . . . . . . . . . . . . 14
     ![]_ ]_](_urbrack.gif)  |
91 | | nfcv 2592 |
. . . . . . . . . . . . . 14
  |
92 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
   |
93 | 92, 89 | nfcsb 3381 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
94 | 90, 91, 93 | nfov 6316 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
95 | | csbeq1a 3372 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)   |
96 | 95 | sumeq2sdv 13770 |
. . . . . . . . . . . . . 14
 
   ![]_ ]_](_urbrack.gif)   |
97 | 95 | csbeq2dv 3781 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
98 | 96, 97 | oveq12d 6308 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
99 | 87, 94, 98 | cbvmpt 4494 |
. . . . . . . . . . . 12
  
  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
100 | 86, 99 | syl6eq 2501 |
. . . . . . . . . . 11
  
            

         
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
101 | 29 | ad2antrr 732 |
. . . . . . . . . . . 12
  
            
TopOn    |
102 | | nfcv 2592 |
. . . . . . . . . . . . . 14
    |
103 | 102, 90, 96 | cbvmpt 4494 |
. . . . . . . . . . . . 13
 
     ![]_ ]_](_urbrack.gif)   |
104 | | simprr 766 |
. . . . . . . . . . . . 13
  
            


     |
105 | 103, 104 | syl5eqelr 2534 |
. . . . . . . . . . . 12
  
            


  ![]_ ]_](_urbrack.gif)      |
106 | | nfcv 2592 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  |
107 | 106, 93, 97 | cbvmpt 4494 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
108 | 69 | adantrr 723 |
. . . . . . . . . . . . . 14
  
            
  |
109 | 54 | ralrimiva 2802 |
. . . . . . . . . . . . . . 15
  
     |
110 | 109 | ad2antrr 732 |
. . . . . . . . . . . . . 14
  
            


     |
111 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
   |
112 | 111, 74 | nfmpt 4491 |
. . . . . . . . . . . . . . . 16
     ![]_ ]_](_urbrack.gif)   |
113 | 112 | nfel1 2606 |
. . . . . . . . . . . . . . 15
     ![]_ ]_](_urbrack.gif)     |
114 | 76 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . 16
      ![]_ ]_](_urbrack.gif)    |
115 | 114 | eleq1d 2513 |
. . . . . . . . . . . . . . 15
         ![]_ ]_](_urbrack.gif)       |
116 | 113, 115 | rspc 3144 |
. . . . . . . . . . . . . 14
  

      ![]_ ]_](_urbrack.gif)       |
117 | 108, 110,
116 | sylc 62 |
. . . . . . . . . . . . 13
  
            

  ![]_ ]_](_urbrack.gif)      |
118 | 107, 117 | syl5eqelr 2534 |
. . . . . . . . . . . 12
  
            

  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      |
119 | 30 | addcn 21897 |
. . . . . . . . . . . . 13
     |
120 | 119 | a1i 11 |
. . . . . . . . . . . 12
  
            
      |
121 | 101, 105,
118, 120 | cnmpt12f 20681 |
. . . . . . . . . . 11
  
            

 
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)       |
122 | 100, 121 | eqeltrd 2529 |
. . . . . . . . . 10
  
            

           |
123 | 122 | exp32 610 |
. . . . . . . . 9
 
        
  

             |
124 | 123 | a2d 29 |
. . . . . . . 8
 
                 
              |
125 | 40, 124 | syl5 33 |
. . . . . . 7
 
        
                   |
126 | 125 | expcom 437 |
. . . . . 6
 
 
          
               |
127 | 126 | adantl 468 |
. . . . 5
 

        
                    |
128 | 127 | a2d 29 |
. . . 4
 

               
               |
129 | 8, 14, 20, 26, 36, 128 | findcard2s 7812 |
. . 3
            |
130 | 2, 129 | mpcom 37 |
. 2
          |
131 | 1, 130 | mpi 20 |
1
        |