MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lcm Structured version   Visualization version   Unicode version

Definition df-lcm 14630
Description: Define the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.)
Assertion
Ref Expression
df-lcm  |- lcm  =  ( x  e.  ZZ , 
y  e.  ZZ  |->  if ( ( x  =  0  \/  y  =  0 ) ,  0 , inf ( { n  e.  NN  |  ( x 
||  n  /\  y  ||  n ) } ,  RR ,  <  ) ) )
Distinct variable group:    x, n, y

Detailed syntax breakdown of Definition df-lcm
StepHypRef Expression
1 clcm 14626 . 2  class lcm
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cz 10961 . . 3  class  ZZ
52cv 1451 . . . . . 6  class  x
6 cc0 9557 . . . . . 6  class  0
75, 6wceq 1452 . . . . 5  wff  x  =  0
83cv 1451 . . . . . 6  class  y
98, 6wceq 1452 . . . . 5  wff  y  =  0
107, 9wo 375 . . . 4  wff  ( x  =  0  \/  y  =  0 )
11 vn . . . . . . . . 9  setvar  n
1211cv 1451 . . . . . . . 8  class  n
13 cdvds 14382 . . . . . . . 8  class  ||
145, 12, 13wbr 4395 . . . . . . 7  wff  x  ||  n
158, 12, 13wbr 4395 . . . . . . 7  wff  y  ||  n
1614, 15wa 376 . . . . . 6  wff  ( x 
||  n  /\  y  ||  n )
17 cn 10631 . . . . . 6  class  NN
1816, 11, 17crab 2760 . . . . 5  class  { n  e.  NN  |  ( x 
||  n  /\  y  ||  n ) }
19 cr 9556 . . . . 5  class  RR
20 clt 9693 . . . . 5  class  <
2118, 19, 20cinf 7973 . . . 4  class inf ( { n  e.  NN  | 
( x  ||  n  /\  y  ||  n ) } ,  RR ,  <  )
2210, 6, 21cif 3872 . . 3  class  if ( ( x  =  0  \/  y  =  0 ) ,  0 , inf ( { n  e.  NN  |  ( x 
||  n  /\  y  ||  n ) } ,  RR ,  <  ) )
232, 3, 4, 4, 22cmpt2 6310 . 2  class  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  \/  y  =  0 ) ,  0 , inf ( { n  e.  NN  |  ( x 
||  n  /\  y  ||  n ) } ,  RR ,  <  ) ) )
241, 23wceq 1452 1  wff lcm  =  ( x  e.  ZZ , 
y  e.  ZZ  |->  if ( ( x  =  0  \/  y  =  0 ) ,  0 , inf ( { n  e.  NN  |  ( x 
||  n  /\  y  ||  n ) } ,  RR ,  <  ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  lcmval  14634
  Copyright terms: Public domain W3C validator