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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( 𝐴 gcd ( 𝐵𝑁 ) ) = 1 ) )

Proof

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