Step | Hyp | Ref
| Expression |
1 | | 1cnd 7929 |
. . . . . . . 8
|
2 | | 0cnd 7906 |
. . . . . . . 8
|
3 | | zsqcl 10539 |
. . . . . . . . . 10
|
4 | 3 | 3ad2ant2 1014 |
. . . . . . . . 9
|
5 | | 1z 9231 |
. . . . . . . . 9
|
6 | | zdceq 9280 |
. . . . . . . . 9
DECID |
7 | 4, 5, 6 | sylancl 411 |
. . . . . . . 8
DECID |
8 | 1, 2, 7 | ifcldcd 3560 |
. . . . . . 7
|
9 | 8 | mulid2d 7931 |
. . . . . 6
|
10 | 9 | ad3antrrr 489 |
. . . . 5
|
11 | | iftrue 3530 |
. . . . . . 7
|
12 | 11 | adantl 275 |
. . . . . 6
|
13 | 12 | oveq1d 5866 |
. . . . 5
|
14 | | simpl1 995 |
. . . . . . . . . . 11
|
15 | 14 | zcnd 9328 |
. . . . . . . . . 10
|
16 | 15 | ad2antrr 485 |
. . . . . . . . 9
|
17 | | simpl2 996 |
. . . . . . . . . . 11
|
18 | 17 | zcnd 9328 |
. . . . . . . . . 10
|
19 | 18 | ad2antrr 485 |
. . . . . . . . 9
|
20 | 16, 19 | sqmuld 10614 |
. . . . . . . 8
|
21 | | simpr 109 |
. . . . . . . . 9
|
22 | 21 | oveq1d 5866 |
. . . . . . . 8
|
23 | 18 | sqcld 10600 |
. . . . . . . . . 10
|
24 | 23 | ad2antrr 485 |
. . . . . . . . 9
|
25 | 24 | mulid2d 7931 |
. . . . . . . 8
|
26 | 20, 22, 25 | 3eqtrd 2207 |
. . . . . . 7
|
27 | 26 | eqeq1d 2179 |
. . . . . 6
|
28 | 27 | ifbid 3546 |
. . . . 5
|
29 | 10, 13, 28 | 3eqtr4d 2213 |
. . . 4
|
30 | 8 | mul02d 8304 |
. . . . . 6
|
31 | 30 | ad3antrrr 489 |
. . . . 5
|
32 | | iffalse 3533 |
. . . . . . 7
|
33 | 32 | adantl 275 |
. . . . . 6
|
34 | 33 | oveq1d 5866 |
. . . . 5
|
35 | | dvdsmul1 11768 |
. . . . . . . . . . . 12
|
36 | 14, 17, 35 | syl2anc 409 |
. . . . . . . . . . 11
|
37 | 14, 17 | zmulcld 9333 |
. . . . . . . . . . . 12
|
38 | | dvdssq 11979 |
. . . . . . . . . . . 12
|
39 | 14, 37, 38 | syl2anc 409 |
. . . . . . . . . . 11
|
40 | 36, 39 | mpbid 146 |
. . . . . . . . . 10
|
41 | 40 | adantr 274 |
. . . . . . . . 9
|
42 | | breq2 3991 |
. . . . . . . . 9
|
43 | 41, 42 | syl5ibcom 154 |
. . . . . . . 8
|
44 | | simprl 526 |
. . . . . . . . . . . . . . . 16
|
45 | 44 | neneqd 2361 |
. . . . . . . . . . . . . . 15
|
46 | | sqeq0 10532 |
. . . . . . . . . . . . . . . 16
|
47 | 15, 46 | syl 14 |
. . . . . . . . . . . . . . 15
|
48 | 45, 47 | mtbird 668 |
. . . . . . . . . . . . . 14
|
49 | | zsqcl2 10546 |
. . . . . . . . . . . . . . . 16
|
50 | 14, 49 | syl 14 |
. . . . . . . . . . . . . . 15
|
51 | | elnn0 9130 |
. . . . . . . . . . . . . . 15
|
52 | 50, 51 | sylib 121 |
. . . . . . . . . . . . . 14
|
53 | 48, 52 | ecased 1344 |
. . . . . . . . . . . . 13
|
54 | 53 | adantr 274 |
. . . . . . . . . . . 12
|
55 | 54 | nnzd 9326 |
. . . . . . . . . . 11
|
56 | | 1nn 8882 |
. . . . . . . . . . 11
|
57 | | dvdsle 11797 |
. . . . . . . . . . 11
|
58 | 55, 56, 57 | sylancl 411 |
. . . . . . . . . 10
|
59 | 54 | nnge1d 8914 |
. . . . . . . . . 10
|
60 | 58, 59 | jctird 315 |
. . . . . . . . 9
|
61 | 54 | nnred 8884 |
. . . . . . . . . 10
|
62 | | 1re 7912 |
. . . . . . . . . 10
|
63 | | letri3 7993 |
. . . . . . . . . 10
|
64 | 61, 62, 63 | sylancl 411 |
. . . . . . . . 9
|
65 | 60, 64 | sylibrd 168 |
. . . . . . . 8
|
66 | 43, 65 | syld 45 |
. . . . . . 7
|
67 | 66 | con3dimp 630 |
. . . . . 6
|
68 | 67 | iffalsed 3535 |
. . . . 5
|
69 | 31, 34, 68 | 3eqtr4d 2213 |
. . . 4
|
70 | | zdceq 9280 |
. . . . . 6
DECID |
71 | 55, 5, 70 | sylancl 411 |
. . . . 5
DECID |
72 | | exmiddc 831 |
. . . . 5
DECID
|
73 | 71, 72 | syl 14 |
. . . 4
|
74 | 29, 69, 73 | mpjaodan 793 |
. . 3
|
75 | | oveq2 5859 |
. . . . 5
|
76 | | lgs0 13673 |
. . . . . 6
|
77 | 14, 76 | syl 14 |
. . . . 5
|
78 | 75, 77 | sylan9eqr 2225 |
. . . 4
|
79 | | oveq2 5859 |
. . . . 5
|
80 | | lgs0 13673 |
. . . . . 6
|
81 | 17, 80 | syl 14 |
. . . . 5
|
82 | 79, 81 | sylan9eqr 2225 |
. . . 4
|
83 | 78, 82 | oveq12d 5869 |
. . 3
|
84 | | oveq2 5859 |
. . . 4
|
85 | | lgs0 13673 |
. . . . 5
|
86 | 37, 85 | syl 14 |
. . . 4
|
87 | 84, 86 | sylan9eqr 2225 |
. . 3
|
88 | 74, 83, 87 | 3eqtr4rd 2214 |
. 2
|
89 | | lgsdilem 13687 |
. . . . 5
|
90 | 89 | adantr 274 |
. . . 4
|
91 | | simpl3 997 |
. . . . . . 7
|
92 | | nnabscl 11057 |
. . . . . . 7
|
93 | 91, 92 | sylan 281 |
. . . . . 6
|
94 | | nnuz 9515 |
. . . . . 6
|
95 | 93, 94 | eleqtrdi 2263 |
. . . . 5
|
96 | | simpll1 1031 |
. . . . . . . 8
|
97 | | simpll3 1033 |
. . . . . . . 8
|
98 | | simpr 109 |
. . . . . . . 8
|
99 | | eqid 2170 |
. . . . . . . . 9
|
100 | 99 | lgsfcl3 13681 |
. . . . . . . 8
|
101 | 96, 97, 98, 100 | syl3anc 1233 |
. . . . . . 7
|
102 | | elnnuz 9516 |
. . . . . . . 8
|
103 | 102 | biimpri 132 |
. . . . . . 7
|
104 | | ffvelrn 5627 |
. . . . . . 7
|
105 | 101, 103,
104 | syl2an 287 |
. . . . . 6
|
106 | 105 | zcnd 9328 |
. . . . 5
|
107 | | simpll2 1032 |
. . . . . . . 8
|
108 | | eqid 2170 |
. . . . . . . . 9
|
109 | 108 | lgsfcl3 13681 |
. . . . . . . 8
|
110 | 107, 97, 98, 109 | syl3anc 1233 |
. . . . . . 7
|
111 | | ffvelrn 5627 |
. . . . . . 7
|
112 | 110, 103,
111 | syl2an 287 |
. . . . . 6
|
113 | 112 | zcnd 9328 |
. . . . 5
|
114 | 96 | adantr 274 |
. . . . . . . . . . . 12
|
115 | 107 | adantr 274 |
. . . . . . . . . . . 12
|
116 | | simpr 109 |
. . . . . . . . . . . 12
|
117 | | lgsdirprm 13694 |
. . . . . . . . . . . 12
|
118 | 114, 115,
116, 117 | syl3anc 1233 |
. . . . . . . . . . 11
|
119 | 118 | oveq1d 5866 |
. . . . . . . . . 10
|
120 | | prmz 12058 |
. . . . . . . . . . . . 13
|
121 | | lgscl 13674 |
. . . . . . . . . . . . 13
|
122 | 96, 120, 121 | syl2an 287 |
. . . . . . . . . . . 12
|
123 | 122 | zcnd 9328 |
. . . . . . . . . . 11
|
124 | | lgscl 13674 |
. . . . . . . . . . . . 13
|
125 | 107, 120,
124 | syl2an 287 |
. . . . . . . . . . . 12
|
126 | 125 | zcnd 9328 |
. . . . . . . . . . 11
|
127 | 97 | adantr 274 |
. . . . . . . . . . . 12
|
128 | 98 | adantr 274 |
. . . . . . . . . . . 12
|
129 | | pczcl 12245 |
. . . . . . . . . . . 12
|
130 | 116, 127,
128, 129 | syl12anc 1231 |
. . . . . . . . . . 11
|
131 | 123, 126,
130 | mulexpd 10617 |
. . . . . . . . . 10
|
132 | 119, 131 | eqtrd 2203 |
. . . . . . . . 9
|
133 | | iftrue 3530 |
. . . . . . . . . 10
|
134 | 133 | adantl 275 |
. . . . . . . . 9
|
135 | | iftrue 3530 |
. . . . . . . . . . 11
|
136 | | iftrue 3530 |
. . . . . . . . . . 11
|
137 | 135, 136 | oveq12d 5869 |
. . . . . . . . . 10
|
138 | 137 | adantl 275 |
. . . . . . . . 9
|
139 | 132, 134,
138 | 3eqtr4d 2213 |
. . . . . . . 8
|
140 | 139 | adantlr 474 |
. . . . . . 7
|
141 | | 1t1e1 9023 |
. . . . . . . . . 10
|
142 | 141 | eqcomi 2174 |
. . . . . . . . 9
|
143 | | iffalse 3533 |
. . . . . . . . 9
|
144 | | iffalse 3533 |
. . . . . . . . . 10
|
145 | | iffalse 3533 |
. . . . . . . . . 10
|
146 | 144, 145 | oveq12d 5869 |
. . . . . . . . 9
|
147 | 142, 143,
146 | 3eqtr4a 2229 |
. . . . . . . 8
|
148 | 147 | adantl 275 |
. . . . . . 7
|
149 | 103 | adantl 275 |
. . . . . . . . 9
|
150 | | prmdc 12077 |
. . . . . . . . 9
DECID
|
151 | 149, 150 | syl 14 |
. . . . . . . 8
DECID |
152 | | exmiddc 831 |
. . . . . . . 8
DECID |
153 | 151, 152 | syl 14 |
. . . . . . 7
|
154 | 140, 148,
153 | mpjaodan 793 |
. . . . . 6
|
155 | | eqid 2170 |
. . . . . . 7
|
156 | | eleq1w 2231 |
. . . . . . . 8
|
157 | | oveq2 5859 |
. . . . . . . . 9
|
158 | | oveq1 5858 |
. . . . . . . . 9
|
159 | 157, 158 | oveq12d 5869 |
. . . . . . . 8
|
160 | 156, 159 | ifbieq1d 3547 |
. . . . . . 7
|
161 | 37 | ad3antrrr 489 |
. . . . . . . . . 10
|
162 | 120 | adantl 275 |
. . . . . . . . . 10
|
163 | | lgscl 13674 |
. . . . . . . . . 10
|
164 | 161, 162,
163 | syl2anc 409 |
. . . . . . . . 9
|
165 | 130 | adantlr 474 |
. . . . . . . . 9
|
166 | | zexpcl 10484 |
. . . . . . . . 9
|
167 | 164, 165,
166 | syl2anc 409 |
. . . . . . . 8
|
168 | | 1zzd 9232 |
. . . . . . . 8
|
169 | 167, 168,
151 | ifcldadc 3554 |
. . . . . . 7
|
170 | 155, 160,
149, 169 | fvmptd3 5587 |
. . . . . 6
|
171 | | oveq2 5859 |
. . . . . . . . . 10
|
172 | 171, 158 | oveq12d 5869 |
. . . . . . . . 9
|
173 | 156, 172 | ifbieq1d 3547 |
. . . . . . . 8
|
174 | 122 | adantlr 474 |
. . . . . . . . . 10
|
175 | | zexpcl 10484 |
. . . . . . . . . 10
|
176 | 174, 165,
175 | syl2anc 409 |
. . . . . . . . 9
|
177 | 176, 168,
151 | ifcldadc 3554 |
. . . . . . . 8
|
178 | 99, 173, 149, 177 | fvmptd3 5587 |
. . . . . . 7
|
179 | | oveq2 5859 |
. . . . . . . . . 10
|
180 | 179, 158 | oveq12d 5869 |
. . . . . . . . 9
|
181 | 156, 180 | ifbieq1d 3547 |
. . . . . . . 8
|
182 | 125 | adantlr 474 |
. . . . . . . . . 10
|
183 | | zexpcl 10484 |
. . . . . . . . . 10
|
184 | 182, 165,
183 | syl2anc 409 |
. . . . . . . . 9
|
185 | 184, 168,
151 | ifcldadc 3554 |
. . . . . . . 8
|
186 | 108, 181,
149, 185 | fvmptd3 5587 |
. . . . . . 7
|
187 | 178, 186 | oveq12d 5869 |
. . . . . 6
|
188 | 154, 170,
187 | 3eqtr4d 2213 |
. . . . 5
|
189 | 95, 106, 113, 188 | prod3fmul 11497 |
. . . 4
|
190 | 90, 189 | oveq12d 5869 |
. . 3
|
191 | 37 | adantr 274 |
. . . 4
|
192 | 155 | lgsval4 13680 |
. . . 4
|
193 | 191, 97, 98, 192 | syl3anc 1233 |
. . 3
|
194 | 99 | lgsval4 13680 |
. . . . . 6
|
195 | 96, 97, 98, 194 | syl3anc 1233 |
. . . . 5
|
196 | 108 | lgsval4 13680 |
. . . . . 6
|
197 | 107, 97, 98, 196 | syl3anc 1233 |
. . . . 5
|
198 | 195, 197 | oveq12d 5869 |
. . . 4
|
199 | | neg1cn 8976 |
. . . . . . 7
|
200 | 199 | a1i 9 |
. . . . . 6
|
201 | | 1cnd 7929 |
. . . . . 6
|
202 | | 0z 9216 |
. . . . . . . 8
|
203 | | zdclt 9282 |
. . . . . . . 8
DECID |
204 | 97, 202, 203 | sylancl 411 |
. . . . . . 7
DECID |
205 | | zdclt 9282 |
. . . . . . . 8
DECID |
206 | 96, 202, 205 | sylancl 411 |
. . . . . . 7
DECID |
207 | | dcan2 929 |
. . . . . . 7
DECID
DECID
DECID
|
208 | 204, 206,
207 | sylc 62 |
. . . . . 6
DECID |
209 | 200, 201,
208 | ifcldcd 3560 |
. . . . 5
|
210 | | 1zzd 9232 |
. . . . . . . 8
|
211 | 101 | ffvelrnda 5629 |
. . . . . . . 8
|
212 | | zmulcl 9258 |
. . . . . . . . 9
|
213 | 212 | adantl 275 |
. . . . . . . 8
|
214 | 94, 210, 211, 213 | seqf 10410 |
. . . . . . 7
|
215 | 214, 93 | ffvelrnd 5630 |
. . . . . 6
|
216 | 215 | zcnd 9328 |
. . . . 5
|
217 | | neg1z 9237 |
. . . . . . . 8
|
218 | 217 | a1i 9 |
. . . . . . 7
|
219 | | zdclt 9282 |
. . . . . . . . 9
DECID |
220 | 107, 202,
219 | sylancl 411 |
. . . . . . . 8
DECID |
221 | | dcan2 929 |
. . . . . . . 8
DECID
DECID
DECID
|
222 | 204, 220,
221 | sylc 62 |
. . . . . . 7
DECID |
223 | 218, 210,
222 | ifcldcd 3560 |
. . . . . 6
|
224 | 223 | zcnd 9328 |
. . . . 5
|
225 | 110 | ffvelrnda 5629 |
. . . . . . . 8
|
226 | 94, 210, 225, 213 | seqf 10410 |
. . . . . . 7
|
227 | 226, 93 | ffvelrnd 5630 |
. . . . . 6
|
228 | 227 | zcnd 9328 |
. . . . 5
|
229 | 209, 216,
224, 228 | mul4d 8067 |
. . . 4
|
230 | 198, 229 | eqtrd 2203 |
. . 3
|
231 | 190, 193,
230 | 3eqtr4d 2213 |
. 2
|
232 | | zdceq 9280 |
. . . 4
DECID |
233 | 91, 202, 232 | sylancl 411 |
. . 3
DECID
|
234 | | dcne 2351 |
. . 3
DECID |
235 | 233, 234 | sylib 121 |
. 2
|
236 | 88, 231, 235 | mpjaodan 793 |
1
|