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

Metamath Proof Explorer

Theorem dvdsexpim

Description: If two numbers are divisible, so are their nonnegative exponents. Similar to dvdssqim for nonnegative exponents. (Contributed by Steven Nguyen, 2-Apr-2023)

Ref Expression
Assertion dvdsexpim ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ 𝐵 → ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 divides ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∥ 𝐵 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝐴 ) = 𝐵 ) )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ 𝐵 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝐴 ) = 𝐵 ) )
3 zexpcl ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑁 ) ∈ ℤ )
4 3 ancoms ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ↑ 𝑁 ) ∈ ℤ )
5 4 adantll ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ↑ 𝑁 ) ∈ ℤ )
6 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
8 dvdsmul2 ⊢ ( ( ( 𝑘 ↑ 𝑁 ) ∈ ℤ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∥ ( ( 𝑘 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) )
9 5 7 8 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∥ ( ( 𝑘 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) )
10 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
11 10 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
12 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
13 12 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → 𝐴 ∈ ℂ )
14 simplr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → 𝑁 ∈ ℕ0 )
15 11 13 14 mulexpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 · 𝐴 ) ↑ 𝑁 ) = ( ( 𝑘 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) )
16 9 15 breqtrrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∥ ( ( 𝑘 · 𝐴 ) ↑ 𝑁 ) )
17 oveq1 ⊢ ( ( 𝑘 · 𝐴 ) = 𝐵 → ( ( 𝑘 · 𝐴 ) ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
18 17 breq2d ⊢ ( ( 𝑘 · 𝐴 ) = 𝐵 → ( ( 𝐴 ↑ 𝑁 ) ∥ ( ( 𝑘 · 𝐴 ) ↑ 𝑁 ) ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
19 16 18 syl5ibcom ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 · 𝐴 ) = 𝐵 → ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
20 19 rexlimdva ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝐴 ) = 𝐵 → ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
21 20 3adant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝐴 ) = 𝐵 → ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
22 2 21 sylbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ 𝐵 → ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )