Step | Hyp | Ref
| Expression |
1 | | esumeq1 28906 |
. . 3

Σ* Σ*  Σ* Σ*    |
2 | | nfv 1772 |
. . . 4
  |
3 | | iuneq1 4306 |
. . . 4


           |
4 | 2, 3 | esumeq1d 28907 |
. . 3

Σ* 
     Σ*         |
5 | 1, 4 | eqeq12d 2477 |
. 2

Σ* Σ*  Σ* 
    
Σ* Σ*  Σ*          |
6 | | esumeq1 28906 |
. . 3

Σ* Σ*  Σ* Σ*    |
7 | | nfv 1772 |
. . . 4
  |
8 | | iuneq1 4306 |
. . . 4
 
    
      |
9 | 7, 8 | esumeq1d 28907 |
. . 3

Σ* 
     Σ*         |
10 | 6, 9 | eqeq12d 2477 |
. 2
 Σ* Σ*  Σ* 
    
Σ* Σ*  Σ*          |
11 | | esumeq1 28906 |
. . 3
     Σ* Σ*  Σ*     Σ*    |
12 | | nfv 1772 |
. . . 4
      |
13 | | iuneq1 4306 |
. . . 4
                      |
14 | 12, 13 | esumeq1d 28907 |
. . 3
     Σ* 
     Σ*              |
15 | 11, 14 | eqeq12d 2477 |
. 2
     Σ* Σ*  Σ*       Σ*     Σ*  Σ*               |
16 | | esumeq1 28906 |
. . 3

Σ* Σ*  Σ* Σ*    |
17 | | nfv 1772 |
. . . 4
  |
18 | | iuneq1 4306 |
. . . 4
 
    
      |
19 | 17, 18 | esumeq1d 28907 |
. . 3

Σ* 
     Σ*         |
20 | 16, 19 | eqeq12d 2477 |
. 2
 Σ* Σ*  Σ* 
    
Σ* Σ*  Σ*          |
21 | | esumnul 28920 |
. . . 4
Σ* 
 |
22 | | 0iun 4349 |
. . . . 5
      |
23 | | esumeq1 28906 |
. . . . 5
 
   
Σ* 
     Σ*    |
24 | 22, 23 | ax-mp 5 |
. . . 4
Σ* 
     Σ*   |
25 | | esumnul 28920 |
. . . 4
Σ* Σ*   |
26 | 21, 24, 25 | 3eqtr4ri 2495 |
. . 3
Σ* Σ*  Σ*        |
27 | 26 | a1i 11 |
. 2
 Σ* Σ*  Σ*         |
28 | | simpr 467 |
. . . . 5
   
    Σ* Σ*  Σ*       
Σ* Σ*  Σ*         |
29 | | nfcsb1v 3391 |
. . . . . . . . 9
  
 ![]_ ]_](_urbrack.gif)  |
30 | | nfcsb1v 3391 |
. . . . . . . . 9
  
 ![]_ ]_](_urbrack.gif)  |
31 | 29, 30 | nfesum2 28913 |
. . . . . . . 8
 Σ*   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  |
32 | | csbeq1a 3384 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)   |
33 | | csbeq1a 3384 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)   |
34 | 32, 33 | esumeq12d 28905 |
. . . . . . . . 9

Σ* 
Σ*   ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)   |
35 | 34 | adantl 472 |
. . . . . . . 8
   
    
Σ* 
Σ*   ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)   |
36 | | simprr 771 |
. . . . . . . 8
 
         |
37 | | difss 3572 |
. . . . . . . . . . 11
   |
38 | 37, 36 | sseldi 3442 |
. . . . . . . . . 10
 
       |
39 | | esum2d.3 |
. . . . . . . . . . . 12
 
   |
40 | 39 | adantlr 726 |
. . . . . . . . . . 11
   
    
  |
41 | 40 | ralrimiva 2814 |
. . . . . . . . . 10
 
     
  |
42 | | rspcsbela 3807 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)   |
43 | 38, 41, 42 | syl2anc 671 |
. . . . . . . . 9
 
     
 ![]_ ]_](_urbrack.gif)
  |
44 | | simpll 765 |
. . . . . . . . . . 11
   
      ![]_ ]_](_urbrack.gif) 
  |
45 | 38 | adantr 471 |
. . . . . . . . . . 11
   
      ![]_ ]_](_urbrack.gif) 
  |
