Step | Hyp | Ref
| Expression |
1 | | zcn 9258 |
. . . . . . . . . 10
   |
2 | 1 | adantr 276 |
. . . . . . . . 9
 
   |
3 | | nncn 8927 |
. . . . . . . . . 10
   |
4 | 3 | adantl 277 |
. . . . . . . . 9
 
   |
5 | | nnap0 8948 |
. . . . . . . . . 10
 #   |
6 | 5 | adantl 277 |
. . . . . . . . 9
 
 #   |
7 | 2, 4, 6 | divclapd 8747 |
. . . . . . . 8
 
     |
8 | 7 | 3adant3 1017 |
. . . . . . 7
 
       |
9 | 8 | adantr 276 |
. . . . . 6
   
  

       |
10 | | zcn 9258 |
. . . . . . . . . 10
   |
11 | 10 | adantr 276 |
. . . . . . . . 9
 
   |
12 | | nncn 8927 |
. . . . . . . . . 10
   |
13 | 12 | adantl 277 |
. . . . . . . . 9
 
   |
14 | | nnap0 8948 |
. . . . . . . . . 10
 #   |
15 | 14 | adantl 277 |
. . . . . . . . 9
 
 #   |
16 | 11, 13, 15 | divclapd 8747 |
. . . . . . . 8
 
     |
17 | 16 | 3adant3 1017 |
. . . . . . 7
 
       |
18 | 17 | adantl 277 |
. . . . . 6
   
  

       |
19 | 3 | 3ad2ant2 1019 |
. . . . . . 7
 
     |
20 | 19 | adantr 276 |
. . . . . 6
   
  

     |
21 | 5 | 3ad2ant2 1019 |
. . . . . . 7
 
   #   |
22 | 21 | adantr 276 |
. . . . . 6
   
  

   #   |
23 | 9, 18, 20, 22 | mulcanapd 8618 |
. . . . 5
   
  

                   |
24 | 2, 4, 6 | divcanap2d 8749 |
. . . . . . . 8
 
       |
25 | 24 | 3adant3 1017 |
. . . . . . 7
 
   
     |
26 | 25 | adantr 276 |
. . . . . 6
   
  

    
    |
27 | 26 | eqeq1d 2186 |
. . . . 5
   
  

                   |
28 | 23, 27 | bitr3d 190 |
. . . 4
   
  

       

      |
29 | 1 | 3ad2ant1 1018 |
. . . . . . 7
 
     |
30 | 29 | adantr 276 |
. . . . . 6
   
  

     |
31 | | mulcl 7938 |
. . . . . . 7
  
   
    |
32 | 19, 17, 31 | syl2an 289 |
. . . . . 6
   
  

    
    |
33 | 12 | 3ad2ant2 1019 |
. . . . . . 7
 
     |
34 | 33 | adantl 277 |
. . . . . 6
   
  

     |
35 | 14 | 3ad2ant2 1019 |
. . . . . . 7
 
   #   |
36 | 35 | adantl 277 |
. . . . . 6
   
  

   #   |
37 | 30, 32, 34, 36 | mulcanap2d 8619 |
. . . . 5
   
  

        
  

      |
38 | 20, 18, 34 | mulassd 7981 |
. . . . . . 7
   
  

                 |
39 | 11, 13, 15 | divcanap1d 8748 |
. . . . . . . . . 10
 
       |
40 | 39 | 3adant3 1017 |
. . . . . . . . 9
 
         |
41 | 40 | adantl 277 |
. . . . . . . 8
   
  

         |
42 | 41 | oveq2d 5891 |
. . . . . . 7
   
  

             |
43 | 38, 42 | eqtrd 2210 |
. . . . . 6
   
  

             |
44 | 43 | eqeq2d 2189 |
. . . . 5
   
  

        
          |
45 | 37, 44 | bitr3d 190 |
. . . 4
   
  

               |
46 | 28, 45 | bitrd 188 |
. . 3
   
  

               |
47 | | nnz 9272 |
. . . . . . . . . 10
   |
48 | 47 | 3ad2ant2 1019 |
. . . . . . . . 9
 
     |
49 | | simp2 998 |
. . . . . . . . 9
 
     |
50 | 48, 49 | anim12i 338 |
. . . . . . . 8
   
  

       |
51 | 50 | adantr 276 |
. . . . . . 7
       
    
        |
52 | 48 | adantr 276 |
. . . . . . . . . 10
   
  

     |
53 | | simpl1 1000 |
. . . . . . . . . 10
   
  

     |
54 | | nnz 9272 |
. . . . . . . . . . . 12
   |
55 | 54 | 3ad2ant2 1019 |
. . . . . . . . . . 11
 
     |
56 | 55 | adantl 277 |
. . . . . . . . . 10
   
  

     |
57 | 52, 53, 56 | 3jca 1177 |
. . . . . . . . 9
   
  

       |
58 | 57 | adantr 276 |
. . . . . . . 8
       
    
        |
59 | | simp1 997 |
. . . . . . . . . . . 12
 
     |
60 | | dvdsmul1 11820 |
. . . . . . . . . . . 12
 
     |
61 | 48, 59, 60 | syl2an 289 |
. . . . . . . . . . 11
   
  

   
   |
62 | 61 | adantr 276 |
. . . . . . . . . 10
       
    
    
   |
63 | | simpr 110 |
. . . . . . . . . 10
       
    
          |
64 | 62, 63 | breqtrrd 4032 |
. . . . . . . . 9
       
    
    
   |
65 | | gcdcom 11974 |
. . . . . . . . . . . . . 14
 
       |
66 | 47, 65 | sylan 283 |
. . . . . . . . . . . . 13
 
       |
67 | 66 | ancoms 268 |
. . . . . . . . . . . 12
 
       |
