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 \in ℤ \land M \in ℤ \land N \in ℕ) \to (K ∥ M \to K ∥ M^{N})$

Proof

Step	Hyp	Ref	Expression
1		divides	$⊢ (K \in ℤ \land M \in ℤ) \to (K ∥ M \leftrightarrow \exists m \in ℤ m K = M)$
2	1	3adant3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℕ) \to (K ∥ M \leftrightarrow \exists m \in ℤ m K = M)$
3		simpl1	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to K \in ℤ$
4		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
5	4	3ad2ant3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℕ) \to N \in ℕ_{0}$
6	5	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to N \in ℕ_{0}$
7		zexpcl	$⊢ (K \in ℤ \land N \in ℕ_{0}) \to K^{N} \in ℤ$
8	3 6 7	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to K^{N} \in ℤ$
9		simpr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to m \in ℤ$
10		zexpcl	$⊢ (m \in ℤ \land N \in ℕ_{0}) \to m^{N} \in ℤ$
11	9 6 10	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to m^{N} \in ℤ$
12	11 8	zmulcld	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to m^{N} K^{N} \in ℤ$
13		simpl3	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to N \in ℕ$
14		iddvdsexp	$⊢ (K \in ℤ \land N \in ℕ) \to K ∥ K^{N}$
15	3 13 14	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to K ∥ K^{N}$
16		dvdsmul2	$⊢ (m^{N} \in ℤ \land K^{N} \in ℤ) \to K^{N} ∥ m^{N} K^{N}$
17	11 8 16	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to K^{N} ∥ m^{N} K^{N}$
18	3 8 12 15 17	dvdstrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to K ∥ m^{N} K^{N}$
19		zcn	$⊢ m \in ℤ \to m \in ℂ$
20	19	adantl	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to m \in ℂ$
21		zcn	$⊢ K \in ℤ \to K \in ℂ$
22	21	3ad2ant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℕ) \to K \in ℂ$
23	22	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to K \in ℂ$
24	20 23 6	mulexpd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to {m K}^{N} = m^{N} K^{N}$
25	18 24	breqtrrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to K ∥ {m K}^{N}$
26		oveq1	$⊢ m K = M \to {m K}^{N} = M^{N}$
27	26	breq2d	$⊢ m K = M \to (K ∥ {m K}^{N} \leftrightarrow K ∥ M^{N})$
28	25 27	syl5ibcom	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℕ) \land m \in ℤ) \to (m K = M \to K ∥ M^{N})$
29	28	rexlimdva	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℕ) \to (\exists m \in ℤ m K = M \to K ∥ M^{N})$
30	2 29	sylbid	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℕ) \to (K ∥ M \to K ∥ M^{N})$

Metamath Proof Explorer

Theorem dvdsexp2im

Proof