46 | | simpr 467 |
. . . . . . . . . . 11
   
      ![]_ ]_](_urbrack.gif) 
  ![]_ ]_](_urbrack.gif)   |
47 | | esum2d.4 |
. . . . . . . . . . . . . . 15
 

 
     |
48 | 47 | ex 440 |
. . . . . . . . . . . . . 14
          |
49 | 48 | sbcimdv 3341 |
. . . . . . . . . . . . 13
    ![]. ].](_drbrack.gif)     ![]. ].](_drbrack.gif)       |
50 | | sbcan 3322 |
. . . . . . . . . . . . . 14
   ![]. ].](_drbrack.gif) 
    ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)
   |
51 | | sbcel1v 3338 |
. . . . . . . . . . . . . . 15
   ![]. ].](_drbrack.gif)
  |
52 | | sbcel2 3790 |
. . . . . . . . . . . . . . 15
   ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
53 | 51, 52 | anbi12i 708 |
. . . . . . . . . . . . . 14
    ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
54 | 50, 53 | bitri 257 |
. . . . . . . . . . . . 13
   ![]. ].](_drbrack.gif) 
 
  ![]_ ]_](_urbrack.gif)    |
55 | | vex 3060 |
. . . . . . . . . . . . . 14
 |
56 | | sbcel1g 3788 |
. . . . . . . . . . . . . 14
  
 ![]. ].](_drbrack.gif)
 
   ![]_ ]_](_urbrack.gif)
      |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . 13
   ![]. ].](_drbrack.gif)      ![]_ ]_](_urbrack.gif)
 
   |
58 | 49, 54, 57 | 3imtr3g 277 |
. . . . . . . . . . . 12
     ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)       |
59 | 58 | imp 435 |
. . . . . . . . . . 11
 

  ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)
 
   |
60 | 44, 45, 46, 59 | syl12anc 1274 |
. . . . . . . . . 10
   
      ![]_ ]_](_urbrack.gif) 
  ![]_ ]_](_urbrack.gif)      |
61 | 60 | ralrimiva 2814 |
. . . . . . . . 9
 
     
 ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)
 
   |
62 | | nfcv 2603 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)  |
63 | 62 | esumcl 28902 |
. . . . . . . . 9
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)
 
 
Σ*   ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)
 
   |
64 | 43, 61, 63 | syl2anc 671 |
. . . . . . . 8
 
     Σ*   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      |
65 | 31, 35, 36, 64 | esumsnf 28936 |
. . . . . . 7
 
     Σ*   Σ*  Σ*   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
66 | | esum2d.0 |
. . . . . . . . 9
   |
67 | | nfv 1772 |
. . . . . . . . 9
   
     |
68 | | nfv 1772 |
. . . . . . . . . . 11
     |
69 | 30 | nfeq2 2618 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)  |
70 | 68, 69 | nfim 2014 |
. . . . . . . . . 10
        ![]_ ]_](_urbrack.gif)   |
71 | | opeq1 4180 |
. . . . . . . . . . . 12
         |
72 | 71 | eqeq2d 2472 |
. . . . . . . . . . 11
    
      |
73 | 33 | eqeq2d 2472 |
. . . . . . . . . . 11
 
  ![]_ ]_](_urbrack.gif)    |
74 | 72, 73 | imbi12d 326 |
. . . . . . . . . 10
      
      ![]_ ]_](_urbrack.gif)     |
75 | | esum2d.1 |
. . . . . . . . . 10
      |
76 | 70, 74, 75 | chvar 2117 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)   |
77 | | ssnid 4009 |
. . . . . . . . . . . . . . . . . 18
   |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . 17
         |
79 | | simpr 467 |
. . . . . . . . . . . . . . . . 17
       |
80 | 78, 79 | jca 539 |
. . . . . . . . . . . . . . . 16
           |
81 | | opelxp 4886 |
. . . . . . . . . . . . . . . 16
       
  
   |
82 | 80, 81 | sylibr 217 |
. . . . . . . . . . . . . . 15
              |
83 | | xp2nd 6856 |
. . . . . . . . . . . . . . . . 17
           |
84 | 83 | adantl 472 |
. . . . . . . . . . . . . . . 16
               |
85 | | eqop 6865 |
. . . . . . . . . . . . . . . . . . . 20
                      |
