| Step | Hyp | Ref
| Expression |
| 1 | | nn0z 9346 |
. . . . . . . . . 10

  |
| 2 | | zq 9700 |
. . . . . . . . . 10
   |
| 3 | 1, 2 | syl 14 |
. . . . . . . . 9

  |
| 4 | 3 | adantl 277 |
. . . . . . . 8
   
 

  |
| 5 | | odzcl 12412 |
. . . . . . . . . 10
 
              |
| 6 | 5 | adantr 276 |
. . . . . . . . 9
   
 
            |
| 7 | | nnq 9707 |
. . . . . . . . 9
                     |
| 8 | 6, 7 | syl 14 |
. . . . . . . 8
   
 
            |
| 9 | 6 | nngt0d 9034 |
. . . . . . . 8
   
 

           |
| 10 | | modqlt 10425 |
. . . . . . . 8
                                           |
| 11 | 4, 8, 9, 10 | syl3anc 1249 |
. . . . . . 7
   
 
                       |
| 12 | 1 | adantl 277 |
. . . . . . . . . 10
   
 

  |
| 13 | 12, 6 | zmodcld 10437 |
. . . . . . . . 9
   
 
              |
| 14 | 13 | nn0zd 9446 |
. . . . . . . 8
   
 
              |
| 15 | 6 | nnzd 9447 |
. . . . . . . 8
   
 
            |
| 16 | | zltnle 9372 |
. . . . . . . 8
                                           
                       |
| 17 | 14, 15, 16 | syl2anc 411 |
. . . . . . 7
   
 
                     
                       |
| 18 | 11, 17 | mpbid 147 |
. . . . . 6
   
 
         
             |
| 19 | | 1zzd 9353 |
. . . . . . . . . 10
                                      
  |
| 20 | | nnuz 9637 |
. . . . . . . . . . 11
     |
| 21 | 20 | rabeqi 2756 |
. . . . . . . . . 10
                     |
| 22 | | oveq2 5930 |
. . . . . . . . . . . . . . 15
                                 |
| 23 | 22 | oveq1d 5937 |
. . . . . . . . . . . . . 14
                                     |
| 24 | 23 | breq2d 4045 |
. . . . . . . . . . . . 13
                  
                    |
| 25 | 24 | elrab 2920 |
. . . . . . . . . . . 12
                   
                                |
| 26 | 25 | biimpri 133 |
. . . . . . . . . . 11
                                                    |
| 27 | 26 | adantl 277 |
. . . . . . . . . 10
                                      
                     |
| 28 | | simp1 999 |
. . . . . . . . . . . 12
 
     |
| 29 | 28 | ad3antrrr 492 |
. . . . . . . . . . 11
                                                       
  |
| 30 | | simp2 1000 |
. . . . . . . . . . . . . 14
 
     |
| 31 | 30 | ad3antrrr 492 |
. . . . . . . . . . . . 13
                                                       
  |
| 32 | | elfznn 10129 |
. . . . . . . . . . . . . . 15
               
  |
| 33 | 32 | nnnn0d 9302 |
. . . . . . . . . . . . . 14
               
  |
| 34 | 33 | adantl 277 |
. . . . . . . . . . . . 13
                                                       
  |
| 35 | | zexpcl 10646 |
. . . . . . . . . . . . 13
 
       |
| 36 | 31, 34, 35 | syl2anc 411 |
. . . . . . . . . . . 12
                                                       
      |
| 37 | | peano2zm 9364 |
. . . . . . . . . . . 12
             |
| 38 | 36, 37 | syl 14 |
. . . . . . . . . . 11
                                                       
        |
| 39 | | dvdsdc 11963 |
. . . . . . . . . . 11
         DECID
        |
| 40 | 29, 38, 39 | syl2anc 411 |
. . . . . . . . . 10
                                                       
DECID
        |
| 41 | 19, 21, 27, 40 | infssuzledc 10324 |
. . . . . . . . 9
                                      
inf          
             |
| 42 | 41 | ex 115 |
. . . . . . . 8
   
 
                                inf 
                       |
| 43 | 42 | ancomsd 269 |
. . . . . . 7
   
 
                                inf          
              |
| 44 | | odzval 12410 |
. . . . . . . . 9
 
            inf          
  |
| 45 | 44 | adantr 276 |
. . . . . . . 8
   
 
          inf          
  |
