Metamath Proof Explorer

Theorem lcmfeq0b

Description: The least common multiple of a set of integers is 0 iff at least one of its element is 0. (Contributed by AV, 21-Aug-2020)

Ref Expression
Assertion lcmfeq0b ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → lcm _ ⁡ Z = 0 ↔ 0 ∈ Z

Proof

Step Hyp Ref Expression
1 df-nel ⊢ 0 ∉ Z ↔ ¬ 0 ∈ Z
2 lcmfn0cl ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ ℕ
3 2 nnne0d ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ≠ 0
4 3 3expia ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → 0 ∉ Z → lcm _ ⁡ Z ≠ 0
5 1 4 syl5bir ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → ¬ 0 ∈ Z → lcm _ ⁡ Z ≠ 0
6 5 necon4bd ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → lcm _ ⁡ Z = 0 → 0 ∈ Z
7 lcmf0val ⊢ Z ⊆ ℤ ∧ 0 ∈ Z → lcm _ ⁡ Z = 0
8 7 ex ⊢ Z ⊆ ℤ → 0 ∈ Z → lcm _ ⁡ Z = 0
9 8 adantr ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → 0 ∈ Z → lcm _ ⁡ Z = 0
10 6 9 impbid ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → lcm _ ⁡ Z = 0 ↔ 0 ∈ Z