rpexp1i

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

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

Step	Hyp	Ref	Expression
1		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
2		rpexp	$⊢ (A \in ℤ \land B \in ℤ \land M \in ℕ) \to (A^{M} \gcd B = 1 \leftrightarrow A \gcd B = 1)$
3	2	biimprd	$⊢ (A \in ℤ \land B \in ℤ \land M \in ℕ) \to (A \gcd B = 1 \to A^{M} \gcd B = 1)$
4	3	3expa	$⊢ ((A \in ℤ \land B \in ℤ) \land M \in ℕ) \to (A \gcd B = 1 \to A^{M} \gcd B = 1)$
5		simpr	$⊢ ((A \in ℤ \land B \in ℤ) \land M = 0) \to M = 0$
6	5	oveq2d	$⊢ ((A \in ℤ \land B \in ℤ) \land M = 0) \to A^{M} = A^{0}$
7		zcn	$⊢ A \in ℤ \to A \in ℂ$
8	7	ad2antrr	$⊢ ((A \in ℤ \land B \in ℤ) \land M = 0) \to A \in ℂ$
9	8	exp0d	$⊢ ((A \in ℤ \land B \in ℤ) \land M = 0) \to A^{0} = 1$
10	6 9	eqtrd	$⊢ ((A \in ℤ \land B \in ℤ) \land M = 0) \to A^{M} = 1$
11	10	oveq1d	$⊢ ((A \in ℤ \land B \in ℤ) \land M = 0) \to A^{M} \gcd B = 1 \gcd B$
12		1gcd	$⊢ B \in ℤ \to 1 \gcd B = 1$
13	12	ad2antlr	$⊢ ((A \in ℤ \land B \in ℤ) \land M = 0) \to 1 \gcd B = 1$
14	11 13	eqtrd	$⊢ ((A \in ℤ \land B \in ℤ) \land M = 0) \to A^{M} \gcd B = 1$
15	14	a1d	$⊢ ((A \in ℤ \land B \in ℤ) \land M = 0) \to (A \gcd B = 1 \to A^{M} \gcd B = 1)$
16	4 15	jaodan	$⊢ ((A \in ℤ \land B \in ℤ) \land (M \in ℕ \lor M = 0)) \to (A \gcd B = 1 \to A^{M} \gcd B = 1)$
17	1 16	sylan2b	$⊢ ((A \in ℤ \land B \in ℤ) \land M \in ℕ_{0}) \to (A \gcd B = 1 \to A^{M} \gcd B = 1)$
18	17	3impa	$⊢ (A \in ℤ \land B \in ℤ \land M \in ℕ_{0}) \to (A \gcd B = 1 \to A^{M} \gcd B = 1)$

Metamath Proof Explorer