Metamath Proof Explorer

Theorem lcmfledvds

Description: A positive integer which is divisible by all elements of a set of integers bounds the least common multiple of the set. (Contributed by AV, 22-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

		Ref	Expression
	Assertion	lcmfledvds	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to ((K \in ℕ \land \forall m \in Z m ∥ K) \to \underline{lcm} (Z) \leq K)$

Proof

Step	Hyp	Ref	Expression
1		lcmfn0val	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \underline{lcm} (Z) = sup (\{k \in ℕ \| \forall m \in Z m ∥ k\} ℝ <)$
2	1	adantr	$⊢ ((Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \land (K \in ℕ \land \forall m \in Z m ∥ K)) \to \underline{lcm} (Z) = sup (\{k \in ℕ \| \forall m \in Z m ∥ k\} ℝ <)$
3		ssrab2	$⊢ \{k \in ℕ \| \forall m \in Z m ∥ k\} \subseteq ℕ$
4		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
5	3 4	sseqtri	$⊢ \{k \in ℕ \| \forall m \in Z m ∥ k\} \subseteq ℤ_{\geq 1}$
6		simpr	$⊢ (Z \subseteq ℤ \land (K \in ℕ \land \forall m \in Z m ∥ K)) \to (K \in ℕ \land \forall m \in Z m ∥ K)$
7		breq2	$⊢ k = K \to (m ∥ k \leftrightarrow m ∥ K)$
8	7	ralbidv	$⊢ k = K \to (\forall m \in Z m ∥ k \leftrightarrow \forall m \in Z m ∥ K)$
9	8	elrab	$⊢ K \in \{k \in ℕ \| \forall m \in Z m ∥ k\} \leftrightarrow (K \in ℕ \land \forall m \in Z m ∥ K)$
10	6 9	sylibr	$⊢ (Z \subseteq ℤ \land (K \in ℕ \land \forall m \in Z m ∥ K)) \to K \in \{k \in ℕ \| \forall m \in Z m ∥ k\}$
11		infssuzle	$⊢ (\{k \in ℕ \| \forall m \in Z m ∥ k\} \subseteq ℤ_{\geq 1} \land K \in \{k \in ℕ \| \forall m \in Z m ∥ k\}) \to sup (\{k \in ℕ \| \forall m \in Z m ∥ k\} ℝ <) \leq K$
12	5 10 11	sylancr	$⊢ (Z \subseteq ℤ \land (K \in ℕ \land \forall m \in Z m ∥ K)) \to sup (\{k \in ℕ \| \forall m \in Z m ∥ k\} ℝ <) \leq K$
13	12	3ad2antl1	$⊢ ((Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \land (K \in ℕ \land \forall m \in Z m ∥ K)) \to sup (\{k \in ℕ \| \forall m \in Z m ∥ k\} ℝ <) \leq K$
14	2 13	eqbrtrd	$⊢ ((Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \land (K \in ℕ \land \forall m \in Z m ∥ K)) \to \underline{lcm} (Z) \leq K$
15	14	ex	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to ((K \in ℕ \land \forall m \in Z m ∥ K) \to \underline{lcm} (Z) \leq K)$