Metamath Proof Explorer

Theorem lcmf0val

Description: The value, by convention, of the least common multiple for a set containing 0 is 0. (Contributed by AV, 21-Apr-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmf0val ⊢Z⊆ℤ∧0∈Z→lcm_⁡Z=0

Proof

Step Hyp Ref Expression
1 df-lcmf ⊢lcm_=z∈𝒫ℤ⟼if0∈z0supn∈ℕ|∀m∈zm∥nℝ<
2 eleq2 ⊢z=Z→0∈z↔0∈Z
3 raleq ⊢z=Z→∀m∈zm∥n↔∀m∈Zm∥n
4 3 rabbidv ⊢z=Z→n∈ℕ|∀m∈zm∥n=n∈ℕ|∀m∈Zm∥n
5 4 infeq1d ⊢z=Z→supn∈ℕ|∀m∈zm∥nℝ<=supn∈ℕ|∀m∈Zm∥nℝ<
6 2 5 ifbieq2d ⊢z=Z→if0∈z0supn∈ℕ|∀m∈zm∥nℝ<=if0∈Z0supn∈ℕ|∀m∈Zm∥nℝ<
7 iftrue ⊢0∈Z→if0∈Z0supn∈ℕ|∀m∈Zm∥nℝ<=0
8 7 adantl ⊢Z⊆ℤ∧0∈Z→if0∈Z0supn∈ℕ|∀m∈Zm∥nℝ<=0
9 6 8 sylan9eqr ⊢Z⊆ℤ∧0∈Z∧z=Z→if0∈z0supn∈ℕ|∀m∈zm∥nℝ<=0
10 zex ⊢ℤ∈V
11 10 ssex ⊢Z⊆ℤ→Z∈V
12 elpwg ⊢Z∈V→Z∈𝒫ℤ↔Z⊆ℤ
13 11 12 syl ⊢Z⊆ℤ→Z∈𝒫ℤ↔Z⊆ℤ
14 13 ibir ⊢Z⊆ℤ→Z∈𝒫ℤ
15 14 adantr ⊢Z⊆ℤ∧0∈Z→Z∈𝒫ℤ
16 simpr ⊢Z⊆ℤ∧0∈Z→0∈Z
17 1 9 15 16 fvmptd2 ⊢Z⊆ℤ∧0∈Z→lcm_⁡Z=0