This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) -> ( K || M -> K || ( M ^ N ) ) )

Proof

Step Hyp Ref Expression
1 divides 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K || M <-> E. m e. ZZ ( m x. K ) = M ) )
2 1 3adant3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) -> ( K || M <-> E. m e. ZZ ( m x. K ) = M ) )
3 simpl1 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> K e. ZZ )
4 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
5 4 3ad2ant3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) -> N e. NN0 )
6 5 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> N e. NN0 )
7 zexpcl 
 |-  ( ( K e. ZZ /\ N e. NN0 ) -> ( K ^ N ) e. ZZ )
8 3 6 7 syl2anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> ( K ^ N ) e. ZZ )
9 simpr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> m e. ZZ )
10 zexpcl 
 |-  ( ( m e. ZZ /\ N e. NN0 ) -> ( m ^ N ) e. ZZ )
11 9 6 10 syl2anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> ( m ^ N ) e. ZZ )
12 11 8 zmulcld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> ( ( m ^ N ) x. ( K ^ N ) ) e. ZZ )
13 simpl3 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> N e. NN )
14 iddvdsexp 
 |-  ( ( K e. ZZ /\ N e. NN ) -> K || ( K ^ N ) )
15 3 13 14 syl2anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> K || ( K ^ N ) )
16 dvdsmul2 
 |-  ( ( ( m ^ N ) e. ZZ /\ ( K ^ N ) e. ZZ ) -> ( K ^ N ) || ( ( m ^ N ) x. ( K ^ N ) ) )
17 11 8 16 syl2anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> ( K ^ N ) || ( ( m ^ N ) x. ( K ^ N ) ) )
18 3 8 12 15 17 dvdstrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> K || ( ( m ^ N ) x. ( K ^ N ) ) )
19 zcn 
 |-  ( m e. ZZ -> m e. CC )
20 19 adantl 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> m e. CC )
21 zcn 
 |-  ( K e. ZZ -> K e. CC )
22 21 3ad2ant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) -> K e. CC )
23 22 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> K e. CC )
24 20 23 6 mulexpd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> ( ( m x. K ) ^ N ) = ( ( m ^ N ) x. ( K ^ N ) ) )
25 18 24 breqtrrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> K || ( ( m x. K ) ^ N ) )
26 oveq1 
 |-  ( ( m x. K ) = M -> ( ( m x. K ) ^ N ) = ( M ^ N ) )
27 26 breq2d 
 |-  ( ( m x. K ) = M -> ( K || ( ( m x. K ) ^ N ) <-> K || ( M ^ N ) ) )
28 25 27 syl5ibcom 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) /\ m e. ZZ ) -> ( ( m x. K ) = M -> K || ( M ^ N ) ) )
29 28 rexlimdva 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) -> ( E. m e. ZZ ( m x. K ) = M -> K || ( M ^ N ) ) )
30 2 29 sylbid 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) -> ( K || M -> K || ( M ^ N ) ) )