Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . 6
|
2 | 1 | simp1d 994 |
. . . . 5
|
3 | 2 | phicld 12085 |
. . . 4
|
4 | | elnnuz 9470 |
. . . 4
|
5 | 3, 4 | sylib 121 |
. . 3
|
6 | | eluzfz2 9929 |
. . 3
|
7 | 5, 6 | syl 14 |
. 2
|
8 | | oveq2 5829 |
. . . . . . 7
|
9 | | oveq2 5829 |
. . . . . . . 8
|
10 | 9 | prodeq1d 11456 |
. . . . . . 7
|
11 | 8, 10 | oveq12d 5839 |
. . . . . 6
|
12 | 11 | oveq1d 5836 |
. . . . 5
|
13 | 9 | prodeq1d 11456 |
. . . . . 6
|
14 | 13 | oveq1d 5836 |
. . . . 5
|
15 | 12, 14 | eqeq12d 2172 |
. . . 4
|
16 | 15 | imbi2d 229 |
. . 3
|
17 | | oveq2 5829 |
. . . . . . 7
|
18 | | oveq2 5829 |
. . . . . . . 8
|
19 | 18 | prodeq1d 11456 |
. . . . . . 7
|
20 | 17, 19 | oveq12d 5839 |
. . . . . 6
|
21 | 20 | oveq1d 5836 |
. . . . 5
|
22 | 18 | prodeq1d 11456 |
. . . . . 6
|
23 | 22 | oveq1d 5836 |
. . . . 5
|
24 | 21, 23 | eqeq12d 2172 |
. . . 4
|
25 | 24 | imbi2d 229 |
. . 3
|
26 | | oveq2 5829 |
. . . . . . 7
|
27 | | oveq2 5829 |
. . . . . . . 8
|
28 | 27 | prodeq1d 11456 |
. . . . . . 7
|
29 | 26, 28 | oveq12d 5839 |
. . . . . 6
|
30 | 29 | oveq1d 5836 |
. . . . 5
|
31 | 27 | prodeq1d 11456 |
. . . . . 6
|
32 | 31 | oveq1d 5836 |
. . . . 5
|
33 | 30, 32 | eqeq12d 2172 |
. . . 4
|
34 | 33 | imbi2d 229 |
. . 3
|
35 | | oveq2 5829 |
. . . . . . 7
|
36 | | oveq2 5829 |
. . . . . . . 8
|
37 | 36 | prodeq1d 11456 |
. . . . . . 7
|
38 | 35, 37 | oveq12d 5839 |
. . . . . 6
|
39 | 38 | oveq1d 5836 |
. . . . 5
|
40 | 36 | prodeq1d 11456 |
. . . . . 6
|
41 | 40 | oveq1d 5836 |
. . . . 5
|
42 | 39, 41 | eqeq12d 2172 |
. . . 4
|
43 | 42 | imbi2d 229 |
. . 3
|
44 | 1 | simp2d 995 |
. . . . . . . 8
|
45 | | eulerth.2 |
. . . . . . . . . . . 12
..^ |
46 | | ssrab2 3213 |
. . . . . . . . . . . 12
..^ ..^ |
47 | 45, 46 | eqsstri 3160 |
. . . . . . . . . . 11
..^ |
48 | | fzo0ssnn0 10109 |
. . . . . . . . . . 11
..^ |
49 | 47, 48 | sstri 3137 |
. . . . . . . . . 10
|
50 | | nn0ssz 9180 |
. . . . . . . . . 10
|
51 | 49, 50 | sstri 3137 |
. . . . . . . . 9
|
52 | | eulerth.4 |
. . . . . . . . . . 11
|
53 | | f1of 5413 |
. . . . . . . . . . 11
|
54 | 52, 53 | syl 14 |
. . . . . . . . . 10
|
55 | | 1nn 8839 |
. . . . . . . . . . . 12
|
56 | 55 | a1i 9 |
. . . . . . . . . . 11
|
57 | 3 | nnge1d 8871 |
. . . . . . . . . . 11
|
58 | | elfz1b 9987 |
. . . . . . . . . . 11
|
59 | 56, 3, 57, 58 | syl3anbrc 1166 |
. . . . . . . . . 10
|
60 | 54, 59 | ffvelrnd 5602 |
. . . . . . . . 9
|
61 | 51, 60 | sseldi 3126 |
. . . . . . . 8
|
62 | 44, 61 | zmulcld 9287 |
. . . . . . 7
|
63 | | zq 9530 |
. . . . . . 7
|
64 | 62, 63 | syl 14 |
. . . . . 6
|
65 | | nnq 9537 |
. . . . . . 7
|
66 | 2, 65 | syl 14 |
. . . . . 6
|
67 | 2 | nngt0d 8872 |
. . . . . 6
|
68 | | modqabs2 10252 |
. . . . . 6
|
69 | 64, 66, 67, 68 | syl3anc 1220 |
. . . . 5
|
70 | | 1z 9188 |
. . . . . . 7
|
71 | 62, 2 | zmodcld 10239 |
. . . . . . . 8
|
72 | 71 | nn0cnd 9140 |
. . . . . . 7
|
73 | | fveq2 5467 |
. . . . . . . . . 10
|
74 | 73 | oveq2d 5837 |
. . . . . . . . 9
|
75 | 74 | oveq1d 5836 |
. . . . . . . 8
|
76 | 75 | fprod1 11486 |
. . . . . . 7
|
77 | 70, 72, 76 | sylancr 411 |
. . . . . 6
|
78 | 77 | oveq1d 5836 |
. . . . 5
|
79 | 44 | zcnd 9282 |
. . . . . . . 8
|
80 | 79 | exp1d 10541 |
. . . . . . 7
|
81 | | nn0sscn 9090 |
. . . . . . . . . 10
|
82 | 49, 81 | sstri 3137 |
. . . . . . . . 9
|
83 | 82, 60 | sseldi 3126 |
. . . . . . . 8
|
84 | 73 | fprod1 11486 |
. . . . . . . 8
|
85 | 70, 83, 84 | sylancr 411 |
. . . . . . 7
|
86 | 80, 85 | oveq12d 5839 |
. . . . . 6
|
87 | 86 | oveq1d 5836 |
. . . . 5
|
88 | 69, 78, 87 | 3eqtr4rd 2201 |
. . . 4
|
89 | 88 | a1i 9 |
. . 3
|
90 | 44 | adantr 274 |
. . . . . . . . . . . 12
..^ |
91 | | elfzo1 10084 |
. . . . . . . . . . . . . . 15
..^ |
92 | 91 | simp1bi 997 |
. . . . . . . . . . . . . 14
..^
|
93 | 92 | adantl 275 |
. . . . . . . . . . . . 13
..^ |
94 | 93 | nnnn0d 9138 |
. . . . . . . . . . . 12
..^ |
95 | | zexpcl 10429 |
. . . . . . . . . . . 12
|
96 | 90, 94, 95 | syl2anc 409 |
. . . . . . . . . . 11
..^ |
97 | 70 | a1i 9 |
. . . . . . . . . . . . 13
..^ |
98 | 93 | nnzd 9280 |
. . . . . . . . . . . . 13
..^ |
99 | 97, 98 | fzfigd 10325 |
. . . . . . . . . . . 12
..^ |
100 | 54 | ad2antrr 480 |
. . . . . . . . . . . . . 14
..^
|
101 | | elfzelz 9923 |
. . . . . . . . . . . . . . . . . 18
|
102 | 101 | zred 9281 |
. . . . . . . . . . . . . . . . 17
|
103 | 102 | adantl 275 |
. . . . . . . . . . . . . . . 16
..^
|
104 | 3 | nnzd 9280 |
. . . . . . . . . . . . . . . . . 18
|
105 | 104 | ad2antrr 480 |
. . . . . . . . . . . . . . . . 17
..^
|
106 | 105 | zred 9281 |
. . . . . . . . . . . . . . . 16
..^
|
107 | 93 | nnred 8841 |
. . . . . . . . . . . . . . . . . 18
..^ |
108 | 107 | adantr 274 |
. . . . . . . . . . . . . . . . 17
..^
|
109 | | elfzle2 9925 |
. . . . . . . . . . . . . . . . . 18
|
110 | 109 | adantl 275 |
. . . . . . . . . . . . . . . . 17
..^
|
111 | | elfzolt2 10050 |
. . . . . . . . . . . . . . . . . 18
..^
|
112 | 111 | ad2antlr 481 |
. . . . . . . . . . . . . . . . 17
..^
|
113 | 103, 108,
106, 110, 112 | lelttrd 7995 |
. . . . . . . . . . . . . . . 16
..^
|
114 | 103, 106,
113 | ltled 7989 |
. . . . . . . . . . . . . . 15
..^
|
115 | | elfzuz 9919 |
. . . . . . . . . . . . . . . 16
|
116 | | elfz5 9915 |
. . . . . . . . . . . . . . . 16
|
117 | 115, 105,
116 | syl2an2 584 |
. . . . . . . . . . . . . . 15
..^
|
118 | 114, 117 | mpbird 166 |
. . . . . . . . . . . . . 14
..^
|
119 | 100, 118 | ffvelrnd 5602 |
. . . . . . . . . . . . 13
..^
|
120 | 51, 119 | sseldi 3126 |
. . . . . . . . . . . 12
..^
|
121 | 99, 120 | fprodzcl 11501 |
. . . . . . . . . . 11
..^ |
122 | 96, 121 | zmulcld 9287 |
. . . . . . . . . 10
..^
|
123 | | zq 9530 |
. . . . . . . . . 10
|
124 | 122, 123 | syl 14 |
. . . . . . . . 9
..^
|
125 | 124 | adantr 274 |
. . . . . . . 8
..^
|
126 | 90 | adantr 274 |
. . . . . . . . . . . . . 14
..^
|
127 | 126, 120 | zmulcld 9287 |
. . . . . . . . . . . . 13
..^
|
128 | 2 | ad2antrr 480 |
. . . . . . . . . . . . 13
..^
|
129 | 127, 128 | zmodcld 10239 |
. . . . . . . . . . . 12
..^
|
130 | 129 | nn0zd 9279 |
. . . . . . . . . . 11
..^
|
131 | 99, 130 | fprodzcl 11501 |
. . . . . . . . . 10
..^ |
132 | | zq 9530 |
. . . . . . . . . 10
|
133 | 131, 132 | syl 14 |
. . . . . . . . 9
..^ |
134 | 133 | adantr 274 |
. . . . . . . 8
..^
|
135 | 44 | ad2antrr 480 |
. . . . . . . . 9
..^
|
136 | 54 | ad2antrr 480 |
. . . . . . . . . . 11
..^
|
137 | | fzofzp1 10121 |
. . . . . . . . . . . 12
..^
|
138 | 137 | ad2antlr 481 |
. . . . . . . . . . 11
..^
|
139 | 136, 138 | ffvelrnd 5602 |
. . . . . . . . . 10
..^
|
140 | 51, 139 | sseldi 3126 |
. . . . . . . . 9
..^
|
141 | 135, 140 | zmulcld 9287 |
. . . . . . . 8
..^
|
142 | 66 | ad2antrr 480 |
. . . . . . . 8
..^
|
143 | 67 | ad2antrr 480 |
. . . . . . . 8
..^
|
144 | | simpr 109 |
. . . . . . . 8
..^
|
145 | 125, 134,
141, 142, 143, 144 | modqmul1 10271 |
. . . . . . 7
..^
|
146 | 145 | ex 114 |
. . . . . 6
..^
|
147 | 96 | zcnd 9282 |
. . . . . . . . . 10
..^ |
148 | 121 | zcnd 9282 |
. . . . . . . . . 10
..^ |
149 | 79 | adantr 274 |
. . . . . . . . . 10
..^ |
150 | 54 | adantr 274 |
. . . . . . . . . . . 12
..^ |
151 | 137 | adantl 275 |
. . . . . . . . . . . 12
..^ |
152 | 150, 151 | ffvelrnd 5602 |
. . . . . . . . . . 11
..^ |
153 | 82, 152 | sseldi 3126 |
. . . . . . . . . 10
..^ |
154 | 147, 148,
149, 153 | mul4d 8025 |
. . . . . . . . 9
..^
|
155 | 149, 94 | expp1d 10547 |
. . . . . . . . . 10
..^ |
156 | | elfzouz 10045 |
. . . . . . . . . . . 12
..^
|
157 | 156 | adantl 275 |
. . . . . . . . . . 11
..^ |
158 | 150 | adantr 274 |
. . . . . . . . . . . . 13
..^
|
159 | | elfzelz 9923 |
. . . . . . . . . . . . . . . . 17
|
160 | 159 | zred 9281 |
. . . . . . . . . . . . . . . 16
|
161 | 160 | adantl 275 |
. . . . . . . . . . . . . . 15
..^
|
162 | | peano2re 8006 |
. . . . . . . . . . . . . . . . 17
|
163 | 107, 162 | syl 14 |
. . . . . . . . . . . . . . . 16
..^ |
164 | 163 | adantr 274 |
. . . . . . . . . . . . . . 15
..^
|
165 | 104 | ad2antrr 480 |
. . . . . . . . . . . . . . . 16
..^
|
166 | 165 | zred 9281 |
. . . . . . . . . . . . . . 15
..^
|
167 | | elfzle2 9925 |
. . . . . . . . . . . . . . . 16
|
168 | 167 | adantl 275 |
. . . . . . . . . . . . . . 15
..^
|
169 | 137 | ad2antlr 481 |
. . . . . . . . . . . . . . . 16
..^
|
170 | | elfzle2 9925 |
. . . . . . . . . . . . . . . 16
|
171 | 169, 170 | syl 14 |
. . . . . . . . . . . . . . 15
..^
|
172 | 161, 164,
166, 168, 171 | letrd 7994 |
. . . . . . . . . . . . . 14
..^
|
173 | | elfzuz 9919 |
. . . . . . . . . . . . . . 15
|
174 | 173, 165,
116 | syl2an2 584 |
. . . . . . . . . . . . . 14
..^
|
175 | 172, 174 | mpbird 166 |
. . . . . . . . . . . . 13
..^
|
176 | 158, 175 | ffvelrnd 5602 |
. . . . . . . . . . . 12
..^
|
177 | 82, 176 | sseldi 3126 |
. . . . . . . . . . 11
..^
|
178 | | fveq2 5467 |
. . . . . . . . . . 11
|
179 | 157, 177,
178 | fprodp1 11492 |
. . . . . . . . . 10
..^ |
180 | 155, 179 | oveq12d 5839 |
. . . . . . . . 9
..^
|
181 | 154, 180 | eqtr4d 2193 |
. . . . . . . 8
..^
|
182 | 181 | oveq1d 5836 |
. . . . . . 7
..^ |
183 | 51, 152 | sseldi 3126 |
. . . . . . . . . . . . 13
..^ |
184 | 90, 183 | zmulcld 9287 |
. . . . . . . . . . . 12
..^ |
185 | 2 | adantr 274 |
. . . . . . . . . . . 12
..^ |
186 | 184, 185 | zmodcld 10239 |
. . . . . . . . . . 11
..^ |
187 | 186 | nn0zd 9279 |
. . . . . . . . . 10
..^ |
188 | | zq 9530 |
. . . . . . . . . 10
|
189 | 187, 188 | syl 14 |
. . . . . . . . 9
..^ |
190 | | zq 9530 |
. . . . . . . . . 10
|
191 | 184, 190 | syl 14 |
. . . . . . . . 9
..^ |
192 | 66 | adantr 274 |
. . . . . . . . 9
..^ |
193 | 67 | adantr 274 |
. . . . . . . . 9
..^ |
194 | | modqabs2 10252 |
. . . . . . . . . 10
|
195 | 191, 192,
193, 194 | syl3anc 1220 |
. . . . . . . . 9
..^ |
196 | 189, 191,
131, 192, 193, 195 | modqmul1 10271 |
. . . . . . . 8
..^ |
197 | 90 | adantr 274 |
. . . . . . . . . . . . . 14
..^
|
198 | 51, 176 | sseldi 3126 |
. . . . . . . . . . . . . 14
..^
|
199 | 197, 198 | zmulcld 9287 |
. . . . . . . . . . . . 13
..^
|
200 | 185 | adantr 274 |
. . . . . . . . . . . . 13
..^
|
201 | 199, 200 | zmodcld 10239 |
. . . . . . . . . . . 12
..^
|
202 | 201 | nn0cnd 9140 |
. . . . . . . . . . 11
..^
|
203 | 178 | oveq2d 5837 |
. . . . . . . . . . . 12
|
204 | 203 | oveq1d 5836 |
. . . . . . . . . . 11
|
205 | 157, 202,
204 | fprodp1 11492 |
. . . . . . . . . 10
..^ |
206 | 186 | nn0cnd 9140 |
. . . . . . . . . . 11
..^ |
207 | 131 | zcnd 9282 |
. . . . . . . . . . 11
..^ |
208 | 206, 207 | mulcomd 7894 |
. . . . . . . . . 10
..^
|
209 | 205, 208 | eqtr4d 2193 |
. . . . . . . . 9
..^
|
210 | 209 | oveq1d 5836 |
. . . . . . . 8
..^ |
211 | 149, 153 | mulcld 7893 |
. . . . . . . . . 10
..^ |
212 | 207, 211 | mulcomd 7894 |
. . . . . . . . 9
..^
|
213 | 212 | oveq1d 5836 |
. . . . . . . 8
..^
|
214 | 196, 210,
213 | 3eqtr4rd 2201 |
. . . . . . 7
..^
|
215 | 182, 214 | eqeq12d 2172 |
. . . . . 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 10133 |
. 2
|
220 | 7, 219 | mpcom 36 |
1
|