Step | Hyp | Ref
| Expression |
1 | | zsqcl 10576 |
. . . . . . . . 9
       |
2 | 1 | adantr 276 |
. . . . . . . 8
 
       |
3 | | 1z 9268 |
. . . . . . . 8
 |
4 | | zdceq 9317 |
. . . . . . . 8
     
 DECID       |
5 | 2, 3, 4 | sylancl 413 |
. . . . . . 7
 
 DECID       |
6 | | iffalse 3542 |
. . . . . . . . 9
                |
7 | 6 | a1i 9 |
. . . . . . . 8
DECID    
                 |
8 | 7 | necon1aidc 2398 |
. . . . . . 7
DECID    
                 |
9 | 5, 8 | syl 14 |
. . . . . 6
 
          
       |
10 | | iftrue 3539 |
. . . . . . 7
                |
11 | | 1ne0 8976 |
. . . . . . . 8
 |
12 | 11 | a1i 9 |
. . . . . . 7
       |
13 | 10, 12 | eqnetrd 2371 |
. . . . . 6
                |
14 | 9, 13 | impbid1 142 |
. . . . 5
 
                  |
15 | 14 | adantr 276 |
. . . 4
    
                 |
16 | | zre 9246 |
. . . . . . 7
   |
17 | 16 | ad2antrr 488 |
. . . . . 6
    
  |
18 | | absresq 11071 |
. . . . . 6
               |
19 | 17, 18 | syl 14 |
. . . . 5
    
              |
20 | | sq1 10599 |
. . . . . 6
     |
21 | 20 | a1i 9 |
. . . . 5
    
      |
22 | 19, 21 | eqeq12d 2192 |
. . . 4
    
            
       |
23 | 17 | recnd 7976 |
. . . . . 6
    
  |
24 | 23 | abscld 11174 |
. . . . 5
    
      |
25 | 23 | absge0d 11177 |
. . . . 5
    
      |
26 | | 1re 7947 |
. . . . . 6
 |
27 | | 0le1 8428 |
. . . . . 6
 |
28 | | sq11 10578 |
. . . . . 6
                                   |
29 | 26, 27, 28 | mpanr12 439 |
. . . . 5
                       
       |
30 | 24, 25, 29 | syl2anc 411 |
. . . 4
    
            
       |
31 | 15, 22, 30 | 3bitr2d 216 |
. . 3
    
                 |
32 | | oveq2 5877 |
. . . . 5
           |
33 | | lgs0 14081 |
. . . . . 6
                |
34 | 33 | adantr 276 |
. . . . 5
 
                |
35 | 32, 34 | sylan9eqr 2232 |
. . . 4
    
               |
36 | 35 | neeq1d 2365 |
. . 3
    
    
            |
37 | | oveq2 5877 |
. . . . 5
       |
38 | | gcdid0 11964 |
. . . . . 6
         |
39 | 38 | adantr 276 |
. . . . 5
 
         |
40 | 37, 39 | sylan9eqr 2232 |
. . . 4
    
        |
41 | 40 | eqeq1d 2186 |
. . 3
    
          |
42 | 31, 36, 41 | 3bitr4d 220 |
. 2
    
    
     |
43 | | lgscl 14082 |
. . . . 5
 
       |
44 | 43 | adantr 276 |
. . . 4
    
      |
45 | | 0z 9253 |
. . . 4
 |
46 | | zapne 9316 |
. . . 4
            #        |
47 | 44, 45, 46 | sylancl 413 |
. . 3
    
     #        |
48 | | eqid 2177 |
. . . . . . 7
           
                
      |
49 | 48 | lgsval4 14088 |
. . . . . 6
 
        
                  
                |
50 | 49 | breq1d 4010 |
. . . . 5
 
      #                                      #    |
51 | | simpr 110 |
. . . . . . . . . . . 12
       
   |
52 | 51 | iftrued 3541 |
. . . . . . . . . . 11
                  |
53 | | neg1ne0 9015 |
. . . . . . . . . . . 12
  |
54 | 53 | a1i 9 |
. . . . . . . . . . 11
          |
55 | 52, 54 | eqnetrd 2371 |
. . . . . . . . . 10
                 |
56 | | simpr 110 |
. . . . . . . . . . . 12
       
   |
57 | 56 | iffalsed 3544 |
. . . . . . . . . . 11
                 |
58 | 11 | a1i 9 |
. . . . . . . . . . 11
         |
59 | 57, 58 | eqnetrd 2371 |
. . . . . . . . . 10
                 |
60 | | simpr 110 |
. . . . . . . . . . . . 13
 
   |
