ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-lcm Unicode version

Definition df-lcm 10925
Description: Define the lcm operator. For example,  ( 6 lcm  9 )  =  1 8. (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 10924 . 2  class lcm
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cz 8683 . . 3  class  ZZ
52cv 1286 . . . . . 6  class  x
6 cc0 7294 . . . . . 6  class  0
75, 6wceq 1287 . . . . 5  wff  x  =  0
83cv 1286 . . . . . 6  class  y
98, 6wceq 1287 . . . . 5  wff  y  =  0
107, 9wo 662 . . . 4  wff  ( x  =  0  \/  y  =  0 )
11 vn . . . . . . . . 9  setvar  n
1211cv 1286 . . . . . . . 8  class  n
13 cdvds 10678 . . . . . . . 8  class  ||
145, 12, 13wbr 3820 . . . . . . 7  wff  x  ||  n
158, 12, 13wbr 3820 . . . . . . 7  wff  y  ||  n
1614, 15wa 102 . . . . . 6  wff  ( x 
||  n  /\  y  ||  n )
17 cn 8357 . . . . . 6  class  NN
1816, 11, 17crab 2359 . . . . 5  class  { n  e.  NN  |  ( x 
||  n  /\  y  ||  n ) }
19 cr 7293 . . . . 5  class  RR
20 clt 7466 . . . . 5  class  <
2118, 19, 20cinf 6622 . . . 4  class inf ( { n  e.  NN  | 
( x  ||  n  /\  y  ||  n ) } ,  RR ,  <  )
2210, 6, 21cif 3379 . . 3  class  if ( ( x  =  0  \/  y  =  0 ) ,  0 , inf ( { n  e.  NN  |  ( x 
||  n  /\  y  ||  n ) } ,  RR ,  <  ) )
232, 3, 4, 4, 22cmpt2 5615 . 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 1287 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 set class
This definition is referenced by:  lcmval  10927
  Copyright terms: Public domain W3C validator