Proof of Theorem muinv
Step | Hyp | Ref
| Expression |
1 | | muinv.1 |
. . 3
       |
2 | 1 | feqmptd 5932 |
. 2
         |
3 | | muinv.2 |
. . . . . . . . . 10
   
        |
4 | 3 | ad2antrr 740 |
. . . . . . . . 9
    
 

  
       |
5 | 4 | fveq1d 5881 |
. . . . . . . 8
    
 
          
       
    |
6 | | breq1 4398 |
. . . . . . . . . . . . . 14
 
   |
7 | 6 | elrab 3184 |
. . . . . . . . . . . . 13
  
    |
8 | 7 | simprbi 471 |
. . . . . . . . . . . 12
  
  |
9 | 8 | adantl 473 |
. . . . . . . . . . 11
    
 
  |
10 | | elrabi 3181 |
. . . . . . . . . . . . . 14
  
  |
11 | 10 | adantl 473 |
. . . . . . . . . . . . 13
    
 
  |
12 | 11 | nnzd 11062 |
. . . . . . . . . . . 12
    
 
  |
13 | 11 | nnne0d 10676 |
. . . . . . . . . . . 12
    
 
  |
14 | | nnz 10983 |
. . . . . . . . . . . . 13
   |
15 | 14 | ad2antlr 741 |
. . . . . . . . . . . 12
    
 
  |
16 | | dvdsval2 14385 |
. . . . . . . . . . . 12
   
     |
17 | 12, 13, 15, 16 | syl3anc 1292 |
. . . . . . . . . . 11
    
 

     |
18 | 9, 17 | mpbid 215 |
. . . . . . . . . 10
    
 
    |
19 | | nnre 10638 |
. . . . . . . . . . . . 13
   |
20 | | nngt0 10660 |
. . . . . . . . . . . . 13
   |
21 | 19, 20 | jca 541 |
. . . . . . . . . . . 12
     |
22 | 21 | ad2antlr 741 |
. . . . . . . . . . 11
    
 
    |
23 | | nnre 10638 |
. . . . . . . . . . . . 13
   |
24 | | nngt0 10660 |
. . . . . . . . . . . . 13
   |
25 | 23, 24 | jca 541 |
. . . . . . . . . . . 12
     |
26 | 11, 25 | syl 17 |
. . . . . . . . . . 11
    
 
    |
27 | | divgt0 10495 |
. . . . . . . . . . 11
      
    |
28 | 22, 26, 27 | syl2anc 673 |
. . . . . . . . . 10
    
 
    |
29 | | elnnz 10971 |
. . . . . . . . . 10
  
        |
30 | 18, 28, 29 | sylanbrc 677 |
. . . . . . . . 9
    
 
    |
31 | | breq2 4399 |
. . . . . . . . . . . 12
   
     |
32 | 31 | rabbidv 3022 |
. . . . . . . . . . 11
    
      |
33 | 32 | sumeq1d 13844 |
. . . . . . . . . 10
    
      
         |
34 | | eqid 2471 |
. . . . . . . . . 10
  
         
      |
35 | | sumex 13831 |
. . . . . . . . . 10
 
        |
36 | 33, 34, 35 | fvmpt 5963 |
. . . . . . . . 9
       
       
  
 
        |
37 | 30, 36 | syl 17 |
. . . . . . . 8
    
 
    
       
  
 
        |
38 | 5, 37 | eqtrd 2505 |
. . . . . . 7
    
 
      
 
        |
39 | 38 | oveq2d 6324 |
. . . . . 6
    
 
                  
          |
40 | | fzfid 12224 |
. . . . . . . 8
    
 
        |
41 | | sgmss 24112 |
. . . . . . . . 9
    
          |
42 | 30, 41 | syl 17 |
. . . . . . . 8
    
 
 
          |
43 | | ssfi 7810 |
. . . . . . . 8
                    
    |
44 | 40, 42, 43 | syl2anc 673 |
. . . . . . 7
    
 
 
    |
45 | | mucl 24147 |
. . . . . . . . 9
       |
46 | 11, 45 | syl 17 |
. . . . . . . 8
    
 
      |
47 | 46 | zcnd 11064 |
. . . . . . 7
    
 
      |
48 | 1 | ad2antrr 740 |
. . . . . . . 8
    
 
      |
49 | | elrabi 3181 |
. . . . . . . 8
  
    |
50 | | ffvelrn 6035 |
. . . . . . . 8
     
       |
51 | 48, 49, 50 | syl2an 485 |
. . . . . . 7
   

   
   
      |
52 | 44, 47, 51 | fsummulc2 13922 |
. . . . . 6
    
 
                
               |
53 | 39, 52 | eqtrd 2505 |
. . . . 5
    
 
            
 
              |
54 | 53 | sumeq2dv 13846 |
. . . 4
 

 
              
    
              |
55 | | simpr 468 |
. . . . 5
 

  |
56 | 47 | adantrr 731 |
. . . . . 6
      

           |
57 | 51 | anasss 659 |
. . . . . 6
      

           |
58 | 56, 57 | mulcld 9681 |
. . . . 5
      

                 |
59 | 55, 58 | fsumdvdsdiag 24192 |
. . . 4
 

 
    
                
 
              |
60 | | ssrab2 3500 |
. . . . . . . . . 10
 
 |
61 | | dvdsdivcl 24189 |
. . . . . . . . . . 11
 
         |
62 | 61 | adantll 728 |
. . . . . . . . . 10
    
 
  
   |
63 | 60, 62 | sseldi 3416 |
. . . . . . . . 9
    
 
    |
64 | | musum 24199 |
. . . . . . . . 9
    
                |
