MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmpwdvds Unicode version

Theorem prmpwdvds 14422
Description: A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.)
Assertion
Ref Expression
prmpwdvds

Proof of Theorem prmpwdvds
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 753 . . 3
2 oveq2 6304 . . . . . . . . . . . . 13
32oveq2d 6312 . . . . . . . . . . . 12
43breq2d 4464 . . . . . . . . . . 11
5 oveq1 6303 . . . . . . . . . . . . . . 15
65oveq2d 6312 . . . . . . . . . . . . . 14
76oveq2d 6312 . . . . . . . . . . . . 13
87breq2d 4464 . . . . . . . . . . . 12
98notbid 294 . . . . . . . . . . 11
104, 9anbi12d 710 . . . . . . . . . 10
112breq1d 4462 . . . . . . . . . 10
1210, 11imbi12d 320 . . . . . . . . 9
1312ralbidv 2896 . . . . . . . 8
1413imbi2d 316 . . . . . . 7
15 oveq2 6304 . . . . . . . . . . . . 13
1615oveq2d 6312 . . . . . . . . . . . 12
1716breq2d 4464 . . . . . . . . . . 11
18 oveq1 6303 . . . . . . . . . . . . . . 15
1918oveq2d 6312 . . . . . . . . . . . . . 14
2019oveq2d 6312 . . . . . . . . . . . . 13
2120breq2d 4464 . . . . . . . . . . . 12
2221notbid 294 . . . . . . . . . . 11
2317, 22anbi12d 710 . . . . . . . . . 10
2415breq1d 4462 . . . . . . . . . 10
2523, 24imbi12d 320 . . . . . . . . 9
2625ralbidv 2896 . . . . . . . 8
2726imbi2d 316 . . . . . . 7
28 oveq2 6304 . . . . . . . . . . . . 13
2928oveq2d 6312 . . . . . . . . . . . 12
3029breq2d 4464 . . . . . . . . . . 11
31 oveq1 6303 . . . . . . . . . . . . . . 15
3231oveq2d 6312 . . . . . . . . . . . . . 14
3332oveq2d 6312 . . . . . . . . . . . . 13
3433breq2d 4464 . . . . . . . . . . . 12
3534notbid 294 . . . . . . . . . . 11
3630, 35anbi12d 710 . . . . . . . . . 10
3728breq1d 4462 . . . . . . . . . 10
3836, 37imbi12d 320 . . . . . . . . 9
3938ralbidv 2896 . . . . . . . 8
4039imbi2d 316 . . . . . . 7
41 oveq2 6304 . . . . . . . . . . . . 13
4241oveq2d 6312 . . . . . . . . . . . 12
4342breq2d 4464 . . . . . . . . . . 11
44 oveq1 6303 . . . . . . . . . . . . . . 15
4544oveq2d 6312 . . . . . . . . . . . . . 14
4645oveq2d 6312 . . . . . . . . . . . . 13
4746breq2d 4464 . . . . . . . . . . . 12
4847notbid 294 . . . . . . . . . . 11
4943, 48anbi12d 710 . . . . . . . . . 10
5041breq1d 4462 . . . . . . . . . 10
5149, 50imbi12d 320 . . . . . . . . 9
5251ralbidv 2896 . . . . . . . 8
5352imbi2d 316 . . . . . . 7
54 breq1 4455 . . . . . . . . . . . . . 14
55 breq1 4455 . . . . . . . . . . . . . . 15
5655notbid 294 . . . . . . . . . . . . . 14
5754, 56anbi12d 710 . . . . . . . . . . . . 13
58 breq2 4456 . . . . . . . . . . . . 13
5957, 58imbi12d 320 . . . . . . . . . . . 12
6059imbi2d 316 . . . . . . . . . . 11
61 simplrl 761 . . . . . . . . . . . . . . . 16
62 simpll 753 . . . . . . . . . . . . . . . 16
63 coprm 14241 . . . . . . . . . . . . . . . 16
6461, 62, 63syl2anc 661 . . . . . . . . . . . . . . 15
65 zcn 10894 . . . . . . . . . . . . . . . . . . . . 21
6665ad2antll 728 . . . . . . . . . . . . . . . . . . . 20
67 prmz 14221 . . . . . . . . . . . . . . . . . . . . . 22
6867ad2antrl 727 . . . . . . . . . . . . . . . . . . . . 21
6968zcnd 10995 . . . . . . . . . . . . . . . . . . . 20
7066, 69mulcomd 9638 . . . . . . . . . . . . . . . . . . 19
7170breq2d 4464 . . . . . . . . . . . . . . . . . 18
72 simpl 457 . . . . . . . . . . . . . . . . . . . 20
73 gcdcom 14158 . . . . . . . . . . . . . . . . . . . 20
7468, 72, 73syl2anc 661 . . . . . . . . . . . . . . . . . . 19
7574eqeq1d 2459 . . . . . . . . . . . . . . . . . 18
7671, 75anbi12d 710 . . . . . . . . . . . . . . . . 17
77 simprr 757 . . . . . . . . . . . . . . . . . 18
78 coprmdvds 14243 . . . . . . . . . . . . . . . . . 18
7972, 68, 77, 78syl3anc 1228 . . . . . . . . . . . . . . . . 17
8076, 79sylbid 215 . . . . . . . . . . . . . . . 16
8180expdimp 437 . . . . . . . . . . . . . . 15
8264, 81sylbid 215 . . . . . . . . . . . . . 14
8382con1d 124 . . . . . . . . . . . . 13
8483expimpd 603 . . . . . . . . . . . 12
8584ex 434 . . . . . . . . . . 11
8660, 85vtoclga 3173 . . . . . . . . . 10
8786impl 620 . . . . . . . . 9
8867zcnd 10995 . . . . . . . . . . . . . 14
8988exp1d 12305 . . . . . . . . . . . . 13
9089ad2antlr 726 . . . . . . . . . . . 12
9190oveq2d 6312 . . . . . . . . . . 11
9291breq2d 4464 . . . . . . . . . 10
93 1m1e0 10629 . . . . . . . . . . . . . . . 16
9493oveq2i 6307 . . . . . . . . . . . . . . 15
9567ad2antlr 726 . . . . . . . . . . . . . . . . 17
9695zcnd 10995 . . . . . . . . . . . . . . . 16
9796exp0d 12304 . . . . . . . . . . . . . . 15
9894, 97syl5eq 2510 . . . . . . . . . . . . . 14
9998oveq2d 6312 . . . . . . . . . . . . 13
10065adantl 466 . . . . . . . . . . . . . 14
101100mulid1d 9634 . . . . . . . . . . . . 13
10299, 101eqtrd 2498 . . . . . . . . . . . 12
103102breq2d 4464 . . . . . . . . . . 11
104103notbid 294 . . . . . . . . . 10
10592, 104anbi12d 710 . . . . . . . . 9
10696exp1d 12305 . . . . . . . . . 10
107106breq1d 4462 . . . . . . . . 9
10887, 105, 1073imtr4d 268 . . . . . . . 8
109108ralrimiva 2871 . . . . . . 7
110 oveq1 6303 . . . . . . . . . . . . . 14
111110breq2d 4464 . . . . . . . . . . . . 13
112 oveq1 6303 . . . . . . . . . . . . . . 15
113112breq2d 4464 . . . . . . . . . . . . . 14
114113notbid 294 . . . . . . . . . . . . 13
115111, 114anbi12d 710 . . . . . . . . . . . 12
116115imbi1d 317 . . . . . . . . . . 11
117116cbvralv 3084 . . . . . . . . . 10
118 simprr 757 . . . . . . . . . . . . . . 15
11967ad2antrl 727 . . . . . . . . . . . . . . 15
120118, 119zmulcld 11000 . . . . . . . . . . . . . 14
121 oveq1 6303 . . . . . . . . . . . . . . . . . 18
122121breq2d 4464 . . . . . . . . . . . . . . . . 17
123 oveq1 6303 . . . . . . . . . . . . . . . . . . 19
124123breq2d 4464 . . . . . . . . . . . . . . . . . 18
125124notbid 294 . . . . . . . . . . . . . . . . 17
126122, 125anbi12d 710 . . . . . . . . . . . . . . . 16
127126imbi1d 317 . . . . . . . . . . . . . . 15
128127rspcv 3206 . . . . . . . . . . . . . 14
129120, 128syl 16 . . . . . . . . . . . . 13
130 nnnn0 10827 . . . . . . . . . . . . . . . . . . . 20
131130ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
132 zexpcl 12181 . . . . . . . . . . . . . . . . . . 19
133119, 131, 132syl2anc 661 . . . . . . . . . . . . . . . . . 18
134 simplr 755 . . . . . . . . . . . . . . . . . 18
135 divides 13988 . . . . . . . . . . . . . . . . . 18
136133, 134, 135syl2anc 661 . . . . . . . . . . . . . . . . 17
13784adantll 713 . . . . . . . . . . . . . . . . . . . . . 22
138 prmnn 14220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
139138ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
140139nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
141130ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142140, 141expp1d 12311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143139, 141nnexpcld 12331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
144143nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
145144, 140mulcomd 9638 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
146142, 145eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
147146oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . 26
14865ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
149148, 140, 144mulassd 9640 . . . . . . . . . . . . . . . . . . . . . . . . . 26
150147, 149eqtr4d 2501 . . . . . . . . . . . . . . . . . . . . . . . . 25
151150breq2d 4464 . . . . . . . . . . . . . . . . . . . . . . . 24
152 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . 25
153 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26
154139nnzd 10993 . . . . . . . . . . . . . . . . . . . . . . . . . 26
155153, 154zmulcld 11000 . . . . . . . . . . . . . . . . . . . . . . . . 25
156143nnzd 10993 . . . . . . . . . . . . . . . . . . . . . . . . 25
157143nnne0d 10605 . . . . . . . . . . . . . . . . . . . . . . . . 25
158 dvdsmulcr 14013 . . . . . . . . . . . . . . . . . . . . . . . . 25
159152, 155, 156, 157, 158syl112anc 1232 . . . . . . . . . . . . . . . . . . . . . . . 24
160151, 159bitrd 253 . . . . . . . . . . . . . . . . . . . . . . 23
161 dvdsmulcr 14013 . . . . . . . . . . . . . . . . . . . . . . . . 25
162152, 153, 156, 157, 161syl112anc 1232 . . . . . . . . . . . . . . . . . . . . . . . 24
163162notbid 294 . . . . . . . . . . . . . . . . . . . . . . 23
164160, 163anbi12d 710 . . . . . . . . . . . . . . . . . . . . . 22
165146breq1d 4462 . . . . . . . . . . . . . . . . . . . . . . 23
166 dvdsmulcr 14013 . . . . . . . . . . . . . . . . . . . . . . . 24
167154, 152, 156, 157, 166syl112anc 1232 . . . . . . . . . . . . . . . . . . . . . . 23
168165, 167bitrd 253 . . . . . . . . . . . . . . . . . . . . . 22
169137, 164, 1683imtr4d 268 . . . . . . . . . . . . . . . . . . . . 21
170169an32s 804 . . . . . . . . . . . . . . . . . . . 20
171 breq1 4455 . . . . . . . . . . . . . . . . . . . . . 22
172 breq1 4455 . . . . . . . . . . . . . . . . . . . . . . 23
173172notbid 294 . . . . . . . . . . . . . . . . . . . . . 22
174171, 173anbi12d 710 . . . . . . . . . . . . . . . . . . . . 21
175 breq2 4456 . . . . . . . . . . . . . . . . . . . . 21
176174, 175imbi12d 320 . . . . . . . . . . . . . . . . . . . 20
177170, 176syl5ibcom 220 . . . . . . . . . . . . . . . . . . 19
178177rexlimdva 2949 . . . . . . . . . . . . . . . . . 18
179178adantlr 714 . . . . . . . . . . . . . . . . 17
180136, 179sylbid 215 . . . . . . . . . . . . . . . 16
181180com23 78 . . . . . . . . . . . . . . 15
182181a2d 26 . . . . . . . . . . . . . 14
18365ad2antll 728 . . . . . . . . . . . . . . . . . . 19
184119zcnd 10995 . . . . . . . . . . . . . . . . . . 19
185133zcnd 10995 . . . . . . . . . . . . . . . . . . 19
186183, 184, 185mulassd 9640 . . . . . . . . . . . . . . . . . 18
187184, 185mulcomd 9638 . . . . . . . . . . . . . . . . . . . 20
188184, 131expp1d 12311 . . . . . . . . . . . . . . . . . . . 20
189187, 188eqtr4d 2501 . . . . . . . . . . . . . . . . . . 19
190189oveq2d 6312 . . . . . . . . . . . . . . . . . 18
191186, 190eqtrd 2498 . . . . . . . . . . . . . . . . 17
192191breq2d 4464 . . . . . . . . . . . . . . . 16