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

Definition df-lcm 15497
Description: Define the lcm operator. For example, (6 lcm 9) = 18 (ex-lcm 27618). (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.)
Assertion
Ref Expression
df-lcm lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥𝑛𝑦𝑛)}, ℝ, < )))
Distinct variable group:   𝑥,𝑛,𝑦

Detailed syntax breakdown of Definition df-lcm
StepHypRef Expression
1 clcm 15495 . 2 class lcm
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cz 11561 . . 3 class
52cv 1623 . . . . . 6 class 𝑥
6 cc0 10120 . . . . . 6 class 0
75, 6wceq 1624 . . . . 5 wff 𝑥 = 0
83cv 1623 . . . . . 6 class 𝑦
98, 6wceq 1624 . . . . 5 wff 𝑦 = 0
107, 9wo 382 . . . 4 wff (𝑥 = 0 ∨ 𝑦 = 0)
11 vn . . . . . . . . 9 setvar 𝑛
1211cv 1623 . . . . . . . 8 class 𝑛
13 cdvds 15174 . . . . . . . 8 class
145, 12, 13wbr 4796 . . . . . . 7 wff 𝑥𝑛
158, 12, 13wbr 4796 . . . . . . 7 wff 𝑦𝑛
1614, 15wa 383 . . . . . 6 wff (𝑥𝑛𝑦𝑛)
17 cn 11204 . . . . . 6 class
1816, 11, 17crab 3046 . . . . 5 class {𝑛 ∈ ℕ ∣ (𝑥𝑛𝑦𝑛)}
19 cr 10119 . . . . 5 class
20 clt 10258 . . . . 5 class <
2118, 19, 20cinf 8504 . . . 4 class inf({𝑛 ∈ ℕ ∣ (𝑥𝑛𝑦𝑛)}, ℝ, < )
2210, 6, 21cif 4222 . . 3 class if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥𝑛𝑦𝑛)}, ℝ, < ))
232, 3, 4, 4, 22cmpt2 6807 . 2 class (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥𝑛𝑦𝑛)}, ℝ, < )))
241, 23wceq 1624 1 wff lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥𝑛𝑦𝑛)}, ℝ, < )))
Colors of variables: wff setvar class
This definition is referenced by:  lcmval  15499
  Copyright terms: Public domain W3C validator