Metamath Proof Explorer


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 ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } , ℝ , < ) )