MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lcmf Structured version   Visualization version   GIF version

Definition df-lcmf 15925
Description: Define the lcm function on a set of integers. (Contributed by AV, 21-Aug-2020.) (Revised by AV, 16-Sep-2020.)
Assertion
Ref Expression
df-lcmf lcm = (𝑧 ∈ 𝒫 ℤ ↦ if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚𝑧 𝑚𝑛}, ℝ, < )))
Distinct variable group:   𝑚,𝑛,𝑧

Detailed syntax breakdown of Definition df-lcmf
StepHypRef Expression
1 clcmf 15923 . 2 class lcm
2 vz . . 3 setvar 𝑧
3 cz 11970 . . . 4 class
43cpw 4542 . . 3 class 𝒫 ℤ
5 cc0 10526 . . . . 5 class 0
62cv 1529 . . . . 5 class 𝑧
75, 6wcel 2107 . . . 4 wff 0 ∈ 𝑧
8 vm . . . . . . . . 9 setvar 𝑚
98cv 1529 . . . . . . . 8 class 𝑚
10 vn . . . . . . . . 9 setvar 𝑛
1110cv 1529 . . . . . . . 8 class 𝑛
12 cdvds 15597 . . . . . . . 8 class
139, 11, 12wbr 5063 . . . . . . 7 wff 𝑚𝑛
1413, 8, 6wral 3143 . . . . . 6 wff 𝑚𝑧 𝑚𝑛
15 cn 11627 . . . . . 6 class
1614, 10, 15crab 3147 . . . . 5 class {𝑛 ∈ ℕ ∣ ∀𝑚𝑧 𝑚𝑛}
17 cr 10525 . . . . 5 class
18 clt 10664 . . . . 5 class <
1916, 17, 18cinf 8894 . . . 4 class inf({𝑛 ∈ ℕ ∣ ∀𝑚𝑧 𝑚𝑛}, ℝ, < )
207, 5, 19cif 4470 . . 3 class if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚𝑧 𝑚𝑛}, ℝ, < ))
212, 4, 20cmpt 5143 . 2 class (𝑧 ∈ 𝒫 ℤ ↦ if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚𝑧 𝑚𝑛}, ℝ, < )))
221, 21wceq 1530 1 wff lcm = (𝑧 ∈ 𝒫 ℤ ↦ if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚𝑧 𝑚𝑛}, ℝ, < )))
Colors of variables: wff setvar class
This definition is referenced by:  lcmfval  15955  lcmf0val  15956
  Copyright terms: Public domain W3C validator