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 simpl1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → A ∈ ℕ
2 simpl2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → B ∈ ℕ
3 simpl3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → N ∈ ℕ
4 3 nnnn0d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → N ∈ ℕ 0
5 2 4 nnexpcld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → B N ∈ ℕ
6 1 5 3 3jca ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → A ∈ ℕ ∧ B N ∈ ℕ ∧ N ∈ ℕ
7 1 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → A ∈ ℤ
8 5 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → B N ∈ ℤ
9 gcdcom ⊢ A ∈ ℤ ∧ B N ∈ ℤ → A gcd B N = B N gcd A
10 7 8 9 syl2anc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → A gcd B N = B N gcd A
11 2 1 3 3jca ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → B ∈ ℕ ∧ A ∈ ℕ ∧ N ∈ ℕ
12 nnz ⊢ A ∈ ℕ → A ∈ ℤ
13 12 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A ∈ ℤ
14 nnz ⊢ B ∈ ℕ → B ∈ ℤ
15 14 3ad2ant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → B ∈ ℤ
16 gcdcom ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B = B gcd A
17 13 15 16 syl2anc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B = B gcd A
18 17 eqeq1d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B = 1 ↔ B gcd A = 1
19 18 biimpa ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → B gcd A = 1
20 rplpwr ⊢ B ∈ ℕ ∧ A ∈ ℕ ∧ N ∈ ℕ → B gcd A = 1 → B N gcd A = 1
21 11 19 20 sylc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → B N gcd A = 1
22 10 21 eqtrd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → A gcd B N = 1
23 rplpwr ⊢ A ∈ ℕ ∧ B N ∈ ℕ ∧ N ∈ ℕ → A gcd B N = 1 → A N gcd B N = 1
24 6 22 23 sylc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ ∧ A gcd B = 1 → A N gcd B N = 1
25 24 ex ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A gcd B = 1 → A N gcd B N = 1