Metamath Proof Explorer

Theorem iddvdsexp

Description: An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012)

Ref Expression
Assertion iddvdsexp 
|- ( ( M e. ZZ /\ N e. NN ) -> M || ( M ^ N ) )

Proof

Step Hyp Ref Expression
1 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
2 zexpcl 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. NN0 ) -> ( M ^ ( N - 1 ) ) e. ZZ )
3 1 2 sylan2 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M ^ ( N - 1 ) ) e. ZZ )
4 simpl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M e. ZZ )
5 dvdsmul2 
 |-  ( ( ( M ^ ( N - 1 ) ) e. ZZ /\ M e. ZZ ) -> M || ( ( M ^ ( N - 1 ) ) x. M ) )
6 3 4 5 syl2anc 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M || ( ( M ^ ( N - 1 ) ) x. M ) )
7 zcn 
 |-  ( M e. ZZ -> M e. CC )
8 expm1t 
 |-  ( ( M e. CC /\ N e. NN ) -> ( M ^ N ) = ( ( M ^ ( N - 1 ) ) x. M ) )
9 7 8 sylan 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M ^ N ) = ( ( M ^ ( N - 1 ) ) x. M ) )
10 6 9 breqtrrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M || ( M ^ N ) )