Step | Hyp | Ref
| Expression |
1 | | ssid 3451 |
. 2
 |
2 | | dvmptfsum.i |
. . 3
   |
3 | | sseq1 3453 |
. . . . . 6


   |
4 | | sumeq1 13755 |
. . . . . . . . 9


   |
5 | 4 | mpteq2dv 4490 |
. . . . . . . 8

 
      |
6 | 5 | oveq2d 6306 |
. . . . . . 7

            |
7 | | sumeq1 13755 |
. . . . . . . 8


   |
8 | 7 | mpteq2dv 4490 |
. . . . . . 7

 
      |
9 | 6, 8 | eqeq12d 2466 |
. . . . . 6

   
   
            |
10 | 3, 9 | imbi12d 322 |
. . . . 5

 
  
   
               |
11 | 10 | imbi2d 318 |
. . . 4

    
        

             |
12 | | sseq1 3453 |
. . . . . 6
 
   |
13 | | sumeq1 13755 |
. . . . . . . . 9
 
   |
14 | 13 | mpteq2dv 4490 |
. . . . . . . 8
     
   |
15 | 14 | oveq2d 6306 |
. . . . . . 7
             |
16 | | sumeq1 13755 |
. . . . . . . 8
 
   |
17 | 16 | mpteq2dv 4490 |
. . . . . . 7
     
   |
18 | 15, 17 | eqeq12d 2466 |
. . . . . 6
           
         |
19 | 12, 18 | imbi12d 322 |
. . . . 5
           

            |
20 | 19 | imbi2d 318 |
. . . 4
  
           
              |
21 | | sseq1 3453 |
. . . . . 6
             |
22 | | sumeq1 13755 |
. . . . . . . . 9
              |
23 | 22 | mpteq2dv 4490 |
. . . . . . . 8
                  |
24 | 23 | oveq2d 6306 |
. . . . . . 7
      
               |
25 | | sumeq1 13755 |
. . . . . . . 8
              |
26 | 25 | mpteq2dv 4490 |
. . . . . . 7
                  |
27 | 24, 26 | eqeq12d 2466 |
. . . . . 6
             
                     |
28 | 21, 27 | imbi12d 322 |
. . . . 5
               
                           |
29 | 28 | imbi2d 318 |
. . . 4
                 
                             |
30 | | sseq1 3453 |
. . . . . 6
 
   |
31 | | sumeq1 13755 |
. . . . . . . . 9
 
   |
32 | 31 | mpteq2dv 4490 |
. . . . . . . 8
     
   |
33 | 32 | oveq2d 6306 |
. . . . . . 7
             |
34 | | sumeq1 13755 |
. . . . . . . 8
 
   |
35 | 34 | mpteq2dv 4490 |
. . . . . . 7
     
   |
36 | 33, 35 | eqeq12d 2466 |
. . . . . 6
           
         |
37 | 30, 36 | imbi12d 322 |
. . . . 5
           

            |
38 | 37 | imbi2d 318 |
. . . 4
  
           
              |
39 | | dvmptfsum.s |
. . . . . . 7
      |
40 | | 0cnd 9636 |
. . . . . . 7
 
   |
41 | | 0cnd 9636 |
. . . . . . . 8
   |
42 | 39, 41 | dvmptc 22912 |
. . . . . . 7
         |
43 | | dvmptfsum.j |
. . . . . . . . 9

↾t   |
44 | | dvmptfsum.k |
. . . . . . . . . . 11
  ℂfld |
45 | 44 | cnfldtopon 21803 |
. . . . . . . . . 10
TopOn   |
46 | | recnprss 22859 |
. . . . . . . . . . 11
   
  |
47 | 39, 46 | syl 17 |
. . . . . . . . . 10

  |
48 | | resttopon 20177 |
. . . . . . . . . 10
  TopOn 

 ↾t  TopOn    |
49 | 45, 47, 48 | sylancr 669 |
. . . . . . . . 9
 
↾t  TopOn    |
50 | 43, 49 | syl5eqel 2533 |
. . . . . . . 8
 TopOn    |
51 | | dvmptfsum.x |
. . . . . . . 8
   |
