Metamath Proof Explorer

Theorem dvdsexpnn

Description: dvdssqlem generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024)

Ref Expression
Assertion dvdsexpnn ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A ∥ B ↔ A N ∥ B N

Proof

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