Step | Hyp | Ref
| Expression |
1 | | ovex 6218 |
. . 3
   |
2 | 1 | elpr 3996 |
. 2
     
        |
3 | | zre 10754 |
. . . . . . 7
   |
4 | 3 | ad2antrr 725 |
. . . . . 6
      
  |
5 | | 1red 9505 |
. . . . . 6
      
  |
6 | | simplr 754 |
. . . . . 6
      
  |
7 | | 8re 10510 |
. . . . . . . 8
 |
8 | | 8pos 10526 |
. . . . . . . 8
 |
9 | 7, 8 | elrpii 11098 |
. . . . . . 7
 |
10 | 9 | a1i 11 |
. . . . . 6
      
  |
11 | | simpr 461 |
. . . . . . 7
      
    |
12 | | lgsdir2lem1 22788 |
. . . . . . . . 9
                 |
13 | 12 | simpli 458 |
. . . . . . . 8
        |
14 | 13 | simpli 458 |
. . . . . . 7
   |
15 | 11, 14 | syl6eqr 2510 |
. . . . . 6
      
      |
16 | | modmul1 11862 |
. . . . . 6
     
       
       |
17 | 4, 5, 6, 10, 15, 16 | syl221anc 1230 |
. . . . 5
      
 
    
   |
18 | | zcn 10755 |
. . . . . . . 8
   |
19 | 18 | ad2antlr 726 |
. . . . . . 7
      
  |
20 | 19 | mulid2d 9508 |
. . . . . 6
      
    |
21 | 20 | oveq1d 6208 |
. . . . 5
      
        |
22 | 17, 21 | eqtrd 2492 |
. . . 4
      
 
      |
23 | 22 | eleq1d 2520 |
. . 3
      
   
   
        |
24 | 3 | ad2antrr 725 |
. . . . . . 7
      
  |
25 | | neg1rr 10530 |
. . . . . . . 8
  |
26 | 25 | a1i 11 |
. . . . . . 7
      
   |
27 | | simplr 754 |
. . . . . . 7
      
  |
28 | 9 | a1i 11 |
. . . . . . 7
      
  |
29 | | simpr 461 |
. . . . . . . 8
      
    |
30 | 13 | simpri 462 |
. . . . . . . 8
 
  |
31 | 29, 30 | syl6eqr 2510 |
. . . . . . 7
      
       |
32 | | modmul1 11862 |
. . . . . . 7
   
  
             
   |
33 | 24, 26, 27, 28, 31, 32 | syl221anc 1230 |
. . . . . 6
      
 
         |
34 | 18 | ad2antlr 726 |
. . . . . . . 8
      
  |
35 | 34 | mulm1d 9900 |
. . . . . . 7
      
      |
36 | 35 | oveq1d 6208 |
. . . . . 6
      
          |
37 | 33, 36 | eqtrd 2492 |
. . . . 5
      
 
       |
38 | 37 | eleq1d 2520 |
. . . 4
      
   
   
         |
39 | | znegcl 10784 |
. . . . . . . 8
    |
40 | | oveq1 6200 |
. . . . . . . . . . 11
  
      |
41 | 40 | eleq1d 2520 |
. . . . . . . . . 10
       
         |
42 | | negeq 9706 |
. . . . . . . . . . . 12
       |
43 | 42 | oveq1d 6208 |
. . . . . . . . . . 11
           |
44 | 43 | eleq1d 2520 |
. . . . . . . . . 10
        
          |
45 | 41, 44 | imbi12d 320 |
. . . . . . . . 9
                      
           |
46 | | zcn 10755 |
. . . . . . . . . . . . . . . . 17
   |
47 | | neg1cn 10529 |
. . . . . . . . . . . . . . . . . . 19
  |
48 | | mulcom 9472 |
. . . . . . . . . . . . . . . . . . 19
            |
49 | 47, 48 | mpan2 671 |
. . . . . . . . . . . . . . . . . 18
         |
50 | | mulm1 9890 |
. . . . . . . . . . . . . . . . . 18
       |
51 | 49, 50 | eqtrd 2492 |
. . . . . . . . . . . . . . . . 17
       |
52 | 46, 51 | syl 16 |
. . . . . . . . . . . . . . . 16
       |
53 | 52 | adantr 465 |
. . . . . . . . . . . . . . 15
  
        |
54 | 53 | oveq1d 6208 |
. . . . . . . . . . . . . 14
  
            |
55 | | zre 10754 |
. . . . . . . . . . . . . . . 16
   |
56 | 55 | adantr 465 |
. . . . . . . . . . . . . . 15
  
    |
57 | | 1red 9505 |
. . . . . . . . . . . . . . 15
  
    |
58 | | neg1z 10785 |
. . . . . . . . . . . . . . . 16
  |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . 15
  
     |
60 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
  
    |
61 | | simpr 461 |
. . . . . . . . . . . . . . . 16
  
      |
62 | 61, 14 | syl6eqr 2510 |
. . . . . . . . . . . . . . 15
  
        |
63 | | modmul1 11862 |
. . . . . . . . . . . . . . 15
      

            
   |
64 | 56, 57, 59, 60, 62, 63 | syl221anc 1230 |
. . . . . . . . . . . . . 14
  
          
   |
65 | 54, 64 | eqtr3d 2494 |
. . . . . . . . . . . . 13
  
        
   |
66 | 47 | mulid2i 9493 |
. . . . . . . . . . . . . . 15
     |
67 | 66 | oveq1i 6203 |
. . . . . . . . . . . . . 14
   
     |
68 | 67, 30 | eqtri 2480 |
. . . . . . . . . . . . 13
   
  |
69 | 65, 68 | syl6eq 2508 |
. . . . . . . . . . . 12
  
       |
70 | 69 | ex 434 |
. . . . . . . . . . 11
          |
71 | 52 | adantr 465 |
. . . . . . . . . . . . . . 15
  
        |
72 | 71 | oveq1d 6208 |
. . . . . . . . . . . . . 14
  
            |
73 | 55 | adantr 465 |
. . . . . . . . . . . . . . 15
  
    |
74 | 25 | a1i 11 |
. . . . . . . . . . . . . . 15
  
     |
75 | 58 | a1i 11 |
. . . . . . . . . . . . . . 15
  
     |
76 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
  
    |
77 | | simpr 461 |
. . . . . . . . . . . . . . . 16
  
      |
78 | 77, 30 | syl6eqr 2510 |
. . . . . . . . . . . . . . 15
  
         |
79 | | modmul1 11862 |
. . . . . . . . . . . . . . 15
   
   

                  |
80 | 73, 74, 75, 76, 78, 79 | syl221anc 1230 |
. . . . . . . . . . . . . 14
  
               |
81 | 72, 80 | eqtr3d 2494 |
. . . . . . . . . . . . 13
  
             |
82 | | neg1mulneg1e1 10643 |
. . . . . . . . . . . . . . 15
     |
83 | 82 | oveq1i 6203 |
. . . . . . . . . . . . . 14
    
    |
84 | 83, 14 | eqtri 2480 |
. . . . . . . . . . . . 13
    
  |
85 | 81, 84 | syl6eq 2508 |
. . . . . . . . . . . 12
  
       |
86 | 85 | ex 434 |
. . . . . . . . . . 11
          |
87 | 70, 86 | orim12d 834 |
. . . . . . . . . 10
       
           |
88 | | ovex 6218 |
. . . . . . . . . . 11
   |
89 | 88 | elpr 3996 |
. . . . . . . . . 10
     
 
 
    |
90 | | ovex 6218 |
. . . . . . . . . . . 12
    |
91 | 90 | elpr 3996 |
. . . . . . . . . . 11
      
          |
92 | | orcom 387 |
. . . . . . . . . . 11
                   |
93 | 91, 92 | bitri 249 |
. . . . . . . . . 10
      
          |
94 | 87, 89, 93 | 3imtr4g 270 |
. . . . . . . . 9
                |
95 | 45, 94 | vtoclga 3135 |
. . . . . . . 8
 
                 |
96 | 39, 95 | syl 16 |
. . . . . . 7
                  |
97 | 18 | negnegd 9814 |
. . . . . . . . 9
     |
98 | 97 | oveq1d 6208 |
. . . . . . . 8
   
     |
99 | 98 | eleq1d 2520 |
. . . . . . 7
        
        |
100 | 96, 99 | sylibd 214 |
. . . . . 6
                |
101 | | oveq1 6200 |
. . . . . . . . 9
 
     |
102 | 101 | eleq1d 2520 |
. . . . . . . 8
      
        |
103 | | negeq 9706 |
. . . . . . . . . 10
     |
104 | 103 | oveq1d 6208 |
. . . . . . . . 9
         |
105 | 104 | eleq1d 2520 |
. . . . . . . 8
       
         |
106 | 102, 105 | imbi12d 320 |
. . . . . . 7
                    
          |
107 | 106, 94 | vtoclga 3135 |
. . . . . 6
                |
108 | 100, 107 | impbid 191 |
. . . . 5
       
        |
109 | 108 | ad2antlr 726 |
. . . 4
      
      
        |
110 | 38, 109 | bitrd 253 |
. . 3
      
   
   
        |
111 | 23, 110 | jaodan 783 |
. 2
                           |
112 | 2, 111 | sylan2b 475 |
1
         
   
   
        |