nndvdslegcd

Description: A positive integer which divides both positive operands of the gcd operator is bounded by it. (Contributed by AV, 9-Aug-2020)

		Ref	Expression
	Assertion	nndvdslegcd	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to ((K ∥ M \land K ∥ N) \to K \leq M \gcd N)$

Step	Hyp	Ref	Expression
1		nnz	$⊢ K \in ℕ \to K \in ℤ$
2		nnz	$⊢ M \in ℕ \to M \in ℤ$
3		nnz	$⊢ N \in ℕ \to N \in ℤ$
4	1 2 3	3anim123i	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to (K \in ℤ \land M \in ℤ \land N \in ℤ)$
5		nnne0	$⊢ M \in ℕ \to M \neq 0$
6	5	neneqd	$⊢ M \in ℕ \to \neg M = 0$
7	6	3ad2ant2	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to \neg M = 0$
8	7	intnanrd	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to \neg (M = 0 \land N = 0)$
9		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)$
10	4 8 9	syl2anc	$⊢ (K \in ℕ \land M \in ℕ \land N \in ℕ) \to ((K ∥ M \land K ∥ N) \to K \leq M \gcd N)$

Metamath Proof Explorer