Step | Hyp | Ref
| Expression |
1 | | oveq1 5858 |
. . . . . 6
|
2 | 1 | breq2d 3999 |
. . . . 5
|
3 | | oveq1 5858 |
. . . . . . 7
|
4 | 3 | breq2d 3999 |
. . . . . 6
|
5 | 4 | notbid 662 |
. . . . 5
|
6 | 2, 5 | anbi12d 470 |
. . . 4
|
7 | 6 | imbi1d 230 |
. . 3
|
8 | | oveq2 5859 |
. . . . . . . . . . . . 13
|
9 | 8 | oveq2d 5867 |
. . . . . . . . . . . 12
|
10 | 9 | breq2d 3999 |
. . . . . . . . . . 11
|
11 | | oveq1 5858 |
. . . . . . . . . . . . . . 15
|
12 | 11 | oveq2d 5867 |
. . . . . . . . . . . . . 14
|
13 | 12 | oveq2d 5867 |
. . . . . . . . . . . . 13
|
14 | 13 | breq2d 3999 |
. . . . . . . . . . . 12
|
15 | 14 | notbid 662 |
. . . . . . . . . . 11
|
16 | 10, 15 | anbi12d 470 |
. . . . . . . . . 10
|
17 | 8 | breq1d 3997 |
. . . . . . . . . 10
|
18 | 16, 17 | imbi12d 233 |
. . . . . . . . 9
|
19 | 18 | ralbidv 2470 |
. . . . . . . 8
|
20 | 19 | imbi2d 229 |
. . . . . . 7
|
21 | | oveq2 5859 |
. . . . . . . . . . . . 13
|
22 | 21 | oveq2d 5867 |
. . . . . . . . . . . 12
|
23 | 22 | breq2d 3999 |
. . . . . . . . . . 11
|
24 | | oveq1 5858 |
. . . . . . . . . . . . . . 15
|
25 | 24 | oveq2d 5867 |
. . . . . . . . . . . . . 14
|
26 | 25 | oveq2d 5867 |
. . . . . . . . . . . . 13
|
27 | 26 | breq2d 3999 |
. . . . . . . . . . . 12
|
28 | 27 | notbid 662 |
. . . . . . . . . . 11
|
29 | 23, 28 | anbi12d 470 |
. . . . . . . . . 10
|
30 | 21 | breq1d 3997 |
. . . . . . . . . 10
|
31 | 29, 30 | imbi12d 233 |
. . . . . . . . 9
|
32 | 31 | ralbidv 2470 |
. . . . . . . 8
|
33 | 32 | imbi2d 229 |
. . . . . . 7
|
34 | | oveq2 5859 |
. . . . . . . . . . . . 13
|
35 | 34 | oveq2d 5867 |
. . . . . . . . . . . 12
|
36 | 35 | breq2d 3999 |
. . . . . . . . . . 11
|
37 | | oveq1 5858 |
. . . . . . . . . . . . . . 15
|
38 | 37 | oveq2d 5867 |
. . . . . . . . . . . . . 14
|
39 | 38 | oveq2d 5867 |
. . . . . . . . . . . . 13
|
40 | 39 | breq2d 3999 |
. . . . . . . . . . . 12
|
41 | 40 | notbid 662 |
. . . . . . . . . . 11
|
42 | 36, 41 | anbi12d 470 |
. . . . . . . . . 10
|
43 | 34 | breq1d 3997 |
. . . . . . . . . 10
|
44 | 42, 43 | imbi12d 233 |
. . . . . . . . 9
|
45 | 44 | ralbidv 2470 |
. . . . . . . 8
|
46 | 45 | imbi2d 229 |
. . . . . . 7
|
47 | | oveq2 5859 |
. . . . . . . . . . . . 13
|
48 | 47 | oveq2d 5867 |
. . . . . . . . . . . 12
|
49 | 48 | breq2d 3999 |
. . . . . . . . . . 11
|
50 | | oveq1 5858 |
. . . . . . . . . . . . . . 15
|
51 | 50 | oveq2d 5867 |
. . . . . . . . . . . . . 14
|
52 | 51 | oveq2d 5867 |
. . . . . . . . . . . . 13
|
53 | 52 | breq2d 3999 |
. . . . . . . . . . . 12
|
54 | 53 | notbid 662 |
. . . . . . . . . . 11
|
55 | 49, 54 | anbi12d 470 |
. . . . . . . . . 10
|
56 | 47 | breq1d 3997 |
. . . . . . . . . 10
|
57 | 55, 56 | imbi12d 233 |
. . . . . . . . 9
|
58 | 57 | ralbidv 2470 |
. . . . . . . 8
|
59 | 58 | imbi2d 229 |
. . . . . . 7
|
60 | | breq1 3990 |
. . . . . . . . . . . . . 14
|
61 | | breq1 3990 |
. . . . . . . . . . . . . . 15
|
62 | 61 | notbid 662 |
. . . . . . . . . . . . . 14
|
63 | 60, 62 | anbi12d 470 |
. . . . . . . . . . . . 13
|
64 | | breq2 3991 |
. . . . . . . . . . . . 13
|
65 | 63, 64 | imbi12d 233 |
. . . . . . . . . . . 12
|
66 | 65 | imbi2d 229 |
. . . . . . . . . . 11
|
67 | | simplrl 530 |
. . . . . . . . . . . . . . . 16
|
68 | | prmnn 12057 |
. . . . . . . . . . . . . . . 16
|
69 | 67, 68 | syl 14 |
. . . . . . . . . . . . . . 15
|
70 | | simpll 524 |
. . . . . . . . . . . . . . 15
|
71 | | dvdsdc 11753 |
. . . . . . . . . . . . . . 15
DECID |
72 | 69, 70, 71 | syl2anc 409 |
. . . . . . . . . . . . . 14
DECID
|
73 | | coprm 12091 |
. . . . . . . . . . . . . . . 16
|
74 | 67, 70, 73 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
75 | | zcn 9210 |
. . . . . . . . . . . . . . . . . . . . 21
|
76 | 75 | ad2antll 488 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | | prmz 12058 |
. . . . . . . . . . . . . . . . . . . . . 22
|
78 | 77 | ad2antrl 487 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | 78 | zcnd 9328 |
. . . . . . . . . . . . . . . . . . . 20
|
80 | 76, 79 | mulcomd 7934 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 80 | breq2d 3999 |
. . . . . . . . . . . . . . . . . 18
|
82 | | simpl 108 |
. . . . . . . . . . . . . . . . . . . 20
|
83 | 78, 82 | gcdcomd 11922 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 83 | eqeq1d 2179 |
. . . . . . . . . . . . . . . . . 18
|
85 | 81, 84 | anbi12d 470 |
. . . . . . . . . . . . . . . . 17
|
86 | | simprr 527 |
. . . . . . . . . . . . . . . . . 18
|
87 | | coprmdvds 12039 |
. . . . . . . . . . . . . . . . . 18
|
88 | 82, 78, 86, 87 | syl3anc 1233 |
. . . . . . . . . . . . . . . . 17
|
89 | 85, 88 | sylbid 149 |
. . . . . . . . . . . . . . . 16
|
90 | 89 | expdimp 257 |
. . . . . . . . . . . . . . 15
|
91 | 74, 90 | sylbid 149 |
. . . . . . . . . . . . . 14
|
92 | | con1dc 851 |
. . . . . . . . . . . . . 14
DECID |
93 | 72, 91, 92 | sylc 62 |
. . . . . . . . . . . . 13
|
94 | 93 | expimpd 361 |
. . . . . . . . . . . 12
|
95 | 94 | ex 114 |
. . . . . . . . . . 11
|
96 | 66, 95 | vtoclga 2796 |
. . . . . . . . . 10
|
97 | 96 | impl 378 |
. . . . . . . . 9
|
98 | 77 | zcnd 9328 |
. . . . . . . . . . . . . 14
|
99 | 98 | exp1d 10597 |
. . . . . . . . . . . . 13
|
100 | 99 | ad2antlr 486 |
. . . . . . . . . . . 12
|
101 | 100 | oveq2d 5867 |
. . . . . . . . . . 11
|
102 | 101 | breq2d 3999 |
. . . . . . . . . 10
|
103 | | 1m1e0 8940 |
. . . . . . . . . . . . . . . 16
|
104 | 103 | oveq2i 5862 |
. . . . . . . . . . . . . . 15
|
105 | 77 | ad2antlr 486 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | zcnd 9328 |
. . . . . . . . . . . . . . . 16
|
107 | 106 | exp0d 10596 |
. . . . . . . . . . . . . . 15
|
108 | 104, 107 | eqtrid 2215 |
. . . . . . . . . . . . . 14
|
109 | 108 | oveq2d 5867 |
. . . . . . . . . . . . 13
|
110 | 75 | adantl 275 |
. . . . . . . . . . . . . 14
|
111 | 110 | mulid1d 7930 |
. . . . . . . . . . . . 13
|
112 | 109, 111 | eqtrd 2203 |
. . . . . . . . . . . 12
|
113 | 112 | breq2d 3999 |
. . . . . . . . . . 11
|
114 | 113 | notbid 662 |
. . . . . . . . . 10
|
115 | 102, 114 | anbi12d 470 |
. . . . . . . . 9
|
116 | 106 | exp1d 10597 |
. . . . . . . . . 10
|
117 | 116 | breq1d 3997 |
. . . . . . . . 9
|
118 | 97, 115, 117 | 3imtr4d 202 |
. . . . . . . 8
|
119 | 118 | ralrimiva 2543 |
. . . . . . 7
|
120 | | oveq1 5858 |
. . . . . . . . . . . . . 14
|
121 | 120 | breq2d 3999 |
. . . . . . . . . . . . 13
|
122 | | oveq1 5858 |
. . . . . . . . . . . . . . 15
|
123 | 122 | breq2d 3999 |
. . . . . . . . . . . . . 14
|
124 | 123 | notbid 662 |
. . . . . . . . . . . . 13
|
125 | 121, 124 | anbi12d 470 |
. . . . . . . . . . . 12
|
126 | 125 | imbi1d 230 |
. . . . . . . . . . 11
|
127 | 126 | cbvralvw 2700 |
. . . . . . . . . 10
|
128 | | simprr 527 |
. . . . . . . . . . . . . . 15
|
129 | 77 | ad2antrl 487 |
. . . . . . . . . . . . . . 15
|
130 | 128, 129 | zmulcld 9333 |
. . . . . . . . . . . . . 14
|
131 | | oveq1 5858 |
. . . . . . . . . . . . . . . . . 18
|
132 | 131 | breq2d 3999 |
. . . . . . . . . . . . . . . . 17
|
133 | | oveq1 5858 |
. . . . . . . . . . . . . . . . . . 19
|
134 | 133 | breq2d 3999 |
. . . . . . . . . . . . . . . . . 18
|
135 | 134 | notbid 662 |
. . . . . . . . . . . . . . . . 17
|
136 | 132, 135 | anbi12d 470 |
. . . . . . . . . . . . . . . 16
|
137 | 136 | imbi1d 230 |
. . . . . . . . . . . . . . 15
|
138 | 137 | rspcv 2830 |
. . . . . . . . . . . . . 14
|
139 | 130, 138 | syl 14 |
. . . . . . . . . . . . 13
|
140 | | nnnn0 9135 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | 140 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . 19
|
142 | | zexpcl 10484 |
. . . . . . . . . . . . . . . . . . 19
|
143 | 129, 141,
142 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
|
144 | | simplr 525 |
. . . . . . . . . . . . . . . . . 18
|
145 | | divides 11744 |
. . . . . . . . . . . . . . . . . 18
|
146 | 143, 144,
145 | syl2anc 409 |
. . . . . . . . . . . . . . . . 17
|
147 | 94 | adantll 473 |
. . . . . . . . . . . . . . . . . . . . . 22
|
148 | 68 | ad2antrl 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
149 | 148 | nncnd 8885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
150 | 140 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
151 | 149, 150 | expp1d 10603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
152 | 148, 150 | nnexpcld 10624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
153 | 152 | nncnd 8885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
154 | 153, 149 | mulcomd 7934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
155 | 151, 154 | eqtrd 2203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
156 | 155 | oveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
157 | 75 | ad2antll 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
158 | 157, 149,
153 | mulassd 7936 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
159 | 156, 158 | eqtr4d 2206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
160 | 159 | breq2d 3999 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
161 | | simplr 525 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
162 | | simprr 527 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
163 | 148 | nnzd 9326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
164 | 162, 163 | zmulcld 9333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
165 | 152 | nnzd 9326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
166 | 152 | nnne0d 8916 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
167 | | dvdsmulcr 11776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
168 | 161, 164,
165, 166, 167 | syl112anc 1237 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
169 | 160, 168 | bitrd 187 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
170 | | dvdsmulcr 11776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
171 | 161, 162,
165, 166, 170 | syl112anc 1237 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
172 | 171 | notbid 662 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
173 | 169, 172 | anbi12d 470 |
. . . . . . . . . . . . . . . . . . . . . 22
|
174 | 155 | breq1d 3997 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
175 | | dvdsmulcr 11776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
176 | 163, 161,
165, 166, 175 | syl112anc 1237 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
177 | 174, 176 | bitrd 187 |
. . . . . . . . . . . . . . . . . . . . . 22
|
178 | 147, 173,
177 | 3imtr4d 202 |
. . . . . . . . . . . . . . . . . . . . 21
|
179 | 178 | an32s 563 |
. . . . . . . . . . . . . . . . . . . 20
|
180 | | breq1 3990 |
. . . . . . . . . . . . . . . . . . . . . 22
|
181 | | breq1 3990 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
182 | 181 | notbid 662 |
. . . . . . . . . . . . . . . . . . . . . 22
|
183 | 180, 182 | anbi12d 470 |
. . . . . . . . . . . . . . . . . . . . 21
|
184 | | breq2 3991 |
. . . . . . . . . . . . . . . . . . . . 21
|
185 | 183, 184 | imbi12d 233 |
. . . . . . . . . . . . . . . . . . . 20
|
186 | 179, 185 | syl5ibcom 154 |
. . . . . . . . . . . . . . . . . . 19
|
187 | 186 | rexlimdva 2587 |
. . . . . . . . . . . . . . . . . 18
|
188 | 187 | adantlr 474 |
. . . . . . . . . . . . . . . . 17
|
189 | 146, 188 | sylbid 149 |
. . . . . . . . . . . . . . . 16
|
190 | 189 | com23 78 |
. . . . . . . . . . . . . . 15
|
191 | 190 | a2d 26 |
. . . . . . . . . . . . . 14
|
192 | 75 | ad2antll 488 |
. . . . . . . . . . . . . . . . . . 19
|
193 | 129 | zcnd 9328 |
. . . . . . . . . . . . . . . . . . 19
|
194 | 143 | zcnd 9328 |
. . . . . . . . . . . . . . . . . . 19
|
195 | 192, 193,
194 | mulassd 7936 |
. . . . . . . . . . . . . . . . . 18
|
196 | 193, 194 | mulcomd 7934 |
. . . . . . . . . . . . . . . . . . . 20
|
197 | 193, 141 | expp1d 10603 |
. . . . . . . . . . . . . . . . . . . 20
|
198 | 196, 197 | eqtr4d 2206 |
. . . . . . . . . . . . . . . . . . 19
|
199 | 198 | oveq2d 5867 |
. . . . . . . . . . . . . . . . . 18
|
200 | 195, 199 | eqtrd 2203 |
. . . . . . . . . . . . . . . . 17
|
201 | 200 | breq2d 3999 |
. . . . . . . . . . . . . . . 16
|
202 | | nnm1nn0 9169 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
203 | 202 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
|
204 | | zexpcl 10484 |
. . . . . . . . . . . . . . . . . . . . . 22
|
205 | 129, 203,
204 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . 21
|
206 | 205 | zcnd 9328 |
. . . . . . . . . . . . . . . . . . . 20
|
207 | 192, 193,
206 | mulassd 7936 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 193, 206 | mulcomd 7934 |
. . . . . . . . . . . . . . . . . . . . 21
|
209 | | simpll 524 |
. . . . . . . . . . . . . . . . . . . . . 22
|
210 | | expm1t 10497 |
. . . . . . . . . . . . . . . . . . . . . 22
|
211 | 193, 209,
210 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . 21
|
212 | 208, 211 | eqtr4d 2206 |
. . . . . . . . . . . . . . . . . . . 20
|
213 | 212 | oveq2d 5867 |
. . . . . . . . . . . . . . . . . . 19
|
214 | 207, 213 | eqtrd 2203 |
. . . . . . . . . . . . . . . . . 18
|
215 | 214 | breq2d 3999 |
. . . . . . . . . . . . . . . . 17
|
216 | 215 | notbid 662 |
. . . . . . . . . . . . . . . 16
|
217 | 201, 216 | anbi12d 470 |
. . . . . . . . . . . . . . 15
|
218 | 217 | imbi1d 230 |
. . . . . . . . . . . . . 14
|
219 | | nncn 8879 |
. . . . . . . . . . . . . . . . . . . . . 22
|
220 | 219 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . . . 21
|
221 | | ax-1cn 7860 |
. . . . . . . . . . . . . . . . . . . . 21
|
222 | | pncan 8118 |
. . . . . . . . . . . . . . . . . . . . 21
|
223 | 220, 221,
222 | sylancl 411 |
. . . . . . . . . . . . . . . . . . . 20
|
224 | 223 | oveq2d 5867 |
. . . . . . . . . . . . . . . . . . 19
|
225 | 224 | oveq2d 5867 |
. . . . . . . . . . . . . . . . . 18
|
226 | 225 | breq2d 3999 |
. . . . . . . . . . . . . . . . 17
|
227 | 226 | notbid 662 |
. . . . . . . . . . . . . . . 16
|
228 | 227 | anbi2d 461 |
. . . . . . . . . . . . . . 15
|
229 | 228 | imbi1d 230 |
. . . . . . . . . . . . . 14
|
230 | 191, 218,
229 | 3imtr4d 202 |
. . . . . . . . . . . . 13
|
231 | 139, 230 | syld 45 |
. . . . . . . . . . . 12
|
232 | 231 | anassrs 398 |
. . . . . . . . . . 11
|
233 | 232 | ralrimdva 2550 |
. . . . . . . . . 10
|
234 | 127, 233 | syl5bi 151 |
. . . . . . . . 9
|
235 | 234 | expl 376 |
. . . . . . . 8
|
236 | 235 | a2d 26 |
. . . . . . 7
|
237 | 20, 33, 46, 59, 119, 236 | nnind 8887 |
. . . . . 6
|
238 | 237 | com12 30 |
. . . . 5
|
239 | 238 | impr 377 |
. . . 4
|
240 | 239 | adantll 473 |
. . 3
|
241 | | simpll 524 |
. . 3
|
242 | 7, 240, 241 | rspcdva 2839 |
. 2
|
243 | 242 | 3impia 1195 |
1
|