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=if0∈Z0supn∈ℕ|∀m∈Zm∥nℝ<

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 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∈Zm∥n⊆ℕ
17 nnssnn0 ⊢ℕ⊆ℕ0
18 16 17 sstri ⊢n∈ℕ|∀m∈Zm∥n⊆ℕ0
19 nnuz ⊢ℕ=ℤ≥1
20 16 19 sseqtri ⊢n∈ℕ|∀m∈Zm∥n⊆ℤ≥1
21 fissn0dvdsn0 ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→n∈ℕ|∀m∈Zm∥n≠∅
22 21 3expa ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→n∈ℕ|∀m∈Zm∥n≠∅
23 infssuzcl ⊢n∈ℕ|∀m∈Zm∥n⊆ℤ≥1∧n∈ℕ|∀m∈Zm∥n≠∅→supn∈ℕ|∀m∈Zm∥nℝ<∈n∈ℕ|∀m∈Zm∥n
24 20 22 23 sylancr ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→supn∈ℕ|∀m∈Zm∥nℝ<∈n∈ℕ|∀m∈Zm∥n
25 18 24 sselid ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→supn∈ℕ|∀m∈Zm∥nℝ<∈ℕ0
26 15 25 sylan2br ⊢Z⊆ℤ∧Z∈Fin∧¬0∈Z→supn∈ℕ|∀m∈Zm∥nℝ<∈ℕ0
27 14 26 ifclda ⊢Z⊆ℤ∧Z∈Fin→if0∈Z0supn∈ℕ|∀m∈Zm∥nℝ<∈ℕ0
28 1 6 12 27 fvmptd3 ⊢Z⊆ℤ∧Z∈Fin→lcm_⁡Z=if0∈Z0supn∈ℕ|∀m∈Zm∥nℝ<