Step | Hyp | Ref
| Expression |
1 | | zmulcl 9282 |
. . . 4
 
     |
2 | 1 | 3adant2 1016 |
. . 3
 
 
   |
3 | | zmulcl 9282 |
. . . 4
 
     |
4 | 3 | 3adant1 1015 |
. . 3
 
 
   |
5 | | simpl 109 |
. . 3
 
    
  |
6 | | congr 12070 |
. . 3
    

        
       
     |
7 | 2, 4, 5, 6 | syl2an3an 1298 |
. 2
  
                             |
8 | | simpl 109 |
. . . . . . . . . . . 12
 
   |
9 | | nnz 9248 |
. . . . . . . . . . . . . 14
   |
10 | | nnne0 8923 |
. . . . . . . . . . . . . 14
   |
11 | 9, 10 | jca 306 |
. . . . . . . . . . . . 13
 
   |
12 | 11 | adantl 277 |
. . . . . . . . . . . 12
 
     |
13 | | eqidd 2178 |
. . . . . . . . . . . 12
 
       |
14 | 8, 12, 13 | 3jca 1177 |
. . . . . . . . . . 11
 
           |
15 | 14 | ex 115 |
. . . . . . . . . 10
 
 
         |
16 | 15 | 3ad2ant3 1020 |
. . . . . . . . 9
 
 
 
         |
17 | 16 | com12 30 |
. . . . . . . 8
  
            |
18 | 17 | adantr 276 |
. . . . . . 7
 
        

         |
19 | 18 | impcom 125 |
. . . . . 6
  
                  |
20 | | divgcdcoprmex 12072 |
. . . . . 6
  
        
        
    |
21 | 19, 20 | syl 14 |
. . . . 5
  
          
        
    |
22 | 21 | adantr 276 |
. . . 4
     
         
        
    |
23 | | oveq2 5876 |
. . . . . . . . . 10
               |
24 | 23 | 3ad2ant2 1019 |
. . . . . . . . 9
     
    
            |
25 | 24 | adantl 277 |
. . . . . . . 8
     
 
          
                      |
26 | | oveq2 5876 |
. . . . . . . . . . 11
     
         |
27 | | oveq2 5876 |
. . . . . . . . . . 11
     
         |
28 | 26, 27 | oveq12d 5886 |
. . . . . . . . . 10
                  
        |
29 | 28 | 3ad2ant1 1018 |
. . . . . . . . 9
     
    
     
                  |
30 | 29 | adantl 277 |
. . . . . . . 8
     
 
          
                         
        |
31 | 25, 30 | eqeq12d 2192 |
. . . . . . 7
     
 
          
                    
                       |
32 | | simpr 110 |
. . . . . . . . . . . . . 14
     
         |
33 | 32 | zcnd 9352 |
. . . . . . . . . . . . 13
     
         |
34 | 33 | adantr 276 |
. . . . . . . . . . . 12
      
            |
35 | | simp3 999 |
. . . . . . . . . . . . . . . 16
 
   |
36 | 35 | adantr 276 |
. . . . . . . . . . . . . . 15
  
          |
37 | 9 | ad2antrl 490 |
. . . . . . . . . . . . . . 15
  
          |
38 | 36, 37 | gcdcld 11939 |
. . . . . . . . . . . . . 14
  
            |
39 | 38 | nn0cnd 9207 |
. . . . . . . . . . . . 13
  
            |
40 | 39 | ad2antrr 488 |
. . . . . . . . . . . 12
      
              |
41 | | simpr 110 |
. . . . . . . . . . . . . 14
 
   |
42 | 41 | zcnd 9352 |
. . . . . . . . . . . . 13
 
   |
43 | 42 | adantl 277 |
. . . . . . . . . . . 12
      
            |
44 | 34, 40, 43 | mul12d 8086 |
. . . . . . . . . . 11
      
                        |
45 | | simp1 997 |
. . . . . . . . . . . . . . 15
 
   |
46 | 45 | zcnd 9352 |
. . . . . . . . . . . . . 14
 
   |
47 | 46 | ad3antrrr 492 |
. . . . . . . . . . . . 13
      
         
  |
48 | 35 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
     
         |
