Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . 6
|
2 | 1 | simp1d 1004 |
. . . . 5
|
3 | 2 | phicld 12172 |
. . . 4
|
4 | | elnnuz 9523 |
. . . 4
|
5 | 3, 4 | sylib 121 |
. . 3
|
6 | | eluzfz2 9988 |
. . 3
|
7 | 5, 6 | syl 14 |
. 2
|
8 | | oveq2 5861 |
. . . . . . 7
|
9 | | oveq2 5861 |
. . . . . . . 8
|
10 | 9 | prodeq1d 11527 |
. . . . . . 7
|
11 | 8, 10 | oveq12d 5871 |
. . . . . 6
|
12 | 11 | oveq1d 5868 |
. . . . 5
|
13 | 9 | prodeq1d 11527 |
. . . . . 6
|
14 | 13 | oveq1d 5868 |
. . . . 5
|
15 | 12, 14 | eqeq12d 2185 |
. . . 4
|
16 | 15 | imbi2d 229 |
. . 3
|
17 | | oveq2 5861 |
. . . . . . 7
|
18 | | oveq2 5861 |
. . . . . . . 8
|
19 | 18 | prodeq1d 11527 |
. . . . . . 7
|
20 | 17, 19 | oveq12d 5871 |
. . . . . 6
|
21 | 20 | oveq1d 5868 |
. . . . 5
|
22 | 18 | prodeq1d 11527 |
. . . . . 6
|
23 | 22 | oveq1d 5868 |
. . . . 5
|
24 | 21, 23 | eqeq12d 2185 |
. . . 4
|
25 | 24 | imbi2d 229 |
. . 3
|
26 | | oveq2 5861 |
. . . . . . 7
|
27 | | oveq2 5861 |
. . . . . . . 8
|
28 | 27 | prodeq1d 11527 |
. . . . . . 7
|
29 | 26, 28 | oveq12d 5871 |
. . . . . 6
|
30 | 29 | oveq1d 5868 |
. . . . 5
|
31 | 27 | prodeq1d 11527 |
. . . . . 6
|
32 | 31 | oveq1d 5868 |
. . . . 5
|
33 | 30, 32 | eqeq12d 2185 |
. . . 4
|
34 | 33 | imbi2d 229 |
. . 3
|
35 | | oveq2 5861 |
. . . . . . 7
|
36 | | oveq2 5861 |
. . . . . . . 8
|
37 | 36 | prodeq1d 11527 |
. . . . . . 7
|
38 | 35, 37 | oveq12d 5871 |
. . . . . 6
|
39 | 38 | oveq1d 5868 |
. . . . 5
|
40 | 36 | prodeq1d 11527 |
. . . . . 6
|
41 | 40 | oveq1d 5868 |
. . . . 5
|
42 | 39, 41 | eqeq12d 2185 |
. . . 4
|
43 | 42 | imbi2d 229 |
. . 3
|
44 | 1 | simp2d 1005 |
. . . . . . . 8
|
45 | | eulerth.2 |
. . . . . . . . . . . 12
..^ |
46 | | ssrab2 3232 |
. . . . . . . . . . . 12
..^ ..^ |
47 | 45, 46 | eqsstri 3179 |
. . . . . . . . . . 11
..^ |
48 | | fzo0ssnn0 10171 |
. . . . . . . . . . 11
..^ |
49 | 47, 48 | sstri 3156 |
. . . . . . . . . 10
|
50 | | nn0ssz 9230 |
. . . . . . . . . 10
|
51 | 49, 50 | sstri 3156 |
. . . . . . . . 9
|
52 | | eulerth.4 |
. . . . . . . . . . 11
|
53 | | f1of 5442 |
. . . . . . . . . . 11
|
54 | 52, 53 | syl 14 |
. . . . . . . . . 10
|
55 | | 1nn 8889 |
. . . . . . . . . . . 12
|
56 | 55 | a1i 9 |
. . . . . . . . . . 11
|
57 | 3 | nnge1d 8921 |
. . . . . . . . . . 11
|
58 | | elfz1b 10046 |
. . . . . . . . . . 11
|
59 | 56, 3, 57, 58 | syl3anbrc 1176 |
. . . . . . . . . 10
|
60 | 54, 59 | ffvelrnd 5632 |
. . . . . . . . 9
|
61 | 51, 60 | sselid 3145 |
. . . . . . . 8
|
62 | 44, 61 | zmulcld 9340 |
. . . . . . 7
|
63 | | zq 9585 |
. . . . . . 7
|
64 | 62, 63 | syl 14 |
. . . . . 6
|
65 | | nnq 9592 |
. . . . . . 7
|
66 | 2, 65 | syl 14 |
. . . . . 6
|
67 | 2 | nngt0d 8922 |
. . . . . 6
|
68 | | modqabs2 10314 |
. . . . . 6
|
69 | 64, 66, 67, 68 | syl3anc 1233 |
. . . . 5
|
70 | | 1z 9238 |
. . . . . . 7
|
71 | 62, 2 | zmodcld 10301 |
. . . . . . . 8
|
72 | 71 | nn0cnd 9190 |
. . . . . . 7
|
73 | | fveq2 5496 |
. . . . . . . . . 10
|
74 | 73 | oveq2d 5869 |
. . . . . . . . 9
|
75 | 74 | oveq1d 5868 |
. . . . . . . 8
|
76 | 75 | fprod1 11557 |
. . . . . . 7
|
77 | 70, 72, 76 | sylancr 412 |
. . . . . 6
|
78 | 77 | oveq1d 5868 |
. . . . 5
|
79 | 44 | zcnd 9335 |
. . . . . . . 8
|
80 | 79 | exp1d 10604 |
. . . . . . 7
|
81 | | nn0sscn 9140 |
. . . . . . . . . 10
|
82 | 49, 81 | sstri 3156 |
. . . . . . . . 9
|
83 | 82, 60 | sselid 3145 |
. . . . . . . 8
|
84 | 73 | fprod1 11557 |
. . . . . . . 8
|
85 | 70, 83, 84 | sylancr 412 |
. . . . . . 7
|
86 | 80, 85 | oveq12d 5871 |
. . . . . 6
|
87 | 86 | oveq1d 5868 |
. . . . 5
|
88 | 69, 78, 87 | 3eqtr4rd 2214 |
. . . 4
|
89 | 88 | a1i 9 |
. . 3
|
90 | 44 | adantr 274 |
. . . . . . . . . . . 12
..^ |
91 | | elfzo1 10146 |
. . . . . . . . . . . . . . 15
..^ |
92 | 91 | simp1bi 1007 |
. . . . . . . . . . . . . 14
..^
|
93 | 92 | adantl 275 |
. . . . . . . . . . . . 13
..^ |
94 | 93 | nnnn0d 9188 |
. . . . . . . . . . . 12
..^ |
95 | | zexpcl 10491 |
. . . . . . . . . . . 12
|
96 | 90, 94, 95 | syl2anc 409 |
. . . . . . . . . . 11
..^ |
97 | 70 | a1i 9 |
. . . . . . . . . . . . 13
..^ |
98 | 93 | nnzd 9333 |
. . . . . . . . . . . . 13
..^ |
99 | 97, 98 | fzfigd 10387 |
. . . . . . . . . . . 12
..^ |
100 | 54 | ad2antrr 485 |
. . . . . . . . . . . . . 14
..^
|
101 | | elfzelz 9981 |
. . . . . . . . . . . . . . . . . 18
|
102 | 101 | zred 9334 |
. . . . . . . . . . . . . . . . 17
|
103 | 102 | adantl 275 |
. . . . . . . . . . . . . . . 16
..^
|
104 | 3 | nnzd 9333 |
. . . . . . . . . . . . . . . . . 18
|
105 | 104 | ad2antrr 485 |
. . . . . . . . . . . . . . . . 17
..^
|
106 | 105 | zred 9334 |
. . . . . . . . . . . . . . . 16
..^
|
107 | 93 | nnred 8891 |
. . . . . . . . . . . . . . . . . 18
..^ |
108 | 107 | adantr 274 |
. . . . . . . . . . . . . . . . 17
..^
|
109 | | elfzle2 9984 |
. . . . . . . . . . . . . . . . . 18
|
110 | 109 | adantl 275 |
. . . . . . . . . . . . . . . . 17
..^
|
111 | | elfzolt2 10112 |
. . . . . . . . . . . . . . . . . 18
..^
|
112 | 111 | ad2antlr 486 |
. . . . . . . . . . . . . . . . 17
..^
|
113 | 103, 108,
106, 110, 112 | lelttrd 8044 |
. . . . . . . . . . . . . . . 16
..^
|
114 | 103, 106,
113 | ltled 8038 |
. . . . . . . . . . . . . . 15
..^
|
115 | | elfzuz 9977 |
. . . . . . . . . . . . . . . 16
|
116 | | elfz5 9973 |
. . . . . . . . . . . . . . . 16
|
117 | 115, 105,
116 | syl2an2 589 |
. . . . . . . . . . . . . . 15
..^
|
118 | 114, 117 | mpbird 166 |
. . . . . . . . . . . . . 14
..^
|
119 | 100, 118 | ffvelrnd 5632 |
. . . . . . . . . . . . 13
..^
|
120 | 51, 119 | sselid 3145 |
. . . . . . . . . . . 12
..^
|
121 | 99, 120 | fprodzcl 11572 |
. . . . . . . . . . 11
..^ |
122 | 96, 121 | zmulcld 9340 |
. . . . . . . . . 10
..^
|
123 | | zq 9585 |
. . . . . . . . . 10
|
124 | 122, 123 | syl 14 |
. . . . . . . . 9
..^
|
125 | 124 | adantr 274 |
. . . . . . . 8
..^
|
126 | 90 | adantr 274 |
. . . . . . . . . . . . . 14
..^
|
127 | 126, 120 | zmulcld 9340 |
. . . . . . . . . . . . 13
..^
|
128 | 2 | ad2antrr 485 |
. . . . . . . . . . . . 13
..^
|
129 | 127, 128 | zmodcld 10301 |
. . . . . . . . . . . 12
..^
|
130 | 129 | nn0zd 9332 |
. . . . . . . . . . 11
..^
|
131 | 99, 130 | fprodzcl 11572 |
. . . . . . . . . 10
..^ |
132 | | zq 9585 |
. . . . . . . . . 10
|
133 | 131, 132 | syl 14 |
. . . . . . . . 9
..^ |
134 | 133 | adantr 274 |
. . . . . . . 8
..^
|
135 | 44 | ad2antrr 485 |
. . . . . . . . 9
..^
|
136 | 54 | ad2antrr 485 |
. . . . . . . . . . 11
..^
|
137 | | fzofzp1 10183 |
. . . . . . . . . . . 12
..^
|
138 | 137 | ad2antlr 486 |
. . . . . . . . . . 11
..^
|
139 | 136, 138 | ffvelrnd 5632 |
. . . . . . . . . 10
..^
|
140 | 51, 139 | sselid 3145 |
. . . . . . . . 9
..^
|
141 | 135, 140 | zmulcld 9340 |
. . . . . . . 8
..^
|
142 | 66 | ad2antrr 485 |
. . . . . . . 8
..^
|
143 | 67 | ad2antrr 485 |
. . . . . . . 8
..^
|
144 | | simpr 109 |
. . . . . . . 8
..^
|
145 | 125, 134,
141, 142, 143, 144 | modqmul1 10333 |
. . . . . . 7
..^
|
146 | 145 | ex 114 |
. . . . . 6
..^
|
147 | 96 | zcnd 9335 |
. . . . . . . . . 10
..^ |
148 | 121 | zcnd 9335 |
. . . . . . . . . 10
..^ |
149 | 79 | adantr 274 |
. . . . . . . . . 10
..^ |
150 | 54 | adantr 274 |
. . . . . . . . . . . 12
..^ |
151 | 137 | adantl 275 |
. . . . . . . . . . . 12
..^ |
152 | 150, 151 | ffvelrnd 5632 |
. . . . . . . . . . 11
..^ |
153 | 82, 152 | sselid 3145 |
. . . . . . . . . 10
..^ |
154 | 147, 148,
149, 153 | mul4d 8074 |
. . . . . . . . 9
..^
|
155 | 149, 94 | expp1d 10610 |
. . . . . . . . . 10
..^ |
156 | | elfzouz 10107 |
. . . . . . . . . . . 12
..^
|
157 | 156 | adantl 275 |
. . . . . . . . . . 11
..^ |
158 | 150 | adantr 274 |
. . . . . . . . . . . . 13
..^
|
159 | | elfzelz 9981 |
. . . . . . . . . . . . . . . . 17
|
160 | 159 | zred 9334 |
. . . . . . . . . . . . . . . 16
|
161 | 160 | adantl 275 |
. . . . . . . . . . . . . . 15
..^
|
162 | | peano2re 8055 |
. . . . . . . . . . . . . . . . 17
|
163 | 107, 162 | syl 14 |
. . . . . . . . . . . . . . . 16
..^ |
164 | 163 | adantr 274 |
. . . . . . . . . . . . . . 15
..^
|
165 | 104 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
..^
|
166 | 165 | zred 9334 |
. . . . . . . . . . . . . . 15
..^
|
167 | | elfzle2 9984 |
. . . . . . . . . . . . . . . 16
|
168 | 167 | adantl 275 |
. . . . . . . . . . . . . . 15
..^
|
169 | 137 | ad2antlr 486 |
. . . . . . . . . . . . . . . 16
..^
|
170 | | elfzle2 9984 |
. . . . . . . . . . . . . . . 16
|
171 | 169, 170 | syl 14 |
. . . . . . . . . . . . . . 15
..^
|
172 | 161, 164,
166, 168, 171 | letrd 8043 |
. . . . . . . . . . . . . 14
..^
|
173 | | elfzuz 9977 |
. . . . . . . . . . . . . . 15
|
174 | 173, 165,
116 | syl2an2 589 |
. . . . . . . . . . . . . 14
..^
|
175 | 172, 174 | mpbird 166 |
. . . . . . . . . . . . 13
..^
|
176 | 158, 175 | ffvelrnd 5632 |
. . . . . . . . . . . 12
..^
|
177 | 82, 176 | sselid 3145 |
. . . . . . . . . . 11
..^
|
178 | | fveq2 5496 |
. . . . . . . . . . 11
|
179 | 157, 177,
178 | fprodp1 11563 |
. . . . . . . . . 10
..^ |
180 | 155, 179 | oveq12d 5871 |
. . . . . . . . 9
..^
|
181 | 154, 180 | eqtr4d 2206 |
. . . . . . . 8
..^
|
182 | 181 | oveq1d 5868 |
. . . . . . 7
..^ |
183 | 51, 152 | sselid 3145 |
. . . . . . . . . . . . 13
..^ |
184 | 90, 183 | zmulcld 9340 |
. . . . . . . . . . . 12
..^ |
185 | 2 | adantr 274 |
. . . . . . . . . . . 12
..^ |
186 | 184, 185 | zmodcld 10301 |
. . . . . . . . . . 11
..^ |
187 | 186 | nn0zd 9332 |
. . . . . . . . . 10
..^ |
188 | | zq 9585 |
. . . . . . . . . 10
|
189 | 187, 188 | syl 14 |
. . . . . . . . 9
..^ |
190 | | zq 9585 |
. . . . . . . . . 10
|
191 | 184, 190 | syl 14 |
. . . . . . . . 9
..^ |
192 | 66 | adantr 274 |
. . . . . . . . 9
..^ |
193 | 67 | adantr 274 |
. . . . . . . . 9
..^ |
194 | | modqabs2 10314 |
. . . . . . . . . 10
|
195 | 191, 192,
193, 194 | syl3anc 1233 |
. . . . . . . . 9
..^ |
196 | 189, 191,
131, 192, 193, 195 | modqmul1 10333 |
. . . . . . . 8
..^ |
197 | 90 | adantr 274 |
. . . . . . . . . . . . . 14
..^
|
198 | 51, 176 | sselid 3145 |
. . . . . . . . . . . . . 14
..^
|
199 | 197, 198 | zmulcld 9340 |
. . . . . . . . . . . . 13
..^
|
200 | 185 | adantr 274 |
. . . . . . . . . . . . 13
..^
|
201 | 199, 200 | zmodcld 10301 |
. . . . . . . . . . . 12
..^
|
202 | 201 | nn0cnd 9190 |
. . . . . . . . . . 11
..^
|
203 | 178 | oveq2d 5869 |
. . . . . . . . . . . 12
|
204 | 203 | oveq1d 5868 |
. . . . . . . . . . 11
|
205 | 157, 202,
204 | fprodp1 11563 |
. . . . . . . . . 10
..^ |
206 | 186 | nn0cnd 9190 |
. . . . . . . . . . 11
..^ |
207 | 131 | zcnd 9335 |
. . . . . . . . . . 11
..^ |
208 | 206, 207 | mulcomd 7941 |
. . . . . . . . . 10
..^
|
209 | 205, 208 | eqtr4d 2206 |
. . . . . . . . 9
..^
|
210 | 209 | oveq1d 5868 |
. . . . . . . 8
..^ |
211 | 149, 153 | mulcld 7940 |
. . . . . . . . . 10
..^ |
212 | 207, 211 | mulcomd 7941 |
. . . . . . . . 9
..^
|
213 | 212 | oveq1d 5868 |
. . . . . . . 8
..^
|
214 | 196, 210,
213 | 3eqtr4rd 2214 |
. . . . . . 7
..^
|
215 | 182, 214 | eqeq12d 2185 |
. . . . . 6
..^
|
216 | 146, 215 | sylibd 148 |
. . . . 5
..^
|
217 | 216 | expcom 115 |
. . . 4
..^
|
218 | 217 | a2d 26 |
. . 3
..^
|
219 | 16, 25, 34, 43, 89, 218 | fzind2 10195 |
. 2
|
220 | 7, 219 | mpcom 36 |
1
|