Metamath Proof Explorer

Theorem lcmledvds

Description: A positive integer which both operands of the lcm operator divide bounds it. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

		Ref	Expression
	Assertion	lcmledvds	$⊢ ((K \in ℕ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to ((M ∥ K \land N ∥ K) \to M lcm N \leq K)$

Proof

Step	Hyp	Ref	Expression
1		lcmn0val	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to M lcm N = inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <)$
2	1	3adantl1	$⊢ ((K \in ℕ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to M lcm N = inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <)$
3	2	adantr	$⊢ (((K \in ℕ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \land (M ∥ K \land N ∥ K)) \to M lcm N = inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <)$
4		breq2	$⊢ n = K \to (M ∥ n \leftrightarrow M ∥ K)$
5		breq2	$⊢ n = K \to (N ∥ n \leftrightarrow N ∥ K)$
6	4 5	anbi12d	$⊢ n = K \to ((M ∥ n \land N ∥ n) \leftrightarrow (M ∥ K \land N ∥ K))$
7	6	elrab	$⊢ K \in \{n \in ℕ \| (M ∥ n \land N ∥ n)\} \leftrightarrow (K \in ℕ \land (M ∥ K \land N ∥ K))$
8		ssrab2	$⊢ \{n \in ℕ \| (M ∥ n \land N ∥ n)\} \subseteq ℕ$
9		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
10	8 9	sseqtri	$⊢ \{n \in ℕ \| (M ∥ n \land N ∥ n)\} \subseteq ℤ_{\geq 1}$
11		infssuzle	$⊢ (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} \subseteq ℤ_{\geq 1} \land K \in \{n \in ℕ \| (M ∥ n \land N ∥ n)\}) \to inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <) \leq K$
12	10 11	mpan	$⊢ K \in \{n \in ℕ \| (M ∥ n \land N ∥ n)\} \to inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <) \leq K$
13	7 12	sylbir	$⊢ (K \in ℕ \land (M ∥ K \land N ∥ K)) \to inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <) \leq K$
14	13	ex	$⊢ K \in ℕ \to ((M ∥ K \land N ∥ K) \to inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <) \leq K)$
15	14	3ad2ant1	$⊢ (K \in ℕ \land M \in ℤ \land N \in ℤ) \to ((M ∥ K \land N ∥ K) \to inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <) \leq K)$
16	15	adantr	$⊢ ((K \in ℕ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to ((M ∥ K \land N ∥ K) \to inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <) \leq K)$
17	16	imp	$⊢ (((K \in ℕ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \land (M ∥ K \land N ∥ K)) \to inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <) \leq K$
18	3 17	eqbrtrd	$⊢ (((K \in ℕ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \land (M ∥ K \land N ∥ K)) \to M lcm N \leq K$
19	18	ex	$⊢ ((K \in ℕ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to ((M ∥ K \land N ∥ K) \to M lcm N \leq K)$