61 | | zdclt 9319 |
. . . . . . . . . . . . 13
 
 DECID   |
62 | 60, 45, 61 | sylancl 413 |
. . . . . . . . . . . 12
 
 DECID   |
63 | | simpl 109 |
. . . . . . . . . . . . 13
 
   |
64 | | zdclt 9319 |
. . . . . . . . . . . . 13
 
 DECID   |
65 | 63, 45, 64 | sylancl 413 |
. . . . . . . . . . . 12
 
 DECID   |
66 | | dcan2 934 |
. . . . . . . . . . . 12
DECID
DECID
DECID 
    |
67 | 62, 65, 66 | sylc 62 |
. . . . . . . . . . 11
 
 DECID     |
68 | | exmiddc 836 |
. . . . . . . . . . 11
DECID    
      |
69 | 67, 68 | syl 14 |
. . . . . . . . . 10
 
    
    |
70 | 55, 59, 69 | mpjaodan 798 |
. . . . . . . . 9
 
           |
71 | 70 | biantrurd 305 |
. . . . . . . 8
 
                                                                     |
72 | 71 | 3adant3 1017 |
. . . . . . 7
 
                                                                     |
73 | | neg1z 9274 |
. . . . . . . . . . . . 13
  |
74 | 73 | a1i 9 |
. . . . . . . . . . . 12
 
    |
75 | | 1zzd 9269 |
. . . . . . . . . . . 12
 
   |
76 | 74, 75, 67 | ifcldcd 3569 |
. . . . . . . . . . 11
 
           |
77 | 76 | 3adant3 1017 |
. . . . . . . . . 10
 
           |
78 | 77 | zcnd 9365 |
. . . . . . . . 9
 
           |
79 | | nnuz 9552 |
. . . . . . . . . . . 12
     |
80 | | 1zzd 9269 |
. . . . . . . . . . . 12
 
   |
81 | 48 | lgsfcl3 14089 |
. . . . . . . . . . . . 13
 
                        |
82 | 81 | ffvelcdmda 5647 |
. . . . . . . . . . . 12
   
                        |
83 | | zmulcl 9295 |
. . . . . . . . . . . . 13
 
     |
84 | 83 | adantl 277 |
. . . . . . . . . . . 12
      
    |
85 | 79, 80, 82, 84 | seqf 10447 |
. . . . . . . . . . 11
 
                           |
86 | | nnabscl 11093 |
. . . . . . . . . . . 12
         |
87 | 86 | 3adant1 1015 |
. . . . . . . . . . 11
 
       |
88 | 85, 87 | ffvelcdmd 5648 |
. . . . . . . . . 10
 
                              |
89 | 88 | zcnd 9365 |
. . . . . . . . 9
 
                              |
90 | 78, 89 | mulap0bd 8603 |
. . . . . . . 8
 
           #                            # 
                                     #    |
91 | | zapne 9316 |
. . . . . . . . . 10
                    #            |
92 | 77, 45, 91 | sylancl 413 |
. . . . . . . . 9
 
          #            |
93 | | zapne 9316 |
. . . . . . . . . 10
               
                                          #                               |
94 | 88, 45, 93 | sylancl 413 |
. . . . . . . . 9
 
                             #                               |
95 | 92, 94 | anbi12d 473 |
. . . . . . . 8
 
           #                            # 
                                        |
96 | 77, 88 | zmulcld 9370 |
. . . . . . . . 9
 
                                        |
97 | | zapne 9316 |
. . . . . . . . 9
                                                                              #                                         |
98 | 96, 45, 97 | sylancl 413 |
. . . . . . . 8
 
                                       #                                         |
99 | 90, 95, 98 | 3bitr3d 218 |
. . . . . . 7
 
                        
             
                                        |
100 | 72, 99 | bitr2d 189 |
. . . . . 6
 
                                                                     |
101 | 100, 98, 94 | 3bitr4d 220 |
. . . . 5
 
                                       #                            #    |
102 | | gcd2n0cl 11953 |
. . . . . . . . . 10
 
     |
103 | 102 | nnzd 9363 |
. . . . . . . . 9
 
     |
104 | | zdceq 9317 |
. . . . . . . . 9
   
 DECID     |
105 | 103, 3, 104 | sylancl 413 |
. . . . . . . 8
 

DECID     |
106 | | eluz2b3 9593 |
. . . . . . . . . . . . 13
               |
107 | | exprmfct 12121 |
. . . . . . . . . . . . 13
      
     |
108 | 106, 107 | sylbir 135 |
. . . . . . . . . . . 12
    
  
    |
109 | | mulcl 7929 |
. . . . . . . . . . . . . . 15
 
     |
110 | 109 | adantl 277 |
. . . . . . . . . . . . . 14
            
    |
111 | 81 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
         
                            |
112 | | elnnuz 9553 |
. . . . . . . . . . . . . . . . . 18

      |
113 | 112 | biimpri 133 |
. . . . . . . . . . . . . . . . 17
    
  |
114 | 113 | adantl 277 |
. . . . . . . . . . . . . . . 16
         
       |
115 | 111, 114 | ffvelcdmd 5648 |
. . . . . . . . . . . . . . 15
         
                            |
116 | 115 | zcnd 9365 |
. . . . . . . . . . . . . 14
         
                            |
117 | | mul02 8334 |
. . . . . . . . . . . . . . 15
     |
118 | 117 | adantl 277 |
. . . . . . . . . . . . . 14
         
     |
119 | | mul01 8336 |
. . . . . . . . . . . . . . 15
     |
120 | 119 | adantl 277 |
. . . . . . . . . . . . . 14
         
     |
121 | | simprr 531 |
. . . . . . . . . . . . . . . . . . 19
    
   
    |
122 | | prmz 12094 |
. . . . . . . . . . . . . . . . . . . . 21

  |
123 | 122 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . 20
    
   
  |
124 | | simpl1 1000 |
. . . . . . . . . . . . . . . . . . . 20
    
   
  |
125 | | simpl2 1001 |
. . . . . . . . . . . . . . . . . . . 20
    
   
  |
126 | | dvdsgcdb 11997 |
. . . . . . . . . . . . . . . . . . . 20
 
  

     |
127 | 123, 124,
125, 126 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . 19
    
   
 

     |
128 | 121, 127 | mpbird 167 |
. . . . . . . . . . . . . . . . . 18
    
   
    |
129 | 128 | simprd 114 |
. . . . . . . . . . . . . . . . 17
    
   
  |
130 | | dvdsabsb 11801 |
. . . . . . . . . . . . . . . . . 18
 
         |
131 | 123, 125,
130 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
    
   

       |
132 | 129, 131 | mpbid 147 |
. . . . . . . . . . . . . . . 16
    
   
      |
133 | 87 | adantr 276 |
. . . . . . . . . . . . . . . . 17
    
   
      |
134 | | dvdsle 11833 |
. . . . . . . . . . . . . . . . 17
                   |
135 | 123, 133,
134 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
    
   
    
       |
136 | 132, 135 | mpd 13 |
. . . . . . . . . . . . . . 15
    
   
      |
137 | | prmnn 12093 |
. . . . . . . . . . . . . . . . . 18

  |
138 | 137 | ad2antrl 490 |
. . . . . . . . . . . . . . . . 17
    
   
  |
139 | 138, 79 | eleqtrdi 2270 |
. . . . . . . . . . . . . . . 16
    
   
      |
140 | 133 | nnzd 9363 |
. . . . . . . . . . . . . . . 16
    
   
      |
141 | | elfz5 10003 |
. . . . . . . . . . . . . . . 16
                   
       |
142 | 139, 140,
141 | syl2anc 411 |
. . . . . . . . . . . . . . 15
    
   
        
       |
143 | 136, 142 | mpbird 167 |
. . . . . . . . . . . . . 14
    
   
          |
144 | | eleq1w 2238 |
. . . . . . . . . . . . . . . . 17
 
   |
145 | | oveq2 5877 |
. . . . . . . . . . . . . . . . . 18
           |
146 | | oveq1 5876 |
. . . . . . . . . . . . . . . . . 18
 
     |
147 | 145, 146 | oveq12d 5887 |
. . . . . . . . . . . . . . . . 17
        
              |
148 | 144, 147 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . 16
  
                       
      |
149 | | simprl 529 |
. . . . . . . . . . . . . . . . . 18
    
   
  |
150 | 149 | iftrued 3541 |
. . . . . . . . . . . . . . . . 17
    
   
          
                |
151 | | lgscl 14082 |
. . . . . . . . . . . . . . . . . . 19
 
       |
152 | 124, 123,
151 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
    
   
      |
153 | | simpl3 1002 |
. . . . . . . . . . . . . . . . . . 19
    
   
  |
154 | | pczcl 12281 |
. . . . . . . . . . . . . . . . . . 19
  
      |
155 | 149, 125,
153, 154 | syl12anc 1236 |
. . . . . . . . . . . . . . . . . 18
    
   
    |
156 | | zexpcl 10521 |
. . . . . . . . . . . . . . . . . 18
                     |
