Theorem iddvdsexp

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

	Ref	Expression
Assertion	iddvdsexp	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∥ ( 𝑀 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
2		zexpcl	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
3	1 2	sylan2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
4		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℤ )
5		dvdsmul2	⊢ ( ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑀 ∥ ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) )
6	3 4 5	syl2anc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∥ ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) )
7		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
8		expm1t	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ↑ 𝑁 ) = ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) )
9	7 8	sylan	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ↑ 𝑁 ) = ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) )
10	6 9	breqtrrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∥ ( 𝑀 ↑ 𝑁 ) )