Step | Hyp | Ref
| Expression |
1 | | nfcv 2612 |
. . 3
       |
2 | | nfcv 2612 |
. . . 4
  
  |
3 | | nfcsb1v 3365 |
. . . 4
  
 ![]_ ]_](_urbrack.gif)  |
4 | 2, 3 | nfsum 13834 |
. . 3
        ![]_ ]_](_urbrack.gif)  |
5 | | breq2 4399 |
. . . . 5
 
   |
6 | 5 | rabbidv 3022 |
. . . 4
  
    |
7 | | csbeq1a 3358 |
. . . . 5
   ![]_ ]_](_urbrack.gif)   |
8 | 7 | adantr 472 |
. . . 4
 
     ![]_ ]_](_urbrack.gif)   |
9 | 6, 8 | sumeq12dv 13849 |
. . 3
  
   
  
 ![]_ ]_](_urbrack.gif)   |
10 | 1, 4, 9 | cbvsumi 13840 |
. 2
 
                ![]_ ]_](_urbrack.gif)  |
11 | | breq2 4399 |
. . . . . 6
   
     |
12 | 11 | rabbidv 3022 |
. . . . 5
    
      |
13 | | csbeq1 3352 |
. . . . . 6
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
14 | 13 | adantr 472 |
. . . . 5
   
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
15 | 12, 14 | sumeq12dv 13849 |
. . . 4
    
  
 ![]_ ]_](_urbrack.gif)

 
       ![]_ ]_](_urbrack.gif)   |
16 | | fzfid 12224 |
. . . . 5
       |
17 | | fsumdvdscom.1 |
. . . . . 6
   |
18 | | sgmss 24112 |
. . . . . 6
  
      |
19 | 17, 18 | syl 17 |
. . . . 5
 
       |
20 | | ssfi 7810 |
. . . . 5
              
  |
21 | 16, 19, 20 | syl2anc 673 |
. . . 4
 
   |
22 | | eqid 2471 |
. . . . . 6
 
   |
23 | | eqid 2471 |
. . . . . 6
  
    
     |
24 | 22, 23 | dvdsflip 24190 |
. . . . 5
   
         
   |
25 | 17, 24 | syl 17 |
. . . 4
             
   |
26 | | oveq2 6316 |
. . . . . 6
       |
27 | | ovex 6336 |
. . . . . 6
   |
28 | 26, 23, 27 | fvmpt3i 5968 |
. . . . 5
  
   
          |
29 | 28 | adantl 473 |
. . . 4
 
      
          |
30 | | fzfid 12224 |
. . . . . 6
 
         |
31 | | ssrab2 3500 |
. . . . . . . 8
 
 |
32 | | simpr 468 |
. . . . . . . 8
 
       |
33 | 31, 32 | sseldi 3416 |
. . . . . . 7
 
     |
34 | | sgmss 24112 |
. . . . . . 7
  
      |
35 | 33, 34 | syl 17 |
. . . . . 6
 
    
      |
36 | | ssfi 7810 |
. . . . . 6
              
  |
37 | 30, 35, 36 | syl2anc 673 |
. . . . 5
 
    
  |
38 | | fsumdvdscom.3 |
. . . . . . . . 9
 
 

   
  |
39 | 38 | ralrimivva 2814 |
. . . . . . . 8
     
     |
40 | | nfv 1769 |
. . . . . . . . 9
  
    |
41 | 3 | nfel1 2626 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)
 |
42 | 2, 41 | nfral 2789 |
. . . . . . . . 9
        ![]_ ]_](_urbrack.gif)  |
43 | 7 | eleq1d 2533 |
. . . . . . . . . 10
 
  ![]_ ]_](_urbrack.gif)    |
44 | 6, 43 | raleqbidv 2987 |
. . . . . . . . 9
  
         ![]_ ]_](_urbrack.gif)    |
45 | 40, 42, 44 | cbvral 3001 |
. . . . . . . 8
 
    
 
 
  
     ![]_ ]_](_urbrack.gif)   |
46 | 39, 45 | sylib 201 |
. . . . . . 7
     
     ![]_ ]_](_urbrack.gif)   |
47 | 46 | r19.21bi 2776 |
. . . . . 6
 
         ![]_ ]_](_urbrack.gif)   |
48 | 47 | r19.21bi 2776 |
. . . . 5
   
 
     ![]_ ]_](_urbrack.gif)
  |
49 | 37, 48 | fsumcl 13876 |
. . . 4
 
         ![]_ ]_](_urbrack.gif)   |
50 | 15, 21, 25, 29, 49 | fsumf1o 13866 |
. . 3
 
         ![]_ ]_](_urbrack.gif)     
 
       ![]_ ]_](_urbrack.gif)   |
51 | | dvdsdivcl 24189 |
. . . . . . . 8
 
     
   |
52 | 17, 51 | sylan 479 |
. . . . . . 7
 
         |
53 | 46 | adantr 472 |
. . . . . . 7
 
       
     ![]_ ]_](_urbrack.gif)   |
54 | 13 | eleq1d 2533 |
. . . . . . . . 9
    
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
   |
55 | 12, 54 | raleqbidv 2987 |
. . . . . . . 8
    
     ![]_ ]_](_urbrack.gif)   
       ![]_ ]_](_urbrack.gif)    |
56 | 55 | rspcv 3132 |
. . . . . . 7
    
 
    
  
 ![]_ ]_](_urbrack.gif)
       
  ![]_ ]_](_urbrack.gif)
   |
57 | 52, 53, 56 | sylc 61 |
. . . . . 6
 
          
  ![]_ ]_](_urbrack.gif)
  |
58 | 57 | r19.21bi 2776 |
. . . . 5
   
 
         ![]_ ]_](_urbrack.gif)
  |
59 | 58 | anasss 659 |
. . . 4
 
 

 
        ![]_ ]_](_urbrack.gif)
  |
60 | 17, 59 | fsumdvdsdiag 24192 |
. . 3
     
 
       ![]_ ]_](_urbrack.gif) 
          
  ![]_ ]_](_urbrack.gif)   |
61 | | oveq2 6316 |
. . . . . . 7
               |
62 | 61 | csbeq1d 3356 |
. . . . . 6
         ![]_ ]_](_urbrack.gif)  
      ![]_ ]_](_urbrack.gif)   |
63 | | fzfid 12224 |
. . . . . . 7
 
           |
64 | | dvdsdivcl 24189 |
. . . . . . . . . 10
 
     
   |
65 | 31, 64 | sseldi 3416 |
. . . . . . . . 9
 
       |
66 | 17, 65 | sylan 479 |
. . . . . . . 8
 
       |
67 | | sgmss 24112 |
. . . . . . . 8
    
          |
68 | 66, 67 | syl 17 |
. . . . . . 7
 
    
          |
69 | | ssfi 7810 |
. . . . . . 7
                  
 
    |
70 | 63, 68, 69 | syl2anc 673 |
. . . . . 6
 
    
    |
71 | | eqid 2471 |
. . . . . . . 8
 
       |
72 | | eqid 2471 |
. . . . . . . 8
  
        
         |
73 | 71, 72 | dvdsflip 24190 |
. . . . . . 7
     
          
    
     |
74 | 66, 73 | syl 17 |
. . . . . 6
 
    
                
     |
75 | | oveq2 6316 |
. . . . . . . 8
           |
76 | | ovex 6336 |
. . . . . . . 8
     |
77 | 75, 72, 76 | fvmpt3i 5968 |
. . . . . . 7
  
                      |
78 | 77 | adantl 473 |
. . . . . 6
   
 
        
                |
79 | 17 | fsumdvdsdiaglem 24191 |
. . . . . . . 8
   

 
     
 
      |
80 | 59 | ex 441 |
. . . . . . . 8
   

 
       ![]_ ]_](_urbrack.gif)
   |
81 | 79, 80 | syld 44 |
. . . . . . 7
   

 
       ![]_ ]_](_urbrack.gif)
   |
82 | 81 | impl 632 |
. . . . . 6
   
 
         ![]_ ]_](_urbrack.gif)
  |
83 | 62, 70, 74, 78, 82 | fsumf1o 13866 |
. . . . 5
 
          
  ![]_ ]_](_urbrack.gif)
 
            ![]_ ]_](_urbrack.gif)   |
