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

Step	Hyp	Ref	Expression
1		rplpwr	$⊢ (B \in ℕ \land A \in ℕ \land N \in ℕ) \to (B \gcd A = 1 \to B^{N} \gcd A = 1)$
2	1	3com12	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (B \gcd A = 1 \to B^{N} \gcd A = 1)$
3		nnz	$⊢ A \in ℕ \to A \in ℤ$
4		nnz	$⊢ B \in ℕ \to B \in ℤ$
5		gcdcom	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B = B \gcd A$
6	3 4 5	syl2an	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B = B \gcd A$
7	6	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to A \gcd B = B \gcd A$
8	7	eqeq1d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A \gcd B = 1 \leftrightarrow B \gcd A = 1)$
9		simp1	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to A \in ℕ$
10	9	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to A \in ℤ$
11		simp2	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to B \in ℕ$
12		simp3	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to N \in ℕ$
13	12	nnnn0d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to N \in ℕ_{0}$
14	11 13	nnexpcld	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to B^{N} \in ℕ$
15	14	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to B^{N} \in ℤ$
16	10 15	gcdcomd	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to A \gcd B^{N} = B^{N} \gcd A$
17	16	eqeq1d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A \gcd B^{N} = 1 \leftrightarrow B^{N} \gcd A = 1)$
18	2 8 17	3imtr4d	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A \gcd B = 1 \to A \gcd B^{N} = 1)$

Metamath Proof Explorer