65 | 63, 64 | syl 17 |
. . . . . . . 8
    
 
 
                |
66 | 65 | oveq1d 6323 |
. . . . . . 7
    
 
 
 
                          |
67 | | fzfid 12224 |
. . . . . . . . 9
    
 
        |
68 | | sgmss 24112 |
. . . . . . . . . 10
    
          |
69 | 63, 68 | syl 17 |
. . . . . . . . 9
    
 
 
          |
70 | | ssfi 7810 |
. . . . . . . . 9
                    
    |
71 | 67, 69, 70 | syl2anc 673 |
. . . . . . . 8
    
 
 
    |
72 | 1 | adantr 472 |
. . . . . . . . 9
 

      |
73 | | elrabi 3181 |
. . . . . . . . 9
  
  |
74 | 72, 73, 50 | syl2an 485 |
. . . . . . . 8
    
 
      |
75 | | ssrab2 3500 |
. . . . . . . . . . 11
 
   |
76 | | simpr 468 |
. . . . . . . . . . 11
   

   
   
      |
77 | 75, 76 | sseldi 3416 |
. . . . . . . . . 10
   

   
   
  |
78 | 77, 45 | syl 17 |
. . . . . . . . 9
   

   
   
      |
79 | 78 | zcnd 11064 |
. . . . . . . 8
   

   
   
      |
80 | 71, 74, 79 | fsummulc1 13923 |
. . . . . . 7
    
 
 
 
            
               |
81 | | ovif 6392 |
. . . . . . . 8
                                 |
82 | | nncn 10639 |
. . . . . . . . . . . 12
   |
83 | 82 | ad2antlr 741 |
. . . . . . . . . . 11
    
 
  |
84 | 73 | adantl 473 |
. . . . . . . . . . . 12
    
 
  |
85 | 84 | nncnd 10647 |
. . . . . . . . . . 11
    
 
  |
86 | | 1cnd 9677 |
. . . . . . . . . . 11
    
 
  |
87 | 84 | nnne0d 10676 |
. . . . . . . . . . 11
    
 
  |
88 | 83, 85, 86, 87 | divmuld 10427 |
. . . . . . . . . 10
    
 
  
     |
89 | 85 | mulid1d 9678 |
. . . . . . . . . . 11
    
 
    |
90 | 89 | eqeq1d 2473 |
. . . . . . . . . 10
    
 
  
   |
91 | 88, 90 | bitrd 261 |
. . . . . . . . 9
    
 
  
   |
92 | 74 | mulid2d 9679 |
. . . . . . . . 9
    
 
            |
93 | 74 | mul02d 9849 |
. . . . . . . . 9
    
 
        |
94 | 91, 92, 93 | ifbieq12d 3899 |
. . . . . . . 8
    
 
                              |
95 | 81, 94 | syl5eq 2517 |
. . . . . . 7
    
 
                        |
96 | 66, 80, 95 | 3eqtr3d 2513 |
. . . . . 6
    
 
 
                        |
97 | 96 | sumeq2dv 13846 |
. . . . 5
 

 
    
                           |
98 | 55 | nnzd 11062 |
. . . . . . . . 9
 

  |
99 | | iddvds 14393 |
. . . . . . . . 9
   |
100 | 98, 99 | syl 17 |
. . . . . . . 8
 

  |
101 | | breq1 4398 |
. . . . . . . . 9
 
   |
102 | 101 | elrab 3184 |
. . . . . . . 8
  
    |
103 | 55, 100, 102 | sylanbrc 677 |
. . . . . . 7
 


   |
104 | 103 | snssd 4108 |
. . . . . 6
 

      |
105 | 104 | sselda 3418 |
. . . . . . . 8
           |
106 | 105, 74 | syldan 478 |
. . . . . . 7
             |
107 | | 0cn 9653 |
. . . . . . 7
 |
108 | | ifcl 3914 |
. . . . . . 7
     
            |
109 | 106, 107,
108 | sylancl 675 |
. . . . . 6
                  |
110 | | eldifsni 4089 |
. . . . . . . . 9
   
     |
111 | 110 | adantl 473 |
. . . . . . . 8
      
      |
112 | 111 | neneqd 2648 |
. . . . . . 7
      
   
  |
113 | 112 | iffalsed 3883 |
. . . . . 6
      
               |
114 | | fzfid 12224 |
. . . . . . 7
 

      |
115 | | sgmss 24112 |
. . . . . . . 8
  
      |
116 | 115 | adantl 473 |
. . . . . . 7
 

 
      |
117 | | ssfi 7810 |
. . . . . . 7
              
  |
118 | 114, 116,
117 | syl2anc 673 |
. . . . . 6
 

 
  |
119 | 104, 109,
113, 118 | fsumss 13868 |
. . . . 5
 

              
             |
120 | 1 | ffvelrnda 6037 |
. . . . . 6
 

      |
121 | | iftrue 3878 |
. . . . . . . 8
                |
122 | | fveq2 5879 |
. . . . . . . 8
           |
123 | 121, 122 | eqtrd 2505 |
. . . . . . 7
                |
124 | 123 | sumsn 13884 |
. . . . . 6
                          |
125 | 55, 120, 124 | syl2anc 673 |
. . . . 5
 

                   |
126 | 97, 119, 125 | 3eqtr2d 2511 |
. . . 4
 

 
    
                  |
127 | 54, 59, 126 | 3eqtrd 2509 |
. . 3
 

 
                   |
128 | 127 | mpteq2dva 4482 |
. 2
    
                     |
129 | 2, 128 | eqtr4d 2508 |
1
   
                |