49 | 5 | nnzd 9350 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
50 | 49 | adantl 277 |
. . . . . . . . . . . . . . . . 17
  
          |
51 | 50 | adantr 276 |
. . . . . . . . . . . . . . . 16
     
         |
52 | 48, 51 | gcdcld 11939 |
. . . . . . . . . . . . . . 15
     
           |
53 | 52 | nn0cnd 9207 |
. . . . . . . . . . . . . 14
     
           |
54 | 53 | adantr 276 |
. . . . . . . . . . . . 13
      
              |
55 | | simpl 109 |
. . . . . . . . . . . . . . 15
 
   |
56 | 55 | zcnd 9352 |
. . . . . . . . . . . . . 14
 
   |
57 | 56 | adantl 277 |
. . . . . . . . . . . . 13
      
            |
58 | 47, 54, 57 | mul12d 8086 |
. . . . . . . . . . . 12
      
                        |
59 | | simp2 998 |
. . . . . . . . . . . . . . 15
 
   |
60 | 59 | zcnd 9352 |
. . . . . . . . . . . . . 14
 
   |
61 | 60 | ad3antrrr 492 |
. . . . . . . . . . . . 13
      
         
  |
62 | 36, 50 | gcdcld 11939 |
. . . . . . . . . . . . . . 15
  
            |
63 | 62 | nn0cnd 9207 |
. . . . . . . . . . . . . 14
  
            |
64 | 63 | ad2antrr 488 |
. . . . . . . . . . . . 13
      
              |
65 | 61, 64, 57 | mul12d 8086 |
. . . . . . . . . . . 12
      
                        |
66 | 58, 65 | oveq12d 5886 |
. . . . . . . . . . 11
      
                                        |
67 | 44, 66 | eqeq12d 2192 |
. . . . . . . . . 10
      
                              
                       |
68 | 45 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
      
         
  |
69 | 55 | adantl 277 |
. . . . . . . . . . . . . . 15
      
            |
70 | 68, 69 | zmulcld 9357 |
. . . . . . . . . . . . . 14
      
              |
71 | 70 | zcnd 9352 |
. . . . . . . . . . . . 13
      
              |
72 | 59 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
      
         
  |
73 | 72, 69 | zmulcld 9357 |
. . . . . . . . . . . . . 14
      
              |
74 | 73 | zcnd 9352 |
. . . . . . . . . . . . 13
      
              |
75 | 64, 71, 74 | subdid 8348 |
. . . . . . . . . . . 12
      
                                    |
76 | 75 | eqcomd 2183 |
. . . . . . . . . . 11
      
                              
     |
77 | 76 | eqeq2d 2189 |
. . . . . . . . . 10
      
                              
                   |
78 | 32 | adantr 276 |
. . . . . . . . . . . . 13
      
            |
79 | | simprr 531 |
. . . . . . . . . . . . 13
      
            |
80 | 78, 79 | zmulcld 9357 |
. . . . . . . . . . . 12
      
              |
81 | 80 | zcnd 9352 |
. . . . . . . . . . 11
      
              |
82 | | zmulcl 9282 |
. . . . . . . . . . . . . . . . . 18
 
     |
83 | 82 | ad2ant2r 509 |
. . . . . . . . . . . . . . . . 17
           |
84 | | zmulcl 9282 |
. . . . . . . . . . . . . . . . . 18
 
     |
85 | 84 | ad2ant2lr 510 |
. . . . . . . . . . . . . . . . 17
           |
86 | 83, 85 | zsubcld 9356 |
. . . . . . . . . . . . . . . 16
          
    |
87 | 86 | zcnd 9352 |
. . . . . . . . . . . . . . 15
          
    |
88 | 87 | ex 115 |
. . . . . . . . . . . . . 14
 
             |
89 | 88 | 3adant3 1017 |
. . . . . . . . . . . . 13
 
       
     |
90 | 89 | ad2antrr 488 |
. . . . . . . . . . . 12
     
                   |
91 | 90 | imp 124 |
. . . . . . . . . . 11
      
             
    |
92 | 10 | ad2antrl 490 |
. . . . . . . . . . . . . . 15
  
          |
