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

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 ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ( lcm ‘ 𝑍 ) = 0 ↔ 0 ∈ 𝑍 ) )

Proof

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