Metamath Proof Explorer

Theorem lcmfval

Description: Value of the _lcm function. ( _lcmZ ) is the least common multiple of the integers contained in the finite subset of integers Z . If at least one of the elements of Z is 0 , the result is defined conventionally as 0 . (Contributed by AV, 21-Apr-2020) (Revised by AV, 16-Sep-2020)

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

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 zex ⊢ ℤ ∈ V
8 7 ssex ⊢ Z ⊆ ℤ → Z ∈ V
9 elpwg ⊢ Z ∈ V → Z ∈ 𝒫 ℤ ↔ Z ⊆ ℤ
10 8 9 syl ⊢ Z ⊆ ℤ → Z ∈ 𝒫 ℤ ↔ Z ⊆ ℤ
11 10 ibir ⊢ Z ⊆ ℤ → Z ∈ 𝒫 ℤ
12 11 adantr ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → Z ∈ 𝒫 ℤ
13 0nn0 ⊢ 0 ∈ ℕ 0
14 13 a1i ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∈ Z → 0 ∈ ℕ 0
15 df-nel ⊢ 0 ∉ Z ↔ ¬ 0 ∈ Z
16 ssrab2 ⊢ n ∈ ℕ | ∀ m ∈ Z m ∥ n ⊆ ℕ
17 nnssnn0 ⊢ ℕ ⊆ ℕ 0
18 16 17 sstri ⊢ n ∈ ℕ | ∀ m ∈ Z m ∥ n ⊆ ℕ 0
19 nnuz ⊢ ℕ = ℤ ≥ 1
20 16 19 sseqtri ⊢ n ∈ ℕ | ∀ m ∈ Z m ∥ n ⊆ ℤ ≥ 1
21 fissn0dvdsn0 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → n ∈ ℕ | ∀ m ∈ Z m ∥ n ≠ ∅
22 21 3expa ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → n ∈ ℕ | ∀ m ∈ Z m ∥ n ≠ ∅
23 infssuzcl ⊢ n ∈ ℕ | ∀ m ∈ Z m ∥ n ⊆ ℤ ≥ 1 ∧ n ∈ ℕ | ∀ m ∈ Z m ∥ n ≠ ∅ → inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < ∈ n ∈ ℕ | ∀ m ∈ Z m ∥ n
24 20 22 23 sylancr ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < ∈ n ∈ ℕ | ∀ m ∈ Z m ∥ n
25 18 24 sselid ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < ∈ ℕ 0
26 15 25 sylan2br ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ ¬ 0 ∈ Z → inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < ∈ ℕ 0
27 14 26 ifclda ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ < ∈ ℕ 0
28 1 6 12 27 fvmptd3 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → lcm _ ⁡ Z = if 0 ∈ Z 0 inf n ∈ ℕ | ∀ m ∈ Z m ∥ n ℝ <