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

Definition df-lcm 11798
 Description: Define the lcm operator. For example, lcm . (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 11797 . 2 lcm
2 vx . . 3
3 vy . . 3
4 cz 9098 . . 3
52cv 1331 . . . . . 6
6 cc0 7664 . . . . . 6
75, 6wceq 1332 . . . . 5
83cv 1331 . . . . . 6
98, 6wceq 1332 . . . . 5
107, 9wo 698 . . . 4
11 vn . . . . . . . . 9
1211cv 1331 . . . . . . . 8
13 cdvds 11549 . . . . . . . 8
145, 12, 13wbr 3938 . . . . . . 7
158, 12, 13wbr 3938 . . . . . . 7
1614, 15wa 103 . . . . . 6
17 cn 8764 . . . . . 6
1816, 11, 17crab 2421 . . . . 5
19 cr 7663 . . . . 5
20 clt 7844 . . . . 5
2118, 19, 20cinf 6880 . . . 4 inf
2210, 6, 21cif 3480 . . 3 inf
232, 3, 4, 4, 22cmpo 5785 . 2 inf
241, 23wceq 1332 1 lcm inf
 Colors of variables: wff set class This definition is referenced by:  lcmval  11800
 Copyright terms: Public domain W3C validator