Step | Hyp | Ref
| Expression |
1 | | fvex 5898 |
. . . . 5
     |
2 | 1 | a1i 11 |
. . . 4
          |
3 | | fveq2 5888 |
. . . . . . . 8
                 |
4 | | df-ov 6318 |
. . . . . . . 8
            |
5 | 3, 4 | syl6eqr 2514 |
. . . . . . 7
              |
6 | 5 | eqeq2d 2472 |
. . . . . 6
        
       |
7 | 6 | biimpa 491 |
. . . . 5
         
      |
8 | | fsumvma.1 |
. . . . 5
       |
9 | 7, 8 | syl 17 |
. . . 4
         
  |
10 | 2, 9 | csbied 3402 |
. . 3
          ![]_ ]_](_urbrack.gif)
  |
11 | | fsumvma.4 |
. . 3
   |
12 | | fsumvma.2 |
. . . . 5
   |
13 | 12 | adantr 471 |
. . . 4
 
   |
14 | | fsumvma.5 |
. . . . . . . . 9
   
           |
15 | 14 | biimpd 212 |
. . . . . . . 8
               |
16 | 15 | impl 630 |
. . . . . . 7
               |
17 | 16 | simprd 469 |
. . . . . 6
           |
18 | 17 | ex 440 |
. . . . 5
 
         |
19 | 16 | simpld 465 |
. . . . . . . . 9
         |
20 | 19 | simpld 465 |
. . . . . . . 8
       |
21 | 20 | adantrr 728 |
. . . . . . 7
    
 
  |
22 | 19 | simprd 469 |
. . . . . . . 8
       |
23 | 22 | adantrr 728 |
. . . . . . 7
    
 
  |
24 | 22 | ex 440 |
. . . . . . . . . 10
 
     |
25 | 24 | ssrdv 3450 |
. . . . . . . . 9
 
   |
26 | 25 | sselda 3444 |
. . . . . . . 8
       |
27 | 26 | adantrl 727 |
. . . . . . 7
    
 
  |
28 | | eqid 2462 |
. . . . . . . 8
 |
29 | | prmexpb 14719 |
. . . . . . . . 9
      
        

    |
30 | 29 | baibd 925 |
. . . . . . . 8
       
             |
31 | 28, 30 | mpan2 682 |
. . . . . . 7
      
        
   |
32 | 21, 21, 23, 27, 31 | syl22anc 1277 |
. . . . . 6
    
 
        
   |
33 | 32 | ex 440 |
. . . . 5
 
  

        
    |
34 | 18, 33 | dom2lem 7635 |
. . . 4
 
             |
35 | | f1fi 7887 |
. . . 4
            
  |
36 | 13, 34, 35 | syl2anc 671 |
. . 3
 
   |
37 | 14 | simplbda 634 |
. . . 4
 

        |
38 | | fsumvma.6 |
. . . . . 6
 
   |
39 | 38 | ralrimiva 2814 |
. . . . 5
 
  |
40 | 39 | adantr 471 |
. . . 4
 

  
  |
41 | 8 | eleq1d 2524 |
. . . . 5
     
   |
42 | 41 | rspcv 3158 |
. . . 4
      
   |
43 | 37, 40, 42 | sylc 62 |
. . 3
 

 
  |
44 | 10, 11, 36, 43 | fsum2d 13881 |
. 2
 
 
           ![]_ ]_](_urbrack.gif)   |
45 | | nfcv 2603 |
. . . 4
   |
46 | | nfcsb1v 3391 |
. . . 4
  
 ![]_ ]_](_urbrack.gif)  |
47 | | csbeq1a 3384 |
. . . 4
   ![]_ ]_](_urbrack.gif)   |
48 | 45, 46, 47 | cbvsumi 13812 |
. . 3
               
            ![]_ ]_](_urbrack.gif)  |
49 | | csbeq1 3378 |
. . . 4
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
50 | | snfi 7676 |
. . . . . . 7
 
 |
51 | | xpfi 7868 |
. . . . . . 7
           |
52 | 50, 36, 51 | sylancr 674 |
. . . . . 6
 
       |
53 | 52 | ralrimiva 2814 |
. . . . 5
        |
54 | | iunfi 7888 |
. . . . 5
               |
55 | 11, 53, 54 | syl2anc 671 |
. . . 4
        |
56 | | fvex 5898 |
. . . . . . 7
     |
57 | 56 | 2a1i 12 |
. . . . . 6
  
           |
58 | | eliunxp 4991 |
. . . . . . . . 9
     
        
    |
59 | 14 | simprbda 633 |
. . . . . . . . . . . . . 14
 

      |
60 | | opelxp 4883 |
. . . . . . . . . . . . . 14
    
     |
61 | 59, 60 | sylibr 217 |
. . . . . . . . . . . . 13
 

     
   |
62 | | eleq1 2528 |
. . . . . . . . . . . . 13
     
    
    |
63 | 61, 62 | syl5ibrcom 230 |
. . . . . . . . . . . 12
 

      
    |
64 | 63 | impancom 446 |
. . . . . . . . . . 11
 
   
 
      |
65 | 64 | expimpd 612 |
. . . . . . . . . 10
      
  
    |
66 | 65 | exlimdvv 1791 |
. . . . . . . . 9
          
  
    |
67 | 58, 66 | syl5bi 225 |
. . . . . . . 8
  
    
    |
68 | 67 | ssrdv 3450 |
. . . . . . . . 9
          |
69 | 68 | sseld 3443 |
. . . . . . . 8
  
    
    |
70 | 67, 69 | anim12d 570 |
. . . . . . 7
               

      |
71 | | 1st2nd2 6857 |
. . . . . . . . . . 11
                |
72 | 71 | fveq2d 5892 |
. . . . . . . . . 10
                        |
73 | | df-ov 6318 |
. . . . . . . . . 10
                            |
74 | 72, 73 | syl6eqr 2514 |
. . . . . . . . 9
                     |
75 | | 1st2nd2 6857 |
. . . . . . . . . . 11
                |
76 | 75 | fveq2d 5892 |
. . . . . . . . . 10
                        |
77 | | df-ov 6318 |
. . . . . . . . . 10
                            |
78 | 76, 77 | syl6eqr 2514 |
. . . . . . . . 9
                     |
79 | 74, 78 | eqeqan12d 2478 |
. . . . . . . 8
    
          
                           |
80 | | xp1st 6850 |
. . . . . . . . . 10
         |
81 | | xp2nd 6851 |
. . . . . . . . . 10
         |
82 | 80, 81 | jca 539 |
. . . . . . . . 9
               |
83 | | xp1st 6850 |
. . . . . . . . . 10
         |
84 | | xp2nd 6851 |
. . . . . . . . . 10
         |
85 | 83, 84 | jca 539 |
. . . . . . . . 9
               |
86 | | prmexpb 14719 |
. . . . . . . . . 10
           
                                   
        
            |
87 | 86 | an4s 840 |
. . . . . . . . 9
                                                                     |
88 | 82, 85, 87 | syl2an 484 |
. . . . . . . 8
    
                          
        
            |
89 | | xpopth 6859 |
. . . . . . . 8
    
                    
   |
90 | 79, 88, 89 | 3bitrd 287 |
. . . . . . 7
    
          
   |
91 | 70, 90 | syl6 34 |
. . . . . 6
                           |
92 | 57, 91 | dom2lem 7635 |
. . . . 5
  
                    |
93 | | f1f1orn 5848 |
. . . . 5
  
                   
                               |
94 | 92, 93 | syl 17 |
. . . 4
  
                               |
95 | | fveq2 5888 |
. . . . . 6
           |
96 | | eqid 2462 |
. . . . . 6
                       |
97 | 95, 96, 1 | fvmpt 5971 |
. . . . 5
                           |
98 | 97 | adantl 472 |
. . . 4
 
                           |
99 | | fveq2 5888 |
. . . . . . . . . . . . . . . 16
                 |
100 | 99, 4 | syl6eqr 2514 |
. . . . . . . . . . . . . . 15
              |
101 | 100 | eleq1d 2524 |
. . . . . . . . . . . . . 14
                |
102 | 37, 101 | syl5ibrcom 230 |
. . . . . . . . . . . . 13
 

             |
103 | 102 | impancom 446 |
. . . . . . . . . . . 12
 
   
 
        |
104 | 103 | expimpd 612 |
. . . . . . . . . . 11
      
         |
105 | 104 | exlimdvv 1791 |
. . . . . . . . . 10
          
         |
106 | 58, 105 | syl5bi 225 |
. . . . . . . . 9
  
           |
107 | 106 | imp 435 |
. . . . . . . 8
 
            |
108 | 107, 96 | fmptd 6069 |
. . . . . . 7
  
                    |
109 | | frn 5758 |
. . . . . . 7
  
                   
           |
110 | 108, 109 | syl 17 |
. . . . . 6
              |
111 | 110 | sselda 3444 |
. . . . 5
 
 
            |
112 | 46 | nfel1 2617 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)
 |
113 | 47 | eleq1d 2524 |
. . . . . . 7
 
  ![]_ ]_](_urbrack.gif)    |
114 | 112, 113 | rspc 3156 |
. . . . . 6
  
  ![]_ ]_](_urbrack.gif)
   |
115 | 39, 114 | mpan9 476 |
. . . . 5
 
   ![]_ ]_](_urbrack.gif)   |
116 | 111, 115 | syldan 477 |
. . . 4
 
 
            ![]_ ]_](_urbrack.gif)
  |
117 | 49, 55, 94, 98, 116 | fsumf1o 13838 |
. . 3
   
            ![]_ ]_](_urbrack.gif) 
           ![]_ ]_](_urbrack.gif)   |
118 | 48, 117 | syl5eq 2508 |
. 2
 
 
          
           ![]_ ]_](_urbrack.gif)   |
119 | 110 | sselda 3444 |
. . . 4
 
 
            |
120 | 119, 38 | syldan 477 |
. . 3
 
 
            |
121 | | eldif 3426 |
. . . . 5
   
            
            |
122 | 96, 56 | elrnmpti 5104 |
. . . . . . . . . 10
            
           |
123 | 100 | eqeq2d 2472 |
. . . . . . . . . . 11
        
       |
124 | 123 | rexiunxp 4994 |
. . . . . . . . . 10
 
         

      |
125 | 122, 124 | bitri 257 |
. . . . . . . . 9
             
      |
126 | | simpr 467 |
. . . . . . . . . . . . . . . 16
        
      |
127 | | simplr 767 |
. . . . . . . . . . . . . . . 16
        
  |
128 | 126, 127 | eqeltrrd 2541 |
. . . . . . . . . . . . . . 15
               |
129 | 14 | rbaibd 926 |
. . . . . . . . . . . . . . . 16
 
      
      |
130 | 129 | adantlr 726 |
. . . . . . . . . . . . . . 15
           

    |
131 | 128, 130 | syldan 477 |
. . . . . . . . . . . . . 14
           

    |
132 | 131 | pm5.32da 651 |
. . . . . . . . . . . . 13
 
         
           |
133 | | ancom 456 |
. . . . . . . . . . . . 13
  

    
     
    |
134 | | ancom 456 |
. . . . . . . . . . . . 13
             

    |
135 | 132, 133,
134 | 3bitr4g 296 |
. . . . . . . . . . . 12
 
         
           |
136 | 135 | 2exbidv 1781 |
. . . . . . . . . . 11
 
       

    
     
         |
137 | | r2ex 2925 |
. . . . . . . . . . 11
  
   
              |
138 | | r2ex 2925 |
. . . . . . . . . . 11
                     |
139 | 136, 137,
138 | 3bitr4g 296 |
. . . . . . . . . 10
 
  

   
 
       |
140 | | fsumvma.3 |
. . . . . . . . . . . 12

  |
141 | 140 | sselda 3444 |
. . . . . . . . . . 11
 
   |
142 | | isppw2 24091 |
. . . . . . . . . . 11
  Λ           |
143 | 141, 142 | syl 17 |
. . . . . . . . . 10
 
  Λ           |
144 | 139, 143 | bitr4d 264 |
. . . . . . . . 9
 
  

   
Λ     |
145 | 125, 144 | syl5bb 265 |
. . . . . . . 8
 
   
        
Λ     |
146 | 145 | necon2bbid 2679 |
. . . . . . 7
 
  Λ 
 
            |
147 | 146 | pm5.32da 651 |
. . . . . 6
   Λ     
             |
148 | | fsumvma.7 |
. . . . . . 7
 

Λ      |
149 | 148 | ex 440 |
. . . . . 6
   Λ      |
150 | 147, 149 | sylbird 243 |
. . . . 5
                  |
151 | 121, 150 | syl5bi 225 |
. . . 4
    
             |
152 | 151 | imp 435 |
. . 3
 

 
          
  |
153 | 110, 120,
152, 12 | fsumss 13840 |
. 2
 
 
             |
154 | 44, 118, 153 | 3eqtr2rd 2503 |
1
 
    |