Definition df-lcmf 15304

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 = ( z e. ~P ZZ |-> if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) ) )

Distinct variable group:   m, n, z

Detailed syntax breakdown of Definition df-lcmf

Step	Hyp	Ref	Expression
1		clcmf 15302	. 2 class lcm
2		vz	. . 3 setvar z
3		cz 11377	. . . 4 class ZZ
4	3	cpw 4158	. . 3 class ~P ZZ
5		cc0 9936	. . . . 5 class 0
6	2	cv 1482	. . . . 5 class z
7	5, 6	wcel 1990	. . . 4 wff 0 e. z
8		vm	. . . . . . . . 9 setvar m
9	8	cv 1482	. . . . . . . 8 class m
10		vn	. . . . . . . . 9 setvar n
11	10	cv 1482	. . . . . . . 8 class n
12		cdvds 14983	. . . . . . . 8 class ||
13	9, 11, 12	wbr 4653	. . . . . . 7 wff m || n
14	13, 8, 6	wral 2912	. . . . . 6 wff A. m e. z m || n
15		cn 11020	. . . . . 6 class NN
16	14, 10, 15	crab 2916	. . . . 5 class { n e. NN | A. m e. z m || n }
17		cr 9935	. . . . 5 class RR
18		clt 10074	. . . . 5 class <
19	16, 17, 18	cinf 8347	. . . 4 class inf ( { n e. NN | A. m e. z m || n } , RR , < )
20	7, 5, 19	cif 4086	. . 3 class if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) )
21	2, 4, 20	cmpt 4729	. 2 class ( z e. ~P ZZ |-> if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) ) )
22	1, 21	wceq 1483	1 wff lcm = ( z e. ~P ZZ |-> if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) ) )

This definition is referenced by:  lcmfval  15334  lcmf0val  15335