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		gcdcom	$⊢ (A^{M} \in ℤ \land B \in ℤ) \to A^{M} \gcd B = B \gcd A^{M}$
12	7 3 11	syl2anc	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to A^{M} \gcd B = B \gcd A^{M}$
13	12	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)$
14		zexpcl	$⊢ (B \in ℤ \land N \in ℕ_{0}) \to B^{N} \in ℤ$
15	3 8 14	syl2anc	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to B^{N} \in ℤ$
16		gcdcom	$⊢ (A^{M} \in ℤ \land B^{N} \in ℤ) \to A^{M} \gcd B^{N} = B^{N} \gcd A^{M}$
17	7 15 16	syl2anc	$⊢ (A \in ℤ \land B \in ℤ \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to A^{M} \gcd B^{N} = B^{N} \gcd A^{M}$
18	17	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)$
19	10 13 18	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)$
20	2 19	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)$

Metamath Proof Explorer

Theorem rpexp12i

Proof