Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcmf 
 |-  _lcm
1 vz 
 |-  z
2 cz 
 |-  ZZ
3 2 cpw 
 |-  ~P ZZ
4 cc0 
 |-  0
5 1 cv 
 |-  z
6 4 5 wcel 
 |-  0 e. z
7 vn 
 |-  n
8 cn 
 |-  NN
9 vm 
 |-  m
10 9 cv 
 |-  m
11 cdvds 
 |-  ||
12 7 cv 
 |-  n
13 10 12 11 wbr 
 |-  m || n
14 13 9 5 wral 
 |-  A. m e. z m || n
15 14 7 8 crab 
 |-  { n e. NN | A. m e. z m || n }
16 cr 
 |-  RR
17 clt 
 |-  <
18 15 16 17 cinf 
 |-  inf ( { n e. NN | A. m e. z m || n } , RR , < )
19 6 4 18 cif 
 |-  if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) )
20 1 3 19 cmpt 
 |-  ( z e. ~P ZZ |-> if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) ) )
21 0 20 wceq 
 |-  _lcm = ( z e. ~P ZZ |-> if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) ) )