gcdadd

Description: The gcd of two numbers is the same as the gcd of the left and their sum. (Contributed by Scott Fenton, 20-Apr-2014)

		Ref	Expression
	Assertion	gcdadd	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = M \gcd (N + M)$

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		gcdaddm	$⊢ (1 \in ℤ \land M \in ℤ \land N \in ℤ) \to M \gcd N = M \gcd (N + 1 \cdot M)$
3	1 2	mp3an1	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = M \gcd (N + 1 \cdot M)$
4		zcn	$⊢ M \in ℤ \to M \in ℂ$
5		mullid	$⊢ M \in ℂ \to 1 \cdot M = M$
6	5	oveq2d	$⊢ M \in ℂ \to N + 1 \cdot M = N + M$
7	6	oveq2d	$⊢ M \in ℂ \to M \gcd (N + 1 \cdot M) = M \gcd (N + M)$
8	4 7	syl	$⊢ M \in ℤ \to M \gcd (N + 1 \cdot M) = M \gcd (N + M)$
9	8	adantr	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd (N + 1 \cdot M) = M \gcd (N + M)$
10	3 9	eqtrd	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = M \gcd (N + M)$

Metamath Proof Explorer