93 | | gcd2n0cl 11940 |
. . . . . . . . . . . . . . 15
 
     |
94 | 36, 50, 92, 93 | syl3anc 1238 |
. . . . . . . . . . . . . 14
  
            |
95 | 94 | nnne0d 8940 |
. . . . . . . . . . . . 13
  
            |
96 | 95 | ad2antrr 488 |
. . . . . . . . . . . 12
      
              |
97 | 52 | adantr 276 |
. . . . . . . . . . . . . 14
      
              |
98 | 97 | nn0zd 9349 |
. . . . . . . . . . . . 13
      
              |
99 | | 0zd 9241 |
. . . . . . . . . . . . 13
      
            |
100 | | zapne 9303 |
. . . . . . . . . . . . 13
   
    #
     |
101 | 98, 99, 100 | syl2anc 411 |
. . . . . . . . . . . 12
      
             #
     |
102 | 96, 101 | mpbird 167 |
. . . . . . . . . . 11
      
            #   |
103 | 81, 91, 64, 102 | mulcanapd 8594 |
. . . . . . . . . 10
      
                                      |
104 | 67, 77, 103 | 3bitrd 214 |
. . . . . . . . 9
      
                              
           |
105 | 104 | adantr 276 |
. . . . . . . 8
     
 
          
                                
           |
106 | | zcn 9234 |
. . . . . . . . . . . . . . . . . 18
   |
107 | | zcn 9234 |
. . . . . . . . . . . . . . . . . 18
   |
108 | 106, 107 | anim12i 338 |
. . . . . . . . . . . . . . . . 17
 
     |
109 | 108 | 3adant3 1017 |
. . . . . . . . . . . . . . . 16
 
 
   |
110 | 109 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
     
           |
111 | 110, 56 | anim12i 338 |
. . . . . . . . . . . . . 14
      
                |
112 | | df-3an 980 |
. . . . . . . . . . . . . 14
 

 
    |
113 | 111, 112 | sylibr 134 |
. . . . . . . . . . . . 13
      
          
   |
114 | | subdir 8320 |
. . . . . . . . . . . . 13
 
        
    |
115 | 113, 114 | syl 14 |
. . . . . . . . . . . 12
      
                      |
116 | 115 | eqcomd 2183 |
. . . . . . . . . . 11
      
             
        |
117 | 116 | adantr 276 |
. . . . . . . . . 10
     
 
          
                        |
118 | 117 | eqeq2d 2189 |
. . . . . . . . 9
     
 
          
                    
         |
119 | 5 | nncnd 8909 |
. . . . . . . . . . . . . . . . 17
 
    
  |
120 | 119 | adantl 277 |
. . . . . . . . . . . . . . . 16
  
          |
121 | 120 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
      
         
  |
122 | 79 | zcnd 9352 |
. . . . . . . . . . . . . . 15
      
            |
123 | 121, 122,
40, 102 | divmulap2d 8757 |
. . . . . . . . . . . . . 14
      
                      |
124 | | simpll 527 |
. . . . . . . . . . . . . . . . 17
     
 
          
        
         |
125 | 69 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
     
 
          
      |
126 | 5 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
  
          |
127 | | divgcdnnr 11947 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
128 | 126, 36, 127 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
  
              |
129 | 128 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . 19
     
 
          
          |
130 | | eleq1 2240 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
131 | 130 | eqcoms 2180 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
132 | 131 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
     
 
          
            |
133 | 129, 132 | mpbird 167 |
. . . . . . . . . . . . . . . . . 18
     
 
          
      |
134 | 125, 133 | jca 306 |
. . . . . . . . . . . . . . . . 17
     
 
          
        |
135 | 124, 134 | jca 306 |
. . . . . . . . . . . . . . . 16
     
 
          
       
 
            |
136 | | simpr 110 |
. . . . . . . . . . . . . . . 16
     
 
          
          |
137 | | nnz 9248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
138 | 137 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
139 | 138 | anim2i 342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
    |
140 | 139 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
141 | | dvdsmul2 11792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
     |
142 | 140, 141 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
143 | | breq2 4004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
 
       |
144 | | zsubcl 9270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
     |
145 | 144 | zcnd 9352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
     |
