Definition df-lcmf 16567

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

Step	Hyp	Ref	Expression
1		clcmf 16565	. 2 class lcm
2		vz	. . 3 setvar 𝑧
3		cz 12545	. . . 4 class ℤ
4	3	cpw 4571	. . 3 class 𝒫 ℤ
5		cc0 11086	. . . . 5 class 0
6	2	cv 1539	. . . . 5 class 𝑧
7	5, 6	wcel 2109	. . . 4 wff 0 ∈ 𝑧
8		vm	. . . . . . . . 9 setvar 𝑚
9	8	cv 1539	. . . . . . . 8 class 𝑚
10		vn	. . . . . . . . 9 setvar 𝑛
11	10	cv 1539	. . . . . . . 8 class 𝑛
12		cdvds 16229	. . . . . . . 8 class ∥
13	9, 11, 12	wbr 5115	. . . . . . 7 wff 𝑚 ∥ 𝑛
14	13, 8, 6	wral 3046	. . . . . 6 wff ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛
15		cn 12197	. . . . . 6 class ℕ
16	14, 10, 15	crab 3411	. . . . 5 class {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}
17		cr 11085	. . . . 5 class ℝ
18		clt 11226	. . . . 5 class <
19	16, 17, 18	cinf 9410	. . . 4 class inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < )
20	7, 5, 19	cif 4496	. . 3 class if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < ))
21	2, 4, 20	cmpt 5196	. 2 class (𝑧 ∈ 𝒫 ℤ ↦ if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < )))
22	1, 21	wceq 1540	1 wff lcm = (𝑧 ∈ 𝒫 ℤ ↦ if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < )))

This definition is referenced by:  lcmfval  16597  lcmf0val  16598