Proof of Theorem m1lgs
Step | Hyp | Ref
| Expression |
1 | | neg1z 10973 |
. . . . . . . . 9
  |
2 | | oddprm 14765 |
. . . . . . . . . 10
           |
3 | 2 | nnnn0d 10925 |
. . . . . . . . 9
           |
4 | | zexpcl 12287 |
. . . . . . . . 9
                   |
5 | 1, 3, 4 | sylancr 669 |
. . . . . . . 8
                |
6 | 5 | peano2zd 11043 |
. . . . . . 7
                  |
7 | | eldifi 3555 |
. . . . . . . 8
    
  |
8 | | prmnn 14625 |
. . . . . . . 8

  |
9 | 7, 8 | syl 17 |
. . . . . . 7
    
  |
10 | 6, 9 | zmodcld 12117 |
. . . . . 6
                    |
11 | 10 | nn0cnd 10927 |
. . . . 5
                    |
12 | | 1cnd 9659 |
. . . . 5
       |
13 | 11, 12, 12 | subaddd 10004 |
. . . 4
                                       |
14 | | 2re 10679 |
. . . . . . . 8
 |
15 | 14 | a1i 11 |
. . . . . . 7
       |
16 | 9 | nnrpd 11339 |
. . . . . . 7
    
  |
17 | | 0le2 10700 |
. . . . . . . 8
 |
18 | 17 | a1i 11 |
. . . . . . 7
    
  |
19 | | eldifsni 4098 |
. . . . . . . 8
       |
20 | 9 | nnred 10624 |
. . . . . . . . 9
    
  |
21 | | prmuz2 14642 |
. . . . . . . . . . 11

      |
22 | 7, 21 | syl 17 |
. . . . . . . . . 10
    
      |
23 | | eluzle 11171 |
. . . . . . . . . 10
    
  |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
    
  |
25 | 15, 20, 24 | leltned 9788 |
. . . . . . . 8
         |
26 | 19, 25 | mpbird 236 |
. . . . . . 7
    
  |
27 | | modid 12121 |
. . . . . . 7
    
 
    |
28 | 15, 16, 18, 26, 27 | syl22anc 1269 |
. . . . . 6
         |
29 | | df-2 10668 |
. . . . . 6
   |
30 | 28, 29 | syl6eq 2501 |
. . . . 5
           |
31 | 30 | eqeq1d 2453 |
. . . 4
                                       |
32 | 19 | neneqd 2629 |
. . . . . . . . . . 11
    
  |
33 | | 2prm 14640 |
. . . . . . . . . . . 12
 |
34 | | dvdsprm 14647 |
. . . . . . . . . . . 12
       
   |
35 | 22, 33, 34 | sylancl 668 |
. . . . . . . . . . 11
         |
36 | 32, 35 | mtbird 303 |
. . . . . . . . . 10
    
  |
37 | 36 | adantr 467 |
. . . . . . . . 9
             |
38 | | 1cnd 9659 |
. . . . . . . . . . . . . . . 16
             |
39 | 2 | adantr 467 |
. . . . . . . . . . . . . . . 16
                 |
40 | | simpr 463 |
. . . . . . . . . . . . . . . 16
                 |
41 | | oexpneg 14368 |
. . . . . . . . . . . . . . . 16
     
                         |
42 | 38, 39, 40, 41 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
                               |
43 | 39 | nnzd 11039 |
. . . . . . . . . . . . . . . . 17
                 |
44 | | 1exp 12301 |
. . . . . . . . . . . . . . . . 17
               |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . 16
                     |
46 | 45 | negeqd 9869 |
. . . . . . . . . . . . . . 15
                       |
47 | 42, 46 | eqtrd 2485 |
. . . . . . . . . . . . . 14
                       |
48 | 47 | oveq1d 6305 |
. . . . . . . . . . . . 13
                           |
49 | | ax-1cn 9597 |
. . . . . . . . . . . . . 14
 |
50 | | neg1cn 10713 |
. . . . . . . . . . . . . 14
  |
51 | | 1pneg1e0 10718 |
. . . . . . . . . . . . . 14
    |
52 | 49, 50, 51 | addcomli 9825 |
. . . . . . . . . . . . 13
    |
53 | 48, 52 | syl6eq 2501 |
. . . . . . . . . . . 12
                        |
54 | 53 | oveq2d 6306 |
. . . . . . . . . . 11
                            |
55 | | 2cn 10680 |
. . . . . . . . . . . 12
 |
56 | 55 | subid1i 9946 |
. . . . . . . . . . 11
   |
57 | 54, 56 | syl6eq 2501 |
. . . . . . . . . 10
                          |
58 | 57 | breq2d 4414 |
. . . . . . . . 9
                        
   |
59 | 37, 58 | mtbird 303 |
. . . . . . . 8
                          |
60 | 59 | ex 436 |
. . . . . . 7
         
                |
61 | 60 | con4d 109 |
. . . . . 6
                  
       |
62 | | 2z 10969 |
. . . . . . . 8
 |
63 | 62 | a1i 11 |
. . . . . . 7
       |
64 | | moddvds 14312 |
. . . . . . 7
 
                           
                |
65 | 9, 63, 6, 64 | syl3anc 1268 |
. . . . . 6
                    
                |
66 | | 4z 10971 |
. . . . . . . . . 10
 |
67 | 66 | a1i 11 |
. . . . . . . . 9
       |
68 | | 4ne0 10706 |
. . . . . . . . . 10
 |
69 | 68 | a1i 11 |
. . . . . . . . 9
       |
70 | | nnm1nn0 10911 |
. . . . . . . . . . 11
 
   |
71 | 9, 70 | syl 17 |
. . . . . . . . . 10
         |
72 | 71 | nn0zd 11038 |
. . . . . . . . 9
         |
73 | | dvdsval2 14308 |
. . . . . . . . 9
  
   
        |
74 | 67, 69, 72, 73 | syl3anc 1268 |
. . . . . . . 8
      
        |
75 | 71 | nn0cnd 10927 |
. . . . . . . . . . 11
         |
76 | 55 | a1i 11 |
. . . . . . . . . . 11
       |
77 | | 2ne0 10702 |
. . . . . . . . . . . 12
 |
78 | 77 | a1i 11 |
. . . . . . . . . . 11
       |
79 | 75, 76, 76, 78, 78 | divdiv1d 10414 |
. . . . . . . . . 10
                   |
80 | | 2t2e4 10759 |
. . . . . . . . . . 11
   |
81 | 80 | oveq2i 6301 |
. . . . . . . . . 10
           |
82 | 79, 81 | syl6eq 2501 |
. . . . . . . . 9
                 |
83 | 82 | eleq1d 2513 |
. . . . . . . 8
                   |
84 | 74, 83 | bitr4d 260 |
. . . . . . 7
      
          |
85 | 2 | nnzd 11039 |
. . . . . . . 8
           |
86 | | dvdsval2 14308 |
. . . . . . . 8
                     |
87 | 63, 78, 85, 86 | syl3anc 1268 |
. . . . . . 7
                   |
88 | 84, 87 | bitr4d 260 |
. . . . . 6
      
        |
89 | 61, 65, 88 | 3imtr4d 272 |
. . . . 5
                    

    |
90 | 50 | a1i 11 |
. . . . . . . . . . 11
      
 
   |
91 | | neg1ne0 10715 |
. . . . . . . . . . . 12
  |
92 | 91 | a1i 11 |
. . . . . . . . . . 11
      
 
   |
93 | 62 | a1i 11 |
. . . . . . . . . . 11
      
 
  |
94 | 84 | biimpa 487 |
. . . . . . . . . . 11
      
 
        |
95 | | expmulz 12318 |
. . . . . . . . . . 11
              
                              |
96 | 90, 92, 93, 94, 95 | syl22anc 1269 |
. . . . . . . . . 10
      
 
                              |
97 | 2 | nncnd 10625 |
. . . . . . . . . . . . 13
           |
98 | 97, 76, 78 | divcan2d 10385 |
. . . . . . . . . . . 12
                   |
99 | 98 | adantr 467 |
. . . . . . . . . . 11
      
 
              |
100 | 99 | oveq2d 6306 |
. . . . . . . . . 10
      
 
                        |
101 | | neg1sqe1 12370 |
. . . . . . . . . . . 12
      |
102 | 101 | oveq1i 6300 |
. . . . . . . . . . 11
                          |
103 | | 1exp 12301 |
. . . . . . . . . . . 12
                   |
104 | 94, 103 | syl 17 |
. . . . . . . . . . 11
      
 
            |
105 | 102, 104 | syl5eq 2497 |
. . . . . . . . . 10
      
 
                 |
106 | 96, 100, 105 | 3eqtr3d 2493 |
. . . . . . . . 9
      
 
           |
107 | 106 | oveq1d 6305 |
. . . . . . . 8
      
 
               |
108 | 107, 29 | syl6reqr 2504 |
. . . . . . 7
      
 
             |
109 | 108 | oveq1d 6305 |
. . . . . 6
      
 
                 |
110 | 109 | ex 436 |
. . . . 5
      
                   |
111 | 89, 110 | impbid 194 |
. . . 4
                     
    |
112 | 13, 31, 111 | 3bitr2d 285 |
. . 3
                     
    |
113 | | lgsval3 24242 |
. . . . 5
       
                      |
114 | 1, 113 | mpan 676 |
. . . 4
                           |
115 | 114 | eqeq1d 2453 |
. . 3
                             |
116 | | 4nn 10769 |
. . . . 5
 |
117 | 116 | a1i 11 |
. . . 4
       |
118 | | prmz 14626 |
. . . . 5

  |
119 | 7, 118 | syl 17 |
. . . 4
    
  |
120 | | 1zzd 10968 |
. . . 4
       |
121 | | moddvds 14312 |
. . . 4
 
     

    |
122 | 117, 119,
120, 121 | syl3anc 1268 |
. . 3
               |
123 | 112, 115,
122 | 3bitr4d 289 |
. 2
                  |
124 | | 1re 9642 |
. . . 4
 |
125 | | nnrp 11311 |
. . . . 5
   |
126 | 116, 125 | ax-mp 5 |
. . . 4
 |
127 | | 0le1 10137 |
. . . 4
 |
128 | | 1lt4 10781 |
. . . 4
 |
129 | | modid 12121 |
. . . 4
    
  
   |
130 | 124, 126,
127, 128, 129 | mp4an 679 |
. . 3
   |
131 | 130 | eqeq2i 2463 |
. 2
    
    |
132 | 123, 131 | syl6bb 265 |
1
                |