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 inf
Distinct variable group:   ,,

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