146 | 145 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
147 | | zcn 9234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
148 | 147 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
  |
149 | 148 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
150 | 146, 149 | mulcomd 7956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   |
151 | 150 | breq2d 4012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                     |
152 | 137 | anim2i 342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
     |
153 | | gcdcom 11944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
       |
154 | 152, 153 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
       |
155 | 154 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
         |
156 | 155 | ad2antll 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                 |
157 | 152 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
    |
158 | 157 | ancomd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
    |
159 | 144, 158 | anim12i 338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                 |
160 | 159 | ancomd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
            
    |
161 | | df-3an 980 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 

 
 
      |
162 | 160, 161 | sylibr 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
               |
163 | | coprmdvds 12062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 

          

    |
164 | 162, 163 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
               
 
     |
165 | | simprr 531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
  |
166 | 165 | anim2i 342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
               |
167 | 166 | ancomd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
               |
168 | | 3anass 982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 

      |
169 | 167, 168 | sylibr 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             |
170 | | moddvds 11777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
     

    |
171 | 169, 170 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
              
    |
172 | 164, 171 | sylibrd 169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
               
         |
173 | 172 | expcomd 1441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           
  
 
        |
174 | 156, 173 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           
  
 
        |
175 | 174 | com23 78 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           
 
 
         |
176 | 151, 175 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             
 
         |
177 | 176 | com3l 81 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                         |
178 | 143, 177 | syl6bi 163 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
                       |
179 | 178 | com14 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
 
                 |
180 | 142, 179 | mpd 13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
               |
181 | 180 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
               
         |
182 | 181 | 3adant3 1017 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     
 
                 |
183 | 182 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
  
          
 
 
                 |
184 | 183 | impl 380 |
. . . . . . . . . . . . . . . . . . . 20
      
                   
        |
185 | 184 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
     
 
          
             
        |
186 | 185 | imp 124 |
. . . . . . . . . . . . . . . . . 18
      
            
             
       |
187 | | eqtr2 2196 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
  |
188 | | oveq2 5876 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
189 | | oveq2 5876 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
190 | 188, 189 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
191 | 187, 190 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
            |
192 | 191 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
        |
193 | 192 | eqcoms 2180 |
. . . . . . . . . . . . . . . . . . . . . 22
              
        |
194 | 193 | ad2antll 491 |
. . . . . . . . . . . . . . . . . . . . 21
  
                          |
195 | 194 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
      
                            |
196 | 195 | imp 124 |
. . . . . . . . . . . . . . . . . . 19
     
 
          
        
       |
197 | 196 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
      
            
                   |
198 | 186, 197 | sylibrd 169 |
. . . . . . . . . . . . . . . . 17
      
            
             
       |
199 | 198 | ex 115 |
. . . . . . . . . . . . . . . 16
     
 
          
             
        |
200 | 135, 136,
199 | syl2anc 411 |
. . . . . . . . . . . . . . 15
     
 
          
             
        |
201 | 200 | ex 115 |
. . . . . . . . . . . . . 14
      
                 
                |
202 | 123, 201 | sylbird 170 |
. . . . . . . . . . . . 13
      
                 
                |
203 | 202 | com3l 81 |
. . . . . . . . . . . 12
            
                            |
204 | 203 | a1i 9 |
. . . . . . . . . . 11
     
           
                             |
205 | 204 | 3imp 1193 |
. . . . . . . . . 10
     
    
      
                           |
206 | 205 | impcom 125 |
. . . . . . . . 9
     
 
          
                          |
207 | 118, 206 | sylbid 150 |
. . . . . . . 8
     
 
          
                            |
208 | 105, 207 | sylbid 150 |
. . . . . . 7
     
 
          
                                        |
209 | 31, 208 | sylbid 150 |
. . . . . 6
     
 
          
                            |
210 | 209 | ex 115 |
. . . . 5
      
                      
      
          |
211 | 210 | rexlimdvva 2602 |
. . . 4
     
                     
      
          |
212 | 22, 211 | mpd 13 |
. . 3
     
             
 
       |
213 | 212 | rexlimdva 2594 |
. 2
  
                         |
214 | 7, 213 | sylbid 150 |
1
  
                
       |