Step | Hyp | Ref
| Expression |
1 | | prmnn 12141 |
. . . 4

  |
2 | | nnnn0 9212 |
. . . 4
   |
3 | | nnexpcl 10563 |
. . . 4
 
       |
4 | 1, 2, 3 | syl2an 289 |
. . 3
         |
5 | | phival 12244 |
. . 3
             ♯                    |
6 | 4, 5 | syl 14 |
. 2
           ♯                    |
7 | | nnm1nn0 9246 |
. . . . . 6
 
   |
8 | | nnexpcl 10563 |
. . . . . 6
  
     
    |
9 | 1, 7, 8 | syl2an 289 |
. . . . 5
           |
10 | 9 | nncnd 8962 |
. . . 4
           |
11 | 1 | nncnd 8962 |
. . . . 5

  |
12 | 11 | adantr 276 |
. . . 4
     |
13 | | ax-1cn 7933 |
. . . . 5
 |
14 | | subdi 8371 |
. . . . 5
     
 
     
                         |
15 | 13, 14 | mp3an3 1337 |
. . . 4
     
 
        
       
              |
16 | 10, 12, 15 | syl2anc 411 |
. . 3
       
                         |
17 | 10 | mulridd 8003 |
. . . 4
       
           |
18 | 17 | oveq2d 5911 |
. . 3
                                       |
19 | | phivalfi 12243 |
. . . . . . 7
                       |
20 | 4, 19 | syl 14 |
. . . . . 6
                     |
21 | | 1zzd 9309 |
. . . . . . . 8
     |
22 | | prmz 12142 |
. . . . . . . . 9

  |
23 | | zexpcl 10565 |
. . . . . . . . 9
 
       |
24 | 22, 2, 23 | syl2an 289 |
. . . . . . . 8
         |
25 | 21, 24 | fzfigd 10461 |
. . . . . . 7
             |
26 | 22 | ad2antrr 488 |
. . . . . . . . 9
            
  |
27 | | elfzelz 10054 |
. . . . . . . . . . 11
           |
28 | 27 | adantl 277 |
. . . . . . . . . 10
            
  |
29 | | 0zd 9294 |
. . . . . . . . . 10
            
  |
30 | 28, 29 | zsubcld 9409 |
. . . . . . . . 9
            
    |
31 | | zdvdsdc 11850 |
. . . . . . . . 9
  
  DECID
    |
32 | 26, 30, 31 | syl2anc 411 |
. . . . . . . 8
            
DECID
    |
33 | 32 | ralrimiva 2563 |
. . . . . . 7
            DECID     |
34 | 25, 33 | ssfirab 6961 |
. . . . . 6
                 |
35 | | inrab 3422 |
. . . . . . 7
                                              
    |
36 | | rpexp 12184 |
. . . . . . . . . . . . . . . . 17
 
             |
37 | 22, 36 | syl3an1 1282 |
. . . . . . . . . . . . . . . 16
               |
38 | 37 | 3expa 1205 |
. . . . . . . . . . . . . . 15
                 |
39 | 38 | an32s 568 |
. . . . . . . . . . . . . 14
                 |
40 | | simpr 110 |
. . . . . . . . . . . . . . . 16
       |
41 | 24 | adantr 276 |
. . . . . . . . . . . . . . . 16
           |
42 | | gcdcom 12005 |
. . . . . . . . . . . . . . . 16
                     |
43 | 40, 41, 42 | syl2anc 411 |
. . . . . . . . . . . . . . 15
                   |
44 | 43 | eqeq1d 2198 |
. . . . . . . . . . . . . 14
                     |
45 | | coprm 12175 |
. . . . . . . . . . . . . . 15
   
     |
46 | 45 | adantlr 477 |
. . . . . . . . . . . . . 14
           |
47 | 39, 44, 46 | 3bitr4d 220 |
. . . . . . . . . . . . 13
           
   |
