Metamath Proof Explorer

Theorem dvdslegcd

Description: An integer which divides both operands of the gcd operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	dvdslegcd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((K ∥ M \land K ∥ N) \to K \leq M \gcd N)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ \{n \in ℤ \| \forall z \in \{M, N\} n ∥ z\} = \{n \in ℤ \| \forall z \in \{M, N\} n ∥ z\}$
2		eqid	$⊢ \{n \in ℤ \| (n ∥ M \land n ∥ N)\} = \{n \in ℤ \| (n ∥ M \land n ∥ N)\}$
3	1 2	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)\} ℝ <)))$
4	3	simp3d	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((K \in ℤ \land K ∥ M \land K ∥ N) \to K \leq sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <))$
5		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)\} ℝ <)$
6	5	breq2d	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (K \leq M \gcd N \leftrightarrow K \leq sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <))$
7	4 6	sylibrd	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((K \in ℤ \land K ∥ M \land K ∥ N) \to K \leq M \gcd N)$
8	7	com12	$⊢ (K \in ℤ \land K ∥ M \land K ∥ N) \to (((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to K \leq M \gcd N)$
9	8	3expb	$⊢ (K \in ℤ \land (K ∥ M \land K ∥ N)) \to (((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to K \leq M \gcd N)$
10	9	com12	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((K \in ℤ \land (K ∥ M \land K ∥ N)) \to K \leq M \gcd N)$
11	10	exp4b	$⊢ (M \in ℤ \land N \in ℤ) \to (\neg (M = 0 \land N = 0) \to (K \in ℤ \to ((K ∥ M \land K ∥ N) \to K \leq M \gcd N)))$
12	11	com23	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in ℤ \to (\neg (M = 0 \land N = 0) \to ((K ∥ M \land K ∥ N) \to K \leq M \gcd N)))$
13	12	impcom	$⊢ (K \in ℤ \land (M \in ℤ \land N \in ℤ)) \to (\neg (M = 0 \land N = 0) \to ((K ∥ M \land K ∥ N) \to K \leq M \gcd N))$
14	13	3impb	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (\neg (M = 0 \land N = 0) \to ((K ∥ M \land K ∥ N) \to K \leq M \gcd N))$
15	14	imp	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to ((K ∥ M \land K ∥ N) \to K \leq M \gcd N)$