86 | | xp1st 6855 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
87 | | fvex 5902 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
88 | 87 | elsnc 4004 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
89 | 86, 88 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . 21
           |
90 | 89 | biantrurd 515 |
. . . . . . . . . . . . . . . . . . . 20
                       |
91 | 85, 90 | bitr4d 264 |
. . . . . . . . . . . . . . . . . . 19
                |
92 | | eqcom 2469 |
. . . . . . . . . . . . . . . . . . 19
    
      |
93 | 91, 92 | syl6bb 269 |
. . . . . . . . . . . . . . . . . 18
                |
94 | 93 | ad2antlr 738 |
. . . . . . . . . . . . . . . . 17
   

    
    
       |
95 | 94 | ralrimiva 2814 |
. . . . . . . . . . . . . . . 16
             
       |
96 | | reu6i 3241 |
. . . . . . . . . . . . . . . 16
          
      
     |
97 | 84, 95, 96 | syl2anc 671 |
. . . . . . . . . . . . . . 15
               |
98 | 82, 97 | f1mptrn 28285 |
. . . . . . . . . . . . . 14
 
         |
99 | 98 | ex 440 |
. . . . . . . . . . . . 13
           |
100 | 99 | sbcimdv 3341 |
. . . . . . . . . . . 12
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)          |
101 | | sbcfung 5628 |
. . . . . . . . . . . . . . 15
  
 ![]. ].](_drbrack.gif)       
 ![]_ ]_](_urbrack.gif)          |
102 | | csbcnv 5040 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)        |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)         |
104 | | csbmpt12 4752 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)       |
105 | | csbopg 4198 |
. . . . . . . . . . . . . . . . . . . . 21
   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 
  ![]_ ]_](_urbrack.gif)    |
106 | | csbvarg 3804 |
. . . . . . . . . . . . . . . . . . . . . 22
   ![]_ ]_](_urbrack.gif)   |
107 | | csbconstg 3388 |
. . . . . . . . . . . . . . . . . . . . . 22
   ![]_ ]_](_urbrack.gif)   |
108 | 106, 107 | opeq12d 4188 |
. . . . . . . . . . . . . . . . . . . . 21
    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
     |
109 | 105, 108 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . 20
   ![]_ ]_](_urbrack.gif)         |
110 | 109 | mpteq2dv 4506 |
. . . . . . . . . . . . . . . . . . 19
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    
   ![]_ ]_](_urbrack.gif)       |
111 | 104, 110 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       |
112 | 111 | cnveqd 5032 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)       |
113 | 103, 112 | eqtr3d 2498 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       |
114 | 113 | funeqd 5626 |
. . . . . . . . . . . . . . 15
    ![]_ ]_](_urbrack.gif)      
    ![]_ ]_](_urbrack.gif)        |
115 | 101, 114 | bitrd 261 |
. . . . . . . . . . . . . 14
  
 ![]. ].](_drbrack.gif)           ![]_ ]_](_urbrack.gif)
       |
116 | 55, 115 | ax-mp 5 |
. . . . . . . . . . . . 13
   ![]. ].](_drbrack.gif)           ![]_ ]_](_urbrack.gif)       |
117 | 51, 116 | imbi12i 332 |
. . . . . . . . . . . 12
    ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)        
    ![]_ ]_](_urbrack.gif)        |
118 | 100, 117 | sylib 201 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)        |
119 | 118 | imp 435 |
. . . . . . . . . 10
 
     ![]_ ]_](_urbrack.gif)       |
120 | 38, 119 | syldan 477 |
. . . . . . . . 9
 
         ![]_ ]_](_urbrack.gif)
      |
121 | 55 | snid 4008 |
. . . . . . . . . . . 12
   |
122 | 121 | a1i 11 |
. . . . . . . . . . 11
   
      ![]_ ]_](_urbrack.gif) 
    |
123 | 122, 46 | jca 539 |
. . . . . . . . . 10
   
      ![]_ ]_](_urbrack.gif) 
  
  ![]_ ]_](_urbrack.gif)    |
124 | | opelxp 4886 |
. . . . . . . . . 10
         ![]_ ]_](_urbrack.gif) 
  
  ![]_ ]_](_urbrack.gif)    |
125 | 123, 124 | sylibr 217 |
. . . . . . . . 9
   
      ![]_ ]_](_urbrack.gif) 
  
     ![]_ ]_](_urbrack.gif)    |
