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 ⊢ lcm _ = z ∈ 𝒫 ℤ ⟼ if 0 ∈ z 0 sup n ∈ ℕ | ∀ m ∈ z m ∥ n ℝ <

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcmf class 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 ∈ z
7 vn setvar n
8 cn class ℕ
9 vm setvar m
10 9 cv setvar m
11 cdvds class ∥
12 7 cv setvar n
13 10 12 11 wbr wff m ∥ n
14 13 9 5 wral wff ∀ m ∈ z m ∥ n
15 14 7 8 crab class n ∈ ℕ | ∀ m ∈ z m ∥ n
16 cr class ℝ
17 clt class <
18 15 16 17 cinf class sup n ∈ ℕ | ∀ m ∈ z m ∥ n ℝ <
19 6 4 18 cif class if 0 ∈ z 0 sup n ∈ ℕ | ∀ m ∈ z m ∥ n ℝ <
20 1 3 19 cmpt class z ∈ 𝒫 ℤ ⟼ if 0 ∈ z 0 sup n ∈ ℕ | ∀ m ∈ z m ∥ n ℝ <
21 0 20 wceq wff lcm _ = z ∈ 𝒫 ℤ ⟼ if 0 ∈ z 0 sup n ∈ ℕ | ∀ m ∈ z m ∥ n ℝ <