52 | | toponss 19944 |
. . . . . . . 8
  TopOn     |
53 | 50, 51, 52 | syl2anc 667 |
. . . . . . 7

  |
54 | 39, 40, 40, 42, 53, 43, 44, 51 | dvmptres 22917 |
. . . . . 6
         |
55 | | sum0 13787 |
. . . . . . . 8
  |
56 | 55 | mpteq2i 4486 |
. . . . . . 7
      |
57 | 56 | oveq2i 6301 |
. . . . . 6
          |
58 | | sum0 13787 |
. . . . . . 7
  |
59 | 58 | mpteq2i 4486 |
. . . . . 6
      |
60 | 54, 57, 59 | 3eqtr4g 2510 |
. . . . 5
           |
61 | 60 | a1d 26 |
. . . 4
 
           |
62 | | ssun1 3597 |
. . . . . . . . . 10
     |
63 | | sstr 3440 |
. . . . . . . . . 10
 
        
  |
64 | 62, 63 | mpan 676 |
. . . . . . . . 9
    
  |
65 | 64 | imim1i 60 |
. . . . . . . 8
 
  
   
 
                |
66 | | simpll 760 |
. . . . . . . . . . . . 13
  
                  |
67 | 66, 39 | syl 17 |
. . . . . . . . . . . 12
  
                 
   |
68 | 2 | ad3antrrr 736 |
. . . . . . . . . . . . . . 15
   

    
   |
69 | 64 | ad2antlr 733 |
. . . . . . . . . . . . . . 15
   

    

  |
70 | | ssfi 7792 |
. . . . . . . . . . . . . . 15
     |
71 | 68, 69, 70 | syl2anc 667 |
. . . . . . . . . . . . . 14
   

    
   |
72 | | simp-4l 776 |
. . . . . . . . . . . . . . 15
         


   |
73 | 69 | sselda 3432 |
. . . . . . . . . . . . . . 15
         


   |
74 | | simplr 762 |
. . . . . . . . . . . . . . 15
         


   |
75 | | nfv 1761 |
. . . . . . . . . . . . . . . . 17
  
  |
76 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . . . 18
  
 ![]_ ]_](_urbrack.gif)  |
77 | 76 | nfel1 2606 |
. . . . . . . . . . . . . . . . 17
  
 ![]_ ]_](_urbrack.gif)
 |
78 | 75, 77 | nfim 2003 |
. . . . . . . . . . . . . . . 16
   
   ![]_ ]_](_urbrack.gif)
  |
79 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . 18
 
   |
80 | 79 | 3anbi3d 1345 |
. . . . . . . . . . . . . . . . 17
  


    |
81 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
82 | 81 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
 
  ![]_ ]_](_urbrack.gif)    |
83 | 80, 82 | imbi12d 322 |
. . . . . . . . . . . . . . . 16
   
   
   ![]_ ]_](_urbrack.gif)
    |
84 | | dvmptfsum.a |
. . . . . . . . . . . . . . . 16
 

  |
85 | 78, 83, 84 | chvar 2106 |
. . . . . . . . . . . . . . 15
 

  ![]_ ]_](_urbrack.gif)   |
86 | 72, 73, 74, 85 | syl3anc 1268 |
. . . . . . . . . . . . . 14
         


   ![]_ ]_](_urbrack.gif)   |
87 | 71, 86 | fsumcl 13799 |
. . . . . . . . . . . . 13
   

    
    ![]_ ]_](_urbrack.gif)
  |
88 | 87 | adantlrr 727 |
. . . . . . . . . . . 12
   

              
    ![]_ ]_](_urbrack.gif)
  |
89 | | sumex 13754 |
. . . . . . . . . . . . 13

  ![]_ ]_](_urbrack.gif)  |
90 | 89 | a1i 11 |
. . . . . . . . . . . 12
   

              
    ![]_ ]_](_urbrack.gif)
  |
91 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
    |
92 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . 18
   |
93 | 92, 76 | nfsum 13757 |
. . . . . . . . . . . . . . . . 17
     ![]_ ]_](_urbrack.gif)  |
94 | 81 | sumeq2sdv 13770 |
. . . . . . . . . . . . . . . . 17
 
   ![]_ ]_](_urbrack.gif)   |
95 | 91, 93, 94 | cbvmpt 4494 |
. . . . . . . . . . . . . . . 16
 
     ![]_ ]_](_urbrack.gif)   |
96 | 95 | oveq2i 6301 |
. . . . . . . . . . . . . . 15
          ![]_ ]_](_urbrack.gif)    |
97 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
    |
98 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . . 17
  
 ![]_ ]_](_urbrack.gif)  |
99 | 92, 98 | nfsum 13757 |
. . . . . . . . . . . . . . . 16
     ![]_ ]_](_urbrack.gif)  |
100 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif)   |
101 | 100 | sumeq2sdv 13770 |
. . . . . . . . . . . . . . . 16
 
   ![]_ ]_](_urbrack.gif)   |
102 | 97, 99, 101 | cbvmpt 4494 |
. . . . . . . . . . . . . . 15
 
     ![]_ ]_](_urbrack.gif)   |
103 | 96, 102 | eqeq12i 2465 |
. . . . . . . . . . . . . 14
   
   
   
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
104 | 103 | biimpi 198 |
. . . . . . . . . . . . 13
   
   
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
105 | 104 | ad2antll 735 |
. . . . . . . . . . . 12
  
                     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
106 | | simplll 768 |
. . . . . . . . . . . . . 14
   

    
   |
107 | | ssun2 3598 |
. . . . . . . . . . . . . . . . 17
 
     |
108 | | sstr 3440 |
. . . . . . . . . . . . . . . . 17
              
  |
109 | 107, 108 | mpan 676 |
. . . . . . . . . . . . . . . 16
         |
110 | | vex 3048 |
. . . . . . . . . . . . . . . . 17
 |
111 | 110 | snss 4096 |
. . . . . . . . . . . . . . . 16

    |
112 | 109, 111 | sylibr 216 |
. . . . . . . . . . . . . . 15
       |
113 | 112 | ad2antlr 733 |
. . . . . . . . . . . . . 14
   

    
   |
114 | | simpr 463 |
. . . . . . . . . . . . . 14
   

    
   |
115 | 84 | 3expb 1209 |
. . . . . . . . . . . . . . . . 17
 

 
  |
116 | 115 | ancom2s 811 |
. . . . . . . . . . . . . . . 16
 

 
  |
117 | 116 | ralrimivva 2809 |
. . . . . . . . . . . . . . 15
  
  |
118 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . . . 18
  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
119 | 118 | nfel1 2606 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
 |
120 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
121 | 120 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
   |
122 | 77, 119, 82, 121 | rspc2 3158 |
. . . . . . . . . . . . . . . 16
 
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
   |
123 | 122 | ancoms 455 |
. . . . . . . . . . . . . . 15
 
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
   |
124 | 117, 123 | mpan9 472 |
. . . . . . . . . . . . . 14
 

  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  |
125 | 106, 113,
114, 124 | syl12anc 1266 |
. . . . . . . . . . . . 13
   

    
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  |
126 | 125 | adantlrr 727 |
. . . . . . . . . . . 12
   

              
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  |
127 | | dvmptfsum.b |
. . . . . . . . . . . . . . . . . 18
 

  |
128 | 127 | 3expb 1209 |
. . . . . . . . . . . . . . . . 17
 

 
  |
129 | 128 | ancom2s 811 |
. . . . . . . . . . . . . . . 16
 

 
  |
130 | 129 | ralrimivva 2809 |
. . . . . . . . . . . . . . 15
  
  |
131 | 98 | nfel1 2606 |
. . . . . . . . . . . . . . . . 17
  
 ![]_ ]_](_urbrack.gif)
 |
132 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . . . 18
  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
133 | 132 | nfel1 2606 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
 |
134 | 100 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
 
  ![]_ ]_](_urbrack.gif)    |
135 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
136 | 135 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
   |
137 | 131, 133,
134, 136 | rspc2 3158 |
. . . . . . . . . . . . . . . 16
 
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
   |
138 | 137 | ancoms 455 |
. . . . . . . . . . . . . . 15
 
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
   |
139 | 130, 138 | mpan9 472 |
. . . . . . . . . . . . . 14
 

  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  |
140 | 106, 113,
114, 139 | syl12anc 1266 |
. . . . . . . . . . . . 13
   

    
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  |
141 | 140 | adantlrr 727 |
. . . . . . . . . . . 12
   

              
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  |
142 | 112 | ad2antrl 734 |
. . . . . . . . . . . . 13
  
                  |
143 | | nfv 1761 |
. . . . . . . . . . . . . . . 16
     |
144 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . 18
   |
145 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . 18
  |
146 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . 19
   |
147 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]_ ]_](_urbrack.gif)  |
148 | 146, 147 | nfmpt 4491 |
. . . . . . . . . . . . . . . . . 18
     ![]_ ]_](_urbrack.gif)   |
149 | 144, 145,
148 | nfov 6316 |
. . . . . . . . . . . . . . . . 17
      ![]_ ]_](_urbrack.gif)    |
150 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . . . 18
  
 ![]_ ]_](_urbrack.gif)  |
151 | 146, 150 | nfmpt 4491 |
. . . . . . . . . . . . . . . . 17
     ![]_ ]_](_urbrack.gif)   |
152 | 149, 151 | nfeq 2603 |
. . . . . . . . . . . . . . . 16
      ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   |
153 | 143, 152 | nfim 2003 |
. . . . . . . . . . . . . . 15
   
     ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
154 | | eleq1 2517 |
. . . . . . . . . . . . . . . . 17
 
   |
155 | 154 | anbi2d 710 |
. . . . . . . . . . . . . . . 16
  

     |
156 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)   |
157 | 156 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . . . 18
      ![]_ ]_](_urbrack.gif)    |
158 | 157 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
      
  ![]_ ]_](_urbrack.gif)     |
159 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
160 | 159 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . . 17
      ![]_ ]_](_urbrack.gif)    |
161 | 158, 160 | eqeq12d 2466 |
. . . . . . . . . . . . . . . 16
         
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)     |
162 | 155, 161 | imbi12d 322 |
. . . . . . . . . . . . . . 15
   
       
  
    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)      |
163 | | dvmptfsum.d |
. . . . . . . . . . . . . . 15
 
         |
164 | 153, 162,
163 | chvar 2106 |
. . . . . . . . . . . . . 14
 
     ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
165 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
  
 ![]_ ]_](_urbrack.gif)  |
166 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
   |
167 | 166, 76 | nfcsb 3381 |
. . . . . . . . . . . . . . . 16
  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
168 | 81 | csbeq2dv 3781 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
169 | 165, 167,
168 | cbvmpt 4494 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
170 | 169 | oveq2i 6301 |
. . . . . . . . . . . . . 14
    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
171 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
  
 ![]_ ]_](_urbrack.gif)  |
172 | 166, 98 | nfcsb 3381 |
. . . . . . . . . . . . . . 15
  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
173 | 100 | csbeq2dv 3781 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
174 | 171, 172,
173 | cbvmpt 4494 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
175 | 164, 170,
174 | 3eqtr3g 2508 |
. . . . . . . . . . . . 13
 
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
176 | 66, 142, 175 | syl2anc 667 |
. . . . . . . . . . . 12
  
                    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
177 | 67, 88, 90, 105, 126, 141, 176 | dvmptadd 22914 |
. . . . . . . . . . 11
  
                      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
178 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
         |
179 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
       |
180 | 179, 76 | nfsum 13757 |
. . . . . . . . . . . . . . 15
          ![]_ ]_](_urbrack.gif)  |
181 | 81 | sumeq2sdv 13770 |
. . . . . . . . . . . . . . 15
               ![]_ ]_](_urbrack.gif)   |
182 | 178, 180,
181 | cbvmpt 4494 |
. . . . . . . . . . . . . 14
                 ![]_ ]_](_urbrack.gif)   |
183 | | simpllr 769 |
. . . . . . . . . . . . . . . . . 18
   

    
   |
184 | | disjsn 4032 |
. . . . . . . . . . . . . . . . . 18
    
  |
185 | 183, 184 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
   

    
       |
186 | | eqidd 2452 |
. . . . . . . . . . . . . . . . 17
   

    
           |
