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

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