157 | 152, 155,
156 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
    
   
            |
158 | 150, 157 | eqeltrd 2254 |
. . . . . . . . . . . . . . . 16
    
   
          
      |
159 | 48, 148, 138, 158 | fvmptd3 5605 |
. . . . . . . . . . . . . . 15
    
   
                               
      |
160 | | oveq2 5877 |
. . . . . . . . . . . . . . . . . . . 20
           |
161 | | lgs2 14085 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
162 | 124, 161 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
    
   
      
               |
163 | 160, 162 | sylan9eqr 2232 |
. . . . . . . . . . . . . . . . . . 19
         
       
               |
164 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . 21
         
   |
165 | 128 | simpld 112 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   
  |
166 | 165 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
         
   |
167 | 164, 166 | eqbrtrrd 4024 |
. . . . . . . . . . . . . . . . . . . 20
         
   |
168 | 167 | iftrued 3541 |
. . . . . . . . . . . . . . . . . . 19
         
                   |
169 | 163, 168 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . 18
         
       |
170 | | simpll1 1036 |
. . . . . . . . . . . . . . . . . . . 20
          
  |
171 | 149 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
          
  |
172 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . 21
             |
173 | | eldifsn 3718 |
. . . . . . . . . . . . . . . . . . . . 21
    

   |
174 | 171, 172,
173 | sylanbrc 417 |
. . . . . . . . . . . . . . . . . . . 20
          
      |
175 | | lgsval3 14086 |
. . . . . . . . . . . . . . . . . . . 20
 
    
                    |
176 | 170, 174,
175 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
                               |
177 | | oddprm 12242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
178 | 174, 177 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 |
179 | 178 | nnnn0d 9218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
180 | | zexpcl 10521 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
181 | 170, 179,
180 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     |
182 | | zq 9615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
183 | 181, 182 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     |
184 | | zq 9615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
185 | 45, 184 | mp1i 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
186 | | 1nn 8919 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
187 | | nnq 9622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
188 | 186, 187 | mp1i 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
189 | 171, 137 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
  |
190 | | nnq 9622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
191 | 189, 190 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
  |
192 | | nngt0 8933 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
193 | 189, 192 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
  |
194 | | 0zd 9254 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
195 | 165 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
196 | | dvdsval3 11782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       |
197 | 189, 170,
196 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 |
198 | 195, 197 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
199 | | q0mod 10341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
200 | 190, 192,
199 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
201 | 189, 200 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
202 | 198, 201 | eqtr4d 2213 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
203 | 170, 194,
179, 191, 193, 202 | modqexp 10632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                 |
204 | 178 | 0expd 10655 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                     |
205 | 204 | oveq1d 5884 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         |
206 | 203, 205 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                         |
207 | 183, 185,
188, 191, 193, 206 | modqadd1 10347 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             |
208 | | 0p1e1 9022 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
209 | 208 | oveq1i 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
210 | 207, 209 | eqtrdi 2226 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
211 | | prmuz2 12114 |
. . . . . . . . . . . . . . . . . . . . . . . 24

      |
212 | 171, 211 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
      |
213 | | eluzelz 9526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
  |
214 | | zq 9615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
215 | 213, 214 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
  |
216 | | eluz2gt1 9591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
  |
217 | | q1mod 10342 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
218 | 215, 216,
217 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
    |
219 | 212, 218 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
220 | 210, 219 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
221 | 220 | oveq1d 5884 |
. . . . . . . . . . . . . . . . . . . 20
                             |
222 | | 1m1e0 8977 |
. . . . . . . . . . . . . . . . . . . 20
   |
223 | 221, 222 | eqtrdi 2226 |
. . . . . . . . . . . . . . . . . . 19
                           |
224 | 176, 223 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . 18
                 |
225 | | 2z 9270 |
. . . . . . . . . . . . . . . . . . . 20
 |
226 | | zdceq 9317 |
. . . . . . . . . . . . . . . . . . . 20
 
 DECID   |
227 | 123, 225,
226 | sylancl 413 |
. . . . . . . . . . . . . . . . . . 19
    
   
DECID
  |
228 | | dcne 2358 |
. . . . . . . . . . . . . . . . . . 19
DECID     |
229 | 227, 228 | sylib 122 |
. . . . . . . . . . . . . . . . . 18
    
   
    |
230 | 169, 224,
229 | mpjaodan 798 |
. . . . . . . . . . . . . . . . 17
    
   
      |
231 | 230 | oveq1d 5884 |
. . . . . . . . . . . . . . . 16
    
   
                  |
