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 ( { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) ) )