84 | | ovex 6336 |
. . . . . . . 8
       |
85 | 84 | a1i 11 |
. . . . . . 7
   
 
             |
86 | | nncn 10639 |
. . . . . . . . . . . . . . . . 17
   |
87 | | nnne0 10664 |
. . . . . . . . . . . . . . . . 17
   |
88 | 86, 87 | jca 541 |
. . . . . . . . . . . . . . . 16
 
   |
89 | 17, 88 | syl 17 |
. . . . . . . . . . . . . . 15
     |
90 | 89 | ad2antrr 740 |
. . . . . . . . . . . . . 14
   
 
         |
91 | 90 | simpld 466 |
. . . . . . . . . . . . 13
   
 
       |
92 | | elrabi 3181 |
. . . . . . . . . . . . . . . 16
  
  |
93 | 92 | adantl 473 |
. . . . . . . . . . . . . . 15
 
     |
94 | 93 | adantr 472 |
. . . . . . . . . . . . . 14
   
 
       |
95 | | nncn 10639 |
. . . . . . . . . . . . . . 15
   |
96 | | nnne0 10664 |
. . . . . . . . . . . . . . 15
   |
97 | 95, 96 | jca 541 |
. . . . . . . . . . . . . 14
     |
98 | 94, 97 | syl 17 |
. . . . . . . . . . . . 13
   
 
         |
99 | | elrabi 3181 |
. . . . . . . . . . . . . . 15
  
    |
100 | 99 | adantl 473 |
. . . . . . . . . . . . . 14
   
 
       |
101 | | nncn 10639 |
. . . . . . . . . . . . . . 15
   |
102 | | nnne0 10664 |
. . . . . . . . . . . . . . 15
   |
103 | 101, 102 | jca 541 |
. . . . . . . . . . . . . 14
     |
104 | 100, 103 | syl 17 |
. . . . . . . . . . . . 13
   
 
         |
105 | | divdiv1 10340 |
. . . . . . . . . . . . 13
                 |
106 | 91, 98, 104, 105 | syl3anc 1292 |
. . . . . . . . . . . 12
   
 
               |
107 | 106 | oveq2d 6324 |
. . . . . . . . . . 11
   
 
                   |
108 | | nnmulcl 10654 |
. . . . . . . . . . . . . 14
 
     |
109 | 93, 99, 108 | syl2an 485 |
. . . . . . . . . . . . 13
   
 
         |
110 | | nncn 10639 |
. . . . . . . . . . . . . 14
       |
111 | | nnne0 10664 |
. . . . . . . . . . . . . 14
       |
112 | 110, 111 | jca 541 |
. . . . . . . . . . . . 13
           |
113 | 109, 112 | syl 17 |
. . . . . . . . . . . 12
   
 
             |
114 | | ddcan 10343 |
. . . . . . . . . . . 12
                     |
115 | 90, 113, 114 | syl2anc 673 |
. . . . . . . . . . 11
   
 
               |
116 | 107, 115 | eqtrd 2505 |
. . . . . . . . . 10
   
 
               |
117 | 116 | eqeq2d 2481 |
. . . . . . . . 9
   
 
                 |
118 | 117 | biimpa 492 |
. . . . . . . 8
   
   
               |
119 | | fsumdvdscom.2 |
. . . . . . . 8
     |
120 | 118, 119 | syl 17 |
. . . . . . 7
   
   
             |
121 | 85, 120 | csbied 3376 |
. . . . . 6
   
 
             ![]_ ]_](_urbrack.gif)
  |
122 | 121 | sumeq2dv 13846 |
. . . . 5
 
          
      ![]_ ]_](_urbrack.gif)
 
      |
123 | 83, 122 | eqtrd 2505 |
. . . 4
 
          
  ![]_ ]_](_urbrack.gif)
 
      |
124 | 123 | sumeq2dv 13846 |
. . 3
     
 
       ![]_ ]_](_urbrack.gif) 
           |
125 | 50, 60, 124 | 3eqtrd 2509 |
. 2
 
         ![]_ ]_](_urbrack.gif)       
     |
126 | 10, 125 | syl5eq 2517 |
1
     
   
           |