232 | | zq 9615 |
. . . . . . . . . . . . . . . . . . . 20
   |
233 | 125, 232 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
    
   
  |
234 | | pcabs 12308 |
. . . . . . . . . . . . . . . . . . 19
   
         |
235 | 149, 233,
234 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
    
   
      
   |
236 | | pcelnn 12303 |
. . . . . . . . . . . . . . . . . . . 20
             
       |
237 | 149, 133,
236 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
    
   
 
    
       |
238 | 132, 237 | mpbird 167 |
. . . . . . . . . . . . . . . . . 18
    
   
        |
239 | 235, 238 | eqeltrrd 2255 |
. . . . . . . . . . . . . . . . 17
    
   
    |
240 | 239 | 0expd 10655 |
. . . . . . . . . . . . . . . 16
    
   
        |
241 | 231, 240 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
    
   
            |
242 | 159, 150,
241 | 3eqtrd 2214 |
. . . . . . . . . . . . . 14
    
   
                       |
243 | 110, 116,
118, 120, 143, 242 | seq3z 10497 |
. . . . . . . . . . . . 13
    
   
                             |
244 | 243 | rexlimdvaa 2595 |
. . . . . . . . . . . 12
 
  
 
                              |
245 | 108, 244 | syl5 32 |
. . . . . . . . . . 11
 
     
                                |
246 | 102, 245 | mpand 429 |
. . . . . . . . . 10
 
                                  |
247 | 246 | a1d 22 |
. . . . . . . . 9
 
 DECID  
  
                               |
248 | 247 | necon1ddc 2425 |
. . . . . . . 8
 
 DECID  
                                  |
249 | 105, 248 | mpd 13 |
. . . . . . 7
 
                                  |
250 | 94, 249 | sylbid 150 |
. . . . . 6
 
                             #      |
251 | | 1zzd 9269 |
. . . . . . . . . 10
    
    |
252 | | eleq1w 2238 |
. . . . . . . . . . . . 13
 
   |
253 | | oveq2 5877 |
. . . . . . . . . . . . . 14
           |
254 | | oveq1 5876 |
. . . . . . . . . . . . . 14
 
     |
255 | 253, 254 | oveq12d 5887 |
. . . . . . . . . . . . 13
        
              |
256 | 252, 255 | ifbieq1d 3556 |
. . . . . . . . . . . 12
  
                       
      |
257 | | simpr 110 |
. . . . . . . . . . . 12
           |
258 | | simp1 997 |
. . . . . . . . . . . . . . . 16
 
   |
259 | 258 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
             |
260 | | prmz 12094 |
. . . . . . . . . . . . . . . 16

  |
261 | 260 | adantl 277 |
. . . . . . . . . . . . . . 15
             |
262 | | lgscl 14082 |
. . . . . . . . . . . . . . 15
 
       |
263 | 259, 261,
262 | syl2anc 411 |
. . . . . . . . . . . . . 14
                 |
264 | | simpr 110 |
. . . . . . . . . . . . . . 15
             |
265 | | simp2 998 |
. . . . . . . . . . . . . . . 16
 
   |
266 | 265 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
             |
267 | | simp3 999 |
. . . . . . . . . . . . . . . 16
 
   |
268 | 267 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
             |
269 | | pczcl 12281 |
. . . . . . . . . . . . . . 15
  
      |
270 | 264, 266,
268, 269 | syl12anc 1236 |
. . . . . . . . . . . . . 14
           
   |
271 | | zexpcl 10521 |
. . . . . . . . . . . . . 14
                     |
272 | 263, 270,
271 | syl2anc 411 |
. . . . . . . . . . . . 13
                  
    |
273 | | 1zzd 9269 |
. . . . . . . . . . . . 13
         
   |
274 | | prmdc 12113 |
. . . . . . . . . . . . . 14

DECID
  |
275 | 274 | adantl 277 |
. . . . . . . . . . . . 13
        
DECID
  |
276 | 272, 273,
275 | ifcldadc 3563 |
. . . . . . . . . . . 12
                          |
277 | 48, 256, 257, 276 | fvmptd3 5605 |
. . . . . . . . . . 11
                                        
      |
278 | | simpll1 1036 |
. . . . . . . . . . . . . . . . . 18
           |
279 | 260 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
           |
280 | 278, 279,
262 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
               |
281 | 280 | zcnd 9365 |
. . . . . . . . . . . . . . . 16
               |
282 | 281 | adantr 276 |
. . . . . . . . . . . . . . 15
                 |
283 | | oveq2 5877 |
. . . . . . . . . . . . . . . . . . . 20
           |
284 | 278 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
             |
285 | 284, 161 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
                                 |
286 | 283, 285 | sylan9eqr 2232 |
. . . . . . . . . . . . . . . . . . 19
     
                             |
287 | | nprmdvds1 12123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
288 | 287 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
289 | | simpll2 1037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
290 | | dvdsgcdb 11997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
  

     |
291 | 279, 278,
289, 290 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          

     |
292 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
293 | 292 | breq2d 4012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
 
   |
294 | 291, 293 | bitrd 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          

   |
295 | 288, 294 | mtbird 673 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
   |
296 | | imnan 690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 
   |
297 | 295, 296 | sylibr 134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
   |
298 | 297 | con2d 624 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
   |
299 | 298 | imp 124 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
300 | | breq1 4003 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
301 | 300 | notbid 667 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
302 | 299, 301 | syl5ibcom 155 |
. . . . . . . . . . . . . . . . . . . . 21
           
   |
303 | 302 | imp 124 |
. . . . . . . . . . . . . . . . . . . 20
     
      
  |
304 | 303 | iffalsed 3544 |
. . . . . . . . . . . . . . . . . . 19
     
                                    |
305 | 286, 304 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . 18
     
                        |
306 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
            |
307 | 306 | iftrued 3541 |
. . . . . . . . . . . . . . . . . . . . . 22
  
                  |
308 | 11 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . 22
  
       |
309 | 307, 308 | eqnetrd 2371 |
. . . . . . . . . . . . . . . . . . . . 21
  
                  |
310 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
       |
311 | 310 | iffalsed 3544 |
. . . . . . . . . . . . . . . . . . . . . 22
                      |
312 | 53 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
313 | 311, 312 | eqnetrd 2371 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
314 | | 8nn 9075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
315 | | zmodcl 10330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
     |
316 | 314, 315 | mpan2 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
317 | 316 | nn0zd 9362 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
318 | | zdceq 9317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 DECID     |
319 | 317, 3, 318 | sylancl 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24

DECID     |
320 | | 7nn 9074 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
321 | 320 | nnzi 9263 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
322 | | zdceq 9317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 DECID     |
323 | 317, 321,
322 | sylancl 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24

DECID     |
324 | | dcor 935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
DECID  
DECID
  DECID          |
325 | 319, 323,
324 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . 23

DECID         |
326 | | elprg 3611 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
     
         |
327 | 316, 326 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
         |
328 | 327 | dcbid 838 |
. . . . . . . . . . . . . . . . . . . . . . 23
 DECID      DECID          |
329 | 325, 328 | mpbird 167 |
. . . . . . . . . . . . . . . . . . . . . 22

DECID        |
330 | | exmiddc 836 |
. . . . . . . . . . . . . . . . . . . . . 22
DECID     
              |
331 | 329, 330 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
               |
332 | 309, 313,
331 | mpjaodan 798 |
. . . . . . . . . . . . . . . . . . . 20
              |
333 | 258, 332 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
 
              |
334 | 333 | ad4antr 494 |
. . . . . . . . . . . . . . . . . 18
     
                    |
335 | 305, 334 | eqnetrd 2371 |
. . . . . . . . . . . . . . . . 17
     
             |
336 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
337 | 336 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
     
         |
338 | 337, 287 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
     
         |
339 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
         |
340 | 337, 260 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
         |
341 | 284 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
         |
342 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
         |
343 | | eldifsn 3718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    

   |
344 | 337, 342,
343 | sylanbrc 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
       
     |
345 | | oddprm 12242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
346 | 344, 345 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
             |
347 | 346 | nnnn0d 9218 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
             |
348 | | zexpcl 10521 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
349 | 341, 347,
348 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                 |
350 | 289 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
         |
351 | | dvdsgcd 11996 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     
             |
352 | 340, 349,
350, 351 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                 
             |
353 | 339, 352 | mpan2d 428 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       
       
             |
354 | 341 | zcnd 9365 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
         |
355 | 354, 347 | absexpd 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
                                 |
356 | 355 | oveq1d 5884 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                                             |
357 | | gcdabs 11972 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
                               |
358 | 349, 350,
357 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                                     |
359 | | gcdabs 11972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
     
         |
360 | 341, 350,
359 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
           
         |
361 | 292 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
           |
362 | 360, 361 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
           
       |
363 | 299 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
         |
364 | | dvds0 11797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
365 | 340, 364 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
         |
366 | | breq2 4004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
367 | 365, 366 | syl5ibrcom 157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
       
   |
368 | 367 | necon3bd 2390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
       
   |
369 | 363, 368 | mpd 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
         |
