Step | Hyp | Ref
| Expression |
1 | | gcdcl 11969 |
. . . . . 6
 
     |
2 | 1 | nn0ge0d 9234 |
. . . . 5
 

    |
3 | | gcddvds 11966 |
. . . . 5
 
    
    |
4 | | 3anass 982 |
. . . . . . . 8
 

      |
5 | | ancom 266 |
. . . . . . . 8
  
        |
6 | 4, 5 | bitri 184 |
. . . . . . 7
 

 
    |
7 | | dvdsgcd 12015 |
. . . . . . 7
 
  
      |
8 | 6, 7 | sylbir 135 |
. . . . . 6
             |
9 | 8 | ralrimiva 2550 |
. . . . 5
 
    

    |
10 | 2, 3, 9 | 3jca 1177 |
. . . 4
 
       
    
       |
11 | 10 | adantr 276 |
. . 3
      
         
 
       |
12 | | breq2 4009 |
. . . . 5
  

     |
13 | | breq1 4008 |
. . . . . 6
  
      |
14 | | breq1 4008 |
. . . . . 6
  
      |
15 | 13, 14 | anbi12d 473 |
. . . . 5
  
  
         |
16 | | breq2 4009 |
. . . . . . 7
  

     |
17 | 16 | imbi2d 230 |
. . . . . 6
  
  
           |
18 | 17 | ralbidv 2477 |
. . . . 5
  
 
 
     

     |
19 | 12, 15, 18 | 3anbi123d 1312 |
. . . 4
  
 

   
  
         
 
        |
20 | 19 | adantl 277 |
. . 3
      
 

   
  
         
 
        |
21 | 11, 20 | mpbird 167 |
. 2
      
   
 
     |
22 | | gcdval 11962 |
. . . 4
 
                
   |
23 | 22 | adantr 276 |
. . 3
      
                      
   |
24 | | iftrue 3541 |
. . . . . . 7
                    |
25 | 24 | adantr 276 |
. . . . . 6
     
  
        
             
   |
26 | | breq2 4009 |
. . . . . . . . . . 11
 
   |
27 | | breq2 4009 |
. . . . . . . . . . 11
 
   |
28 | 26, 27 | bi2anan9 606 |
. . . . . . . . . 10
     
     |
29 | | breq2 4009 |
. . . . . . . . . . . . 13
 
   |
30 | | breq2 4009 |
. . . . . . . . . . . . 13
 
   |
31 | 29, 30 | bi2anan9 606 |
. . . . . . . . . . . 12
     

    |
32 | 31 | imbi1d 231 |
. . . . . . . . . . 11
      
  
     |
33 | 32 | ralbidv 2477 |
. . . . . . . . . 10
        
        |
34 | 28, 33 | 3anbi23d 1315 |
. . . . . . . . 9
       
 
  
   
 
      |
35 | | dvdszrcl 11801 |
. . . . . . . . . . . . 13
 
   |
36 | | dvds0 11815 |
. . . . . . . . . . . . . . . . . . . 20
   |
37 | 36, 36 | jca 306 |
. . . . . . . . . . . . . . . . . . 19
 
   |
38 | 37 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
  

     |
39 | | pm5.5 242 |
. . . . . . . . . . . . . . . . . 18
           |
40 | 38, 39 | syl 14 |
. . . . . . . . . . . . . . . . 17
  

         |
41 | 40 | ralbidva 2473 |
. . . . . . . . . . . . . . . 16
        
    |
42 | | 0z 9266 |
. . . . . . . . . . . . . . . . . . 19
 |
43 | | breq1 4008 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
44 | 43 | rspcv 2839 |
. . . . . . . . . . . . . . . . . . 19
  
   |
45 | 42, 44 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
 
  |
46 | | 0dvds 11820 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
47 | 46 | biimpd 144 |
. . . . . . . . . . . . . . . . . . 19
 
   |
48 | | eqcom 2179 |
. . . . . . . . . . . . . . . . . . 19

  |
49 | 47, 48 | imbitrrdi 162 |
. . . . . . . . . . . . . . . . . 18
 
   |
50 | 45, 49 | syl5 32 |
. . . . . . . . . . . . . . . . 17
  
   |
51 | 50 | adantr 276 |
. . . . . . . . . . . . . . . 16
        |
52 | 41, 51 | sylbid 150 |
. . . . . . . . . . . . . . 15
            |
53 | 52 | ex 115 |
. . . . . . . . . . . . . 14
 
    
     |
