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

Metamath Proof Explorer

Theorem 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 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∥ 𝑀 → 𝐾 ∥ ( 𝑀 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 divides ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 ∥ 𝑀 ↔ ∃ 𝑚 ∈ ℤ ( 𝑚 · 𝐾 ) = 𝑀 ) )
2 1 3adant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∥ 𝑀 ↔ ∃ 𝑚 ∈ ℤ ( 𝑚 · 𝐾 ) = 𝑀 ) )
3 simpl1 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → 𝐾 ∈ ℤ )
4 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
5 4 3ad2ant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
6 5 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → 𝑁 ∈ ℕ0 )
7 zexpcl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑁 ) ∈ ℤ )
8 3 6 7 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → ( 𝐾 ↑ 𝑁 ) ∈ ℤ )
9 simpr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ )
10 zexpcl ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑚 ↑ 𝑁 ) ∈ ℤ )
11 9 6 10 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → ( 𝑚 ↑ 𝑁 ) ∈ ℤ )
12 11 8 zmulcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑚 ↑ 𝑁 ) · ( 𝐾 ↑ 𝑁 ) ) ∈ ℤ )
13 simpl3 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → 𝑁 ∈ ℕ )
14 iddvdsexp ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐾 ∥ ( 𝐾 ↑ 𝑁 ) )
15 3 13 14 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → 𝐾 ∥ ( 𝐾 ↑ 𝑁 ) )
16 dvdsmul2 ⊢ ( ( ( 𝑚 ↑ 𝑁 ) ∈ ℤ ∧ ( 𝐾 ↑ 𝑁 ) ∈ ℤ ) → ( 𝐾 ↑ 𝑁 ) ∥ ( ( 𝑚 ↑ 𝑁 ) · ( 𝐾 ↑ 𝑁 ) ) )
17 11 8 16 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → ( 𝐾 ↑ 𝑁 ) ∥ ( ( 𝑚 ↑ 𝑁 ) · ( 𝐾 ↑ 𝑁 ) ) )
18 3 8 12 15 17 dvdstrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → 𝐾 ∥ ( ( 𝑚 ↑ 𝑁 ) · ( 𝐾 ↑ 𝑁 ) ) )
19 zcn ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℂ )
20 19 adantl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℂ )
21 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
22 21 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℂ )
23 22 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → 𝐾 ∈ ℂ )
24 20 23 6 mulexpd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑚 · 𝐾 ) ↑ 𝑁 ) = ( ( 𝑚 ↑ 𝑁 ) · ( 𝐾 ↑ 𝑁 ) ) )
25 18 24 breqtrrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → 𝐾 ∥ ( ( 𝑚 · 𝐾 ) ↑ 𝑁 ) )
26 oveq1 ⊢ ( ( 𝑚 · 𝐾 ) = 𝑀 → ( ( 𝑚 · 𝐾 ) ↑ 𝑁 ) = ( 𝑀 ↑ 𝑁 ) )
27 26 breq2d ⊢ ( ( 𝑚 · 𝐾 ) = 𝑀 → ( 𝐾 ∥ ( ( 𝑚 · 𝐾 ) ↑ 𝑁 ) ↔ 𝐾 ∥ ( 𝑀 ↑ 𝑁 ) ) )
28 25 27 syl5ibcom ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑚 · 𝐾 ) = 𝑀 → 𝐾 ∥ ( 𝑀 ↑ 𝑁 ) ) )
29 28 rexlimdva ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑚 ∈ ℤ ( 𝑚 · 𝐾 ) = 𝑀 → 𝐾 ∥ ( 𝑀 ↑ 𝑁 ) ) )
30 2 29 sylbid ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∥ 𝑀 → 𝐾 ∥ ( 𝑀 ↑ 𝑁 ) ) )