Step | Hyp | Ref
| Expression |
1 | | simpl1 1000 |
. . . 4
  

   |
2 | | simpl2 1001 |
. . . 4
  

   |
3 | | lgsdir2 14101 |
. . . 4
 
                   |
4 | 1, 2, 3 | syl2anc 411 |
. . 3
  

                   |
5 | | simpr 110 |
. . . 4
  

   |
6 | 5 | oveq2d 5885 |
. . 3
  

               |
7 | 5 | oveq2d 5885 |
. . . 4
  

           |
8 | 5 | oveq2d 5885 |
. . . 4
  

           |
9 | 7, 8 | oveq12d 5887 |
. . 3
  

                       |
10 | 4, 6, 9 | 3eqtr4d 2220 |
. 2
  

                   |
11 | | simpl1 1000 |
. . . . . 6
  
 
  |
12 | | simpl2 1001 |
. . . . . 6
  
 
  |
13 | 11, 12 | zmulcld 9370 |
. . . . 5
  
      |
14 | | simpl3 1002 |
. . . . . 6
  
 
  |
15 | | prmz 12094 |
. . . . . 6

  |
16 | 14, 15 | syl 14 |
. . . . 5
  
 
  |
17 | | lgscl 14082 |
. . . . 5
   
         |
18 | 13, 16, 17 | syl2anc 411 |
. . . 4
  
          |
19 | 18 | zcnd 9365 |
. . 3
  
          |
20 | | lgscl 14082 |
. . . . . 6
 
       |
21 | 11, 16, 20 | syl2anc 411 |
. . . . 5
  
        |
22 | | lgscl 14082 |
. . . . . 6
 
       |
23 | 12, 16, 22 | syl2anc 411 |
. . . . 5
  
        |
24 | 21, 23 | zmulcld 9370 |
. . . 4
  
              |
25 | 24 | zcnd 9365 |
. . 3
  
              |
26 | 19, 25 | subcld 8258 |
. . . 4
  
                      |
27 | 18, 24 | zsubcld 9369 |
. . . . . . 7
  
                      |
28 | | zabscl 11079 |
. . . . . . 7
                                           |
29 | | zq 9615 |
. . . . . . 7
                      
                        |
30 | 27, 28, 29 | 3syl 17 |
. . . . . 6
  
                          |
31 | | prmnn 12093 |
. . . . . . 7

  |
32 | | nnq 9622 |
. . . . . . 7
   |
33 | 14, 31, 32 | 3syl 17 |
. . . . . 6
  
 
  |
34 | 26 | absge0d 11177 |
. . . . . 6
  
 
                        |
35 | 26 | abscld 11174 |
. . . . . . 7
  
                          |
36 | | 2re 8978 |
. . . . . . . 8
 |
37 | 36 | a1i 9 |
. . . . . . 7
  
    |
38 | 14, 31 | syl 14 |
. . . . . . . 8
  
 
  |
39 | 38 | nnred 8921 |
. . . . . . 7
  
 
  |
40 | 19 | abscld 11174 |
. . . . . . . . 9
  
              |
41 | 25 | abscld 11174 |
. . . . . . . . 9
  
                  |
42 | 40, 41 | readdcld 7977 |
. . . . . . . 8
  
                              |
43 | 19, 25 | abs2dif2d 11191 |
. . . . . . . 8
  
                                                    |
44 | | 1red 7963 |
. . . . . . . . . 10
  
    |
45 | | lgsle1 14083 |
. . . . . . . . . . 11
   
             |
46 | 13, 16, 45 | syl2anc 411 |
. . . . . . . . . 10
  
              |
47 | | eqid 2177 |
. . . . . . . . . . . . . 14
     
       |
48 | 47 | lgscl2 14080 |
. . . . . . . . . . . . 13
 
         
   |
49 | 11, 16, 48 | syl2anc 411 |
. . . . . . . . . . . 12
  
          
   |
50 | 47 | lgscl2 14080 |
. . . . . . . . . . . . 13
 
         
   |
51 | 12, 16, 50 | syl2anc 411 |
. . . . . . . . . . . 12
  
          
   |
52 | 47 | lgslem3 14070 |
. . . . . . . . . . . 12
          
         
 
                  |
53 | 49, 51, 52 | syl2anc 411 |
. . . . . . . . . . 11
  
                
   |
54 | | fveq2 5511 |
. . . . . . . . . . . . . 14
                               |
55 | 54 | breq1d 4010 |
. . . . . . . . . . . . 13
                                 |
56 | 55 | elrab 2893 |
. . . . . . . . . . . 12
                                         
   |
57 | 56 | simprbi 275 |
. . . . . . . . . . 11
                                 |
58 | 53, 57 | syl 14 |
. . . . . . . . . 10
  
                  |
59 | 40, 41, 44, 44, 46, 58 | le2addd 8510 |
. . . . . . . . 9
  
                                |
60 | | df-2 8967 |
. . . . . . . . 9
   |
61 | 59, 60 | breqtrrdi 4042 |
. . . . . . . 8
  
                              |
62 | 35, 42, 37, 43, 61 | letrd 8071 |
. . . . . . 7
  
                          |
63 | | prmuz2 12114 |
. . . . . . . . 9

      |
64 | | eluzle 9529 |
. . . . . . . . 9
    
  |
65 | 14, 63, 64 | 3syl 17 |
. . . . . . . 8
  
 
  |
66 | | simpr 110 |
. . . . . . . 8
  
    |
67 | | 2z 9270 |
. . . . . . . . 9
 |
68 | | zltlen 9320 |
. . . . . . . . 9
 
  
    |
69 | 67, 16, 68 | sylancr 414 |
. . . . . . . 8
  
   
    |
70 | 65, 66, 69 | mpbir2and 944 |
. . . . . . 7
  
 
  |
71 | 35, 37, 39, 62, 70 | lelttrd 8072 |
. . . . . 6
  
                          |
72 | | modqid 10335 |
. . . . . 6
                          
                                             
                                                |
73 | 30, 33, 34, 71, 72 | syl22anc 1239 |
. . . . 5
  
                                                  |
74 | 11 | zcnd 9365 |
. . . . . . . . . . . 12
  
 
  |
75 | 12 | zcnd 9365 |
. . . . . . . . . . . 12
  
 
  |
76 | | eldifsn 3718 |
. . . . . . . . . . . . . . 15
    

   |
77 | 14, 66, 76 | sylanbrc 417 |
. . . . . . . . . . . . . 14
  
 
      |
78 | | oddprm 12242 |
. . . . . . . . . . . . . 14
           |
79 | 77, 78 | syl 14 |
. . . . . . . . . . . . 13
  
        |
80 | 79 | nnnn0d 9218 |
. . . . . . . . . . . 12
  
        |
81 | 74, 75, 80 | mulexpd 10654 |
. . . . . . . . . . 11
  
                                |
82 | | zexpcl 10521 |
. . . . . . . . . . . . . 14
                 |
83 | 11, 80, 82 | syl2anc 411 |
. . . . . . . . . . . . 13
  
            |
84 | 83 | zcnd 9365 |
. . . . . . . . . . . 12
  
            |
85 | | zexpcl 10521 |
. . . . . . . . . . . . . 14
                 |
86 | 12, 80, 85 | syl2anc 411 |
. . . . . . . . . . . . 13
  
            |
87 | 86 | zcnd 9365 |
. . . . . . . . . . . 12
  
            |
88 | 84, 87 | mulcomd 7969 |
. . . . . . . . . . 11
  
                                        |
89 | 81, 88 | eqtrd 2210 |
. . . . . . . . . 10
  
                                |
90 | 89 | oveq1d 5884 |
. . . . . . . . 9
  
                                    |
91 | | lgsvalmod 14087 |
. . . . . . . . . 10
   
    
                      |
92 | 13, 77, 91 | syl2anc 411 |
. . . . . . . . 9
  
                        |
93 | | zq 9615 |
. . . . . . . . . . . 12
           |
94 | 21, 93 | syl 14 |
. . . . . . . . . . 11
  
        |
95 | | zq 9615 |
. . . . . . . . . . . 12
                   |
96 | 83, 95 | syl 14 |
. . . . . . . . . . 11
  
            |
97 | 38 | nngt0d 8952 |
. . . . . . . . . . 11
  
 
  |
98 | | lgsvalmod 14087 |
. . . . . . . . . . . 12
 
    
                  |
99 | 11, 77, 98 | syl2anc 411 |
. . . . . . . . . . 11
  
                    |
100 | 94, 96, 23, 33, 97, 99 | modqmul1 10363 |
. . . . . . . . . 10
  
                                |
101 | 23 | zcnd 9365 |
. . . . . . . . . . . 12
  
        |
102 | 84, 101 | mulcomd 7969 |
. . . . . . . . . . 11
  
                                |
103 | 102 | oveq1d 5884 |
. . . . . . . . . 10
  
                                    |
104 | | zq 9615 |
. . . . . . . . . . . 12
           |
105 | 23, 104 | syl 14 |
. . . . . . . . . . 11
  
        |
106 | | zq 9615 |
. . . . . . . . . . . 12
                   |
107 | 86, 106 | syl 14 |
. . . . . . . . . . 11
  
            |
108 | | lgsvalmod 14087 |
. . . . . . . . . . . 12
 
    
                  |
109 | 12, 77, 108 | syl2anc 411 |
. . . . . . . . . . 11
  
                    |
110 | 105, 107,
83, 33, 97, 109 | modqmul1 10363 |
. . . . . . . . . 10
  
                                        |
111 | 100, 103,
110 | 3eqtrd 2214 |
. . . . . . . . 9
  
                                    |
112 | 90, 92, 111 | 3eqtr4d 2220 |
. . . . . . . 8
  
                        |
113 | | moddvds 11790 |
. . . . . . . . 9
                                       
                     |
114 | 38, 18, 24, 113 | syl3anc 1238 |
. . . . . . . 8
  
                      
                     |
115 | 112, 114 | mpbid 147 |
. . . . . . 7
  
                      |
116 | | dvdsabsb 11801 |
. . . . . . . 8
                                       
                         |
117 | 16, 27, 116 | syl2anc 411 |
. . . . . . 7
  
                    
                         |
118 | 115, 117 | mpbid 147 |
. . . . . 6
  
                          |
119 | | dvdsmod0 11784 |
. . . . . 6
                                                   |
120 | 38, 118, 119 | syl2anc 411 |
. . . . 5
  
                            |
121 | 73, 120 | eqtr3d 2212 |
. . . 4
  
                          |
122 | 26, 121 | abs00d 11179 |
. . 3
  
                      |
123 | 19, 25, 122 | subeq0d 8266 |
. 2
  
                    |
124 | 15 | 3ad2ant3 1020 |
. . . 4
 
   |
125 | 67 | a1i 9 |
. . . 4
 
   |
126 | | zdceq 9317 |
. . . 4
 
 DECID   |
127 | 124, 125,
126 | syl2anc 411 |
. . 3
 

DECID
  |
128 | | dcne 2358 |
. . 3
DECID     |
129 | 127, 128 | sylib 122 |
. 2
 
 
   |
130 | 10, 123, 129 | mpjaodan 798 |
1
 
                   |