Step | Hyp | Ref
| Expression |
1 | | nnz 9248 |
. . . . . . . . . 10
   |
2 | | gcddvds 11934 |
. . . . . . . . . . 11
 
     
   |
3 | 2 | simpld 112 |
. . . . . . . . . 10
 
  
  |
4 | 1, 3 | sylan2 286 |
. . . . . . . . 9
 
  
  |
5 | | gcdcl 11937 |
. . . . . . . . . . . 12
 
     |
6 | 1, 5 | sylan2 286 |
. . . . . . . . . . 11
 
     |
7 | 6 | nn0zd 9349 |
. . . . . . . . . 10
 
     |
8 | | simpl 109 |
. . . . . . . . . . . 12
 
   |
9 | 1 | adantl 277 |
. . . . . . . . . . . 12
 
   |
10 | | nnne0 8923 |
. . . . . . . . . . . . . . 15
   |
11 | 10 | neneqd 2368 |
. . . . . . . . . . . . . 14

  |
12 | 11 | intnand 931 |
. . . . . . . . . . . . 13
     |
13 | 12 | adantl 277 |
. . . . . . . . . . . 12
 
     |
14 | | gcdn0cl 11933 |
. . . . . . . . . . . 12
           |
15 | 8, 9, 13, 14 | syl21anc 1237 |
. . . . . . . . . . 11
 
     |
16 | 15 | nnne0d 8940 |
. . . . . . . . . 10
 
     |
17 | | dvdsval2 11768 |
. . . . . . . . . 10
           
     |
18 | 7, 16, 8, 17 | syl3anc 1238 |
. . . . . . . . 9
 
           |
19 | 4, 18 | mpbid 147 |
. . . . . . . 8
 
  
    |
20 | 19 | 3adant3 1017 |
. . . . . . 7
 
    
    |
21 | 2 | simprd 114 |
. . . . . . . . . . . 12
 
  
  |
22 | 1, 21 | sylan2 286 |
. . . . . . . . . . 11
 
  
  |
23 | | dvdsval2 11768 |
. . . . . . . . . . . 12
           
     |
24 | 7, 16, 9, 23 | syl3anc 1238 |
. . . . . . . . . . 11
 
           |
25 | 22, 24 | mpbid 147 |
. . . . . . . . . 10
 
  
    |
26 | | nnre 8902 |
. . . . . . . . . . . 12
   |
27 | 26 | adantl 277 |
. . . . . . . . . . 11
 
   |
28 | 6 | nn0red 9206 |
. . . . . . . . . . 11
 
     |
29 | | nngt0 8920 |
. . . . . . . . . . . 12
   |
30 | 29 | adantl 277 |
. . . . . . . . . . 11
 
   |
31 | 15 | nngt0d 8939 |
. . . . . . . . . . 11
 
     |
32 | 27, 28, 30, 31 | divgt0d 8868 |
. . . . . . . . . 10
 
       |
33 | 25, 32 | jca 306 |
. . . . . . . . 9
 
             |
34 | 33 | 3adant3 1017 |
. . . . . . . 8
 
               |
35 | | elnnz 9239 |
. . . . . . . 8
    
      
     |
36 | 34, 35 | sylibr 134 |
. . . . . . 7
 
    
    |
37 | | opelxpi 4654 |
. . . . . . 7
   
  

                  |
38 | 20, 36, 37 | syl2anc 411 |
. . . . . 6
 
     
            |
39 | | fveq2 5510 |
. . . . . . . . . 10
                                 |
40 | | simp1 997 |
. . . . . . . . . . . 12
 
     |
41 | 15 | 3adant3 1017 |
. . . . . . . . . . . 12
 
       |
42 | | znq 9600 |
. . . . . . . . . . . 12
           |
43 | 40, 41, 42 | syl2anc 411 |
. . . . . . . . . . 11
 
    
    |
44 | 9 | 3adant3 1017 |
. . . . . . . . . . . 12
 
  
  |
45 | | znq 9600 |
. . . . . . . . . . . 12
           |
46 | 44, 41, 45 | syl2anc 411 |
. . . . . . . . . . 11
 
    
    |
47 | | op1stg 6144 |
. . . . . . . . . . 11
   
  

                        |
48 | 43, 46, 47 | syl2anc 411 |
. . . . . . . . . 10
 
                        |
49 | 39, 48 | sylan9eqr 2232 |
. . . . . . . . 9
  
  
       
         
    |
50 | | fveq2 5510 |
. . . . . . . . . 10
                                 |
51 | | op2ndg 6145 |
. . . . . . . . . . 11
   
  

                        |
52 | 43, 46, 51 | syl2anc 411 |
. . . . . . . . . 10
 
                        |
53 | 50, 52 | sylan9eqr 2232 |
. . . . . . . . 9
  
  
       
         
    |
54 | 49, 53 | oveq12d 5886 |
. . . . . . . 8
  
  
       
        
                 |
55 | 54 | eqeq1d 2186 |
. . . . . . 7
  
  
       
         
           
      |
56 | 49, 53 | oveq12d 5886 |
. . . . . . . 8
  
  
       
                          |
57 | 56 | eqeq2d 2189 |
. . . . . . 7
  
  
       
    
         
             |
58 | 55, 57 | anbi12d 473 |
. . . . . 6
  
  
       
                                                    |
59 | 19, 25 | gcdcld 11939 |
. . . . . . . . . 10
 
             |
60 | 59 | nn0cnd 9207 |
. . . . . . . . 9
 
             |
61 | | 1cnd 7951 |
. . . . . . . . 9
 
   |
62 | 6 | nn0cnd 9207 |
. . . . . . . . 9
 
     |
63 | 15 | nnap0d 8941 |
. . . . . . . . 9
 
   #   |
