lcmfnnval

Description: The value of the _lcm function for a subset of the positive integers. (Contributed by AV, 21-Aug-2020) (Revised by AV, 16-Sep-2020)

		Ref	Expression
	Assertion	lcmfnnval	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to \underline{lcm} (Z) = inf (\{n \in ℕ \| \forall m \in Z m ∥ n\} ℝ <)$

Step	Hyp	Ref	Expression
1		id	$⊢ Z \subseteq ℕ \to Z \subseteq ℕ$
2		nnssz	$⊢ ℕ \subseteq ℤ$
3	1 2	sstrdi	$⊢ Z \subseteq ℕ \to Z \subseteq ℤ$
4	3	adantr	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to Z \subseteq ℤ$
5		simpr	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to Z \in Fin$
6		0nnn	$⊢ \neg 0 \in ℕ$
7	6	nelir	$⊢ 0 \notin ℕ$
8		ssel	$⊢ Z \subseteq ℕ \to (0 \in Z \to 0 \in ℕ)$
9	8	nelcon3d	$⊢ Z \subseteq ℕ \to (0 \notin ℕ \to 0 \notin Z)$
10	7 9	mpi	$⊢ Z \subseteq ℕ \to 0 \notin Z$
11	10	adantr	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to 0 \notin Z$
12		lcmfn0val	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \underline{lcm} (Z) = inf (\{n \in ℕ \| \forall m \in Z m ∥ n\} ℝ <)$
13	4 5 11 12	syl3anc	$⊢ (Z \subseteq ℕ \land Z \in Fin) \to \underline{lcm} (Z) = inf (\{n \in ℕ \| \forall m \in Z m ∥ n\} ℝ <)$

Metamath Proof Explorer