Metamath Proof Explorer

Theorem rprpwr

Description: If A and B are relatively prime, then so are A and B ^ N . Originally a subproof of rppwr . (Contributed by SN, 21-Aug-2024)

Ref Expression
Assertion rprpwr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B = 1 → A gcd B N = 1

Proof

Step Hyp Ref Expression
1 rplpwr ⊢ B ∈ ℕ ∧ A ∈ ℕ ∧ N ∈ ℕ → B gcd A = 1 → B N gcd A = 1
2 1 3com12 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → B gcd A = 1 → B N gcd A = 1
3 nnz ⊢ A ∈ ℕ → A ∈ ℤ
4 nnz ⊢ B ∈ ℕ → B ∈ ℤ
5 gcdcom ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B = B gcd A
6 3 4 5 syl2an ⊢ A ∈ ℕ ∧ B ∈ ℕ → A gcd B = B gcd A
7 6 3adant3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B = B gcd A
8 7 eqeq1d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B = 1 ↔ B gcd A = 1
9 simp1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A ∈ ℕ
10 9 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A ∈ ℤ
11 simp2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → B ∈ ℕ
12 simp3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → N ∈ ℕ
13 12 nnnn0d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → N ∈ ℕ 0
14 11 13 nnexpcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → B N ∈ ℕ
15 14 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → B N ∈ ℤ
16 10 15 gcdcomd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B N = B N gcd A
17 16 eqeq1d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B N = 1 ↔ B N gcd A = 1
18 2 8 17 3imtr4d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B = 1 → A gcd B N = 1