Metamath Proof Explorer


Theorem dvdsexp2im

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 KMNKMKMN

Proof

Step Hyp Ref Expression
1 divides KMKMmmK=M
2 1 3adant3 KMNKMmmK=M
3 simpl1 KMNmK
4 nnnn0 NN0
5 4 3ad2ant3 KMNN0
6 5 adantr KMNmN0
7 zexpcl KN0KN
8 3 6 7 syl2anc KMNmKN
9 simpr KMNmm
10 zexpcl mN0mN
11 9 6 10 syl2anc KMNmmN
12 11 8 zmulcld KMNmmNKN
13 simpl3 KMNmN
14 iddvdsexp KNKKN
15 3 13 14 syl2anc KMNmKKN
16 dvdsmul2 mNKNKNmNKN
17 11 8 16 syl2anc KMNmKNmNKN
18 3 8 12 15 17 dvdstrd KMNmKmNKN
19 zcn mm
20 19 adantl KMNmm
21 zcn KK
22 21 3ad2ant1 KMNK
23 22 adantr KMNmK
24 20 23 6 mulexpd KMNmmKN=mNKN
25 18 24 breqtrrd KMNmKmKN
26 oveq1 mK=MmKN=MN
27 26 breq2d mK=MKmKNKMN
28 25 27 syl5ibcom KMNmmK=MKMN
29 28 rexlimdva KMNmmK=MKMN
30 2 29 sylbid KMNKMKMN