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 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcm ⊢ lcm
1 vx ⊢ 𝑥
2 cz ⊢ ℤ
3 vy ⊢ 𝑦
4 1 cv ⊢ 𝑥
5 cc0 ⊢ 0
6 4 5 wceq ⊢ 𝑥 = 0
7 3 cv ⊢ 𝑦
8 7 5 wceq ⊢ 𝑦 = 0
9 6 8 wo ⊢ ( 𝑥 = 0 ∨ 𝑦 = 0 )
10 vn ⊢ 𝑛
11 cn ⊢ ℕ
12 cdvds ⊢ ∥
13 10 cv ⊢ 𝑛
14 4 13 12 wbr ⊢ 𝑥 ∥ 𝑛
15 7 13 12 wbr ⊢ 𝑦 ∥ 𝑛
16 14 15 wa ⊢ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 )
17 16 10 11 crab ⊢ { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) }
18 cr ⊢ ℝ
19 clt ⊢ <
20 17 18 19 cinf ⊢ inf ( { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < )
21 9 5 20 cif ⊢ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) )
22 1 3 2 2 21 cmpo ⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) ) )
23 0 22 wceq ⊢ lcm = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) ) )