Definition df-lcmf

Description: Define the _lcm function on a set of integers. (Contributed by AV, 21-Aug-2020) (Revised by AV, 16-Sep-2020)

	Ref	Expression
Assertion	df-lcmf	$$⊢\underset{\_}{\mathrm{lcm}}=\left(z\in 𝒫\mathbb{Z}⟼if\left(0\in z,0,sup\left(\left\{n\in \mathbb{N}|\forall m\in zm\parallel n\right\},ℝ,<\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clcmf	$$class\underset{\_}{\mathrm{lcm}}$$
1		vz	$$setvarz$$
2		cz	$$class\mathbb{Z}$$
3	2	cpw	$$class𝒫\mathbb{Z}$$
4		cc0	$$class0$$
5	1	cv	$$setvarz$$
6	4 5	wcel	$$wff0\in z$$
7		vn	$$setvarn$$
8		cn	$$class\mathbb{N}$$
9		vm	$$setvarm$$
10	9	cv	$$setvarm$$
11		cdvds	$$class\parallel$$
12	7	cv	$$setvarn$$
13	10 12 11	wbr	$$wffm\parallel n$$
14	13 9 5	wral	$$wff\forall m\in zm\parallel n$$
15	14 7 8	crab	$$class\left\{n\in \mathbb{N}|\forall m\in zm\parallel n\right\}$$
16		cr	$$classℝ$$
17		clt	$$class<$$
18	15 16 17	cinf	$$classsup\left(\left\{n\in \mathbb{N}|\forall m\in zm\parallel n\right\},ℝ,<\right)$$
19	6 4 18	cif	$$classif\left(0\in z,0,sup\left(\left\{n\in \mathbb{N}|\forall m\in zm\parallel n\right\},ℝ,<\right)\right)$$
20	1 3 19	cmpt	$$class\left(z\in 𝒫\mathbb{Z}⟼if\left(0\in z,0,sup\left(\left\{n\in \mathbb{N}|\forall m\in zm\parallel n\right\},ℝ,<\right)\right)\right)$$
21	0 20	wceq	$$wff\underset{\_}{\mathrm{lcm}}=\left(z\in 𝒫\mathbb{Z}⟼if\left(0\in z,0,sup\left(\left\{n\in \mathbb{N}|\forall m\in zm\parallel n\right\},ℝ,<\right)\right)\right)$$