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

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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∥ ( 𝑀 ↑ 𝑁 ) )

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 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∥ ( 𝑀 ↑ 𝑁 ) )