Description: If an integer divides another integer, then it also divides any of its powers. (Contributed by Scott Fenton, 7-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdsexp2im | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | divides | |
|
2 | 1 | 3adant3 | |
3 | simpl1 | |
|
4 | nnnn0 | |
|
5 | 4 | 3ad2ant3 | |
6 | 5 | adantr | |
7 | zexpcl | |
|
8 | 3 6 7 | syl2anc | |
9 | simpr | |
|
10 | zexpcl | |
|
11 | 9 6 10 | syl2anc | |
12 | 11 8 | zmulcld | |
13 | simpl3 | |
|
14 | iddvdsexp | |
|
15 | 3 13 14 | syl2anc | |
16 | dvdsmul2 | |
|
17 | 11 8 16 | syl2anc | |
18 | 3 8 12 15 17 | dvdstrd | |
19 | zcn | |
|
20 | 19 | adantl | |
21 | zcn | |
|
22 | 21 | 3ad2ant1 | |
23 | 22 | adantr | |
24 | 20 23 6 | mulexpd | |
25 | 18 24 | breqtrrd | |
26 | oveq1 | |
|
27 | 26 | breq2d | |
28 | 25 27 | syl5ibcom | |
29 | 28 | rexlimdva | |
30 | 2 29 | sylbid | |