Step | Hyp | Ref
| Expression |
1 | | oveq1 5876 |
. . . . . . . . 9
           |
2 | 1 | oveq1d 5884 |
. . . . . . . 8
                       |
3 | 2 | eqeq2d 2189 |
. . . . . . 7
               
                 |
4 | | id 19 |
. . . . . . . . . . . . . . 15
   |
5 | | nn0z 9262 |
. . . . . . . . . . . . . . 15

  |
6 | | lgscl 14082 |
. . . . . . . . . . . . . . 15
 
       |
7 | 4, 5, 6 | syl2anr 290 |
. . . . . . . . . . . . . 14
 
       |
8 | 7 | zcnd 9365 |
. . . . . . . . . . . . 13
 
       |
9 | 8 | adantr 276 |
. . . . . . . . . . . 12
               |
10 | 9 | mul01d 8340 |
. . . . . . . . . . 11
                 |
11 | | simpr 110 |
. . . . . . . . . . . 12
               |
12 | 11 | oveq2d 5885 |
. . . . . . . . . . 11
                           |
13 | 10, 12, 11 | 3eqtr4rd 2221 |
. . . . . . . . . 10
                         |
14 | | 0z 9253 |
. . . . . . . . . . . . . . 15
 |
15 | 5 | adantr 276 |
. . . . . . . . . . . . . . 15
 
   |
16 | | lgsne0 14106 |
. . . . . . . . . . . . . . 15
 
           |
17 | 14, 15, 16 | sylancr 414 |
. . . . . . . . . . . . . 14
 
           |
18 | | gcdcom 11957 |
. . . . . . . . . . . . . . . . . 18
 
       |
19 | 14, 15, 18 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
 
       |
20 | | nn0gcdid0 11965 |
. . . . . . . . . . . . . . . . . 18

    |
21 | 20 | adantr 276 |
. . . . . . . . . . . . . . . . 17
 
     |
22 | 19, 21 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
 
     |
23 | 22 | eqeq1d 2186 |
. . . . . . . . . . . . . . 15
 
       |
24 | | lgs1 14112 |
. . . . . . . . . . . . . . . . 17
       |
25 | 24 | adantl 277 |
. . . . . . . . . . . . . . . 16
 
       |
26 | | oveq2 5877 |
. . . . . . . . . . . . . . . . 17
           |
27 | 26 | eqeq1d 2186 |
. . . . . . . . . . . . . . . 16
             |
28 | 25, 27 | syl5ibrcom 157 |
. . . . . . . . . . . . . . 15
 
         |
29 | 23, 28 | sylbid 150 |
. . . . . . . . . . . . . 14
 
           |
30 | 17, 29 | sylbid 150 |
. . . . . . . . . . . . 13
 
     
       |
31 | 30 | imp 124 |
. . . . . . . . . . . 12
               |
32 | 31 | oveq1d 5884 |
. . . . . . . . . . 11
                           |
33 | 5 | ad2antrr 488 |
. . . . . . . . . . . . . 14
           |
34 | | lgscl 14082 |
. . . . . . . . . . . . . 14
 
       |
35 | 14, 33, 34 | sylancr 414 |
. . . . . . . . . . . . 13
               |
36 | 35 | zcnd 9365 |
. . . . . . . . . . . 12
               |
37 | 36 | mulid2d 7966 |
. . . . . . . . . . 11
                     |
38 | 32, 37 | eqtr2d 2211 |
. . . . . . . . . 10
                         |
39 | 14, 15, 34 | sylancr 414 |
. . . . . . . . . . . 12
 
       |
40 | | zdceq 9317 |
. . . . . . . . . . . 12
       DECID       |
41 | 39, 14, 40 | sylancl 413 |
. . . . . . . . . . 11
 
 DECID       |
42 | | dcne 2358 |
. . . . . . . . . . 11
DECID    
            |
43 | 41, 42 | sylib 122 |
. . . . . . . . . 10
 
             |
44 | 13, 38, 43 | mpjaodan 798 |
. . . . . . . . 9
 
                 |
45 | 44 | ralrimiva 2550 |
. . . . . . . 8

                 |
