This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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