54 | 53 | adantr 276 |
. . . . . . . . . . . . 13
 
            |
55 | 35, 54 | syl 14 |
. . . . . . . . . . . 12
 
    
     |
56 | 55 | adantr 276 |
. . . . . . . . . . 11
              |
57 | 56 | com12 30 |
. . . . . . . . . 10
  
           |
58 | 57 | 3imp 1193 |
. . . . . . . . 9
 

         |
59 | 34, 58 | biimtrdi 163 |
. . . . . . . 8
       
 
      |
60 | 59 | adantld 278 |
. . . . . . 7
     
  
           |
61 | 60 | imp 124 |
. . . . . 6
     
  
        
  |
62 | 25, 61 | eqtrd 2210 |
. . . . 5
     
  
        
             
   |
63 | 62 | ancoms 268 |
. . . 4
     

   
    
           
       |
64 | | iffalse 3544 |
. . . . . . 7
  
             
    
      |
65 | 64 | adantr 276 |
. . . . . 6
         
       
             
    
      |
66 | | lttri3 8039 |
. . . . . . . 8
 
  
    |
67 | 66 | adantl 277 |
. . . . . . 7
        

   
         
    |
68 | | dvdszrcl 11801 |
. . . . . . . . . . . 12
 
   |
69 | 68 | simpld 112 |
. . . . . . . . . . 11
   |
70 | 69 | zred 9377 |
. . . . . . . . . 10
   |
71 | 70 | adantr 276 |
. . . . . . . . 9
  
  |
72 | 71 | 3ad2ant2 1019 |
. . . . . . . 8
 

   
     |
73 | 72 | ad2antll 491 |
. . . . . . 7
         
       
  |
74 | | breq1 4008 |
. . . . . . . . . . 11
 
   |
75 | | breq1 4008 |
. . . . . . . . . . 11
 
   |
76 | 74, 75 | anbi12d 473 |
. . . . . . . . . 10
  
 
    |
77 | 76 | elrab 2895 |
. . . . . . . . 9
    
      |
78 | | breq1 4008 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
79 | | breq1 4008 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
80 | 78, 79 | anbi12d 473 |
. . . . . . . . . . . . . . . . . . . 20
  
 
    |
81 | | breq1 4008 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
82 | 80, 81 | imbi12d 234 |
. . . . . . . . . . . . . . . . . . 19
    

 

    |
83 | 82 | rspcv 2839 |
. . . . . . . . . . . . . . . . . 18
  
  
  
     |
84 | 83 | com23 78 |
. . . . . . . . . . . . . . . . 17
  
           |
85 | 84 | imp 124 |
. . . . . . . . . . . . . . . 16
  
 
 
 
 
   |
86 | 85 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
          
           |
87 | | elnn0z 9268 |
. . . . . . . . . . . . . . . . . . . . . 22

    |
88 | 87 | simplbi2 385 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
89 | 88 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
90 | 68, 89 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
 
   |
91 | 90 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
       |
92 | 91 | impcom 125 |
. . . . . . . . . . . . . . . . 17
 

    |
93 | | zre 9259 |
. . . . . . . . . . . . . . . . . . . . 21
   |
94 | 93 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
   
  
 
  |
95 | 94 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . 19
       
     
  
        |
96 | 71 | ad3antlr 493 |
. . . . . . . . . . . . . . . . . . 19
       
     
  
        |
97 | | simp-5l 543 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  
    
  
     |
98 | | elnn0 9180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

    |
99 | | 2a1 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
                 |
100 | | breq1 4008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
101 | | breq1 4008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
102 | 100, 101 | anbi12d 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  
 
    |
103 | 102 | anbi2d 464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
         |
104 | 103 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
             
 
     |
105 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
          
      |
106 | | zdceq 9330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
 DECID   |
107 | 42, 106 | mpan2 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37

DECID
  |
108 | | ianordc 899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
DECID
 
 
    |
109 | 107, 108 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
    |
110 | 109 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
          
    

    |
111 | 105, 110 | mpbid 147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
          
      |
112 | | dvdszrcl 11801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
   |
113 | | 0dvds 11820 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
   |
114 | | pm2.24 621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
   |
115 | 113, 114 | biimtrdi 163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
     |
116 | 115 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
  
    |
117 | 112, 116 | mpcom 36 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   |
118 | 117 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
   |
119 | 118 | com12 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   
   |
120 | | dvdszrcl 11801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
   |
121 | | 0dvds 11820 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
   |
122 | | pm2.24 621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 
   |
123 | 121, 122 | biimtrdi 163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
     |
