# 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 ${⊢}\mathrm{lcm}=\left({x}\in ℤ,{y}\in ℤ⟼if\left(\left({x}=0\vee {y}=0\right),0,sup\left(\left\{{n}\in ℕ|\left({x}\parallel {n}\wedge {y}\parallel {n}\right)\right\},ℝ,<\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 clcm ${class}\mathrm{lcm}$
1 vx ${setvar}{x}$
2 cz ${class}ℤ$
3 vy ${setvar}{y}$
4 1 cv ${setvar}{x}$
5 cc0 ${class}0$
6 4 5 wceq ${wff}{x}=0$
7 3 cv ${setvar}{y}$
8 7 5 wceq ${wff}{y}=0$
9 6 8 wo ${wff}\left({x}=0\vee {y}=0\right)$
10 vn ${setvar}{n}$
11 cn ${class}ℕ$
12 cdvds ${class}\parallel$
13 10 cv ${setvar}{n}$
14 4 13 12 wbr ${wff}{x}\parallel {n}$
15 7 13 12 wbr ${wff}{y}\parallel {n}$
16 14 15 wa ${wff}\left({x}\parallel {n}\wedge {y}\parallel {n}\right)$
17 16 10 11 crab ${class}\left\{{n}\in ℕ|\left({x}\parallel {n}\wedge {y}\parallel {n}\right)\right\}$
18 cr ${class}ℝ$
19 clt ${class}<$
20 17 18 19 cinf ${class}sup\left(\left\{{n}\in ℕ|\left({x}\parallel {n}\wedge {y}\parallel {n}\right)\right\},ℝ,<\right)$
21 9 5 20 cif ${class}if\left(\left({x}=0\vee {y}=0\right),0,sup\left(\left\{{n}\in ℕ|\left({x}\parallel {n}\wedge {y}\parallel {n}\right)\right\},ℝ,<\right)\right)$
22 1 3 2 2 21 cmpo ${class}\left({x}\in ℤ,{y}\in ℤ⟼if\left(\left({x}=0\vee {y}=0\right),0,sup\left(\left\{{n}\in ℕ|\left({x}\parallel {n}\wedge {y}\parallel {n}\right)\right\},ℝ,<\right)\right)\right)$
23 0 22 wceq ${wff}\mathrm{lcm}=\left({x}\in ℤ,{y}\in ℤ⟼if\left(\left({x}=0\vee {y}=0\right),0,sup\left(\left\{{n}\in ℕ|\left({x}\parallel {n}\wedge {y}\parallel {n}\right)\right\},ℝ,<\right)\right)\right)$