This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )