Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . 6
  
    |
2 | | eulerth.2 |
. . . . . 6
  ..^     |
3 | | eulerth.4 |
. . . . . 6
               |
4 | 1, 2, 3 | eulerthlema 12230 |
. . . . 5
           
                                     |
5 | 1 | simp1d 1009 |
. . . . . 6
   |
6 | 1 | simp2d 1010 |
. . . . . . . 8
   |
7 | 5 | phicld 12218 |
. . . . . . . . 9
       |
8 | 7 | nnnn0d 9229 |
. . . . . . . 8
       |
9 | | zexpcl 10535 |
. . . . . . . 8
                 |
10 | 6, 8, 9 | syl2anc 411 |
. . . . . . 7
           |
11 | | 1zzd 9280 |
. . . . . . . . 9
   |
12 | 7 | nnzd 9374 |
. . . . . . . . 9
       |
13 | 11, 12 | fzfigd 10431 |
. . . . . . . 8
           |
14 | | ssrab2 3241 |
. . . . . . . . . . 11
  ..^     ..^  |
15 | 2, 14 | eqsstri 3188 |
. . . . . . . . . 10
 ..^  |
16 | | fzo0ssnn0 10215 |
. . . . . . . . . . 11
 ..^  |
17 | | nn0ssz 9271 |
. . . . . . . . . . 11
 |
18 | 16, 17 | sstri 3165 |
. . . . . . . . . 10
 ..^  |
19 | 15, 18 | sstri 3165 |
. . . . . . . . 9
 |
20 | | f1of 5462 |
. . . . . . . . . . 11
            
              |
21 | 3, 20 | syl 14 |
. . . . . . . . . 10
               |
22 | 21 | ffvelcdmda 5652 |
. . . . . . . . 9
 
        
      |
23 | 19, 22 | sselid 3154 |
. . . . . . . 8
 
        
      |
24 | 13, 23 | fprodzcl 11617 |
. . . . . . 7
                 |
25 | 10, 24 | zmulcld 9381 |
. . . . . 6
                           |
26 | | fveq2 5516 |
. . . . . . . . 9
             
                       |
27 | | eqid 2177 |
. . . . . . . . . 10
                                           |
28 | 1, 2, 3, 27 | eulerthlemh 12231 |
. . . . . . . . 9
                  
                         |
29 | | eqid 2177 |
. . . . . . . . . . . . 13
                 |
30 | | fveq2 5516 |
. . . . . . . . . . . . . . . 16
           |
31 | 30 | oveq2d 5891 |
. . . . . . . . . . . . . . 15
 
             |
32 | 31 | oveq1d 5890 |
. . . . . . . . . . . . . 14
       
           |
33 | 32 | cbvmptv 4100 |
. . . . . . . . . . . . 13
                                     |
34 | 1, 2, 29, 3, 33 | eulerthlem1 12227 |
. . . . . . . . . . . 12
                
                |
35 | | fveq2 5516 |
. . . . . . . . . . . . . . . 16
           |
36 | 35 | oveq2d 5891 |
. . . . . . . . . . . . . . 15
 
             |
37 | 36 | oveq1d 5890 |
. . . . . . . . . . . . . 14
       
           |
38 | 37 | cbvmptv 4100 |
. . . . . . . . . . . . 13
                                     |
39 | 38 | feq1i 5359 |
. . . . . . . . . . . 12
                
                             
                |
40 | 34, 39 | sylib 122 |
. . . . . . . . . . 11
                
                |
41 | | fvco3 5588 |
. . . . . . . . . . 11
                 
                                                                             |
42 | 40, 41 | sylan 283 |
. . . . . . . . . 10
 
        
  
               
                          
        |
43 | | eqid 2177 |
. . . . . . . . . . . 12
                                     |
44 | | fveq2 5516 |
. . . . . . . . . . . . . 14
           |
45 | 44 | oveq2d 5891 |
. . . . . . . . . . . . 13
 
             |
46 | 45 | oveq1d 5890 |
. . . . . . . . . . . 12
       
           |
47 | | simpr 110 |
. . . . . . . . . . . 12
 
        
          |
48 | 6 | adantr 276 |
. . . . . . . . . . . . . 14
 
        
  |
49 | 48, 23 | zmulcld 9381 |
. . . . . . . . . . . . 13
 
        
        |
50 | 5 | adantr 276 |
. . . . . . . . . . . . 13
 
        
  |
51 | | zmodfzo 10347 |
. . . . . . . . . . . . 13
       
          ..^   |
52 | 49, 50, 51 | syl2anc 411 |
. . . . . . . . . . . 12
 
        
 
       ..^   |
53 | 43, 46, 47, 52 | fvmptd3 5610 |
. . . . . . . . . . 11
 
        
                
               |
54 | 53 | fveq2d 5520 |
. . . . . . . . . 10
 
        
                    
                     |
55 | 42, 54 | eqtrd 2210 |
. . . . . . . . 9
 
        
  
               
                     |
56 | 21 | ffvelcdmda 5652 |
. . . . . . . . . . 11
 
        
      |
57 | 19, 56 | sselid 3154 |
. . . . . . . . . 10
 
        
      |
58 | 57 | zcnd 9376 |
. . . . . . . . 9
 
        
      |
59 | 26, 13, 28, 55, 58 | fprodf1o 11596 |
. . . . . . . 8
                                            |
60 | 3 | adantr 276 |
. . . . . . . . . 10
 
        
              |
61 | | modgcd 11992 |
. . . . . . . . . . . . 13
       
                     |
62 | 49, 50, 61 | syl2anc 411 |
. . . . . . . . . . . 12
 
        
       
        
   |
63 | 50 | nnzd 9374 |
. . . . . . . . . . . . 13
 
        
  |
64 | 63, 49 | gcdcomd 11975 |
. . . . . . . . . . . 12
 
        
              
   |
65 | 5 | nnzd 9374 |
. . . . . . . . . . . . . . . 16
   |
66 | 6, 65 | gcdcomd 11975 |
. . . . . . . . . . . . . . 15
       |
67 | 1 | simp3d 1011 |
. . . . . . . . . . . . . . 15
     |
68 | 66, 67 | eqtr3d 2212 |
. . . . . . . . . . . . . 14
     |
69 | 68 | adantr 276 |
. . . . . . . . . . . . 13
 
        
    |
70 | 23, 63 | gcdcomd 11975 |
. . . . . . . . . . . . . 14
 
        
              |
71 | | oveq1 5882 |
. . . . . . . . . . . . . . . . . 18
     
         |
72 | 71 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . 17
            
    |
73 | 72, 2 | elrab2 2897 |
. . . . . . . . . . . . . . . 16
    
      ..^          |
74 | 22, 73 | sylib 122 |
. . . . . . . . . . . . . . 15
 
        
      ..^          |
75 | 74 | simprd 114 |
. . . . . . . . . . . . . 14
 
        
        |
76 | 70, 75 | eqtr3d 2212 |
. . . . . . . . . . . . 13
 
        
        |
77 | | rpmul 12098 |
. . . . . . . . . . . . . 14
 
                 
         |
78 | 63, 48, 23, 77 | syl3anc 1238 |
. . . . . . . . . . . . 13
 
        
            
         |
79 | 69, 76, 78 | mp2and 433 |
. . . . . . . . . . . 12
 
        
          |
80 | 62, 64, 79 | 3eqtr2d 2216 |
. . . . . . . . . . 11
 
        
       
    |
81 | | oveq1 5882 |
. . . . . . . . . . . . 13
         
             |
82 | 81 | eqeq1d 2186 |
. . . . . . . . . . . 12
                         |
83 | 82, 2 | elrab2 2897 |
. . . . . . . . . . 11
       

          ..^              |
84 | 52, 80, 83 | sylanbrc 417 |
. . . . . . . . . 10
 
        
 
        |
85 | | f1ocnvfv2 5779 |
. . . . . . . . . 10
                                                  |
86 | 60, 84, 85 | syl2anc 411 |
. . . . . . . . 9
 
        
                       
   |
87 | 86 | prodeq2dv 11574 |
. . . . . . . 8
                                                |
88 | 59, 87 | eqtr2d 2211 |
. . . . . . 7
                 
                 |
89 | | fveq2 5516 |
. . . . . . . . 9
           |
90 | 89 | cbvprodv 11567 |
. . . . . . . 8
                             |
91 | 90, 24 | eqeltrid 2264 |
. . . . . . 7
                 |
92 | 88, 91 | eqeltrd 2254 |
. . . . . 6
                 
   |
93 | | moddvds 11806 |
. . . . . 6
                                                        
                                  
                                         
     |
94 | 5, 25, 92, 93 | syl3anc 1238 |
. . . . 5
            
                                  
                                         
     |
95 | 4, 94 | mpbid 147 |
. . . 4
                                               |
96 | 24 | zcnd 9376 |
. . . . . . . 8
                 |
97 | 96 | mulid2d 7976 |
. . . . . . 7
                                 |
98 | 90, 88, 97 | 3eqtr4a 2236 |
. . . . . 6
                 
  
                |
99 | 98 | oveq2d 5891 |
. . . . 5
           
                                                                             |
100 | 10 | zcnd 9376 |
. . . . . 6
           |
101 | | ax-1cn 7904 |
. . . . . . 7
 |
102 | | subdir 8343 |
. . . . . . 7
                                                             
                                 |
103 | 101, 102 | mp3an2 1325 |
. . . . . 6
                                                                             
                 |
104 | 100, 96, 103 | syl2anc 411 |
. . . . 5
                                     
                                 |
105 | 10, 11 | zsubcld 9380 |
. . . . . . 7
             |
106 | 105 | zcnd 9376 |
. . . . . 6
             |
107 | 106, 96 | mulcomd 7979 |
. . . . 5
                                                       |
108 | 99, 104, 107 | 3eqtr2d 2216 |
. . . 4
           
                                                             |
109 | 95, 108 | breqtrd 4030 |
. . 3
                             |
110 | 1, 2, 3 | eulerthlemrprm 12229 |
. . 3
                   |
111 | | coprmdvds 12092 |
. . . 4
                                                       
               
             |
112 | 65, 24, 105, 111 | syl3anc 1238 |
. . 3
                             
               
             |
113 | 109, 110,
112 | mp2and 433 |
. 2
             |
114 | | 1z 9279 |
. . . 4
 |
115 | | moddvds 11806 |
. . . 4
                       
             |
116 | 114, 115 | mp3an3 1326 |
. . 3
                       
             |
117 | 5, 10, 116 | syl2anc 411 |
. 2
             
             |
118 | 113, 117 | mpbird 167 |
1
               |