370 | | nnabscl 11093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
371 | 341, 369,
370 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
             |
372 | | simpll3 1038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
373 | 289, 372,
86 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
374 | 373 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
             |
375 | | rplpwr 12011 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                               |
376 | 371, 374,
346, 375 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
            
    
                     |
377 | 362, 376 | mpd 13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                           |
378 | 356, 358,
377 | 3eqtr3d 2218 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                   |
379 | 378 | breq2d 4012 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       
         
   |
380 | 353, 379 | sylibd 149 |
. . . . . . . . . . . . . . . . . . . . 21
     
       
       
   |
381 | 338, 380 | mtod 663 |
. . . . . . . . . . . . . . . . . . . 20
     
                 |
382 | | prmnn 12093 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
383 | 382 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
384 | 383 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
     
         |
385 | | dvdsval3 11782 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
             |
386 | 384, 349,
385 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . 21
     
       
       
             |
387 | 386 | necon3bbid 2387 |
. . . . . . . . . . . . . . . . . . . 20
     
       
       
             |
388 | 381, 387 | mpbid 147 |
. . . . . . . . . . . . . . . . . . 19
     
                   |
389 | | lgsvalmod 14087 |
. . . . . . . . . . . . . . . . . . . 20
 
    
                  |
390 | 341, 344,
389 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
     
                         |
391 | | nnq 9622 |
. . . . . . . . . . . . . . . . . . . . 21
   |
392 | | nngt0 8933 |
. . . . . . . . . . . . . . . . . . . . 21
   |
393 | | q0mod 10341 |
. . . . . . . . . . . . . . . . . . . . 21
       |
394 | 391, 392,
393 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
395 | 384, 394 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
     
       
   |
396 | 388, 390,
395 | 3netr4d 2380 |
. . . . . . . . . . . . . . . . . 18
     
                 |
397 | | oveq1 5876 |
. . . . . . . . . . . . . . . . . . 19
               |
398 | 397 | necon3i 2395 |
. . . . . . . . . . . . . . . . . 18
               |
399 | 396, 398 | syl 14 |
. . . . . . . . . . . . . . . . 17
     
             |
400 | 279 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
             |
401 | | zdceq 9317 |
. . . . . . . . . . . . . . . . . . 19
 
 DECID   |
402 | 400, 225,
401 | sylancl 413 |
. . . . . . . . . . . . . . . . . 18
          
DECID
  |
403 | | dcne 2358 |
. . . . . . . . . . . . . . . . . 18
DECID     |
404 | 402, 403 | sylib 122 |
. . . . . . . . . . . . . . . . 17
               |
405 | 335, 399,
404 | mpjaodan 798 |
. . . . . . . . . . . . . . . 16
                 |
406 | 280 | adantr 276 |
. . . . . . . . . . . . . . . . 17
                 |
407 | | zapne 9316 |
. . . . . . . . . . . . . . . . 17
            #        |
408 | 406, 45, 407 | sylancl 413 |
. . . . . . . . . . . . . . . 16
                #        |
409 | 405, 408 | mpbird 167 |
. . . . . . . . . . . . . . 15
               #   |
410 | 336, 289,
372, 269 | syl12anc 1236 |
. . . . . . . . . . . . . . . . 17
         
   |
411 | 410 | nn0zd 9362 |
. . . . . . . . . . . . . . . 16
         
   |
412 | 411 | adantr 276 |
. . . . . . . . . . . . . . 15
           
   |
413 | | expclzaplem 10530 |
. . . . . . . . . . . . . . 15
          #               #    |
414 | 282, 409,
412, 413 | syl3anc 1238 |
. . . . . . . . . . . . . 14
                  
   #    |
415 | | dvdsabsb 11801 |
. . . . . . . . . . . . . . . . . . . . 21
 
         |
416 | 279, 289,
415 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
         
       |
417 | 416 | notbid 667 |
. . . . . . . . . . . . . . . . . . 19
         
       |
418 | | pceq0 12304 |
. . . . . . . . . . . . . . . . . . . 20
             
       |
419 | 336, 373,
418 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
               
       |
420 | 289, 232 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
           |
421 | | pcabs 12308 |
. . . . . . . . . . . . . . . . . . . . 21
   
         |
422 | 336, 420,
421 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
         
         |
423 | 422 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . . . 19
               
     |
424 | 417, 419,
423 | 3bitr2rd 217 |
. . . . . . . . . . . . . . . . . 18
               |
425 | 424 | biimpar 297 |
. . . . . . . . . . . . . . . . 17
               |
