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

  |
2 | | nnnn0 8778 |
. . . 4
   |
3 | | nnexpcl 10083 |
. . . 4
 
       |
4 | 1, 2, 3 | syl2an 284 |
. . 3
         |
5 | | phival 11616 |
. . 3
             ♯                    |
6 | 4, 5 | syl 14 |
. 2
           ♯                    |
7 | | nnm1nn0 8812 |
. . . . . 6
 
   |
8 | | nnexpcl 10083 |
. . . . . 6
  
     
    |
9 | 1, 7, 8 | syl2an 284 |
. . . . 5
           |
10 | 9 | nncnd 8534 |
. . . 4
           |
11 | 1 | nncnd 8534 |
. . . . 5

  |
12 | 11 | adantr 271 |
. . . 4
     |
13 | | ax-1cn 7535 |
. . . . 5
 |
14 | | subdi 7960 |
. . . . 5
     
 
     
                         |
15 | 13, 14 | mp3an3 1269 |
. . . 4
     
 
        
       
              |
16 | 10, 12, 15 | syl2anc 404 |
. . 3
       
                         |
17 | 10 | mulid1d 7602 |
. . . 4
       
           |
18 | 17 | oveq2d 5706 |
. . 3
                                       |
19 | | phivalfi 11615 |
. . . . . . 7
                       |
20 | 4, 19 | syl 14 |
. . . . . 6
                     |
21 | | 1zzd 8875 |
. . . . . . . 8
     |
22 | | prmz 11520 |
. . . . . . . . 9

  |
23 | | zexpcl 10085 |
. . . . . . . . 9
 
       |
24 | 22, 2, 23 | syl2an 284 |
. . . . . . . 8
         |
25 | 21, 24 | fzfigd 9987 |
. . . . . . 7
             |
26 | 22 | ad2antrr 473 |
. . . . . . . . 9
            
  |
27 | | elfzelz 9589 |
. . . . . . . . . . 11
           |
28 | 27 | adantl 272 |
. . . . . . . . . 10
            
  |
29 | | 0zd 8860 |
. . . . . . . . . 10
            
  |
30 | 28, 29 | zsubcld 8972 |
. . . . . . . . 9
            
    |
31 | | zdvdsdc 11244 |
. . . . . . . . 9
  
  DECID
    |
32 | 26, 30, 31 | syl2anc 404 |
. . . . . . . 8
            
DECID
    |
33 | 32 | ralrimiva 2458 |
. . . . . . 7
            DECID     |
34 | 25, 33 | ssfirab 6723 |
. . . . . 6
                 |
35 | | inrab 3287 |
. . . . . . 7
                                              
    |
36 | | rpexp 11559 |
. . . . . . . . . . . . . . . . 17
 
             |
37 | 22, 36 | syl3an1 1214 |
. . . . . . . . . . . . . . . 16
               |
38 | 37 | 3expa 1146 |
. . . . . . . . . . . . . . 15
                 |
39 | 38 | an32s 536 |
. . . . . . . . . . . . . 14
                 |
40 | | simpr 109 |
. . . . . . . . . . . . . . . 16
       |
41 | 24 | adantr 271 |
. . . . . . . . . . . . . . . 16
           |
42 | | gcdcom 11392 |
. . . . . . . . . . . . . . . 16
                     |
43 | 40, 41, 42 | syl2anc 404 |
. . . . . . . . . . . . . . 15
                   |
44 | 43 | eqeq1d 2103 |
. . . . . . . . . . . . . 14
                     |
45 | | coprm 11550 |
. . . . . . . . . . . . . . 15
   
     |
46 | 45 | adantlr 462 |
. . . . . . . . . . . . . 14
           |
47 | 39, 44, 46 | 3bitr4d 219 |
. . . . . . . . . . . . 13
           
   |
48 | | zcn 8853 |
. . . . . . . . . . . . . . . . 17
   |
49 | 48 | adantl 272 |
. . . . . . . . . . . . . . . 16
       |
50 | 49 | subid1d 7879 |
. . . . . . . . . . . . . . 15
         |
51 | 50 | breq2d 3879 |
. . . . . . . . . . . . . 14
      

   |
52 | 51 | notbid 630 |
. . . . . . . . . . . . 13
       
   |
53 | 47, 52 | bitr4d 190 |
. . . . . . . . . . . 12
           
     |
54 | 27, 53 | sylan2 281 |
. . . . . . . . . . 11
            
 
    
     |
55 | 54 | biimpd 143 |
. . . . . . . . . 10
            
 
    
     |
56 | | imnan 662 |
. . . . . . . . . 10
          
            |
57 | 55, 56 | sylib 121 |
. . . . . . . . 9
            
            |
58 | 57 | ralrimiva 2458 |
. . . . . . . 8
                   
    |
59 | | rabeq0 3331 |
. . . . . . . 8
                    
                
    |
60 | 58, 59 | sylibr 133 |
. . . . . . 7
                   
     |
61 | 35, 60 | syl5eq 2139 |
. . . . . 6
    
                              |
62 | | hashun 10328 |
. . . . . 6
                               
                             ♯                                 ♯                  ♯                 |
63 | 20, 34, 61, 62 | syl3anc 1181 |
. . . . 5
   ♯                                 ♯                  ♯                 |
64 | 54 | biimprd 157 |
. . . . . . . . . . . 12
            
   
        |
65 | | con1dc 794 |
. . . . . . . . . . . 12
DECID 

 
               
      |
66 | 32, 64, 65 | sylc 62 |
. . . . . . . . . . 11
            
 
          |
67 | 24 | adantr 271 |
. . . . . . . . . . . . . . 15
            
      |
68 | 28, 67 | gcdcld 11387 |
. . . . . . . . . . . . . 14
            
        |
69 | 68 | nn0zd 8965 |
. . . . . . . . . . . . 13
            
        |
70 | | 1zzd 8875 |
. . . . . . . . . . . . 13
            
  |
71 | | zdceq 8920 |
. . . . . . . . . . . . 13
        
DECID         |
72 | 69, 70, 71 | syl2anc 404 |
. . . . . . . . . . . 12
            
DECID         |
73 | | dfordc 832 |
. . . . . . . . . . . 12
DECID      
          
 
           |
74 | 72, 73 | syl 14 |
. . . . . . . . . . 11
            
          
 
           |
75 | 66, 74 | mpbird 166 |
. . . . . . . . . 10
            
 
     
    |
76 | 75 | ralrimiva 2458 |
. . . . . . . . 9
                         |
77 | | rabid2 2557 |
. . . . . . . . 9
                         
  
                      |
78 | 76, 77 | sylibr 133 |
. . . . . . . 8
                           
     |
79 | | unrab 3286 |
. . . . . . . 8
                                              
    |
80 | 78, 79 | syl6reqr 2146 |
. . . . . . 7
    
                                      |
81 | 80 | fveq2d 5344 |
. . . . . 6
   ♯                                ♯            |
82 | 4 | nnnn0d 8824 |
. . . . . . 7
         |
83 | | hashfz1 10306 |
. . . . . . 7
    
♯                |
84 | 82, 83 | syl 14 |
. . . . . 6
   ♯                |
85 | | expm1t 10098 |
. . . . . . 7
 
               |
86 | 11, 85 | sylan 278 |
. . . . . 6
                 |
87 | 81, 84, 86 | 3eqtrd 2131 |
. . . . 5
   ♯                                          |
88 | | hashcl 10304 |
. . . . . . . 8
                 ♯                    |
89 | 20, 88 | syl 14 |
. . . . . . 7
   ♯                    |
90 | 89 | nn0cnd 8826 |
. . . . . 6
   ♯                    |
