Metamath Proof Explorer

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 
|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcm 
 |-  lcm
1 vx 
 |-  x
2 cz 
 |-  ZZ
3 vy 
 |-  y
4 1 cv 
 |-  x
5 cc0 
 |-  0
6 4 5 wceq 
 |-  x = 0
7 3 cv 
 |-  y
8 7 5 wceq 
 |-  y = 0
9 6 8 wo 
 |-  ( x = 0 \/ y = 0 )
10 vn 
 |-  n
11 cn 
 |-  NN
12 cdvds 
 |-  ||
13 10 cv 
 |-  n
14 4 13 12 wbr 
 |-  x || n
15 7 13 12 wbr 
 |-  y || n
16 14 15 wa 
 |-  ( x || n /\ y || n )
17 16 10 11 crab 
 |-  { n e. NN | ( x || n /\ y || n ) }
18 cr 
 |-  RR
19 clt 
 |-  <
20 17 18 19 cinf 
 |-  inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < )
21 9 5 20 cif 
 |-  if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) )
22 1 3 2 2 21 cmpo 
 |-  ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
23 0 22 wceq 
 |-  lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )