Metamath Proof Explorer

Theorem dvdsexpb

Description: dvdssq generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 nn0abscl ⊢ A ∈ ℤ → A ∈ ℕ 0
2 nn0abscl ⊢ B ∈ ℤ → B ∈ ℕ 0
3 dvdsexpnn0 ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ N ∈ ℕ → A ∥ B ↔ A N ∥ B N
4 1 2 3 syl3an12 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A ∥ B ↔ A N ∥ B N
5 simp1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A ∈ ℤ
6 5 zcnd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A ∈ ℂ
7 simp3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → N ∈ ℕ
8 7 nnnn0d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → N ∈ ℕ 0
9 6 8 absexpd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A N = A N
10 simp2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → B ∈ ℤ
11 10 zcnd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → B ∈ ℂ
12 11 8 absexpd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → B N = B N
13 9 12 breq12d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A N ∥ B N ↔ A N ∥ B N
14 4 13 bitr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A ∥ B ↔ A N ∥ B N
15 absdvdsabsb ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∥ B ↔ A ∥ B
16 15 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A ∥ B ↔ A ∥ B
17 5 8 zexpcld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A N ∈ ℤ
18 10 8 zexpcld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → B N ∈ ℤ
19 absdvdsabsb ⊢ A N ∈ ℤ ∧ B N ∈ ℤ → A N ∥ B N ↔ A N ∥ B N
20 17 18 19 syl2anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A N ∥ B N ↔ A N ∥ B N
21 14 16 20 3bitr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A ∥ B ↔ A N ∥ B N