gcddvds

Description: The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step	Hyp	Ref	Expression
1		0z	$⊢ 0 \in ℤ$
2		dvds0	$⊢ 0 \in ℤ \to 0 ∥ 0$
3	1 2	ax-mp	$⊢ 0 ∥ 0$
4		breq2	$⊢ M = 0 \to (0 ∥ M \leftrightarrow 0 ∥ 0)$
5		breq2	$⊢ N = 0 \to (0 ∥ N \leftrightarrow 0 ∥ 0)$
6	4 5	bi2anan9	$⊢ (M = 0 \land N = 0) \to ((0 ∥ M \land 0 ∥ N) \leftrightarrow (0 ∥ 0 \land 0 ∥ 0))$
7		anidm	$⊢ (0 ∥ 0 \land 0 ∥ 0) \leftrightarrow 0 ∥ 0$
8	6 7	bitrdi	$⊢ (M = 0 \land N = 0) \to ((0 ∥ M \land 0 ∥ N) \leftrightarrow 0 ∥ 0)$
9	3 8	mpbiri	$⊢ (M = 0 \land N = 0) \to (0 ∥ M \land 0 ∥ N)$
10		oveq12	$⊢ (M = 0 \land N = 0) \to M \gcd N = 0 \gcd 0$
11		gcd0val	$⊢ 0 \gcd 0 = 0$
12	10 11	eqtrdi	$⊢ (M = 0 \land N = 0) \to M \gcd N = 0$
13	12	breq1d	$⊢ (M = 0 \land N = 0) \to ((M \gcd N) ∥ M \leftrightarrow 0 ∥ M)$
14	12	breq1d	$⊢ (M = 0 \land N = 0) \to ((M \gcd N) ∥ N \leftrightarrow 0 ∥ N)$
15	13 14	anbi12d	$⊢ (M = 0 \land N = 0) \to (((M \gcd N) ∥ M \land (M \gcd N) ∥ N) \leftrightarrow (0 ∥ M \land 0 ∥ N))$
16	9 15	mpbird	$⊢ (M = 0 \land N = 0) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
17	16	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (M = 0 \land N = 0)) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
18		eqid	$⊢ \{n \in ℤ \| \forall z \in \{M, N\} n ∥ z\} = \{n \in ℤ \| \forall z \in \{M, N\} n ∥ z\}$
19		eqid	$⊢ \{n \in ℤ \| (n ∥ M \land n ∥ N)\} = \{n \in ℤ \| (n ∥ M \land n ∥ N)\}$
20	18 19	gcdcllem3	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) \in ℕ \land (sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ M \land sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ N) \land ((K \in ℤ \land K ∥ M \land K ∥ N) \to K \leq sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)))$
21	20	simp2d	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ M \land sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ N)$
22		gcdn0val	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N = sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)$
23	22	breq1d	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((M \gcd N) ∥ M \leftrightarrow sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ M)$
24	22	breq1d	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((M \gcd N) ∥ N \leftrightarrow sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ N)$
25	23 24	anbi12d	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (((M \gcd N) ∥ M \land (M \gcd N) ∥ N) \leftrightarrow (sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ M \land sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) ∥ N))$
26	21 25	mpbird	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
27	17 26	pm2.61dan	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$

Metamath Proof Explorer

Theorem gcddvds

Proof