68 | 67 | 3adant3 1017 |
. . . . . . . . . . 11
 
         |
69 | | simp3 999 |
. . . . . . . . . . 11
 
       |
70 | 68, 69 | eqtrd 2210 |
. . . . . . . . . 10
 
       |
71 | 70 | ad2antrr 488 |
. . . . . . . . 9
       
    
        |
72 | 64, 71 | jca 306 |
. . . . . . . 8
       
    
     

     |
73 | | coprmdvds 12092 |
. . . . . . . 8
 
   
       |
74 | 58, 72, 73 | sylc 62 |
. . . . . . 7
       
    
      |
75 | | dvdsle 11850 |
. . . . . . 7
 
 
   |
76 | 51, 74, 75 | sylc 62 |
. . . . . 6
       
    
      |
77 | | simp2 998 |
. . . . . . . . . 10
 
     |
78 | 55, 77 | anim12i 338 |
. . . . . . . . 9
   
  

       |
79 | 78 | ancoms 268 |
. . . . . . . 8
   
  

       |
80 | 79 | adantr 276 |
. . . . . . 7
       
    
        |
81 | | simpr1 1003 |
. . . . . . . . . 10
   
  

     |
82 | 56, 81, 52 | 3jca 1177 |
. . . . . . . . 9
   
  

       |
83 | 82 | adantr 276 |
. . . . . . . 8
       
    
        |
84 | | simp1 997 |
. . . . . . . . . . . 12
 
     |
85 | | dvdsmul2 11821 |
. . . . . . . . . . . 12
 
     |
86 | 84, 55, 85 | syl2an 289 |
. . . . . . . . . . 11
   
  

   
   |
87 | 86 | adantr 276 |
. . . . . . . . . 10
       
    
    
   |
88 | 10 | 3ad2ant1 1018 |
. . . . . . . . . . . . 13
 
     |
89 | | mulcom 7940 |
. . . . . . . . . . . . 13
 
       |
90 | 19, 88, 89 | syl2an 289 |
. . . . . . . . . . . 12
   
  

         |
91 | 90 | adantr 276 |
. . . . . . . . . . 11
       
    
          |
92 | 63, 91 | eqtrd 2210 |
. . . . . . . . . 10
       
    
          |
93 | 87, 92 | breqtrd 4030 |
. . . . . . . . 9
       
    
    
   |
94 | | gcdcom 11974 |
. . . . . . . . . . . . . 14
 
       |
95 | 54, 94 | sylan 283 |
. . . . . . . . . . . . 13
 
       |
96 | 95 | ancoms 268 |
. . . . . . . . . . . 12
 
       |
97 | 96 | 3adant3 1017 |
. . . . . . . . . . 11
 
         |
98 | | simp3 999 |
. . . . . . . . . . 11
 
       |
99 | 97, 98 | eqtrd 2210 |
. . . . . . . . . 10
 
       |
100 | 99 | ad2antlr 489 |
. . . . . . . . 9
       
    
        |
101 | 93, 100 | jca 306 |
. . . . . . . 8
       
    
     

     |
102 | | coprmdvds 12092 |
. . . . . . . 8
 
   
       |
103 | 83, 101, 102 | sylc 62 |
. . . . . . 7
       
    
      |
104 | | dvdsle 11850 |
. . . . . . 7
 
 
   |
105 | 80, 103, 104 | sylc 62 |
. . . . . 6
       
    
      |
106 | | nnre 8926 |
. . . . . . . . 9
   |
107 | 106 | 3ad2ant2 1019 |
. . . . . . . 8
 
     |
108 | 107 | ad2antrr 488 |
. . . . . . 7
       
    
      |
109 | | nnre 8926 |
. . . . . . . . 9
   |
110 | 109 | 3ad2ant2 1019 |
. . . . . . . 8
 
     |
111 | 110 | ad2antlr 489 |
. . . . . . 7
       
    
      |
112 | 108, 111 | letri3d 8073 |
. . . . . 6
       
    
          |
113 | 76, 105, 112 | mpbir2and 944 |
. . . . 5
       
    
      |
114 | | oveq2 5883 |
. . . . . . . . . 10
 
     |
115 | 114 | eqeq1d 2186 |
. . . . . . . . 9
     
       |
116 | 115 | anbi2d 464 |
. . . . . . . 8
        
    
          
    
       |
117 | | mulcom 7940 |
. . . . . . . . . . . . . 14
 
       |
118 | 1, 3, 117 | syl2an 289 |
. . . . . . . . . . . . 13
 
       |
119 | 118 | 3adant3 1017 |
. . . . . . . . . . . 12
 
   
     |
120 | 119 | adantr 276 |
. . . . . . . . . . 11
   
  

         |
121 | 120 | eqeq1d 2186 |
. . . . . . . . . 10
   
  

               |
122 | 88 | adantl 277 |
. . . . . . . . . . 11
   
  

     |
123 | 30, 122, 20, 22 | mulcanapd 8618 |
. . . . . . . . . 10
   
  

       
   |
124 | 121, 123 | bitrd 188 |
. . . . . . . . 9
   
  

       
   |
125 | 124 | biimpa 296 |
. . . . . . . 8
       
    
      |
126 | 116, 125 | syl6bir 164 |
. . . . . . 7
        
    
       |
127 | 126 | com12 30 |
. . . . . 6
       
    
    
   |
128 | 127 | ancrd 326 |
. . . . 5
       
    
    

    |
129 | 113, 128 | mpd 13 |
. . . 4
       
    
        |
130 | 129 | ex 115 |
. . 3
   
  

       

    |
131 | 46, 130 | sylbid 150 |
. 2
   
  

       

    |
132 | 131 | 3impia 1200 |
1
   
  

  
        |