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 ∈ 𝒫 ℤ ⟼ if 0 ∈ z 0 inf n ∈ ℕ | ∀ m ∈ z m ∥ n ℝ <
2 eleq2 ⊢ z = Z → 0 ∈ z ↔ 0 ∈ Z
3 raleq ⊢ z = Z → ∀ m ∈ z m ∥ n ↔ ∀ m ∈ Z m ∥ n
4 3 rabbidv ⊢ z = Z → n ∈ ℕ | ∀ m ∈ z m ∥ n = n ∈ ℕ | ∀ m ∈ Z m ∥ n
5 4 infeq1d ⊢ z = Z → inf n ∈ ℕ | ∀ m ∈ z m ∥ n ℝ < = inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <
6 2 5 ifbieq2d ⊢ z = Z → if 0 ∈ z 0 inf n ∈ ℕ | ∀ m ∈ z m ∥ n ℝ < = if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <
7 iftrue ⊢ 0 ∈ Z → if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < = 0
8 7 adantl ⊢ Z ⊆ ℤ ∧ 0 ∈ Z → if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < = 0
9 6 8 sylan9eqr ⊢ Z ⊆ ℤ ∧ 0 ∈ Z ∧ z = Z → if 0 ∈ z 0 inf n ∈ ℕ | ∀ m ∈ z m ∥ 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