Metamath Proof Explorer

Theorem lcmfn0val

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

Ref Expression
Assertion lcmfn0val ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z = inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <

Proof

Step Hyp Ref Expression
1 lcmfval ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → lcm _ ⁡ Z = if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <
2 1 3adant3 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z = if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <
3 df-nel ⊢ 0 ∉ Z ↔ ¬ 0 ∈ Z
4 iffalse ⊢ ¬ 0 ∈ Z → if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < = inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <
5 3 4 sylbi ⊢ 0 ∉ Z → if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < = inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <
6 5 3ad2ant3 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < = inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <
7 2 6 eqtrd ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z = inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <