Proof of Theorem m1lgs
Step | Hyp | Ref
| Expression |
1 | | neg1z 11413 |
. . . . . . . . 9
|
2 | | oddprm 15515 |
. . . . . . . . . 10
|
3 | 2 | nnnn0d 11351 |
. . . . . . . . 9
|
4 | | zexpcl 12875 |
. . . . . . . . 9
|
5 | 1, 3, 4 | sylancr 695 |
. . . . . . . 8
|
6 | 5 | peano2zd 11485 |
. . . . . . 7
|
7 | | eldifi 3732 |
. . . . . . . 8
|
8 | | prmnn 15388 |
. . . . . . . 8
|
9 | 7, 8 | syl 17 |
. . . . . . 7
|
10 | 6, 9 | zmodcld 12691 |
. . . . . 6
|
11 | 10 | nn0cnd 11353 |
. . . . 5
|
12 | | 1cnd 10056 |
. . . . 5
|
13 | 11, 12, 12 | subaddd 10410 |
. . . 4
|
14 | | 2re 11090 |
. . . . . . . 8
|
15 | 14 | a1i 11 |
. . . . . . 7
|
16 | 9 | nnrpd 11870 |
. . . . . . 7
|
17 | | 0le2 11111 |
. . . . . . . 8
|
18 | 17 | a1i 11 |
. . . . . . 7
|
19 | | eldifsni 4320 |
. . . . . . . 8
|
20 | 9 | nnred 11035 |
. . . . . . . . 9
|
21 | | prmuz2 15408 |
. . . . . . . . . . 11
|
22 | 7, 21 | syl 17 |
. . . . . . . . . 10
|
23 | | eluzle 11700 |
. . . . . . . . . 10
|
24 | 22, 23 | syl 17 |
. . . . . . . . 9
|
25 | 15, 20, 24 | leltned 10190 |
. . . . . . . 8
|
26 | 19, 25 | mpbird 247 |
. . . . . . 7
|
27 | | modid 12695 |
. . . . . . 7
|
28 | 15, 16, 18, 26, 27 | syl22anc 1327 |
. . . . . 6
|
29 | | df-2 11079 |
. . . . . 6
|
30 | 28, 29 | syl6eq 2672 |
. . . . 5
|
31 | 30 | eqeq1d 2624 |
. . . 4
|
32 | 19 | neneqd 2799 |
. . . . . . . . . . 11
|
33 | | 2prm 15405 |
. . . . . . . . . . . 12
|
34 | | dvdsprm 15415 |
. . . . . . . . . . . 12
|
35 | 22, 33, 34 | sylancl 694 |
. . . . . . . . . . 11
|
36 | 32, 35 | mtbird 315 |
. . . . . . . . . 10
|
37 | 36 | adantr 481 |
. . . . . . . . 9
|
38 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
|
39 | 2 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
40 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
41 | | oexpneg 15069 |
. . . . . . . . . . . . . . . 16
|
42 | 38, 39, 40, 41 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
43 | 39 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
44 | | 1exp 12889 |
. . . . . . . . . . . . . . . . 17
|
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . 16
|
46 | 45 | negeqd 10275 |
. . . . . . . . . . . . . . 15
|
47 | 42, 46 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
48 | 47 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
49 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
|
50 | | neg1cn 11124 |
. . . . . . . . . . . . . 14
|
51 | | 1pneg1e0 11129 |
. . . . . . . . . . . . . 14
|
52 | 49, 50, 51 | addcomli 10228 |
. . . . . . . . . . . . 13
|
53 | 48, 52 | syl6eq 2672 |
. . . . . . . . . . . 12
|
54 | 53 | oveq2d 6666 |
. . . . . . . . . . 11
|
55 | | 2cn 11091 |
. . . . . . . . . . . 12
|
56 | 55 | subid1i 10353 |
. . . . . . . . . . 11
|
57 | 54, 56 | syl6eq 2672 |
. . . . . . . . . 10
|
58 | 57 | breq2d 4665 |
. . . . . . . . 9
|
59 | 37, 58 | mtbird 315 |
. . . . . . . 8
|
60 | 59 | ex 450 |
. . . . . . 7
|
61 | 60 | con4d 114 |
. . . . . 6
|
62 | | 2z 11409 |
. . . . . . . 8
|
63 | 62 | a1i 11 |
. . . . . . 7
|
64 | | moddvds 14991 |
. . . . . . 7
|
65 | 9, 63, 6, 64 | syl3anc 1326 |
. . . . . 6
|
66 | | 4z 11411 |
. . . . . . . . . 10
|
67 | 66 | a1i 11 |
. . . . . . . . 9
|
68 | | 4ne0 11117 |
. . . . . . . . . 10
|
69 | 68 | a1i 11 |
. . . . . . . . 9
|
70 | | nnm1nn0 11334 |
. . . . . . . . . . 11
|
71 | 9, 70 | syl 17 |
. . . . . . . . . 10
|
72 | 71 | nn0zd 11480 |
. . . . . . . . 9
|
73 | | dvdsval2 14986 |
. . . . . . . . 9
|
74 | 67, 69, 72, 73 | syl3anc 1326 |
. . . . . . . 8
|
75 | 71 | nn0cnd 11353 |
. . . . . . . . . . 11
|
76 | 55 | a1i 11 |
. . . . . . . . . . 11
|
77 | | 2ne0 11113 |
. . . . . . . . . . . 12
|
78 | 77 | a1i 11 |
. . . . . . . . . . 11
|
79 | 75, 76, 76, 78, 78 | divdiv1d 10832 |
. . . . . . . . . 10
|
80 | | 2t2e4 11177 |
. . . . . . . . . . 11
|
81 | 80 | oveq2i 6661 |
. . . . . . . . . 10
|
82 | 79, 81 | syl6eq 2672 |
. . . . . . . . 9
|
83 | 82 | eleq1d 2686 |
. . . . . . . 8
|
84 | 74, 83 | bitr4d 271 |
. . . . . . 7
|
85 | 2 | nnzd 11481 |
. . . . . . . 8
|
86 | | dvdsval2 14986 |
. . . . . . . 8
|
87 | 63, 78, 85, 86 | syl3anc 1326 |
. . . . . . 7
|
88 | 84, 87 | bitr4d 271 |
. . . . . 6
|
89 | 61, 65, 88 | 3imtr4d 283 |
. . . . 5
|
90 | 50 | a1i 11 |
. . . . . . . . . . 11
|
91 | | neg1ne0 11126 |
. . . . . . . . . . . 12
|
92 | 91 | a1i 11 |
. . . . . . . . . . 11
|
93 | 62 | a1i 11 |
. . . . . . . . . . 11
|
94 | 84 | biimpa 501 |
. . . . . . . . . . 11
|
95 | | expmulz 12906 |
. . . . . . . . . . 11
|
96 | 90, 92, 93, 94, 95 | syl22anc 1327 |
. . . . . . . . . 10
|
97 | 2 | nncnd 11036 |
. . . . . . . . . . . . 13
|
98 | 97, 76, 78 | divcan2d 10803 |
. . . . . . . . . . . 12
|
99 | 98 | adantr 481 |
. . . . . . . . . . 11
|
100 | 99 | oveq2d 6666 |
. . . . . . . . . 10
|
101 | | neg1sqe1 12959 |
. . . . . . . . . . . 12
|
102 | 101 | oveq1i 6660 |
. . . . . . . . . . 11
|
103 | | 1exp 12889 |
. . . . . . . . . . . 12
|
104 | 94, 103 | syl 17 |
. . . . . . . . . . 11
|
105 | 102, 104 | syl5eq 2668 |
. . . . . . . . . 10
|
106 | 96, 100, 105 | 3eqtr3d 2664 |
. . . . . . . . 9
|
107 | 106 | oveq1d 6665 |
. . . . . . . 8
|
108 | 107, 29 | syl6reqr 2675 |
. . . . . . 7
|
109 | 108 | oveq1d 6665 |
. . . . . 6
|
110 | 109 | ex 450 |
. . . . 5
|
111 | 89, 110 | impbid 202 |
. . . 4
|
112 | 13, 31, 111 | 3bitr2d 296 |
. . 3
|
113 | | lgsval3 25040 |
. . . . 5
|
114 | 1, 113 | mpan 706 |
. . . 4
|
115 | 114 | eqeq1d 2624 |
. . 3
|
116 | | 4nn 11187 |
. . . . 5
|
117 | 116 | a1i 11 |
. . . 4
|
118 | | prmz 15389 |
. . . . 5
|
119 | 7, 118 | syl 17 |
. . . 4
|
120 | | 1zzd 11408 |
. . . 4
|
121 | | moddvds 14991 |
. . . 4
|
122 | 117, 119,
120, 121 | syl3anc 1326 |
. . 3
|
123 | 112, 115,
122 | 3bitr4d 300 |
. 2
|
124 | | 1re 10039 |
. . . 4
|
125 | | nnrp 11842 |
. . . . 5
|
126 | 116, 125 | ax-mp 5 |
. . . 4
|
127 | | 0le1 10551 |
. . . 4
|
128 | | 1lt4 11199 |
. . . 4
|
129 | | modid 12695 |
. . . 4
|
130 | 124, 126,
127, 128, 129 | mp4an 709 |
. . 3
|
131 | 130 | eqeq2i 2634 |
. 2
|
132 | 123, 131 | syl6bb 276 |
1
|