91 | 1 | adantr 271 |
. . . . . . . . 9
     |
92 | | nn0uz 9152 |
. . . . . . . . . . 11
     |
93 | | 1m1e0 8589 |
. . . . . . . . . . . 12
   |
94 | 93 | fveq2i 5343 |
. . . . . . . . . . 11
           |
95 | 92, 94 | eqtr4i 2118 |
. . . . . . . . . 10
       |
96 | 82, 95 | syl6eleq 2187 |
. . . . . . . . 9
               |
97 | | 0zd 8860 |
. . . . . . . . 9
     |
98 | 91, 21, 96, 97 | hashdvds 11624 |
. . . . . . . 8
   ♯                                        |
99 | 4 | nncnd 8534 |
. . . . . . . . . . . . . 14
         |
100 | 99 | subid1d 7879 |
. . . . . . . . . . . . 13
               |
101 | 100 | oveq1d 5705 |
. . . . . . . . . . . 12
                   |
102 | 91 | nnap0d 8566 |
. . . . . . . . . . . . 13
   #   |
103 | | nnz 8867 |
. . . . . . . . . . . . . 14
   |
104 | 103 | adantl 272 |
. . . . . . . . . . . . 13
     |
105 | 12, 102, 104 | expm1apd 10211 |
. . . . . . . . . . . 12
                 |
106 | 101, 105 | eqtr4d 2130 |
. . . . . . . . . . 11
                   |
107 | 106 | fveq2d 5344 |
. . . . . . . . . 10
                           |
108 | 9 | nnzd 8966 |
. . . . . . . . . . 11
           |
109 | | flid 9840 |
. . . . . . . . . . 11
                    
    |
110 | 108, 109 | syl 14 |
. . . . . . . . . 10
                
    |
111 | 107, 110 | eqtrd 2127 |
. . . . . . . . 9
                  
    |
112 | 93 | oveq1i 5700 |
. . . . . . . . . . . . . 14
       |
113 | | 0m0e0 8632 |
. . . . . . . . . . . . . 14
   |
114 | 112, 113 | eqtri 2115 |
. . . . . . . . . . . . 13
     |
115 | 114 | oveq1i 5700 |
. . . . . . . . . . . 12
         |
116 | 12, 102 | div0apd 8351 |
. . . . . . . . . . . 12
       |
117 | 115, 116 | syl5eq 2139 |
. . . . . . . . . . 11
           |
118 | 117 | fveq2d 5344 |
. . . . . . . . . 10
                   |
119 | | 0z 8859 |
. . . . . . . . . . 11
 |
120 | | flid 9840 |
. . . . . . . . . . 11
       |
121 | 119, 120 | ax-mp 7 |
. . . . . . . . . 10
     |
122 | 118, 121 | syl6eq 2143 |
. . . . . . . . 9
               |
123 | 111, 122 | oveq12d 5708 |
. . . . . . . 8
                                     |
124 | 10 | subid1d 7879 |
. . . . . . . 8
       
           |
125 | 98, 123, 124 | 3eqtrd 2131 |
. . . . . . 7
   ♯                      |
126 | 125 | oveq2d 5706 |
. . . . . 6
    ♯                  ♯                ♯                           |
127 | 90, 10, 126 | comraddd 7736 |
. . . . 5
    ♯                  ♯                   
  ♯                     |
128 | 63, 87, 127 | 3eqtr3rd 2136 |
. . . 4
       
  ♯                             |
129 | 10, 12 | mulcld 7605 |
. . . . 5
       
     |
130 | 129, 10, 90 | subaddd 7908 |
. . . 4
                    ♯                         ♯                       
      |
131 | 128, 130 | mpbird 166 |
. . 3
                   ♯                    |
132 | 16, 18, 131 | 3eqtrrd 2132 |
. 2
   ♯                              |
133 | 6, 132 | eqtrd 2127 |
1
                  
    |