Metamath Proof Explorer

Theorem dvdsexp

Description: A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014)

		Ref	Expression
	Assertion	dvdsexp	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A^{M} ∥ A^{N}$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A \in ℤ$
2		uznn0sub	$⊢ N \in ℤ_{\geq M} \to N - M \in ℕ_{0}$
3	2	3ad2ant3	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to N - M \in ℕ_{0}$
4		zexpcl	$⊢ (A \in ℤ \land N - M \in ℕ_{0}) \to A^{N - M} \in ℤ$
5	1 3 4	syl2anc	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A^{N - M} \in ℤ$
6		zexpcl	$⊢ (A \in ℤ \land M \in ℕ_{0}) \to A^{M} \in ℤ$
7	6	3adant3	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A^{M} \in ℤ$
8		dvdsmul2	$⊢ (A^{N - M} \in ℤ \land A^{M} \in ℤ) \to A^{M} ∥ A^{N - M} A^{M}$
9	5 7 8	syl2anc	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A^{M} ∥ A^{N - M} A^{M}$
10	1	zcnd	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A \in ℂ$
11		simp2	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to M \in ℕ_{0}$
12	10 11 3	expaddd	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A^{N - M + M} = A^{N - M} A^{M}$
13		eluzelcn	$⊢ N \in ℤ_{\geq M} \to N \in ℂ$
14	13	3ad2ant3	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to N \in ℂ$
15	11	nn0cnd	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to M \in ℂ$
16	14 15	npcand	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to N - M + M = N$
17	16	oveq2d	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A^{N - M + M} = A^{N}$
18	12 17	eqtr3d	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A^{N - M} A^{M} = A^{N}$
19	9 18	breqtrd	$⊢ (A \in ℤ \land M \in ℕ_{0} \land N \in ℤ_{\geq M}) \to A^{M} ∥ A^{N}$