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

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℕ )
2		simp3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
3	2	nnnn0d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
4	1 3	nnexpcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
5		simp2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐵 ∈ ℕ )
6	4 5 2	3jca	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
7		rplpwr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ) )
8		rprpwr	⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )
9	6 7 8	sylsyld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )