Step | Hyp | Ref
| Expression |
1 | | phimul.4 |
. . . . 5
..^ |
2 | | fzofi 12773 |
. . . . . 6
..^ |
3 | | ssrab2 3687 |
. . . . . 6
..^ ..^ |
4 | | ssfi 8180 |
. . . . . 6
..^ ..^ ..^ ..^ |
5 | 2, 3, 4 | mp2an 708 |
. . . . 5
..^ |
6 | 1, 5 | eqeltri 2697 |
. . . 4
|
7 | | phimul.5 |
. . . . 5
..^ |
8 | | fzofi 12773 |
. . . . . 6
..^ |
9 | | ssrab2 3687 |
. . . . . 6
..^ ..^ |
10 | | ssfi 8180 |
. . . . . 6
..^ ..^ ..^ ..^ |
11 | 8, 9, 10 | mp2an 708 |
. . . . 5
..^ |
12 | 7, 11 | eqeltri 2697 |
. . . 4
|
13 | | hashxp 13221 |
. . . 4
|
14 | 6, 12, 13 | mp2an 708 |
. . 3
|
15 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
16 | 15 | eqeq1d 2624 |
. . . . . . . . . . . . 13
|
17 | | phimul.6 |
. . . . . . . . . . . . 13
|
18 | 16, 17 | elrab2 3366 |
. . . . . . . . . . . 12
|
19 | 18 | simplbi 476 |
. . . . . . . . . . 11
|
20 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
21 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
22 | 20, 21 | opeq12d 4410 |
. . . . . . . . . . . 12
|
23 | | crth.3 |
. . . . . . . . . . . 12
|
24 | | opex 4932 |
. . . . . . . . . . . 12
|
25 | 22, 23, 24 | fvmpt 6282 |
. . . . . . . . . . 11
|
26 | 19, 25 | syl 17 |
. . . . . . . . . 10
|
27 | 26 | adantl 482 |
. . . . . . . . 9
|
28 | | crth.1 |
. . . . . . . . . . . . . . 15
..^ |
29 | 19, 28 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
..^ |
30 | 29 | adantl 482 |
. . . . . . . . . . . . 13
..^ |
31 | | elfzoelz 12470 |
. . . . . . . . . . . . 13
..^
|
32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
|
33 | | crth.4 |
. . . . . . . . . . . . . 14
|
34 | 33 | simp1d 1073 |
. . . . . . . . . . . . 13
|
35 | 34 | adantr 481 |
. . . . . . . . . . . 12
|
36 | | zmodfzo 12693 |
. . . . . . . . . . . 12
..^ |
37 | 32, 35, 36 | syl2anc 693 |
. . . . . . . . . . 11
..^ |
38 | | modgcd 15253 |
. . . . . . . . . . . . 13
|
39 | 32, 35, 38 | syl2anc 693 |
. . . . . . . . . . . 12
|
40 | 35 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
41 | | gcddvds 15225 |
. . . . . . . . . . . . . . . . 17
|
42 | 32, 40, 41 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
43 | 42 | simpld 475 |
. . . . . . . . . . . . . . 15
|
44 | 42 | simprd 479 |
. . . . . . . . . . . . . . . 16
|
45 | 33 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . 19
|
46 | 45 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
47 | 46 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
48 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . . . 17
|
49 | 40, 47, 48 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
50 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
52 | 51 | necon3ai 2819 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | 35, 50, 52 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
|
54 | | gcdn0cl 15224 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 32, 40, 53, 54 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
57 | 35, 46 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . . 18
|
58 | 57 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
59 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . 17
|
60 | 56, 40, 58, 59 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
61 | 44, 49, 60 | mp2and 715 |
. . . . . . . . . . . . . . 15
|
62 | | nnne0 11053 |
. . . . . . . . . . . . . . . . 17
|
63 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
64 | 63 | necon3ai 2819 |
. . . . . . . . . . . . . . . . 17
|
65 | 57, 62, 64 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
66 | | dvdslegcd 15226 |
. . . . . . . . . . . . . . . 16
|
67 | 56, 32, 58, 65, 66 | syl31anc 1329 |
. . . . . . . . . . . . . . 15
|
68 | 43, 61, 67 | mp2and 715 |
. . . . . . . . . . . . . 14
|
69 | 18 | simprbi 480 |
. . . . . . . . . . . . . . 15
|
70 | 69 | adantl 482 |
. . . . . . . . . . . . . 14
|
71 | 68, 70 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
72 | | nnle1eq1 11048 |
. . . . . . . . . . . . . 14
|
73 | 55, 72 | syl 17 |
. . . . . . . . . . . . 13
|
74 | 71, 73 | mpbid 222 |
. . . . . . . . . . . 12
|
75 | 39, 74 | eqtrd 2656 |
. . . . . . . . . . 11
|
76 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
77 | 76 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
78 | 77, 1 | elrab2 3366 |
. . . . . . . . . . 11
..^ |
79 | 37, 75, 78 | sylanbrc 698 |
. . . . . . . . . 10
|
80 | | zmodfzo 12693 |
. . . . . . . . . . . 12
..^ |
81 | 32, 46, 80 | syl2anc 693 |
. . . . . . . . . . 11
..^ |
82 | | modgcd 15253 |
. . . . . . . . . . . . 13
|
83 | 32, 46, 82 | syl2anc 693 |
. . . . . . . . . . . 12
|
84 | | gcddvds 15225 |
. . . . . . . . . . . . . . . . 17
|
85 | 32, 47, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
86 | 85 | simpld 475 |
. . . . . . . . . . . . . . 15
|
87 | 85 | simprd 479 |
. . . . . . . . . . . . . . . 16
|
88 | | dvdsmul2 15004 |
. . . . . . . . . . . . . . . . 17
|
89 | 40, 47, 88 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
90 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . 20
|
91 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | 91 | necon3ai 2819 |
. . . . . . . . . . . . . . . . . . . 20
|
93 | 46, 90, 92 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
|
94 | | gcdn0cl 15224 |
. . . . . . . . . . . . . . . . . . 19
|
95 | 32, 47, 93, 94 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . 18
|
96 | 95 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
97 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . 17
|
98 | 96, 47, 58, 97 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
99 | 87, 89, 98 | mp2and 715 |
. . . . . . . . . . . . . . 15
|
100 | | dvdslegcd 15226 |
. . . . . . . . . . . . . . . 16
|
101 | 96, 32, 58, 65, 100 | syl31anc 1329 |
. . . . . . . . . . . . . . 15
|
102 | 86, 99, 101 | mp2and 715 |
. . . . . . . . . . . . . 14
|
103 | 102, 70 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
104 | | nnle1eq1 11048 |
. . . . . . . . . . . . . 14
|
105 | 95, 104 | syl 17 |
. . . . . . . . . . . . 13
|
106 | 103, 105 | mpbid 222 |
. . . . . . . . . . . 12
|
107 | 83, 106 | eqtrd 2656 |
. . . . . . . . . . 11
|
108 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
109 | 108 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
110 | 109, 7 | elrab2 3366 |
. . . . . . . . . . 11
..^ |
111 | 81, 107, 110 | sylanbrc 698 |
. . . . . . . . . 10
|
112 | | opelxpi 5148 |
. . . . . . . . . 10
|
113 | 79, 111, 112 | syl2anc 693 |
. . . . . . . . 9
|
114 | 27, 113 | eqeltrd 2701 |
. . . . . . . 8
|
115 | 114 | ralrimiva 2966 |
. . . . . . 7
|
116 | | crth.2 |
. . . . . . . . . 10
..^ ..^ |
117 | 28, 116, 23, 33 | crth 15483 |
. . . . . . . . 9
|
118 | | f1ofn 6138 |
. . . . . . . . 9
|
119 | | fnfun 5988 |
. . . . . . . . 9
|
120 | 117, 118,
119 | 3syl 18 |
. . . . . . . 8
|
121 | | ssrab2 3687 |
. . . . . . . . . 10
|
122 | 17, 121 | eqsstri 3635 |
. . . . . . . . 9
|
123 | | fndm 5990 |
. . . . . . . . . 10
|
124 | 117, 118,
123 | 3syl 18 |
. . . . . . . . 9
|
125 | 122, 124 | syl5sseqr 3654 |
. . . . . . . 8
|
126 | | funimass4 6247 |
. . . . . . . 8
|
127 | 120, 125,
126 | syl2anc 693 |
. . . . . . 7
|
128 | 115, 127 | mpbird 247 |
. . . . . 6
|
129 | 1, 3 | eqsstri 3635 |
. . . . . . . . . . . . 13
..^ |
130 | 7, 9 | eqsstri 3635 |
. . . . . . . . . . . . 13
..^ |
131 | | xpss12 5225 |
. . . . . . . . . . . . 13
..^ ..^
..^ ..^ |
132 | 129, 130,
131 | mp2an 708 |
. . . . . . . . . . . 12
..^ ..^ |
133 | 132, 116 | sseqtr4i 3638 |
. . . . . . . . . . 11
|
134 | 133 | sseli 3599 |
. . . . . . . . . 10
|
135 | | f1ocnvfv2 6533 |
. . . . . . . . . 10
|
136 | 117, 134,
135 | syl2an 494 |
. . . . . . . . 9
|
137 | | f1ocnv 6149 |
. . . . . . . . . . . . 13
|
138 | | f1of 6137 |
. . . . . . . . . . . . 13
|
139 | 117, 137,
138 | 3syl 18 |
. . . . . . . . . . . 12
|
140 | | ffvelrn 6357 |
. . . . . . . . . . . 12
|
141 | 139, 134,
140 | syl2an 494 |
. . . . . . . . . . 11
|
142 | 141, 28 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
..^ |
143 | | elfzoelz 12470 |
. . . . . . . . . . . . . . 15
..^
|
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . 14
|
145 | 34 | adantr 481 |
. . . . . . . . . . . . . 14
|
146 | | modgcd 15253 |
. . . . . . . . . . . . . 14
|
147 | 144, 145,
146 | syl2anc 693 |
. . . . . . . . . . . . 13
|
148 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
149 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
150 | 148, 149 | opeq12d 4410 |
. . . . . . . . . . . . . . . . . . . . 21
|
151 | 22 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . . . . . 22
|
152 | 23, 151 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . 21
|
153 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . 21
|
154 | 150, 152,
153 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . 20
|
155 | 141, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
156 | 136, 155 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . 18
|
157 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
158 | 156, 157 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
|
159 | | opelxp 5146 |
. . . . . . . . . . . . . . . . 17
|
160 | 158, 159 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
161 | 160 | simpld 475 |
. . . . . . . . . . . . . . 15
|
162 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
163 | 162 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
|
164 | 163, 1 | elrab2 3366 |
. . . . . . . . . . . . . . 15
..^
|
165 | 161, 164 | sylib 208 |
. . . . . . . . . . . . . 14
..^
|
166 | 165 | simprd 479 |
. . . . . . . . . . . . 13
|
167 | 147, 166 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
168 | 45 | adantr 481 |
. . . . . . . . . . . . . 14
|
169 | | modgcd 15253 |
. . . . . . . . . . . . . 14
|
170 | 144, 168,
169 | syl2anc 693 |
. . . . . . . . . . . . 13
|
171 | 160 | simprd 479 |
. . . . . . . . . . . . . . 15
|
172 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
173 | 172 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
|
174 | 173, 7 | elrab2 3366 |
. . . . . . . . . . . . . . 15
..^
|
175 | 171, 174 | sylib 208 |
. . . . . . . . . . . . . 14
..^
|
176 | 175 | simprd 479 |
. . . . . . . . . . . . 13
|
177 | 170, 176 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
178 | 34 | nnzd 11481 |
. . . . . . . . . . . . . 14
|
179 | 178 | adantr 481 |
. . . . . . . . . . . . 13
|
180 | 45 | nnzd 11481 |
. . . . . . . . . . . . . 14
|
181 | 180 | adantr 481 |
. . . . . . . . . . . . 13
|
182 | | rpmul 15373 |
. . . . . . . . . . . . 13
|
183 | 144, 179,
181, 182 | syl3anc 1326 |
. . . . . . . . . . . 12
|
184 | 167, 177,
183 | mp2and 715 |
. . . . . . . . . . 11
|
185 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
186 | 185 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
187 | 186, 17 | elrab2 3366 |
. . . . . . . . . . 11
|
188 | 141, 184,
187 | sylanbrc 698 |
. . . . . . . . . 10
|
189 | | funfvima2 6493 |
. . . . . . . . . . . 12
|
190 | 120, 125,
189 | syl2anc 693 |
. . . . . . . . . . 11
|
191 | 190 | imp 445 |
. . . . . . . . . 10
|
192 | 188, 191 | syldan 487 |
. . . . . . . . 9
|
193 | 136, 192 | eqeltrrd 2702 |
. . . . . . . 8
|
194 | 193 | ex 450 |
. . . . . . 7
|
195 | 194 | ssrdv 3609 |
. . . . . 6
|
196 | 128, 195 | eqssd 3620 |
. . . . 5
|
197 | | f1of1 6136 |
. . . . . . 7
|
198 | 117, 197 | syl 17 |
. . . . . 6
|
199 | | fzofi 12773 |
. . . . . . . . . 10
..^ |
200 | 28, 199 | eqeltri 2697 |
. . . . . . . . 9
|
201 | | ssfi 8180 |
. . . . . . . . 9
|
202 | 200, 122,
201 | mp2an 708 |
. . . . . . . 8
|
203 | 202 | elexi 3213 |
. . . . . . 7
|
204 | 203 | f1imaen 8018 |
. . . . . 6
|
205 | 198, 122,
204 | sylancl 694 |
. . . . 5
|
206 | 196, 205 | eqbrtrrd 4677 |
. . . 4
|
207 | | xpfi 8231 |
. . . . . 6
|
208 | 6, 12, 207 | mp2an 708 |
. . . . 5
|
209 | | hashen 13135 |
. . . . 5
|
210 | 208, 202,
209 | mp2an 708 |
. . . 4
|
211 | 206, 210 | sylibr 224 |
. . 3
|
212 | 14, 211 | syl5reqr 2671 |
. 2
|
213 | 34, 45 | nnmulcld 11068 |
. . 3
|
214 | | dfphi2 15479 |
. . . 4
..^ |
215 | | rabeq 3192 |
. . . . . . 7
..^
..^ |
216 | 28, 215 | ax-mp 5 |
. . . . . 6
..^
|
217 | 17, 216 | eqtri 2644 |
. . . . 5
..^
|
218 | 217 | fveq2i 6194 |
. . . 4
..^ |
219 | 214, 218 | syl6eqr 2674 |
. . 3
|
220 | 213, 219 | syl 17 |
. 2
|
221 | | dfphi2 15479 |
. . . . 5
..^ |
222 | 1 | fveq2i 6194 |
. . . . 5
..^ |
223 | 221, 222 | syl6eqr 2674 |
. . . 4
|
224 | 34, 223 | syl 17 |
. . 3
|
225 | | dfphi2 15479 |
. . . . 5
..^ |
226 | 7 | fveq2i 6194 |
. . . . 5
..^ |
227 | 225, 226 | syl6eqr 2674 |
. . . 4
|
228 | 45, 227 | syl 17 |
. . 3
|
229 | 224, 228 | oveq12d 6668 |
. 2
|
230 | 212, 220,
229 | 3eqtr4d 2666 |
1
|