48 | | zcn 9287 |
. . . . . . . . . . . . . . . . 17
   |
49 | 48 | adantl 277 |
. . . . . . . . . . . . . . . 16
       |
50 | 49 | subid1d 8286 |
. . . . . . . . . . . . . . 15
         |
51 | 50 | breq2d 4030 |
. . . . . . . . . . . . . 14
      

   |
52 | 51 | notbid 668 |
. . . . . . . . . . . . 13
       
   |
53 | 47, 52 | bitr4d 191 |
. . . . . . . . . . . 12
           
     |
54 | 27, 53 | sylan2 286 |
. . . . . . . . . . 11
            
 
    
     |
55 | 54 | biimpd 144 |
. . . . . . . . . 10
            
 
    
     |
56 | | imnan 691 |
. . . . . . . . . 10
          
            |
57 | 55, 56 | sylib 122 |
. . . . . . . . 9
            
            |
58 | 57 | ralrimiva 2563 |
. . . . . . . 8
                   
    |
59 | | rabeq0 3467 |
. . . . . . . 8
                    
                
    |
60 | 58, 59 | sylibr 134 |
. . . . . . 7
                   
     |
61 | 35, 60 | eqtrid 2234 |
. . . . . 6
    
                              |
62 | | hashun 10816 |
. . . . . 6
                               
                             ♯                                 ♯                  ♯                 |
63 | 20, 34, 61, 62 | syl3anc 1249 |
. . . . 5
   ♯                                 ♯                  ♯                 |
64 | | unrab 3421 |
. . . . . . . 8
                                              
    |
65 | 54 | biimprd 158 |
. . . . . . . . . . . 12
            
   
        |
66 | | con1dc 857 |
. . . . . . . . . . . 12
DECID 

 
               
      |
67 | 32, 65, 66 | sylc 62 |
. . . . . . . . . . 11
            
 
          |
68 | 24 | adantr 276 |
. . . . . . . . . . . . . . 15
            
      |
69 | 28, 68 | gcdcld 12000 |
. . . . . . . . . . . . . 14
            
        |
70 | 69 | nn0zd 9402 |
. . . . . . . . . . . . 13
            
        |
71 | | 1zzd 9309 |
. . . . . . . . . . . . 13
            
  |
72 | | zdceq 9357 |
. . . . . . . . . . . . 13
        
DECID         |
73 | 70, 71, 72 | syl2anc 411 |
. . . . . . . . . . . 12
            
DECID         |
74 | | dfordc 893 |
. . . . . . . . . . . 12
DECID      
          
 
           |
75 | 73, 74 | syl 14 |
. . . . . . . . . . 11
            
          
 
           |
76 | 67, 75 | mpbird 167 |
. . . . . . . . . 10
            
 
     
    |
77 | 76 | ralrimiva 2563 |
. . . . . . . . 9
                         |
78 | | rabid2 2667 |
. . . . . . . . 9
                         
  
                      |
79 | 77, 78 | sylibr 134 |
. . . . . . . 8
                           
     |
80 | 64, 79 | eqtr4id 2241 |
. . . . . . 7
    
                                      |
81 | 80 | fveq2d 5538 |
. . . . . 6
   ♯                                ♯            |
82 | 4 | nnnn0d 9258 |
. . . . . . 7
         |
83 | | hashfz1 10794 |
. . . . . . 7
    
♯                |
84 | 82, 83 | syl 14 |
. . . . . 6
   ♯                |
85 | | expm1t 10578 |
. . . . . . 7
 
               |
86 | 11, 85 | sylan 283 |
. . . . . 6
                 |
87 | 81, 84, 86 | 3eqtrd 2226 |
. . . . 5
   ♯                                          |
88 | | hashcl 10792 |
. . . . . . . 8
                 ♯                    |
89 | 20, 88 | syl 14 |
. . . . . . 7
   ♯                    |
90 | 89 | nn0cnd 9260 |
. . . . . 6
   ♯                    |
91 | 1 | adantr 276 |
. . . . . . . . 9
     |
92 | | nn0uz 9591 |
. . . . . . . . . . 11
     |
93 | | 1m1e0 9017 |
. . . . . . . . . . . 12
   |
94 | 93 | fveq2i 5537 |
. . . . . . . . . . 11
           |
95 | 92, 94 | eqtr4i 2213 |
. . . . . . . . . 10
       |
96 | 82, 95 | eleqtrdi 2282 |
. . . . . . . . 9
               |
97 | | 0zd 9294 |
. . . . . . . . 9
     |
98 | 91, 21, 96, 97 | hashdvds 12252 |
. . . . . . . 8
   ♯                                        |
99 | 4 | nncnd 8962 |
. . . . . . . . . . . . . 14
         |
100 | 99 | subid1d 8286 |
. . . . . . . . . . . . 13
               |
101 | 100 | oveq1d 5910 |
. . . . . . . . . . . 12
                   |
102 | 91 | nnap0d 8994 |
. . . . . . . . . . . . 13
   #   |
103 | | nnz 9301 |
. . . . . . . . . . . . . 14
   |
104 | 103 | adantl 277 |
. . . . . . . . . . . . 13
     |
105 | 12, 102, 104 | expm1apd 10694 |
. . . . . . . . . . . 12
                 |
106 | 101, 105 | eqtr4d 2225 |
. . . . . . . . . . 11
                   |
107 | 106 | fveq2d 5538 |
. . . . . . . . . 10
                           |
108 | 9 | nnzd 9403 |
. . . . . . . . . . 11
           |
109 | | flid 10314 |
. . . . . . . . . . 11
                    
    |
110 | 108, 109 | syl 14 |
. . . . . . . . . 10
                
    |
111 | 107, 110 | eqtrd 2222 |
. . . . . . . . 9
                  
    |
112 | 93 | oveq1i 5905 |
. . . . . . . . . . . . . 14
       |
113 | | 0m0e0 9060 |
. . . . . . . . . . . . . 14
   |
114 | 112, 113 | eqtri 2210 |
. . . . . . . . . . . . 13
     |
115 | 114 | oveq1i 5905 |
. . . . . . . . . . . 12
         |
116 | 12, 102 | div0apd 8773 |
. . . . . . . . . . . 12
       |
117 | 115, 116 | eqtrid 2234 |
. . . . . . . . . . 11
           |
118 | 117 | fveq2d 5538 |
. . . . . . . . . 10
                   |
119 | | 0z 9293 |
. . . . . . . . . . 11
 |
120 | | flid 10314 |
. . . . . . . . . . 11
       |
121 | 119, 120 | ax-mp 5 |
. . . . . . . . . 10
     |
122 | 118, 121 | eqtrdi 2238 |
. . . . . . . . 9
               |
123 | 111, 122 | oveq12d 5913 |
. . . . . . . 8
                                     |
124 | 10 | subid1d 8286 |
. . . . . . . 8
       
           |
125 | 98, 123, 124 | 3eqtrd 2226 |
. . . . . . 7
   ♯                      |
126 | 125 | oveq2d 5911 |
. . . . . 6
    ♯                  ♯                ♯                           |
127 | 90, 10, 126 | comraddd 8143 |
. . . . 5
    ♯                  ♯                   
  ♯                     |
128 | 63, 87, 127 | 3eqtr3rd 2231 |
. . . 4
       
  ♯                             |
129 | 10, 12 | mulcld 8007 |
. . . . 5
       
     |
130 | 129, 10, 90 | subaddd 8315 |
. . . 4
                    ♯                         ♯                       
      |
131 | 128, 130 | mpbird 167 |
. . 3
                   ♯                    |
132 | 16, 18, 131 | 3eqtrrd 2227 |
. 2
   ♯                              |
133 | 6, 132 | eqtrd 2222 |
1
                  
    |