Theorem 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	⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) = inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑍 ⊆ ℕ → 𝑍 ⊆ ℕ )
2		nnssz	⊢ ℕ ⊆ ℤ
3	1 2	sstrdi	⊢ ( 𝑍 ⊆ ℕ → 𝑍 ⊆ ℤ )
4	3	adantr	⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → 𝑍 ⊆ ℤ )
5		simpr	⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → 𝑍 ∈ Fin )
6		0nnn	⊢ ¬ 0 ∈ ℕ
7	6	nelir	⊢ 0 ∉ ℕ
8		ssel	⊢ ( 𝑍 ⊆ ℕ → ( 0 ∈ 𝑍 → 0 ∈ ℕ ) )
9	8	nelcon3d	⊢ ( 𝑍 ⊆ ℕ → ( 0 ∉ ℕ → 0 ∉ 𝑍 ) )
10	7 9	mpi	⊢ ( 𝑍 ⊆ ℕ → 0 ∉ 𝑍 )
11	10	adantr	⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → 0 ∉ 𝑍 )
12		lcmfn0val	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm ‘ 𝑍 ) = inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) )
13	4 5 11 12	syl3anc	⊢ ( ( 𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) = inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) )