Theorem dvdsexp

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

	Ref	Expression
Assertion	dvdsexp	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑀 ) ∥ ( 𝐴 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℤ )
2		uznn0sub	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
3	2	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
4		zexpcl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) ∈ ℤ )
5	1 3 4	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) ∈ ℤ )
6		zexpcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℤ )
7	6	3adant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℤ )
8		dvdsmul2	⊢ ( ( ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) ∈ ℤ ∧ ( 𝐴 ↑ 𝑀 ) ∈ ℤ ) → ( 𝐴 ↑ 𝑀 ) ∥ ( ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) · ( 𝐴 ↑ 𝑀 ) ) )
9	5 7 8	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑀 ) ∥ ( ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) · ( 𝐴 ↑ 𝑀 ) ) )
10	1	zcnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℂ )
11		simp2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℕ0 )
12	10 11 3	expaddd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) = ( ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) · ( 𝐴 ↑ 𝑀 ) ) )
13		eluzelcn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℂ )
14	13	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℂ )
15	11	nn0cnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℂ )
16	14 15	npcand	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑁 − 𝑀 ) + 𝑀 ) = 𝑁 )
17	16	oveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ ( ( 𝑁 − 𝑀 ) + 𝑀 ) ) = ( 𝐴 ↑ 𝑁 ) )
18	12 17	eqtr3d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐴 ↑ ( 𝑁 − 𝑀 ) ) · ( 𝐴 ↑ 𝑀 ) ) = ( 𝐴 ↑ 𝑁 ) )
19	9 18	breqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑀 ) ∥ ( 𝐴 ↑ 𝑁 ) )