124 | 123 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
  
    |
125 | 120, 124 | mpcom 36 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   |
126 | 125 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
   |
127 | 126 | com12 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   
   |
128 | 119, 127 | jaoi 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    
    |
129 | 111, 128 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
          
    
   |
130 | 129 | adantld 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
          
          |
131 | 130 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
           
     |
132 | 104, 131 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
             
   |
133 | 132 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
                 |
134 | 99, 133 | jaoi 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
     
  
              |
135 | 98, 134 | sylbi 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

          
           |
136 | 135 | impcom 125 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
       
         |
137 | 136 | imp 124 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  
    
  
     |
138 | | dvdsle 11852 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 
   |
139 | 97, 137, 138 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
  
    
  
   
   |
140 | 139 | exp31 364 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
        
     |
141 | 140 | com14 88 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
 
          
 
     |
142 | 141 | imp 124 |
. . . . . . . . . . . . . . . . . . . . 21
 
          
       
    |
143 | 142 | impcom 125 |
. . . . . . . . . . . . . . . . . . . 20
   
         
  
    
   |
144 | 143 | imp 124 |
. . . . . . . . . . . . . . . . . . 19
       
     
  
        |
145 | 95, 96, 144 | lensymd 8081 |
. . . . . . . . . . . . . . . . . 18
       
     
  
     
  |
146 | 145 | exp31 364 |
. . . . . . . . . . . . . . . . 17
 

         
       
    |
147 | 92, 146 | mpan2d 428 |
. . . . . . . . . . . . . . . 16
 

       
  
    
    |
148 | 147 | com13 80 |
. . . . . . . . . . . . . . 15
          
            |
149 | 86, 148 | syld 45 |
. . . . . . . . . . . . . 14
          
          
 
    |
150 | 149 | com13 80 |
. . . . . . . . . . . . 13
 

            
       
    |
151 | 150 | 3impia 1200 |
. . . . . . . . . . . 12
 

   
       
       
   |
152 | 151 | com12 30 |
. . . . . . . . . . 11
          
     
     
   |
153 | 152 | expimpd 363 |
. . . . . . . . . 10
   
  
 
      
      
   |
154 | 153 | expimpd 363 |
. . . . . . . . 9
  
 
     
  
        
   |
155 | 77, 154 | sylbi 121 |
. . . . . . . 8
            

   
    
   |
156 | 155 | impcom 125 |
. . . . . . 7
        

   
      
     |
157 | 69 | adantr 276 |
. . . . . . . . . . . . 13
  
  |
158 | 157 | ancri 324 |
. . . . . . . . . . . 12
    
    |
159 | 158 | 3ad2ant2 1019 |
. . . . . . . . . . 11
 

   
   
     |
160 | 159 | ad2antll 491 |
. . . . . . . . . 10
         
       
      |
161 | 160 | adantr 276 |
. . . . . . . . 9
        

   
         
    |
162 | | breq1 4008 |
. . . . . . . . . . 11
 
   |
163 | | breq1 4008 |
. . . . . . . . . . 11
 
   |
164 | 162, 163 | anbi12d 473 |
. . . . . . . . . 10
  
 
    |
165 | 164 | elrab 2895 |
. . . . . . . . 9
    
      |
166 | 161, 165 | sylibr 134 |
. . . . . . . 8
        

   
       
      |
167 | | breq2 4009 |
. . . . . . . . 9
 
   |
168 | 167 | adantl 277 |
. . . . . . . 8
    
    

   
       
     |
169 | | simprr 531 |
. . . . . . . 8
        

   
       
  |
170 | 166, 168,
169 | rspcedvd 2849 |
. . . . . . 7
        

   
        
       |
171 | 67, 73, 156, 170 | eqsuptid 6998 |
. . . . . 6
         
       
  
       |
172 | 65, 171 | eqtrd 2210 |
. . . . 5
         
       
             
   |
173 | 172 | ancoms 268 |
. . . 4
     

   
                
       |
174 | | gcdmndc 11947 |
. . . . . 6
 
 DECID     |
175 | 174 | adantr 276 |
. . . . 5
      
       DECID     |
176 | | exmiddc 836 |
. . . . 5
DECID      
    |
177 | 175, 176 | syl 14 |
. . . 4
      
               |
178 | 63, 173, 177 | mpjaodan 798 |
. . 3
      
                        |
179 | 23, 178 | eqtr2d 2211 |
. 2
      
           |
180 | 21, 179 | impbida 596 |
1
 
     
          |