126 | 66, 67, 62, 76, 43, 120, 60, 125 | esumc 28923 |
. . . . . . . 8
 
     Σ*   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) Σ*  
 ![]_ ]_](_urbrack.gif)         |
127 | | nfab1 2605 |
. . . . . . . . . 10
   
 ![]_ ]_](_urbrack.gif)       |
128 | | nfcv 2603 |
. . . . . . . . . 10
       ![]_ ]_](_urbrack.gif)   |
129 | | opeq1 4180 |
. . . . . . . . . . . . . 14
         |
130 | 129 | eqeq2d 2472 |
. . . . . . . . . . . . 13
    
      |
131 | 130 | rexbidv 2913 |
. . . . . . . . . . . 12
  
 ![]_ ]_](_urbrack.gif)    
  ![]_ ]_](_urbrack.gif)        |
132 | 55, 131 | rexsn 4023 |
. . . . . . . . . . 11
       ![]_ ]_](_urbrack.gif)    
  ![]_ ]_](_urbrack.gif)       |
133 | | elxp2 4874 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)       |
134 | | abid 2450 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)     
  ![]_ ]_](_urbrack.gif)       |
135 | 132, 133,
134 | 3bitr4ri 286 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)     
     ![]_ ]_](_urbrack.gif)    |
136 | 127, 128,
135 | eqri 28203 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)   |
137 | | esumeq1 28906 |
. . . . . . . . 9
    ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif) 
Σ*    ![]_ ]_](_urbrack.gif)       Σ*
     ![]_ ]_](_urbrack.gif)     |
138 | 136, 137 | ax-mp 5 |
. . . . . . . 8
Σ*    ![]_ ]_](_urbrack.gif)       Σ*
     ![]_ ]_](_urbrack.gif)    |
139 | 126, 138 | syl6eq 2512 |
. . . . . . 7
 
     Σ*   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) Σ*      ![]_ ]_](_urbrack.gif)     |
140 | 65, 139 | eqtrd 2496 |
. . . . . 6
 
     Σ*   Σ*  Σ*      ![]_ ]_](_urbrack.gif)     |
141 | 140 | adantr 471 |
. . . . 5
   
    Σ* Σ*  Σ*       
Σ*   Σ*  Σ*      ![]_ ]_](_urbrack.gif)     |
142 | 28, 141 | oveq12d 6338 |
. . . 4
   
    Σ* Σ*  Σ*       
Σ* Σ*    Σ*   Σ*   Σ*         Σ*      ![]_ ]_](_urbrack.gif)      |
143 | | nfv 1772 |
. . . . . 6
   
     |
144 | | nfcv 2603 |
. . . . . 6
   |
145 | | nfcv 2603 |
. . . . . 6
     |
146 | | vex 3060 |
. . . . . . 7
 |
147 | 146 | a1i 11 |
. . . . . 6
 
       |
148 | | snex 4658 |
. . . . . . 7
   |
149 | 148 | a1i 11 |
. . . . . 6
 
         |
150 | 36 | eldifbd 3429 |
. . . . . . 7
 
    
  |
151 | | disjsn 4044 |
. . . . . . 7
    
  |
152 | 150, 151 | sylibr 217 |
. . . . . 6
 
           |
153 | | simpll 765 |
. . . . . . 7
   
    
  |
154 | | simprl 769 |
. . . . . . . 8
 
    
  |
155 | 154 | sselda 3444 |
. . . . . . 7
   
    
  |
156 | 47 | anassrs 658 |
. . . . . . . . 9
          |
157 | 156 | ralrimiva 2814 |
. . . . . . . 8
 
 
     |
158 | | nfcv 2603 |
. . . . . . . . 9
   |
159 | 158 | esumcl 28902 |
. . . . . . . 8
      
Σ* 
     |
160 | 39, 157, 159 | syl2anc 671 |
. . . . . . 7
 

Σ* 
     |
161 | 153, 155,
160 | syl2anc 671 |
. . . . . 6
   
    
Σ* 
     |
162 | | simpll 765 |
. . . . . . 7
   
         |
163 | 55 | snss 4109 |
. . . . . . . . 9

    |
164 | 38, 163 | sylib 201 |
. . . . . . . 8
 
         |
165 | 164 | sselda 3444 |
. . . . . . 7
   
         |
166 | 162, 165,
160 | syl2anc 671 |
. . . . . 6
   
       Σ*       |
