Metamath Proof Explorer

Theorem dvdsexpb

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

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

Proof

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