Metamath Proof Explorer

Theorem dvdsexpnn

Description: Two positive integers are divisible iff their positive integer powers are. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) Generalized to arbitrary positive integer exponents. (Revised by SN, 20-Aug-2024)

Ref Expression
Assertion dvdsexpnn ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
2 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
3 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
4 dvdsexpim ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ 𝐵 → ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
5 1 2 3 4 syl3an ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∥ 𝐵 → ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
6 gcdnncl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
7 6 nnrpd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℝ+ )
8 7 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℝ+ )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℝ+ )
10 simpl1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → 𝐴 ∈ ℕ )
11 10 nnrpd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → 𝐴 ∈ ℝ+ )
12 simpl3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → 𝑁 ∈ ℕ )
13 expgcd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
14 3 13 syl3an3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) )
16 simp1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℕ )
17 3 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
18 16 17 nnexpcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
19 simp2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐵 ∈ ℕ )
20 19 17 nnexpcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) ∈ ℕ )
21 gcdeq ⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℕ ∧ ( 𝐵 ↑ 𝑁 ) ∈ ℕ ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( 𝐴 ↑ 𝑁 ) ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
22 18 20 21 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( 𝐴 ↑ 𝑁 ) ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
23 22 biimpar ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( 𝐴 ↑ 𝑁 ) )
24 15 23 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → ( ( 𝐴 gcd 𝐵 ) ↑ 𝑁 ) = ( 𝐴 ↑ 𝑁 ) )
25 9 11 12 24 exp11nnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → ( 𝐴 gcd 𝐵 ) = 𝐴 )
26 gcddvds ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
27 26 simprd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
28 1 2 27 syl2an ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
29 28 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
30 29 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
31 25 30 eqbrtrrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) → 𝐴 ∥ 𝐵 )
32 31 ex ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) → 𝐴 ∥ 𝐵 ) )
33 5 32 impbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )