Proof of Theorem gausslemma2dlem0i
Step | Hyp | Ref
| Expression |
1 | | 2z 9331 |
. . . 4
 |
2 | | gausslemma2dlem0.p |
. . . . 5
       |
3 | | id 19 |
. . . . . . 7
    
      |
4 | 3 | gausslemma2dlem0a 15093 |
. . . . . 6
    
  |
5 | 4 | nnzd 9424 |
. . . . 5
    
  |
6 | 2, 5 | syl 14 |
. . . 4
   |
7 | | lgscl1 15067 |
. . . 4
 
            |
8 | 1, 6, 7 | sylancr 414 |
. . 3
            |
9 | | eltpg 3659 |
. . . 4
                   
                  |
10 | 8, 9 | syl 14 |
. . 3
          
                  |
11 | 8, 10 | mpbid 147 |
. 2
                  |
12 | | gausslemma2dlem0.m |
. . . . . . . . 9
       |
13 | | gausslemma2dlem0.h |
. . . . . . . . 9
     |
14 | | gausslemma2dlem0.n |
. . . . . . . . 9
   |
15 | 2, 12, 13, 14 | gausslemma2dlem0h 15100 |
. . . . . . . 8
   |
16 | 15 | nn0zd 9423 |
. . . . . . 7
   |
17 | | m1expcl2 10606 |
. . . . . . 7
            |
18 | 16, 17 | syl 14 |
. . . . . 6
            |
19 | | elprg 3634 |
. . . . . . 7
                   
                |
20 | 18, 19 | syl 14 |
. . . . . 6
                           |
21 | 18, 20 | mpbid 147 |
. . . . 5
                |
22 | | eqcom 2191 |
. . . . . . . 8
               |
23 | 22 | biimpi 120 |
. . . . . . 7
               |
24 | 23 | 2a1d 23 |
. . . . . 6
                 
           |
25 | 2 | gausslemma2dlem0a 15093 |
. . . . . . . . . . 11
   |
26 | | nnq 9684 |
. . . . . . . . . . 11
   |
27 | 25, 26 | syl 14 |
. . . . . . . . . 10
   |
28 | 2 | eldifad 3160 |
. . . . . . . . . . 11
   |
29 | | prmgt1 12244 |
. . . . . . . . . . 11

  |
30 | 28, 29 | syl 14 |
. . . . . . . . . 10
   |
31 | | q1mod 10413 |
. . . . . . . . . 10
       |
32 | 27, 30, 31 | syl2anc 411 |
. . . . . . . . 9
     |
33 | 32 | eqeq2d 2201 |
. . . . . . . 8
             |
34 | | oddprmge3 12247 |
. . . . . . . . 9
    
      |
35 | | m1modge3gt1 10428 |
. . . . . . . . . 10
    
     |
36 | | breq2 4029 |
. . . . . . . . . . 11
           |
37 | | 1re 8004 |
. . . . . . . . . . . . 13
 |
38 | 37 | ltnri 8098 |
. . . . . . . . . . . 12
 |
39 | 38 | pm2.21i 647 |
. . . . . . . . . . 11
    |
40 | 36, 39 | biimtrdi 163 |
. . . . . . . . . 10
            |
41 | 35, 40 | syl5com 29 |
. . . . . . . . 9
    
        |
42 | 2, 34, 41 | 3syl 17 |
. . . . . . . 8
         |
43 | 33, 42 | sylbid 150 |
. . . . . . 7
           |
44 | | oveq1 5913 |
. . . . . . . . 9
                 |
45 | 44 | eqeq2d 2201 |
. . . . . . . 8
                         |
46 | | eqeq2 2199 |
. . . . . . . 8
                 |
47 | 45, 46 | imbi12d 234 |
. . . . . . 7
         
                 
        |
48 | 43, 47 | imbitrrid 156 |
. . . . . 6
      
         
           |
49 | 24, 48 | jaoi 717 |
. . . . 5
              
         
           |
50 | 21, 49 | mpcom 36 |
. . . 4
           
         |
51 | | oveq1 5913 |
. . . . . 6
                 |
52 | 51 | eqeq1d 2198 |
. . . . 5
                                 |
53 | | eqeq1 2196 |
. . . . 5
               
         |
54 | 52, 53 | imbi12d 234 |
. . . 4
                              
                     |
55 | 50, 54 | imbitrrid 156 |
. . 3
                    
             |
56 | 25 | nngt0d 9012 |
. . . . . . 7
   |
57 | | q0mod 10412 |
. . . . . . 7
       |
58 | 27, 56, 57 | syl2anc 411 |
. . . . . 6
     |
59 | 58 | eqeq1d 2198 |
. . . . 5
                     |
60 | | oveq1 5913 |
. . . . . . . . . . 11
               
   |
61 | 60 | eqeq2d 2201 |
. . . . . . . . . 10
                     |
62 | 61 | adantr 276 |
. . . . . . . . 9
       
               |
63 | | 1z 9329 |
. . . . . . . . . . . . . 14
 |
64 | | zq 9677 |
. . . . . . . . . . . . . 14
   |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . . . . . 13
 |
66 | | negqmod0 10388 |
. . . . . . . . . . . . 13
 
          |
67 | 65, 27, 56, 66 | mp3an2i 1353 |
. . . . . . . . . . . 12
          |
68 | | eqcom 2191 |
. . . . . . . . . . . 12
         |
69 | 67, 68 | bitrdi 196 |
. . . . . . . . . . 11
     
    |
70 | 32 | eqeq1d 2198 |
. . . . . . . . . . . 12
       |
71 | | 1ne0 9036 |
. . . . . . . . . . . . 13
 |
72 | | eqneqall 2370 |
. . . . . . . . . . . . 13
          |
73 | 71, 72 | mpi 15 |
. . . . . . . . . . . 12
        |
74 | 70, 73 | biimtrdi 163 |
. . . . . . . . . . 11
            |
75 | 69, 74 | sylbird 170 |
. . . . . . . . . 10
    
        |
76 | 75 | adantl 277 |
. . . . . . . . 9
       
    
        |
77 | 62, 76 | sylbid 150 |
. . . . . . . 8
       
        
        |
78 | 77 | ex 115 |
. . . . . . 7
              
          |
79 | 44 | eqeq2d 2201 |
. . . . . . . . . 10
                   |
80 | 79 | adantr 276 |
. . . . . . . . 9
                     |
81 | | eqcom 2191 |
. . . . . . . . . . . 12
  
    |
82 | 81, 70 | bitrid 192 |
. . . . . . . . . . 11
       |
83 | 82, 73 | biimtrdi 163 |
. . . . . . . . . 10
            |
84 | 83 | adantl 277 |
. . . . . . . . 9
                   |
85 | 80, 84 | sylbid 150 |
. . . . . . . 8
               
        |
86 | 85 | ex 115 |
. . . . . . 7
      
                 |
87 | 78, 86 | jaoi 717 |
. . . . . 6
              
                 |
88 | 21, 87 | mpcom 36 |
. . . . 5
        
        |
89 | 59, 88 | sylbid 150 |
. . . 4
          
        |
90 | | oveq1 5913 |
. . . . . 6
               |
91 | 90 | eqeq1d 2198 |
. . . . 5
                               |
92 | | eqeq1 2196 |
. . . . 5
              
        |
93 | 91, 92 | imbi12d 234 |
. . . 4
                             
 
                 |
94 | 89, 93 | imbitrrid 156 |
. . 3
     
            
              |
95 | 32 | eqeq1d 2198 |
. . . . 5
                     |
96 | | eqcom 2191 |
. . . . . . . . 9
   
     |
97 | | eqcom 2191 |
. . . . . . . . 9
 
   |
98 | 42, 96, 97 | 3imtr4g 205 |
. . . . . . . 8
    
    |
99 | 60 | eqeq2d 2201 |
. . . . . . . . 9
                     |
100 | | eqeq2 2199 |
. . . . . . . . 9
                 |
101 | 99, 100 | imbi12d 234 |
. . . . . . . 8
               
     
         |
102 | 98, 101 | imbitrrid 156 |
. . . . . . 7
              
          |
103 | | eqcom 2191 |
. . . . . . . . 9
             |
104 | 103 | biimpi 120 |
. . . . . . . 8
             |
105 | 104 | 2a1d 23 |
. . . . . . 7
      
                 |
106 | 102, 105 | jaoi 717 |
. . . . . 6
              
                 |
107 | 21, 106 | mpcom 36 |
. . . . 5
        
        |
108 | 95, 107 | sylbid 150 |
. . . 4
          
        |
109 | | oveq1 5913 |
. . . . . 6
               |
110 | 109 | eqeq1d 2198 |
. . . . 5
                               |
111 | | eqeq1 2196 |
. . . . 5
              
        |
112 | 110, 111 | imbi12d 234 |
. . . 4
                             
 
                 |
113 | 108, 112 | imbitrrid 156 |
. . 3
     
            
              |
114 | 55, 94, 113 | 3jaoi 1314 |
. 2
                              
             |
115 | 11, 114 | mpcom 36 |
1
              
            |