| 46 | 45 | breq1d 4043 |
. . . . . . 7
   
 
                     
inf          
              |
| 47 | 43, 46 | sylibrd 169 |
. . . . . 6
   
 
                                        
              |
| 48 | 18, 47 | mtod 664 |
. . . . 5
   
 
                   
             |
| 49 | | imnan 691 |
. . . . 5
                                                               |
| 50 | 48, 49 | sylibr 134 |
. . . 4
   
 
                                 |
| 51 | | elnn0 9251 |
. . . . . 6
           
                          |
| 52 | 13, 51 | sylib 122 |
. . . . 5
   
 
                           |
| 53 | 52 | ord 725 |
. . . 4
   
 
            
              |
| 54 | 50, 53 | syld 45 |
. . 3
   
 
                                 |
| 55 | | simpl1 1002 |
. . . . . . 7
   
 

  |
| 56 | 55 | nnzd 9447 |
. . . . . 6
   
 

  |
| 57 | | dvds0 11971 |
. . . . . 6
   |
| 58 | 56, 57 | syl 14 |
. . . . 5
   
 
   |
| 59 | | simpl2 1003 |
. . . . . . . . 9
   
 

  |
| 60 | 59 | zcnd 9449 |
. . . . . . . 8
   
 

  |
| 61 | 60 | exp0d 10759 |
. . . . . . 7
   
 
       |
| 62 | 61 | oveq1d 5937 |
. . . . . 6
   
 
           |
| 63 | | 1m1e0 9059 |
. . . . . 6
   |
| 64 | 62, 63 | eqtrdi 2245 |
. . . . 5
   
 
         |
| 65 | 58, 64 | breqtrrd 4061 |
. . . 4
   
 
         |
| 66 | | oveq2 5930 |
. . . . . 6
                                 |
| 67 | 66 | oveq1d 5937 |
. . . . 5
                                     |
| 68 | 67 | breq2d 4045 |
. . . 4
                             
         |
| 69 | 65, 68 | syl5ibrcom 157 |
. . 3
   
 
                                 |
| 70 | 54, 69 | impbid 129 |
. 2
   
 
                  
              |
| 71 | 6 | nnnn0d 9302 |
. . . . . . . . 9
   
 
            |
| 72 | | znq 9698 |
. . . . . . . . . . 11
                         |
| 73 | 12, 6, 72 | syl2anc 411 |
. . . . . . . . . 10
   
 
              |
| 74 | | nn0ge0 9274 |
. . . . . . . . . . . 12

  |
| 75 | 74 | adantl 277 |
. . . . . . . . . . 11
   
 

  |
| 76 | | nn0re 9258 |
. . . . . . . . . . . . 13

  |
| 77 | 76 | adantl 277 |
. . . . . . . . . . . 12
   
 

  |
| 78 | 6 | nnred 9003 |
. . . . . . . . . . . 12
   
 
            |
| 79 | | ge0div 8898 |
. . . . . . . . . . . 12
                                    |
| 80 | 77, 78, 9, 79 | syl3anc 1249 |
. . . . . . . . . . 11
   
 
                |
| 81 | 75, 80 | mpbid 147 |
. . . . . . . . . 10
   
 

             |
| 82 | | flqge0nn0 10383 |
. . . . . . . . . 10
            
               
             |
| 83 | 73, 81, 82 | syl2anc 411 |
. . . . . . . . 9
   
 
                  |
| 84 | 71, 83 | nn0mulcld 9307 |
. . . . . . . 8
   
 
                             |
| 85 | | zexpcl 10646 |
. . . . . . . 8
                                                             |
| 86 | 59, 84, 85 | syl2anc 411 |
. . . . . . 7
   
 
                                 |
| 87 | | zq 9700 |
. . . . . . 7
                                                               |
| 88 | 86, 87 | syl 14 |
. . . . . 6
   
 
                                 |
| 89 | | 1z 9352 |
. . . . . . 7
 |
| 90 | | zq 9700 |
. . . . . . 7
   |
| 91 | 89, 90 | mp1i 10 |
. . . . . 6
   
 
   |
| 92 | | zexpcl 10646 |
. . . . . . 7
  
                            |
| 93 | 59, 13, 92 | syl2anc 411 |
. . . . . 6
   
 
                  |
| 94 | | nnq 9707 |
. . . . . . 7
   |