426 | 425 | oveq2d 5885 |
. . . . . . . . . . . . . . . 16
                               |
427 | 281 | adantr 276 |
. . . . . . . . . . . . . . . . 17
                 |
428 | 427 | exp0d 10633 |
. . . . . . . . . . . . . . . 16
                     |
429 | 426, 428 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
                       |
430 | | ax-1cn 7895 |
. . . . . . . . . . . . . . . 16
 |
431 | | 1ap0 8537 |
. . . . . . . . . . . . . . . 16
#  |
432 | | breq1 4003 |
. . . . . . . . . . . . . . . . 17
  #
#    |
433 | 432 | elrab 2893 |
. . . . . . . . . . . . . . . 16
  #   #    |
434 | 430, 431,
433 | mpbir2an 942 |
. . . . . . . . . . . . . . 15
 #
  |
435 | 429, 434 | eqeltrdi 2268 |
. . . . . . . . . . . . . 14
                      #    |
436 | | dvdsdc 11789 |
. . . . . . . . . . . . . . . 16
 
 DECID   |
437 | 383, 289,
436 | syl2anc 411 |
. . . . . . . . . . . . . . 15
        
DECID
  |
438 | | exmiddc 836 |
. . . . . . . . . . . . . . 15
DECID 
   |
439 | 437, 438 | syl 14 |
. . . . . . . . . . . . . 14
         
   |
440 | 414, 435,
439 | mpjaodan 798 |
. . . . . . . . . . . . 13
                
   #    |
441 | 440 | adantlr 477 |
. . . . . . . . . . . 12
                  
   #    |
442 | 434 | a1i 9 |
. . . . . . . . . . . 12
         
  #    |
443 | 441, 442,
275 | ifcldadc 3563 |
. . . . . . . . . . 11
                         #    |
444 | 277, 443 | eqeltrd 2254 |
. . . . . . . . . 10
                               #    |
445 | | breq1 4003 |
. . . . . . . . . . . . . 14
  #
#    |
446 | 445 | elrab 2893 |
. . . . . . . . . . . . 13
  #   #    |
447 | | breq1 4003 |
. . . . . . . . . . . . . 14
  #
#    |
448 | 447 | elrab 2893 |
. . . . . . . . . . . . 13
  #   #    |
449 | | mulcl 7929 |
. . . . . . . . . . . . . . 15
 
     |
450 | 449 | ad2ant2r 509 |
. . . . . . . . . . . . . 14
   #   #       |
451 | | mulap0 8600 |
. . . . . . . . . . . . . 14
   #   #     #   |
452 | 450, 451 | jca 306 |
. . . . . . . . . . . . 13
   #   #        #    |
453 | 446, 448,
452 | syl2anb 291 |
. . . . . . . . . . . 12
   #   #
 
     #    |
454 | | breq1 4003 |
. . . . . . . . . . . . 13
    #
  #    |
455 | 454 | elrab 2893 |
. . . . . . . . . . . 12
    #       #    |
456 | 453, 455 | sylibr 134 |
. . . . . . . . . . 11
   #   #
 
   #    |
457 | 456 | adantl 277 |
. . . . . . . . . 10
          #   #
      #    |
458 | 79, 251, 444, 457 | seqf 10447 |
. . . . . . . . 9
    
                           #    |
459 | 87 | adantr 276 |
. . . . . . . . 9
    
        |
460 | 458, 459 | ffvelcdmd 5648 |
. . . . . . . 8
    
                              #    |
461 | | breq1 4003 |
. . . . . . . . . 10
                           
 #              
             #    |
462 | 461 | elrab 2893 |
. . . . . . . . 9
                             # 
                                                       #    |
463 | 462 | simprbi 275 |
. . . . . . . 8
                             #                             #   |
464 | 460, 463 | syl 14 |
. . . . . . 7
    
                             #   |
465 | 464 | ex 115 |
. . . . . 6
 
                               #    |
466 | 250, 465 | impbid 129 |
. . . . 5
 
                             #      |
467 | 50, 101, 466 | 3bitrd 214 |
. . . 4
 
      #      |
468 | 467 | 3expa 1203 |
. . 3
    
     #      |
469 | 47, 468 | bitr3d 190 |
. 2
    
    
     |
470 | | zdceq 9317 |
. . . 4
 
 DECID   |
471 | 60, 45, 470 | sylancl 413 |
. . 3
 
 DECID   |
472 | | dcne 2358 |
. . 3
DECID     |
473 | 471, 472 | sylib 122 |
. 2
 
     |
474 | 42, 469, 473 | mpjaodan 798 |
1
 
           |