46 | 45 | 3ad2ant3 1020 |
. . . . . . 7
 
                  |
47 | | simp2 998 |
. . . . . . 7
 
   |
48 | 3, 46, 47 | rspcdva 2846 |
. . . . . 6
 
                 |
49 | 48 | adantr 276 |
. . . . 5
  

                 |
50 | 5 | 3ad2ant3 1020 |
. . . . . . . . 9
 
   |
51 | 14, 50, 34 | sylancr 414 |
. . . . . . . 8
 
       |
52 | 51 | zcnd 9365 |
. . . . . . 7
 
       |
53 | 52 | adantr 276 |
. . . . . 6
  

       |
54 | | lgscl 14082 |
. . . . . . . . 9
 
       |
55 | 47, 50, 54 | syl2anc 411 |
. . . . . . . 8
 
       |
56 | 55 | zcnd 9365 |
. . . . . . 7
 
       |
57 | 56 | adantr 276 |
. . . . . 6
  

       |
58 | 53, 57 | mulcomd 7969 |
. . . . 5
  

                       |
59 | 49, 58 | eqtr4d 2213 |
. . . 4
  

                 |
60 | | oveq1 5876 |
. . . . . 6
 
     |
61 | | zcn 9247 |
. . . . . . . 8
   |
62 | 61 | 3ad2ant2 1019 |
. . . . . . 7
 
   |
63 | 62 | mul02d 8339 |
. . . . . 6
 
     |
64 | 60, 63 | sylan9eqr 2232 |
. . . . 5
  

     |
65 | 64 | oveq1d 5884 |
. . . 4
  

             |
66 | | simpr 110 |
. . . . . 6
  

   |
67 | 66 | oveq1d 5884 |
. . . . 5
  

           |
68 | 67 | oveq1d 5884 |
. . . 4
  

                       |
69 | 59, 65, 68 | 3eqtr4d 2220 |
. . 3
  

                   |
70 | | oveq1 5876 |
. . . . . . . 8
           |
71 | 70 | oveq1d 5884 |
. . . . . . 7
                       |
72 | 71 | eqeq2d 2189 |
. . . . . 6
               
                 |
73 | | simp1 997 |
. . . . . 6
 
   |
74 | 72, 46, 73 | rspcdva 2846 |
. . . . 5
 
                 |
75 | 74 | adantr 276 |
. . . 4
  

                 |
76 | | oveq2 5877 |
. . . . . 6
 
     |
77 | 73 | zcnd 9365 |
. . . . . . 7
 
   |
78 | 77 | mul01d 8340 |
. . . . . 6
 
 
   |
79 | 76, 78 | sylan9eqr 2232 |
. . . . 5
  

     |
80 | 79 | oveq1d 5884 |
. . . 4
  

             |
81 | | simpr 110 |
. . . . . 6
  

   |
82 | 81 | oveq1d 5884 |
. . . . 5
  

           |
83 | 82 | oveq2d 5885 |
. . . 4
  

                       |
84 | 75, 80, 83 | 3eqtr4d 2220 |
. . 3
  

                   |
85 | 69, 84 | jaodan 797 |
. 2
  
 
                    |
86 | | neanior 2434 |
. . 3
       |
87 | | lgsdir 14103 |
. . . 4
  
 
                    |
88 | 5, 87 | syl3anl3 1288 |
. . 3
  
 
                    |
89 | 86, 88 | sylan2br 288 |
. 2
  
                      |
90 | | zdceq 9317 |
. . . . 5
 
 DECID   |
91 | 73, 14, 90 | sylancl 413 |
. . . 4
 

DECID
  |
92 | | zdceq 9317 |
. . . . 5
 
 DECID   |
93 | 47, 14, 92 | sylancl 413 |
. . . 4
 

DECID
  |
94 | | dcor 935 |
. . . 4
DECID
DECID
DECID      |
95 | 91, 93, 94 | sylc 62 |
. . 3
 

DECID     |
96 | | exmiddc 836 |
. . 3
DECID      
    |
97 | 95, 96 | syl 14 |
. 2
 
    
    |
98 | 85, 89, 97 | mpjaodan 798 |
1
 
                   |