| 95 | 55, 94 | syl 14 |
. . . . . 6
   
 

  |
| 96 | 55 | nngt0d 9034 |
. . . . . 6
   
 

  |
| 97 | 60, 83, 71 | expmuld 10768 |
. . . . . . . 8
   
 
                                                                 |
| 98 | 97 | oveq1d 5937 |
. . . . . . 7
   
 
                                                                     |
| 99 | | zexpcl 10646 |
. . . . . . . . 9
                           |
| 100 | 59, 71, 99 | syl2anc 411 |
. . . . . . . 8
   
 
                |
| 101 | | 1zzd 9353 |
. . . . . . . 8
   
 
   |
| 102 | | odzid 12413 |
. . . . . . . . . 10
 
                    |
| 103 | 102 | adantr 276 |
. . . . . . . . 9
   
 
                  |
| 104 | | moddvds 11964 |
. . . . . . . . . 10
              
                  
                  |
| 105 | 55, 100, 101, 104 | syl3anc 1249 |
. . . . . . . . 9
   
 
                  
                  |
| 106 | 103, 105 | mpbird 167 |
. . . . . . . 8
   
 
                    |
| 107 | 100, 101,
83, 95, 96, 106 | modqexp 10758 |
. . . . . . 7
   
 
                                          
               |
| 108 | 73 | flqcld 10367 |
. . . . . . . . 9
   
 
                  |
| 109 | | 1exp 10660 |
. . . . . . . . 9
                                     |
| 110 | 108, 109 | syl 14 |
. . . . . . . 8
   
 
                      |
| 111 | 110 | oveq1d 5937 |
. . . . . . 7
   
 
                          |
| 112 | 98, 107, 111 | 3eqtrd 2233 |
. . . . . 6
   
 
                                     |
| 113 | 88, 91, 93, 95, 96, 112 | modqmul1 10469 |
. . . . 5
   
 
                                                                       |
| 114 | 60, 13, 84 | expaddd 10767 |
. . . . . . 7
   
 
                                                                                             |
| 115 | | modqval 10416 |
. . . . . . . . . . 11
                                                              |
| 116 | 4, 8, 9, 115 | syl3anc 1249 |
. . . . . . . . . 10
   
 
                                          |
| 117 | 116 | oveq2d 5938 |
. . . . . . . . 9
   
 
                                                                                                  |
| 118 | 84 | nn0cnd 9304 |
. . . . . . . . . 10
   
 
                             |
| 119 | 77 | recnd 8055 |
. . . . . . . . . 10
   
 

  |
| 120 | 118, 119 | pncan3d 8340 |
. . . . . . . . 9
   
 
                                                           |
| 121 | 117, 120 | eqtrd 2229 |
. . . . . . . 8
   
 
                                          |
| 122 | 121 | oveq2d 5938 |
. . . . . . 7
   
 
                                                  |
| 123 | 114, 122 | eqtr3d 2231 |
. . . . . 6
   
 
                                                      |
| 124 | 123 | oveq1d 5937 |
. . . . 5
   
 
                                                          |
| 125 | 93 | zcnd 9449 |
. . . . . . 7
   
 
                  |
| 126 | 125 | mulid2d 8045 |
. . . . . 6
   
 
                                   |
| 127 | 126 | oveq1d 5937 |
. . . . 5
   
 
                                       |
| 128 | 113, 124,
127 | 3eqtr3d 2237 |
. . . 4
   
 
                          |
| 129 | 128 | eqeq1d 2205 |
. . 3
   
 
                                |
| 130 | | zexpcl 10646 |
. . . . 5
 
       |
| 131 | 59, 130 | sylancom 420 |
. . . 4
   
 
       |
| 132 | | moddvds 11964 |
. . . 4
               
         |
| 133 | 55, 131, 101, 132 | syl3anc 1249 |
. . 3
   
 
         
         |
| 134 | | moddvds 11964 |
. . . 4
                                     
                    |
| 135 | 55, 93, 101, 134 | syl3anc 1249 |
. . 3
   
 
                    
                    |
| 136 | 129, 133,
135 | 3bitr3d 218 |
. 2
   
 
       
                    |
| 137 | | dvdsval3 11956 |
. . 3
          
                         |
| 138 | 6, 12, 137 | syl2anc 411 |
. 2
   
 
                         |
| 139 | 70, 136, 138 | 3bitr4d 220 |
1
   
 
                
   |