dvdsgcd

Description: An integer which divides each of two others also divides their gcd. (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 30-May-2014)

		Ref	Expression
	Assertion	dvdsgcd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land K ∥ N) \to K ∥ (M \gcd N))$

Proof

Step	Hyp	Ref	Expression
1		bezout	$⊢ (M \in ℤ \land N \in ℤ) \to \exists x \in ℤ \exists y \in ℤ M \gcd N = M x + N y$
2	1	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to \exists x \in ℤ \exists y \in ℤ M \gcd N = M x + N y$
3		dvds2ln	$⊢ ((x \in ℤ \land y \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to ((K ∥ M \land K ∥ N) \to K ∥ (x \cdot M + y \cdot N))$
4	3	3impia	$⊢ ((x \in ℤ \land y \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N)) \to K ∥ (x \cdot M + y \cdot N)$
5	4	3coml	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to K ∥ (x \cdot M + y \cdot N)$
6		simp3l	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to x \in ℤ$
7		simp12	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to M \in ℤ$
8		zcn	$⊢ x \in ℤ \to x \in ℂ$
9		zcn	$⊢ M \in ℤ \to M \in ℂ$
10		mulcom	$⊢ (x \in ℂ \land M \in ℂ) \to x \cdot M = M x$
11	8 9 10	syl2an	$⊢ (x \in ℤ \land M \in ℤ) \to x \cdot M = M x$
12	6 7 11	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to x \cdot M = M x$
13		simp3r	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to y \in ℤ$
14		simp13	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to N \in ℤ$
15		zcn	$⊢ y \in ℤ \to y \in ℂ$
16		zcn	$⊢ N \in ℤ \to N \in ℂ$
17		mulcom	$⊢ (y \in ℂ \land N \in ℂ) \to y \cdot N = N y$
18	15 16 17	syl2an	$⊢ (y \in ℤ \land N \in ℤ) \to y \cdot N = N y$
19	13 14 18	syl2anc	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to y \cdot N = N y$
20	12 19	oveq12d	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to x \cdot M + y \cdot N = M x + N y$
21	5 20	breqtrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to K ∥ (M x + N y)$
22		breq2	$⊢ M \gcd N = M x + N y \to (K ∥ (M \gcd N) \leftrightarrow K ∥ (M x + N y))$
23	21 22	syl5ibrcom	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N) \land (x \in ℤ \land y \in ℤ)) \to (M \gcd N = M x + N y \to K ∥ (M \gcd N))$
24	23	3expia	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N)) \to ((x \in ℤ \land y \in ℤ) \to (M \gcd N = M x + N y \to K ∥ (M \gcd N)))$
25	24	rexlimdvv	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K ∥ M \land K ∥ N)) \to (\exists x \in ℤ \exists y \in ℤ M \gcd N = M x + N y \to K ∥ (M \gcd N))$
26	25	ex	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land K ∥ N) \to (\exists x \in ℤ \exists y \in ℤ M \gcd N = M x + N y \to K ∥ (M \gcd N)))$
27	2 26	mpid	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \land K ∥ N) \to K ∥ (M \gcd N))$

Metamath Proof Explorer

Theorem dvdsgcd

Proof