Step | Hyp | Ref
| Expression |
1 | | zmulcl 8404 |
. . . 4
|
2 | 1 | 3adant2 957 |
. . 3
|
3 | | zmulcl 8404 |
. . . 4
|
4 | 3 | 3adant1 956 |
. . 3
|
5 | | simpl 107 |
. . 3
|
6 | | congr 10482 |
. . 3
|
7 | 2, 4, 5, 6 | syl2an3an 1229 |
. 2
|
8 | | simpl 107 |
. . . . . . . . . . . 12
|
9 | | nnz 8370 |
. . . . . . . . . . . . . 14
|
10 | | nnne0 8067 |
. . . . . . . . . . . . . 14
|
11 | 9, 10 | jca 300 |
. . . . . . . . . . . . 13
|
12 | 11 | adantl 271 |
. . . . . . . . . . . 12
|
13 | | eqidd 2082 |
. . . . . . . . . . . 12
|
14 | 8, 12, 13 | 3jca 1118 |
. . . . . . . . . . 11
|
15 | 14 | ex 113 |
. . . . . . . . . 10
|
16 | 15 | 3ad2ant3 961 |
. . . . . . . . 9
|
17 | 16 | com12 30 |
. . . . . . . 8
|
18 | 17 | adantr 270 |
. . . . . . 7
|
19 | 18 | impcom 123 |
. . . . . 6
|
20 | | divgcdcoprmex 10484 |
. . . . . 6
|
21 | 19, 20 | syl 14 |
. . . . 5
|
22 | 21 | adantr 270 |
. . . 4
|
23 | | oveq2 5540 |
. . . . . . . . . 10
|
24 | 23 | 3ad2ant2 960 |
. . . . . . . . 9
|
25 | 24 | adantl 271 |
. . . . . . . 8
|
26 | | oveq2 5540 |
. . . . . . . . . . 11
|
27 | | oveq2 5540 |
. . . . . . . . . . 11
|
28 | 26, 27 | oveq12d 5550 |
. . . . . . . . . 10
|
29 | 28 | 3ad2ant1 959 |
. . . . . . . . 9
|
30 | 29 | adantl 271 |
. . . . . . . 8
|
31 | 25, 30 | eqeq12d 2095 |
. . . . . . 7
|
32 | | simpr 108 |
. . . . . . . . . . . . . 14
|
33 | 32 | zcnd 8470 |
. . . . . . . . . . . . 13
|
34 | 33 | adantr 270 |
. . . . . . . . . . . 12
|
35 | | simp3 940 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | adantr 270 |
. . . . . . . . . . . . . . 15
|
37 | 9 | ad2antrl 473 |
. . . . . . . . . . . . . . 15
|
38 | 36, 37 | gcdcld 10360 |
. . . . . . . . . . . . . 14
|
39 | 38 | nn0cnd 8343 |
. . . . . . . . . . . . 13
|
40 | 39 | ad2antrr 471 |
. . . . . . . . . . . 12
|
41 | | simpr 108 |
. . . . . . . . . . . . . 14
|
42 | 41 | zcnd 8470 |
. . . . . . . . . . . . 13
|
43 | 42 | adantl 271 |
. . . . . . . . . . . 12
|
44 | 34, 40, 43 | mul12d 7260 |
. . . . . . . . . . 11
|
45 | | simp1 938 |
. . . . . . . . . . . . . . 15
|
46 | 45 | zcnd 8470 |
. . . . . . . . . . . . . 14
|
47 | 46 | ad3antrrr 475 |
. . . . . . . . . . . . 13
|
48 | 35 | ad2antrr 471 |
. . . . . . . . . . . . . . . 16
|
49 | 5 | nnzd 8468 |
. . . . . . . . . . . . . . . . . 18
|
50 | 49 | adantl 271 |
. . . . . . . . . . . . . . . . 17
|
51 | 50 | adantr 270 |
. . . . . . . . . . . . . . . 16
|
52 | 48, 51 | gcdcld 10360 |
. . . . . . . . . . . . . . 15
|
53 | 52 | nn0cnd 8343 |
. . . . . . . . . . . . . 14
|
54 | 53 | adantr 270 |
. . . . . . . . . . . . 13
|
55 | | simpl 107 |
. . . . . . . . . . . . . . 15
|
56 | 55 | zcnd 8470 |
. . . . . . . . . . . . . 14
|
57 | 56 | adantl 271 |
. . . . . . . . . . . . 13
|
58 | 47, 54, 57 | mul12d 7260 |
. . . . . . . . . . . 12
|
59 | | simp2 939 |
. . . . . . . . . . . . . . 15
|
60 | 59 | zcnd 8470 |
. . . . . . . . . . . . . 14
|
61 | 60 | ad3antrrr 475 |
. . . . . . . . . . . . 13
|
62 | 36, 50 | gcdcld 10360 |
. . . . . . . . . . . . . . 15
|
63 | 62 | nn0cnd 8343 |
. . . . . . . . . . . . . 14
|
64 | 63 | ad2antrr 471 |
. . . . . . . . . . . . 13
|
65 | 61, 64, 57 | mul12d 7260 |
. . . . . . . . . . . 12
|
66 | 58, 65 | oveq12d 5550 |
. . . . . . . . . . 11
|
67 | 44, 66 | eqeq12d 2095 |
. . . . . . . . . 10
|
68 | 45 | ad3antrrr 475 |
. . . . . . . . . . . . . . 15
|
69 | 55 | adantl 271 |
. . . . . . . . . . . . . . 15
|
70 | 68, 69 | zmulcld 8475 |
. . . . . . . . . . . . . 14
|
71 | 70 | zcnd 8470 |
. . . . . . . . . . . . 13
|
72 | 59 | ad3antrrr 475 |
. . . . . . . . . . . . . . 15
|
73 | 72, 69 | zmulcld 8475 |
. . . . . . . . . . . . . 14
|
74 | 73 | zcnd 8470 |
. . . . . . . . . . . . 13
|
75 | 64, 71, 74 | subdid 7518 |
. . . . . . . . . . . 12
|
76 | 75 | eqcomd 2086 |
. . . . . . . . . . 11
|
77 | 76 | eqeq2d 2092 |
. . . . . . . . . 10
|
78 | 32 | adantr 270 |
. . . . . . . . . . . . 13
|
79 | | simprr 498 |
. . . . . . . . . . . . 13
|
80 | 78, 79 | zmulcld 8475 |
. . . . . . . . . . . 12
|
81 | 80 | zcnd 8470 |
. . . . . . . . . . 11
|
82 | | zmulcl 8404 |
. . . . . . . . . . . . . . . . . 18
|
83 | 82 | ad2ant2r 492 |
. . . . . . . . . . . . . . . . 17
|
84 | | zmulcl 8404 |
. . . . . . . . . . . . . . . . . 18
|
85 | 84 | ad2ant2lr 493 |
. . . . . . . . . . . . . . . . 17
|
86 | 83, 85 | zsubcld 8474 |
. . . . . . . . . . . . . . . 16
|
87 | 86 | zcnd 8470 |
. . . . . . . . . . . . . . 15
|
88 | 87 | ex 113 |
. . . . . . . . . . . . . 14
|
89 | 88 | 3adant3 958 |
. . . . . . . . . . . . 13
|
90 | 89 | ad2antrr 471 |
. . . . . . . . . . . 12
|
91 | 90 | imp 122 |
. . . . . . . . . . 11
|
92 | 10 | ad2antrl 473 |
. . . . . . . . . . . . . . 15
|
93 | | gcd2n0cl 10361 |
. . . . . . . . . . . . . . 15
|
94 | 36, 50, 92, 93 | syl3anc 1169 |
. . . . . . . . . . . . . 14
|
95 | 94 | nnne0d 8083 |
. . . . . . . . . . . . 13
|
96 | 95 | ad2antrr 471 |
. . . . . . . . . . . 12
|
97 | 52 | adantr 270 |
. . . . . . . . . . . . . 14
|
98 | 97 | nn0zd 8467 |
. . . . . . . . . . . . 13
|
99 | | 0zd 8363 |
. . . . . . . . . . . . 13
|
100 | | zapne 8422 |
. . . . . . . . . . . . 13
#
|
101 | 98, 99, 100 | syl2anc 403 |
. . . . . . . . . . . 12
#
|
102 | 96, 101 | mpbird 165 |
. . . . . . . . . . 11
# |
103 | 81, 91, 64, 102 | mulcanapd 7751 |
. . . . . . . . . 10
|
104 | 67, 77, 103 | 3bitrd 212 |
. . . . . . . . 9
|
105 | 104 | adantr 270 |
. . . . . . . 8
|
106 | | zcn 8356 |
. . . . . . . . . . . . . . . . . 18
|
107 | | zcn 8356 |
. . . . . . . . . . . . . . . . . 18
|
108 | 106, 107 | anim12i 331 |
. . . . . . . . . . . . . . . . 17
|
109 | 108 | 3adant3 958 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | ad2antrr 471 |
. . . . . . . . . . . . . . 15
|
111 | 110, 56 | anim12i 331 |
. . . . . . . . . . . . . 14
|
112 | | df-3an 921 |
. . . . . . . . . . . . . 14
|
113 | 111, 112 | sylibr 132 |
. . . . . . . . . . . . 13
|
114 | | subdir 7490 |
. . . . . . . . . . . . 13
|
115 | 113, 114 | syl 14 |
. . . . . . . . . . . 12
|
116 | 115 | eqcomd 2086 |
. . . . . . . . . . 11
|
117 | 116 | adantr 270 |
. . . . . . . . . 10
|
118 | 117 | eqeq2d 2092 |
. . . . . . . . 9
|
119 | 5 | nncnd 8053 |
. . . . . . . . . . . . . . . . 17
|
120 | 119 | adantl 271 |
. . . . . . . . . . . . . . . 16
|
121 | 120 | ad2antrr 471 |
. . . . . . . . . . . . . . 15
|
122 | 79 | zcnd 8470 |
. . . . . . . . . . . . . . 15
|
123 | 121, 122,
40, 102 | divmulap2d 7910 |
. . . . . . . . . . . . . 14
|
124 | | simpll 495 |
. . . . . . . . . . . . . . . . 17
|
125 | 69 | adantr 270 |
. . . . . . . . . . . . . . . . . 18
|
126 | 5 | adantl 271 |
. . . . . . . . . . . . . . . . . . . . 21
|
127 | | divgcdnnr 10367 |
. . . . . . . . . . . . . . . . . . . . 21
|
128 | 126, 36, 127 | syl2anc 403 |
. . . . . . . . . . . . . . . . . . . 20
|
129 | 128 | ad3antrrr 475 |
. . . . . . . . . . . . . . . . . . 19
|
130 | | eleq1 2141 |
. . . . . . . . . . . . . . . . . . . . 21
|
131 | 130 | eqcoms 2084 |
. . . . . . . . . . . . . . . . . . . 20
|
132 | 131 | adantl 271 |
. . . . . . . . . . . . . . . . . . 19
|
133 | 129, 132 | mpbird 165 |
. . . . . . . . . . . . . . . . . 18
|
134 | 125, 133 | jca 300 |
. . . . . . . . . . . . . . . . 17
|
135 | 124, 134 | jca 300 |
. . . . . . . . . . . . . . . 16
|
136 | | simpr 108 |
. . . . . . . . . . . . . . . 16
|
137 | | nnz 8370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
138 | 137 | adantl 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
139 | 138 | anim2i 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
140 | 139 | adantl 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
141 | | dvdsmul2 10218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
142 | 140, 141 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
143 | | breq2 3789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
144 | | zsubcl 8392 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
145 | 144 | zcnd 8470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
146 | 145 | adantr 270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
147 | | zcn 8356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
148 | 147 | ad2antrl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
149 | 148 | adantl 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
150 | 146, 149 | mulcomd 7140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
151 | 150 | breq2d 3797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
152 | 137 | anim2i 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
153 | | gcdcom 10365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
154 | 152, 153 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
155 | 154 | eqeq1d 2089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
156 | 155 | ad2antll 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
157 | 152 | adantl 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
158 | 157 | ancomd 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
159 | 144, 158 | anim12i 331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
160 | 159 | ancomd 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
161 | | df-3an 921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
162 | 160, 161 | sylibr 132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
163 | | coprmdvds 10474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
164 | 162, 163 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
165 | | simprr 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
166 | 165 | anim2i 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
167 | 166 | ancomd 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
168 | | 3anass 923 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
169 | 167, 168 | sylibr 132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
170 | | moddvds 10204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
171 | 169, 170 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
172 | 164, 171 | sylibrd 167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
173 | 172 | expcomd 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
174 | 156, 173 | sylbid 148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
175 | 174 | com23 77 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
176 | 151, 175 | sylbid 148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
177 | 176 | com3l 80 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
178 | 143, 177 | syl6bi 161 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
179 | 178 | com14 87 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
180 | 142, 179 | mpd 13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
181 | 180 | ex 113 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
182 | 181 | 3adant3 958 |
. . . . . . . . . . . . . . . . . . . . . 22
|
183 | 182 | adantr 270 |
. . . . . . . . . . . . . . . . . . . . 21
|
184 | 183 | impl 372 |
. . . . . . . . . . . . . . . . . . . 20
|
185 | 184 | adantr 270 |
. . . . . . . . . . . . . . . . . . 19
|
186 | 185 | imp 122 |
. . . . . . . . . . . . . . . . . 18
|
187 | | eqtr2 2099 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
188 | | oveq2 5540 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
189 | | oveq2 5540 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
190 | 188, 189 | eqeq12d 2095 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
191 | 187, 190 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
192 | 191 | ex 113 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
193 | 192 | eqcoms 2084 |
. . . . . . . . . . . . . . . . . . . . . 22
|
194 | 193 | ad2antll 474 |
. . . . . . . . . . . . . . . . . . . . 21
|
195 | 194 | ad2antrr 471 |
. . . . . . . . . . . . . . . . . . . 20
|
196 | 195 | imp 122 |
. . . . . . . . . . . . . . . . . . 19
|
197 | 196 | adantr 270 |
. . . . . . . . . . . . . . . . . 18
|
198 | 186, 197 | sylibrd 167 |
. . . . . . . . . . . . . . . . 17
|
199 | 198 | ex 113 |
. . . . . . . . . . . . . . . 16
|
200 | 135, 136,
199 | syl2anc 403 |
. . . . . . . . . . . . . . 15
|
201 | 200 | ex 113 |
. . . . . . . . . . . . . 14
|
202 | 123, 201 | sylbird 168 |
. . . . . . . . . . . . 13
|
203 | 202 | com3l 80 |
. . . . . . . . . . . 12
|
204 | 203 | a1i 9 |
. . . . . . . . . . 11
|
205 | 204 | 3imp 1132 |
. . . . . . . . . 10
|
206 | 205 | impcom 123 |
. . . . . . . . 9
|
207 | 118, 206 | sylbid 148 |
. . . . . . . 8
|
208 | 105, 207 | sylbid 148 |
. . . . . . 7
|
209 | 31, 208 | sylbid 148 |
. . . . . 6
|
210 | 209 | ex 113 |
. . . . 5
|
211 | 210 | rexlimdvva 2484 |
. . . 4
|
212 | 22, 211 | mpd 13 |
. . 3
|
213 | 212 | rexlimdva 2477 |
. 2
|
214 | 7, 213 | sylbid 148 |
1
|