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