Metamath Proof Explorer

Theorem rppwr

Description: If A and B are relatively prime, then so are A ^ N and B ^ N . (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A ∈ ℕ
2 simp3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → N ∈ ℕ
3 2 nnnn0d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → N ∈ ℕ 0
4 1 3 nnexpcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A N ∈ ℕ
5 simp2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → B ∈ ℕ
6 4 5 2 3jca ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A N ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ
7 rplpwr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B = 1 → A N gcd B = 1
8 rprpwr ⊢ A N ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A N gcd B = 1 → A N gcd B N = 1
9 6 7 8 sylsyld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B = 1 → A N gcd B N = 1