Definition df-lcm

Description: Define the lcm operator. For example, ( 6 lcm 9 ) = 1 8 ( ex-lcm ). (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 16-Sep-2020)

	Ref	Expression
Assertion	df-lcm	$$⊢\mathrm{lcm}=\left(x\in \mathbb{Z},y\in \mathbb{Z}⟼if\left(\left(x=0\vee y=0\right),0,inf\left(\left\{n\in \mathbb{N}|\left(x\parallel n\wedge y\parallel n\right)\right\},ℝ,<\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clcm	$$class\mathrm{lcm}$$
1		vx	$$setvarx$$
2		cz	$$class\mathbb{Z}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5		cc0	$$class0$$
6	4 5	wceq	$$wffx=0$$
7	3	cv	$$setvary$$
8	7 5	wceq	$$wffy=0$$
9	6 8	wo	$$wff\left(x=0\vee y=0\right)$$
10		vn	$$setvarn$$
11		cn	$$class\mathbb{N}$$
12		cdvds	$$class\parallel$$
13	10	cv	$$setvarn$$
14	4 13 12	wbr	$$wffx\parallel n$$
15	7 13 12	wbr	$$wffy\parallel n$$
16	14 15	wa	$$wff\left(x\parallel n\wedge y\parallel n\right)$$
17	16 10 11	crab	$$class\left\{n\in \mathbb{N}|\left(x\parallel n\wedge y\parallel n\right)\right\}$$
18		cr	$$classℝ$$
19		clt	$$class<$$
20	17 18 19	cinf	$$classinf\left(\left\{n\in \mathbb{N}|\left(x\parallel n\wedge y\parallel n\right)\right\},ℝ,<\right)$$
21	9 5 20	cif	$$classif\left(\left(x=0\vee y=0\right),0,inf\left(\left\{n\in \mathbb{N}|\left(x\parallel n\wedge y\parallel n\right)\right\},ℝ,<\right)\right)$$
22	1 3 2 2 21	cmpo	$$class\left(x\in \mathbb{Z},y\in \mathbb{Z}⟼if\left(\left(x=0\vee y=0\right),0,inf\left(\left\{n\in \mathbb{N}|\left(x\parallel n\wedge y\parallel n\right)\right\},ℝ,<\right)\right)\right)$$
23	0 22	wceq	$$wff\mathrm{lcm}=\left(x\in \mathbb{Z},y\in \mathbb{Z}⟼if\left(\left(x=0\vee y=0\right),0,inf\left(\left\{n\in \mathbb{N}|\left(x\parallel n\wedge y\parallel n\right)\right\},ℝ,<\right)\right)\right)$$