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 \in ℕ \land B \in ℕ \land N \in ℕ) \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to A \in ℕ$
2		simp3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to N \in ℕ$
3	2	nnnn0d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to N \in ℕ_{0}$
4	1 3	nnexpcld	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to A^{N} \in ℕ$
5		simp2	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to B \in ℕ$
6	4 5 2	3jca	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A^{N} \in ℕ \land B \in ℕ \land N \in ℕ)$
7		rplpwr	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A \gcd B = 1 \to A^{N} \gcd B = 1)$
8		rprpwr	$⊢ (A^{N} \in ℕ \land B \in ℕ \land N \in ℕ) \to (A^{N} \gcd B = 1 \to A^{N} \gcd B^{N} = 1)$
9	6 7 8	sylsyld	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A \gcd B = 1 \to A^{N} \gcd B^{N} = 1)$