iddvdsexp

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

		Ref	Expression
	Assertion	iddvdsexp	$⊢ (M \in ℤ \land N \in ℕ) \to M ∥ M^{N}$

Step	Hyp	Ref	Expression
1		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
2		zexpcl	$⊢ (M \in ℤ \land N - 1 \in ℕ_{0}) \to M^{N - 1} \in ℤ$
3	1 2	sylan2	$⊢ (M \in ℤ \land N \in ℕ) \to M^{N - 1} \in ℤ$
4		simpl	$⊢ (M \in ℤ \land N \in ℕ) \to M \in ℤ$
5		dvdsmul2	$⊢ (M^{N - 1} \in ℤ \land M \in ℤ) \to M ∥ M^{N - 1} \cdot M$
6	3 4 5	syl2anc	$⊢ (M \in ℤ \land N \in ℕ) \to M ∥ M^{N - 1} \cdot M$
7		zcn	$⊢ M \in ℤ \to M \in ℂ$
8		expm1t	$⊢ (M \in ℂ \land N \in ℕ) \to M^{N} = M^{N - 1} \cdot M$
9	7 8	sylan	$⊢ (M \in ℤ \land N \in ℕ) \to M^{N} = M^{N - 1} \cdot M$
10	6 9	breqtrrd	$⊢ (M \in ℤ \land N \in ℕ) \to M ∥ M^{N}$

Metamath Proof Explorer