Proof of Theorem modfsummods
Step | Hyp | Ref
| Expression |
1 | | snssi 4116 |
. . 3
  
  |
2 | | ssequn1 3604 |
. . . 4
         |
3 | | uncom 3578 |
. . . . . . . 8
         |
4 | 3 | eqeq1i 2456 |
. . . . . . 7
           |
5 | | sumeq1 13755 |
. . . . . . . . . 10
              |
6 | 5 | oveq1d 6305 |
. . . . . . . . 9
                  |
7 | | sumeq1 13755 |
. . . . . . . . . 10
                  |
8 | 7 | oveq1d 6305 |
. . . . . . . . 9
       
              |
9 | 6, 8 | eqeq12d 2466 |
. . . . . . . 8
       
  
  
 
                   |
10 | 9 | eqcoms 2459 |
. . . . . . 7
       
   
 
 
                   |
11 | 4, 10 | sylbi 199 |
. . . . . 6
       
   
 
 
                   |
12 | 11 | biimpd 211 |
. . . . 5
       
   
           
      
    |
13 | 12 | a1d 26 |
. . . 4
                
  
            
      
     |
14 | 2, 13 | sylbi 199 |
. . 3
    
         
  
            
      
     |
15 | 1, 14 | syl 17 |
. 2
            
   
           
      
     |
16 | | df-nel 2625 |
. . 3

  |
17 | | simp1 1008 |
. . . . . . . . . 10
 

        |
18 | 17 | adantl 468 |
. . . . . . . . 9
  
          |
19 | | simpl 459 |
. . . . . . . . 9
  
          |
20 | | simpr3 1016 |
. . . . . . . . 9
  
                |
21 | 18, 19, 20 | 3jca 1188 |
. . . . . . . 8
  
        
         |
22 | 21 | adantr 467 |
. . . . . . 7
                 
   
         |
23 | | fsumsplitsnun 13816 |
. . . . . . 7
  
             
  ![]_ ]_](_urbrack.gif)    |
24 | 22, 23 | syl 17 |
. . . . . 6
                 
          
  ![]_ ]_](_urbrack.gif)    |
25 | 24 | oveq1d 6305 |
. . . . 5
                 
             
  ![]_ ]_](_urbrack.gif)     |
26 | | ralunb 3615 |
. . . . . . . . . . . . . 14
 
    
 
       |
27 | | simpl 459 |
. . . . . . . . . . . . . 14
  

  
 
  |
28 | 26, 27 | sylbi 199 |
. . . . . . . . . . . . 13
 
        |
29 | | fsumzcl2 13804 |
. . . . . . . . . . . . 13
    
  |
30 | 28, 29 | sylan2 477 |
. . . . . . . . . . . 12
         
  |
31 | 30 | 3adant2 1027 |
. . . . . . . . . . 11
 

      
  |
32 | 31 | adantl 468 |
. . . . . . . . . 10
  
        
  |
33 | 32 | zred 11040 |
. . . . . . . . 9
  
        
  |
34 | | modfsummodslem1 13852 |
. . . . . . . . . . . 12
 
       ![]_ ]_](_urbrack.gif)
  |
35 | 34 | 3ad2ant3 1031 |
. . . . . . . . . . 11
 

        ![]_ ]_](_urbrack.gif)
  |
36 | 35 | adantl 468 |
. . . . . . . . . 10
  
          ![]_ ]_](_urbrack.gif)   |
37 | 36 | zred 11040 |
. . . . . . . . 9
  
          ![]_ ]_](_urbrack.gif)   |
38 | | nnrp 11311 |
. . . . . . . . . . 11
   |
39 | 38 | 3ad2ant2 1030 |
. . . . . . . . . 10
 

        |
40 | 39 | adantl 468 |
. . . . . . . . 9
  
          |
41 | | modaddabs 12135 |
. . . . . . . . 9
  
  ![]_ ]_](_urbrack.gif) 
        ![]_ ]_](_urbrack.gif)      
  ![]_ ]_](_urbrack.gif)     |
42 | 33, 37, 40, 41 | syl3anc 1268 |
. . . . . . . 8
  
           
    ![]_ ]_](_urbrack.gif)      
  ![]_ ]_](_urbrack.gif)     |
43 | 42 | eqcomd 2457 |
. . . . . . 7
  
          
  ![]_ ]_](_urbrack.gif)      
    ![]_ ]_](_urbrack.gif)      |
44 | 43 | adantr 467 |
. . . . . 6
                 
     
  ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)      |
45 | | simpr 463 |
. . . . . . . 8
                 
    
  
     |
46 | 34 | zred 11040 |
. . . . . . . . . . . . 13
 
       ![]_ ]_](_urbrack.gif)
  |
47 | 46 | 3ad2ant3 1031 |
. . . . . . . . . . . 12
 

        ![]_ ]_](_urbrack.gif)
  |
48 | 47 | adantl 468 |
. . . . . . . . . . 11
  
          ![]_ ]_](_urbrack.gif)   |
49 | 48, 40 | jca 535 |
. . . . . . . . . 10
  
         
 ![]_ ]_](_urbrack.gif)
   |
50 | 49 | adantr 467 |
. . . . . . . . 9
                 
      ![]_ ]_](_urbrack.gif)    |
51 | | modabs2 12131 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)
     ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
52 | 51 | eqcomd 2457 |
. . . . . . . . 9
    ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
    |
53 | 50, 52 | syl 17 |
. . . . . . . 8
                 
      ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif) 
   |
54 | 45, 53 | oveq12d 6308 |
. . . . . . 7
                 
     
    ![]_ ]_](_urbrack.gif)
     
      ![]_ ]_](_urbrack.gif)      |
55 | 54 | oveq1d 6305 |
. . . . . 6
                 
           ![]_ ]_](_urbrack.gif)        
      ![]_ ]_](_urbrack.gif)       |
56 | 44, 55 | eqtrd 2485 |
. . . . 5
                 
     
  ![]_ ]_](_urbrack.gif)       
      ![]_ ]_](_urbrack.gif)       |
57 | | zmodcl 12116 |
. . . . . . . . . . . . . . . . . . 19
 
     |
58 | 57 | nn0zd 11038 |
. . . . . . . . . . . . . . . . . 18
 
     |
59 | 58 | expcom 437 |
. . . . . . . . . . . . . . . . 17
 
     |
60 | 59 | ralimdv 2798 |
. . . . . . . . . . . . . . . 16
  
      |
61 | 60 | com12 32 |
. . . . . . . . . . . . . . 15
 


     |
62 | 61 | adantr 467 |
. . . . . . . . . . . . . 14
  

  
 

     |
63 | 26, 62 | sylbi 199 |
. . . . . . . . . . . . 13
 
            |
64 | 63 | impcom 432 |
. . . . . . . . . . . 12
          
   |
65 | 64 | 3adant1 1026 |
. . . . . . . . . . 11
 

       
   |
66 | 17, 65 | jca 535 |
. . . . . . . . . 10
 

      

     |
67 | | fsumzcl2 13804 |
. . . . . . . . . . 11
           |
68 | 67 | zred 11040 |
. . . . . . . . . 10
           |
69 | 66, 68 | syl 17 |
. . . . . . . . 9
 

       
   |
70 | 69 | adantl 468 |
. . . . . . . 8
  
        
    |
71 | 70 | adantr 467 |
. . . . . . 7
                 
    
   |
72 | 34 | anim1i 572 |
. . . . . . . . . . . . 13
          
 ![]_ ]_](_urbrack.gif)
   |
73 | 72 | ancoms 455 |
. . . . . . . . . . . 12
            ![]_ ]_](_urbrack.gif)    |
74 | | zmodcl 12116 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
75 | 73, 74 | syl 17 |
. . . . . . . . . . 11
            ![]_ ]_](_urbrack.gif)    |
76 | 75 | nn0red 10926 |
. . . . . . . . . 10
            ![]_ ]_](_urbrack.gif)    |
77 | 76 | 3adant1 1026 |
. . . . . . . . 9
 

         ![]_ ]_](_urbrack.gif)    |
78 | 77 | adantl 468 |
. . . . . . . 8
  
         
 ![]_ ]_](_urbrack.gif)
   |
79 | 78 | adantr 467 |
. . . . . . 7
                 
      ![]_ ]_](_urbrack.gif)    |
80 | 40 | adantr 467 |
. . . . . . 7
                 
     |
81 | | modaddabs 12135 |
. . . . . . 7
   
  
 ![]_ ]_](_urbrack.gif)
     
       ![]_ ]_](_urbrack.gif)
      
     ![]_ ]_](_urbrack.gif)
     |
82 | 71, 79, 80, 81 | syl3anc 1268 |
. . . . . 6
                 
       
      ![]_ ]_](_urbrack.gif)        
    ![]_ ]_](_urbrack.gif)      |
83 | 18 | adantr 467 |
. . . . . . . . . 10
                 
     |
84 | 19 | adantr 467 |
. . . . . . . . . 10
                 
     |
85 | 59 | ralimdv 2798 |
. . . . . . . . . . . . . 14
  

   
           |
86 | 85 | imp 431 |
. . . . . . . . . . . . 13
                   |
87 | 86 | 3adant1 1026 |
. . . . . . . . . . . 12
 

                |
88 | 87 | adantl 468 |
. . . . . . . . . . 11
  
                  |
89 | 88 | adantr 467 |
. . . . . . . . . 10
                 
             |
90 | | fsumsplitsnun 13816 |
. . . . . . . . . 10
  
                  
   ![]_ ]_](_urbrack.gif)      |
91 | 83, 84, 89, 90 | syl3anc 1268 |
. . . . . . . . 9
                 
             
   ![]_ ]_](_urbrack.gif)      |
92 | | vex 3048 |
. . . . . . . . . . 11
 |
93 | | csbov1g 6327 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
94 | 92, 93 | mp1i 13 |
. . . . . . . . . 10
                 
     ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
95 | 94 | oveq2d 6306 |
. . . . . . . . 9
                 
    
    ![]_ ]_](_urbrack.gif)     
     ![]_ ]_](_urbrack.gif)
    |
96 | 91, 95 | eqtrd 2485 |
. . . . . . . 8
                 
             
    ![]_ ]_](_urbrack.gif)     |
97 | 96 | eqcomd 2457 |
. . . . . . 7
                 
    
     ![]_ ]_](_urbrack.gif)
            |
98 | 97 | oveq1d 6305 |
. . . . . 6
                 
     
     ![]_ ]_](_urbrack.gif)     
      
   |
99 | 82, 98 | eqtrd 2485 |
. . . . 5
                 
       
      ![]_ ]_](_urbrack.gif)      
      
   |
100 | 25, 56, 99 | 3eqtrd 2489 |
. . . 4
                 
                       |
101 | 100 | exp31 609 |
. . 3
            
   
           
      
     |
102 | 16, 101 | sylbir 217 |
. 2
  
         
  
            
      
     |
103 | 15, 102 | pm2.61i 168 |
1
 

        
   
           
      
    |