Metamath Proof Explorer

Theorem rpexp12i

Description: Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014)

		Ref	Expression
	Assertion	rpexp12i	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (A \gcd B = 1 \to A^{M} \gcd B^{N} = 1)$

Proof

Step	Hyp	Ref	Expression
1		rpexp1i	$⊢ (A \in ℤ \land B \in ℤ \land M \in ℕ_{0}) \to (A \gcd B = 1 \to A^{M} \gcd B = 1)$
2	1	3adant3r	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (A \gcd B = 1 \to A^{M} \gcd B = 1)$
3		simp2	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to B \in ℤ$
4		simp1	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to A \in ℤ$
5		simp3l	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to M \in ℕ_{0}$
6		zexpcl	$⊢ (A \in ℤ \land M \in ℕ_{0}) \to A^{M} \in ℤ$
7	4 5 6	syl2anc	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to A^{M} \in ℤ$
8		simp3r	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to N \in ℕ_{0}$
9		rpexp1i	$⊢ (B \in ℤ \land A^{M} \in ℤ \land N \in ℕ_{0}) \to (B \gcd A^{M} = 1 \to B^{N} \gcd A^{M} = 1)$
10	3 7 8 9	syl3anc	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (B \gcd A^{M} = 1 \to B^{N} \gcd A^{M} = 1)$
11	7 3	gcdcomd	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to A^{M} \gcd B = B \gcd A^{M}$
12	11	eqeq1d	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (A^{M} \gcd B = 1 \leftrightarrow B \gcd A^{M} = 1)$
13		zexpcl	$⊢ (B \in ℤ \land N \in ℕ_{0}) \to B^{N} \in ℤ$
14	3 8 13	syl2anc	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to B^{N} \in ℤ$
15	7 14	gcdcomd	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to A^{M} \gcd B^{N} = B^{N} \gcd A^{M}$
16	15	eqeq1d	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (A^{M} \gcd B^{N} = 1 \leftrightarrow B^{N} \gcd A^{M} = 1)$
17	10 12 16	3imtr4d	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (A^{M} \gcd B = 1 \to A^{M} \gcd B^{N} = 1)$
18	2 17	syld	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (A \gcd B = 1 \to A^{M} \gcd B^{N} = 1)$