167 | 143, 144,
145, 147, 149, 152, 161, 166 | esumsplit 28925 |
. . . . 5
 
     Σ*     Σ*  Σ* Σ*    Σ*   Σ*     |
168 | 167 | adantr 471 |
. . . 4
   
    Σ* Σ*  Σ*       
Σ*     Σ*  Σ* Σ*    Σ*   Σ*     |
169 | | iunxun 4377 |
. . . . . . . 8
                         |
170 | 145, 29 | nfxp 4883 |
. . . . . . . . . . 11
       ![]_ ]_](_urbrack.gif)   |
171 | | sneq 3990 |
. . . . . . . . . . . 12
       |
172 | 171, 32 | xpeq12d 4881 |
. . . . . . . . . . 11
          ![]_ ]_](_urbrack.gif)    |
173 | 170, 172 | iunxsngf 28227 |
. . . . . . . . . 10
             ![]_ ]_](_urbrack.gif)    |
174 | 55, 173 | ax-mp 5 |
. . . . . . . . 9
            ![]_ ]_](_urbrack.gif)   |
175 | 174 | uneq2i 3597 |
. . . . . . . 8
 
    
        
         ![]_ ]_](_urbrack.gif)    |
176 | 169, 175 | eqtri 2484 |
. . . . . . 7
                     ![]_ ]_](_urbrack.gif)    |
177 | | esumeq1 28906 |
. . . . . . 7
 
                    ![]_ ]_](_urbrack.gif)  
Σ* 
          Σ*  
         ![]_ ]_](_urbrack.gif)      |
178 | 176, 177 | ax-mp 5 |
. . . . . 6
Σ* 
          Σ*  
         ![]_ ]_](_urbrack.gif)     |
179 | | nfv 1772 |
. . . . . . 7
   
     |
180 | | nfcv 2603 |
. . . . . . 7
  
     |
181 | | nfcv 2603 |
. . . . . . 7
       ![]_ ]_](_urbrack.gif)   |
182 | | snex 4658 |
. . . . . . . . . 10
   |
183 | 155, 40 | syldan 477 |
. . . . . . . . . 10
   
    
  |
184 | | xpexg 6625 |
. . . . . . . . . 10
    
      |
185 | 182, 183,
184 | sylancr 674 |
. . . . . . . . 9
   
    
      |
186 | 185 | ralrimiva 2814 |
. . . . . . . 8
 
     
      |
187 | | iunexg 6801 |
. . . . . . . 8
               |
188 | 147, 186,
187 | syl2anc 671 |
. . . . . . 7
 
     
      |
189 | | xpexg 6625 |
. . . . . . . 8
      ![]_ ]_](_urbrack.gif) 
     ![]_ ]_](_urbrack.gif)    |
190 | 148, 43, 189 | sylancr 674 |
. . . . . . 7
 
          ![]_ ]_](_urbrack.gif)    |
191 | | simpr 467 |
. . . . . . . . . . . 12
   
    
  |
192 | 150 | adantr 471 |
. . . . . . . . . . . 12
   
    
  |
193 | | nelne2 2733 |
. . . . . . . . . . . 12
 

  |
194 | 191, 192,
193 | syl2anc 671 |
. . . . . . . . . . 11
   
    
  |
195 | | disjsn2 4045 |
. . . . . . . . . . 11
         |
196 | | xpdisj1 5280 |
. . . . . . . . . . 11
           
     ![]_ ]_](_urbrack.gif)     |
197 | 194, 195,
196 | 3syl 18 |
. . . . . . . . . 10
   
    
          ![]_ ]_](_urbrack.gif)     |
198 | 197 | ralrimiva 2814 |
. . . . . . . . 9
 
     
          ![]_ ]_](_urbrack.gif)     |
199 | | iuneq2 4309 |
. . . . . . . . 9
 
          ![]_ ]_](_urbrack.gif)  

          ![]_ ]_](_urbrack.gif)      |
200 | 198, 199 | syl 17 |
. . . . . . . 8
 
     
          ![]_ ]_](_urbrack.gif)   
  |
201 | 170 | iunin1f 28226 |
. . . . . . . 8

          ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    |
202 | | iun0 4348 |
. . . . . . . 8

 |
203 | 200, 201,
202 | 3eqtr3g 2519 |
. . . . . . 7
 
                ![]_ ]_](_urbrack.gif)     |
204 | | simpll 765 |
. . . . . . . 8
   
    
       |
205 | | iunss1 4304 |
. . . . . . . . . 10
 
   
       |
206 | 154, 205 | syl 17 |
. . . . . . . . 9
 
     
           |
207 | 206 | sselda 3444 |
. . . . . . . 8
   
    
     
      |
208 | | nfv 1772 |
. . . . . . . . . 10
   |
209 | | nfcv 2603 |
. . . . . . . . . . 11
   |
210 | | nfiu1 4322 |
. . . . . . . . . . 11
  
     |
211 | 209, 210 | nfel 2615 |
. . . . . . . . . 10
 
     |
212 | 208, 211 | nfan 2022 |
. . . . . . . . 9
          |
213 | | nfv 1772 |
. . . . . . . . . 10
     
            |
214 | | nfcv 2603 |
. . . . . . . . . . 11
      |
215 | 66, 214 | nfel 2615 |
. . . . . . . . . 10
     |
216 | 75 | adantl 472 |
. . . . . . . . . . 11
     
     

    

      |
217 | | simp-5l 783 |
. . . . . . . . . . . 12
     
     

    

      |
218 | | simp-4r 782 |
. . . . . . . . . . . 12
     
     

    

      |
219 | | simplr 767 |
. . . . . . . . . . . 12
     
     

    

      |
220 | 217, 218,
219, 47 | syl12anc 1274 |
. . . . . . . . . . 11
     
     

    

         |
221 | 216, 220 | eqeltrd 2540 |
. . . . . . . . . 10
     
     

    

         |
222 | | elsnxp 5401 |
. . . . . . . . . . . 12
      
      |
223 | 222 | biimpa 491 |
. . . . . . . . . . 11
 
     
     |
224 | 223 | adantll 725 |
. . . . . . . . . 10
   
            
     |
225 | 213, 215,
221, 224 | r19.29af2 2940 |
. . . . . . . . 9
   
                 |
226 | | simpr 467 |
. . . . . . . . . 10
 
      
      |
227 | | eliun 4297 |
. . . . . . . . . 10
      
      |
228 | 226, 227 | sylib 201 |
. . . . . . . . 9
 
      
      |
229 | 212, 225,
228 | r19.29af 2942 |
. . . . . . . 8
 
     
     |
230 | 204, 207,
229 | syl2anc 671 |
. . . . . . 7
   
    
    
     |
231 | | simpll 765 |
. . . . . . . 8
   
         ![]_ ]_](_urbrack.gif)     |
232 | | nfcv 2603 |
. . . . . . . . . . 11
   |
233 | | nfcv 2603 |
. . . . . . . . . . 11
   |
234 | 232, 233,
170, 172 | ssiun2sf 28229 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)  
      |
235 | 38, 234 | syl 17 |
. . . . . . . . 9
 
          ![]_ ]_](_urbrack.gif)         |
236 | 235 | sselda 3444 |
. . . . . . . 8
   
         ![]_ ]_](_urbrack.gif)   
      |
237 | 231, 236,
229 | syl2anc 671 |
. . . . . . 7
   
         ![]_ ]_](_urbrack.gif)  
     |
238 | 179, 180,
181, 188, 190, 203, 230, 237 | esumsplit 28925 |
. . . . . 6
 
     Σ*            ![]_ ]_](_urbrack.gif)    Σ* 
       Σ*      ![]_ ]_](_urbrack.gif)      |
239 | 178, 238 | syl5eq 2508 |
. . . . 5
 
     Σ*            Σ*         Σ*      ![]_ ]_](_urbrack.gif)      |
240 | 239 | adantr 471 |
. . . 4
   
    Σ* Σ*  Σ*       
Σ* 
          Σ* 
       Σ*      ![]_ ]_](_urbrack.gif)      |
241 | 142, 168,
240 | 3eqtr4d 2506 |
. . 3
   
    Σ* Σ*  Σ*       
Σ*     Σ*  Σ*              |
242 | 241 | ex 440 |
. 2
 
     Σ* Σ*  Σ*       Σ*     Σ*  Σ*               |
243 | | esum2dlem.e |
. 2
   |
244 | 5, 10, 15, 20, 27, 242, 243 | findcard2d 7844 |
1
 Σ* Σ*  Σ* 
       |