Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . . . 6
   |
2 | | 8nn 9072 |
. . . . . . 7
 |
3 | 2 | a1i 9 |
. . . . . 6
   |
4 | 1, 3 | zmodcld 10328 |
. . . . 5
     |
5 | | elprg 3611 |
. . . . 5
  
     
         |
6 | 4, 5 | syl 14 |
. . . 4
      
         |
7 | 6 | adantr 276 |
. . 3
 
                |
8 | 7 | pm5.32i 454 |
. 2
                      |
9 | | zq 9612 |
. . . . . . 7
   |
10 | 9 | ad2antrr 488 |
. . . . . 6
      
  |
11 | | 1nn 8916 |
. . . . . . . 8
 |
12 | | nnq 9619 |
. . . . . . . 8
   |
13 | 11, 12 | ax-mp 5 |
. . . . . . 7
 |
14 | 13 | a1i 9 |
. . . . . 6
      
  |
15 | | simplr 528 |
. . . . . 6
      
  |
16 | | nnq 9619 |
. . . . . . . 8
   |
17 | 2, 16 | ax-mp 5 |
. . . . . . 7
 |
18 | 17 | a1i 9 |
. . . . . 6
      
  |
19 | | 8pos 9008 |
. . . . . . 7
 |
20 | 19 | a1i 9 |
. . . . . 6
      
  |
21 | | simpr 110 |
. . . . . . 7
      
    |
22 | | lgsdir2lem1 14089 |
. . . . . . . . 9
                 |
23 | 22 | simpli 111 |
. . . . . . . 8
        |
24 | 23 | simpli 111 |
. . . . . . 7
   |
25 | 21, 24 | eqtr4di 2228 |
. . . . . 6
      
      |
26 | 10, 14, 15, 18, 20, 25 | modqmul1 10360 |
. . . . 5
      
 
    
   |
27 | | zcn 9244 |
. . . . . . . 8
   |
28 | 27 | ad2antlr 489 |
. . . . . . 7
      
  |
29 | 28 | mulid2d 7963 |
. . . . . 6
      
    |
30 | 29 | oveq1d 5884 |
. . . . 5
      
        |
31 | 26, 30 | eqtrd 2210 |
. . . 4
      
 
      |
32 | 31 | eleq1d 2246 |
. . 3
      
   
   
        |
33 | 9 | ad2antrr 488 |
. . . . . . 7
      
  |
34 | | qnegcl 9622 |
. . . . . . . . 9
    |
35 | 13, 34 | ax-mp 5 |
. . . . . . . 8
  |
36 | 35 | a1i 9 |
. . . . . . 7
      
   |
37 | | simplr 528 |
. . . . . . 7
      
  |
38 | 17 | a1i 9 |
. . . . . . 7
      
  |
39 | 19 | a1i 9 |
. . . . . . 7
      
  |
40 | | simpr 110 |
. . . . . . . 8
      
    |
41 | 23 | simpri 113 |
. . . . . . . 8
 
  |
42 | 40, 41 | eqtr4di 2228 |
. . . . . . 7
      
       |
43 | 33, 36, 37, 38, 39, 42 | modqmul1 10360 |
. . . . . 6
      
 
         |
44 | 27 | ad2antlr 489 |
. . . . . . . 8
      
  |
45 | 44 | mulm1d 8354 |
. . . . . . 7
      
      |
46 | 45 | oveq1d 5884 |
. . . . . 6
      
          |
47 | 43, 46 | eqtrd 2210 |
. . . . 5
      
 
       |
48 | 47 | eleq1d 2246 |
. . . 4
      
   
   
         |
49 | | znegcl 9270 |
. . . . . . . 8
    |
50 | | oveq1 5876 |
. . . . . . . . . . 11
  
      |
51 | 50 | eleq1d 2246 |
. . . . . . . . . 10
       
         |
52 | | negeq 8137 |
. . . . . . . . . . . 12
       |
53 | 52 | oveq1d 5884 |
. . . . . . . . . . 11
           |
54 | 53 | eleq1d 2246 |
. . . . . . . . . 10
        
          |
55 | 51, 54 | imbi12d 234 |
. . . . . . . . 9
                      
           |
56 | | zcn 9244 |
. . . . . . . . . . . . . . . . 17
   |
57 | | neg1cn 9010 |
. . . . . . . . . . . . . . . . . . 19
  |
58 | | mulcom 7928 |
. . . . . . . . . . . . . . . . . . 19
            |
59 | 57, 58 | mpan2 425 |
. . . . . . . . . . . . . . . . . 18
         |
60 | | mulm1 8344 |
. . . . . . . . . . . . . . . . . 18
       |
61 | 59, 60 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
       |
62 | 56, 61 | syl 14 |
. . . . . . . . . . . . . . . 16
       |
63 | 62 | adantr 276 |
. . . . . . . . . . . . . . 15
  
        |
64 | 63 | oveq1d 5884 |
. . . . . . . . . . . . . 14
  
            |
65 | | zq 9612 |
. . . . . . . . . . . . . . . 16
   |
66 | 65 | adantr 276 |
. . . . . . . . . . . . . . 15
  
    |
67 | 13 | a1i 9 |
. . . . . . . . . . . . . . 15
  
    |
68 | | neg1z 9271 |
. . . . . . . . . . . . . . . 16
  |
69 | 68 | a1i 9 |
. . . . . . . . . . . . . . 15
  
     |
70 | 17 | a1i 9 |
. . . . . . . . . . . . . . 15
  
    |
71 | 19 | a1i 9 |
. . . . . . . . . . . . . . 15
  
    |
72 | | simpr 110 |
. . . . . . . . . . . . . . . 16
  
      |
73 | 72, 24 | eqtr4di 2228 |
. . . . . . . . . . . . . . 15
  
        |
74 | 66, 67, 69, 70, 71, 73 | modqmul1 10360 |
. . . . . . . . . . . . . 14
  
          
   |
75 | 64, 74 | eqtr3d 2212 |
. . . . . . . . . . . . 13
  
        
   |
76 | 57 | mulid2i 7948 |
. . . . . . . . . . . . . . 15
     |
77 | 76 | oveq1i 5879 |
. . . . . . . . . . . . . 14
   
     |
78 | 77, 41 | eqtri 2198 |
. . . . . . . . . . . . 13
   
  |
79 | 75, 78 | eqtrdi 2226 |
. . . . . . . . . . . 12
  
       |
80 | 79 | ex 115 |
. . . . . . . . . . 11
          |
81 | 62 | adantr 276 |
. . . . . . . . . . . . . . 15
  
        |
82 | 81 | oveq1d 5884 |
. . . . . . . . . . . . . 14
  
            |
83 | 65 | adantr 276 |
. . . . . . . . . . . . . . 15
  
    |
84 | 35 | a1i 9 |
. . . . . . . . . . . . . . 15
  
     |
85 | 68 | a1i 9 |
. . . . . . . . . . . . . . 15
  
     |
86 | 17 | a1i 9 |
. . . . . . . . . . . . . . 15
  
    |
87 | 19 | a1i 9 |
. . . . . . . . . . . . . . 15
  
    |
88 | | simpr 110 |
. . . . . . . . . . . . . . . 16
  
      |
89 | 88, 41 | eqtr4di 2228 |
. . . . . . . . . . . . . . 15
  
         |
90 | 83, 84, 85, 86, 87, 89 | modqmul1 10360 |
. . . . . . . . . . . . . 14
  
               |
91 | 82, 90 | eqtr3d 2212 |
. . . . . . . . . . . . 13
  
             |
92 | | neg1mulneg1e1 9117 |
. . . . . . . . . . . . . . 15
     |
93 | 92 | oveq1i 5879 |
. . . . . . . . . . . . . 14
    
    |
94 | 93, 24 | eqtri 2198 |
. . . . . . . . . . . . 13
    
  |
95 | 91, 94 | eqtrdi 2226 |
. . . . . . . . . . . 12
  
       |
96 | 95 | ex 115 |
. . . . . . . . . . 11
          |
97 | 80, 96 | orim12d 786 |
. . . . . . . . . 10
       
           |
98 | | zmodcl 10327 |
. . . . . . . . . . . 12
 
     |
99 | 2, 98 | mpan2 425 |
. . . . . . . . . . 11
 
   |
100 | | elprg 3611 |
. . . . . . . . . . 11
  
     
 
 
     |
101 | 99, 100 | syl 14 |
. . . . . . . . . 10
      
 
 
     |
102 | | znegcl 9270 |
. . . . . . . . . . . . 13
    |
103 | 2 | a1i 9 |
. . . . . . . . . . . . 13
   |
104 | 102, 103 | zmodcld 10328 |
. . . . . . . . . . . 12
      |
105 | | elprg 3611 |
. . . . . . . . . . . 12
                      |
106 | 104, 105 | syl 14 |
. . . . . . . . . . 11
       
           |
107 | | orcom 728 |
. . . . . . . . . . 11
                   |
108 | 106, 107 | bitrdi 196 |
. . . . . . . . . 10
       
           |
109 | 97, 101, 108 | 3imtr4d 203 |
. . . . . . . . 9
                |
110 | 55, 109 | vtoclga 2803 |
. . . . . . . 8
 
                 |
111 | 49, 110 | syl 14 |
. . . . . . 7
                  |
112 | 27 | negnegd 8246 |
. . . . . . . . 9
     |
113 | 112 | oveq1d 5884 |
. . . . . . . 8
   
     |
114 | 113 | eleq1d 2246 |
. . . . . . 7
        
        |
115 | 111, 114 | sylibd 149 |
. . . . . 6
                |
116 | | oveq1 5876 |
. . . . . . . . 9
 
     |
117 | 116 | eleq1d 2246 |
. . . . . . . 8
      
        |
118 | | negeq 8137 |
. . . . . . . . . 10
     |
119 | 118 | oveq1d 5884 |
. . . . . . . . 9
         |
120 | 119 | eleq1d 2246 |
. . . . . . . 8
       
         |
121 | 117, 120 | imbi12d 234 |
. . . . . . 7
                    
          |
122 | 121, 109 | vtoclga 2803 |
. . . . . 6
                |
123 | 115, 122 | impbid 129 |
. . . . 5
       
        |
124 | 123 | ad2antlr 489 |
. . . 4
      
      
        |
125 | 48, 124 | bitrd 188 |
. . 3
      
   
   
        |
126 | 32, 125 | jaodan 797 |
. 2
                           |
127 | 8, 126 | sylbi 121 |
1
         
   
   
        |