# Metamath Proof Explorer

## Definition df-lcmf

Description: Define the _lcm function on a set of integers. (Contributed by AV, 21-Aug-2020) (Revised by AV, 16-Sep-2020)

Ref Expression
Assertion df-lcmf ${⊢}\underset{_}{\mathrm{lcm}}=\left({z}\in 𝒫ℤ⟼if\left(0\in {z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 clcmf ${class}\underset{_}{\mathrm{lcm}}$
1 vz ${setvar}{z}$
2 cz ${class}ℤ$
3 2 cpw ${class}𝒫ℤ$
4 cc0 ${class}0$
5 1 cv ${setvar}{z}$
6 4 5 wcel ${wff}0\in {z}$
7 vn ${setvar}{n}$
8 cn ${class}ℕ$
9 vm ${setvar}{m}$
10 9 cv ${setvar}{m}$
11 cdvds ${class}\parallel$
12 7 cv ${setvar}{n}$
13 10 12 11 wbr ${wff}{m}\parallel {n}$
14 13 9 5 wral ${wff}\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}$
15 14 7 8 crab ${class}\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\}$
16 cr ${class}ℝ$
17 clt ${class}<$
18 15 16 17 cinf ${class}sup\left(\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)$
19 6 4 18 cif ${class}if\left(0\in {z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)$
20 1 3 19 cmpt ${class}\left({z}\in 𝒫ℤ⟼if\left(0\in {z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)\right)$
21 0 20 wceq ${wff}\underset{_}{\mathrm{lcm}}=\left({z}\in 𝒫ℤ⟼if\left(0\in {z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)\right)$