This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ lcm = x ∈ ℤ , y ∈ ℤ ⟼ if x = 0 ∨ y = 0 0 inf n ∈ ℕ | x ∥ n ∧ y ∥ n ℝ <

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcm class 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 x = 0 ∨ y = 0
10 vn setvar n
11 cn class ℕ
12 cdvds class ∥
13 10 cv setvar n
14 4 13 12 wbr wff x ∥ n
15 7 13 12 wbr wff y ∥ n
16 14 15 wa wff x ∥ n ∧ y ∥ n
17 16 10 11 crab class n ∈ ℕ | x ∥ n ∧ y ∥ n
18 cr class ℝ
19 clt class <
20 17 18 19 cinf class inf n ∈ ℕ | x ∥ n ∧ y ∥ n ℝ <
21 9 5 20 cif class if x = 0 ∨ y = 0 0 inf n ∈ ℕ | x ∥ n ∧ y ∥ n ℝ <
22 1 3 2 2 21 cmpo class x ∈ ℤ , y ∈ ℤ ⟼ if x = 0 ∨ y = 0 0 inf n ∈ ℕ | x ∥ n ∧ y ∥ n ℝ <
23 0 22 wceq wff lcm = x ∈ ℤ , y ∈ ℤ ⟼ if x = 0 ∨ y = 0 0 inf n ∈ ℕ | x ∥ n ∧ y ∥ n ℝ <