64 | 62 | mulid1d 7952 |
. . . . . . . . . 10
 
         |
65 | | zcn 9234 |
. . . . . . . . . . . . 13
   |
66 | 65 | adantr 276 |
. . . . . . . . . . . 12
 
   |
67 | 66, 62, 63 | divcanap2d 8725 |
. . . . . . . . . . 11
 
           |
68 | | nncn 8903 |
. . . . . . . . . . . . 13
   |
69 | 68 | adantl 277 |
. . . . . . . . . . . 12
 
   |
70 | 69, 62, 63 | divcanap2d 8725 |
. . . . . . . . . . 11
 
           |
71 | 67, 70 | oveq12d 5886 |
. . . . . . . . . 10
 
      
                |
72 | | mulgcd 11987 |
. . . . . . . . . . 11
     
  

                                     |
73 | 6, 19, 25, 72 | syl3anc 1238 |
. . . . . . . . . 10
 
      
                     
      |
74 | 64, 71, 73 | 3eqtr2rd 2217 |
. . . . . . . . 9
 
      
 
            |
75 | 60, 61, 62, 63, 74 | mulcanapad 8596 |
. . . . . . . 8
 
             |
76 | 75 | 3adant3 1017 |
. . . . . . 7
 
               |
77 | | nnap0 8924 |
. . . . . . . . . . 11
 #   |
78 | 77 | adantl 277 |
. . . . . . . . . 10
 
 #   |
79 | 66, 69, 62, 78, 63 | divcanap7d 8752 |
. . . . . . . . 9
 
               |
80 | 79 | eqeq2d 2189 |
. . . . . . . 8
 
    
            |
81 | 80 | biimp3ar 1346 |
. . . . . . 7
 
  
            |
82 | 76, 81 | jca 306 |
. . . . . 6
 
          
     
          |
83 | 38, 58, 82 | rspcedvd 2847 |
. . . . 5
 
   
        
                  |
84 | | elxp6 6163 |
. . . . . . 7
  
                         |
85 | | elxp6 6163 |
. . . . . . 7
  
                         |
86 | | simprl 529 |
. . . . . . . . . . . 12
            
                 |
87 | 86 | ad2antrr 488 |
. . . . . . . . . . 11
                                                        
                                              |
88 | | simprr 531 |
. . . . . . . . . . . 12
            
                 |
89 | 88 | ad2antrr 488 |
. . . . . . . . . . 11
                                                        
                                              |
90 | | simprll 537 |
. . . . . . . . . . 11
                                                        
                                            
       |
91 | | simprl 529 |
. . . . . . . . . . . 12
            
                 |
92 | 91 | ad2antlr 489 |
. . . . . . . . . . 11
                                                        
                                              |
93 | | simprr 531 |
. . . . . . . . . . . 12
            
                 |
94 | 93 | ad2antlr 489 |
. . . . . . . . . . 11
                                                        
                                              |
95 | | simprrl 539 |
. . . . . . . . . . 11
                                                        
                                            
       |
96 | | simprlr 538 |
. . . . . . . . . . . 12
                                                        
                                                    |
97 | | simprrr 540 |
. . . . . . . . . . . 12
                                                        
                                                    |
98 | 96, 97 | eqtr3d 2212 |
. . . . . . . . . . 11
                                                        
                                                              |
99 | | qredeq 12066 |
. . . . . . . . . . 11
               
                   
                                               |
100 | 87, 89, 90, 92, 94, 95, 98, 99 | syl331anc 1263 |
. . . . . . . . . 10
                                                        
                                                            |
101 | | vex 2740 |
. . . . . . . . . . . 12
 |
102 | | 1stexg 6161 |
. . . . . . . . . . . 12
       |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . 11
     |
104 | | 2ndexg 6162 |
. . . . . . . . . . . 12
       |
105 | 101, 104 | ax-mp 5 |
. . . . . . . . . . 11
     |
106 | 103, 105 | opth 4233 |
. . . . . . . . . 10
                                           |
107 | 100, 106 | sylibr 134 |
. . . . . . . . 9
                                                        
                                                                |
108 | | simplll 533 |
. . . . . . . . 9
                                                        
                                                     |
109 | | simplrl 535 |
. . . . . . . . 9
                                                        
                                                     |
110 | 107, 108,
109 | 3eqtr4d 2220 |
. . . . . . . 8
                                                        
                                          |
111 | 110 | ex 115 |
. . . . . . 7
             
                      
                   
                                      
   |
112 | 84, 85, 111 | syl2anb 291 |
. . . . . 6
   
          
                                      
   |
113 | 112 | rgen2a 2531 |
. . . . 5
               
                                      
  |
114 | 83, 113 | jctir 313 |
. . . 4
 
                                             
                                      
    |
115 | 114 | 3expia 1205 |
. . 3
 
                                              
                                      
     |
116 | 115 | rexlimivv 2600 |
. 2
  
   
        
                               
                                      
    |
117 | | elq 9598 |
. 2

      |
118 | | fveq2 5510 |
. . . . . 6
           |
119 | | fveq2 5510 |
. . . . . 6
           |
120 | 118, 119 | oveq12d 5886 |
. . . . 5
     
         
       |
121 | 120 | eqeq1d 2186 |
. . . 4
      
                  |
122 | 118, 119 | oveq12d 5886 |
. . . . 5
                       |
123 | 122 | eqeq2d 2189 |
. . . 4
 
         
             |
124 | 121, 123 | anbi12d 473 |
. . 3
                                                 |
125 | 124 | reu4 2931 |
. 2
          
                                                          
                                      
    |
126 | 116, 117,
125 | 3imtr4i 201 |
1
 
        
                  |