187 | | simplr 762 |
. . . . . . . . . . . . . . . . . 18
   

    
       |
188 | | ssfi 7792 |
. . . . . . . . . . . . . . . . . 18
             |
189 | 68, 187, 188 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
   

    
       |
190 | | simp-4l 776 |
. . . . . . . . . . . . . . . . . 18
         


       |
191 | 187 | sselda 3432 |
. . . . . . . . . . . . . . . . . 18
         


       |
192 | | simplr 762 |
. . . . . . . . . . . . . . . . . 18
         


       |
193 | 190, 191,
192, 85 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
         


       ![]_ ]_](_urbrack.gif)
  |
194 | 185, 186,
189, 193 | fsumsplit 13806 |
. . . . . . . . . . . . . . . 16
   

    
         ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)    |
195 | | sumsns 13811 |
. . . . . . . . . . . . . . . . . 18
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
196 | 110, 125,
195 | sylancr 669 |
. . . . . . . . . . . . . . . . 17
   

    
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
197 | 196 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
   

    
     ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
198 | 194, 197 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
   

    
         ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
199 | 198 | mpteq2dva 4489 |
. . . . . . . . . . . . . 14
  
               ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
200 | 182, 199 | syl5eq 2497 |
. . . . . . . . . . . . 13
  
                   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
201 | 200 | adantrr 723 |
. . . . . . . . . . . 12
  
                          
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
202 | 201 | oveq2d 6306 |
. . . . . . . . . . 11
  
                 
           
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      |
203 | | nfcv 2592 |
. . . . . . . . . . . . . 14
         |
204 | 179, 98 | nfsum 13757 |
. . . . . . . . . . . . . 14
          ![]_ ]_](_urbrack.gif)  |
205 | 100 | sumeq2sdv 13770 |
. . . . . . . . . . . . . 14
               ![]_ ]_](_urbrack.gif)   |
206 | 203, 204,
205 | cbvmpt 4494 |
. . . . . . . . . . . . 13
                 ![]_ ]_](_urbrack.gif)   |
207 | 75, 131 | nfim 2003 |
. . . . . . . . . . . . . . . . . 18
   
   ![]_ ]_](_urbrack.gif)
  |
208 | 80, 134 | imbi12d 322 |
. . . . . . . . . . . . . . . . . 18
   
   
   ![]_ ]_](_urbrack.gif)
    |
209 | 207, 208,
127 | chvar 2106 |
. . . . . . . . . . . . . . . . 17
 

  ![]_ ]_](_urbrack.gif)   |
210 | 190, 191,
192, 209 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
         


       ![]_ ]_](_urbrack.gif)
  |
211 | 185, 186,
189, 210 | fsumsplit 13806 |
. . . . . . . . . . . . . . 15
   

    
         ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)    |
212 | | sumsns 13811 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
213 | 110, 140,
212 | sylancr 669 |
. . . . . . . . . . . . . . . 16
   

    
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
214 | 213 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
   

    
     ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
215 | 211, 214 | eqtrd 2485 |
. . . . . . . . . . . . . 14
   

    
         ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
216 | 215 | mpteq2dva 4489 |
. . . . . . . . . . . . 13
  
               ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
217 | 206, 216 | syl5eq 2497 |
. . . . . . . . . . . 12
  
                   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
218 | 217 | adantrr 723 |
. . . . . . . . . . 11
  
                          
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
219 | 177, 202,
218 | 3eqtr4d 2495 |
. . . . . . . . . 10
  
                 
                  |
220 | 219 | exp32 610 |
. . . . . . . . 9
 
                                     |
221 | 220 | a2d 29 |
. . . . . . . 8
 
                                           |
222 | 65, 221 | syl5 33 |
. . . . . . 7
 
                  
                    |
223 | 222 | expcom 437 |
. . . . . 6
 
 
  
   
 
                            |
224 | 223 | adantl 468 |
. . . . 5
 

    
                                   |
225 | 224 | a2d 29 |
. . . 4
 

    
               
                     |
226 | 11, 20, 29, 38, 61, 225 | findcard2s 7812 |
. . 3
    
          |
227 | 2, 226 | mpcom 37 |
. 2
             |
228 | 1, 227 | mpi 20 |
1
           |