mulgcdr

Description: Reverse distribution law for the gcd operator. (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	mulgcdr	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to A C \gcd B C = (A \gcd B) C$

Step	Hyp	Ref	Expression
1		mulgcd	$⊢ (C \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to C A \gcd C B = C (A \gcd B)$
2	1	3coml	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to C A \gcd C B = C (A \gcd B)$
3		zcn	$⊢ A \in ℤ \to A \in ℂ$
4	3	3ad2ant1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to A \in ℂ$
5		nn0cn	$⊢ C \in ℕ_{0} \to C \in ℂ$
6	5	3ad2ant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to C \in ℂ$
7	4 6	mulcomd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to A C = C A$
8		zcn	$⊢ B \in ℤ \to B \in ℂ$
9	8	3ad2ant2	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to B \in ℂ$
10	9 6	mulcomd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to B C = C B$
11	7 10	oveq12d	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to A C \gcd B C = C A \gcd C B$
12		gcdcl	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B \in ℕ_{0}$
13	12	3adant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to A \gcd B \in ℕ_{0}$
14	13	nn0cnd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to A \gcd B \in ℂ$
15	14 6	mulcomd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to (A \gcd B) C = C (A \gcd B)$
16	2 11 15	3eqtr4d	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℕ_{0}) \to A C \gcd B C = (A \gcd B) C$

Metamath Proof Explorer