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 = ( 𝑧 ∈ 𝒫 ℤ ↦ if ( 0 ∈ 𝑧 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } , ℝ , < ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clcmf	⊢ lcm
1		vz	⊢ 𝑧
2		cz	⊢ ℤ
3	2	cpw	⊢ 𝒫 ℤ
4		cc0	⊢ 0
5	1	cv	⊢ 𝑧
6	4 5	wcel	⊢ 0 ∈ 𝑧
7		vn	⊢ 𝑛
8		cn	⊢ ℕ
9		vm	⊢ 𝑚
10	9	cv	⊢ 𝑚
11		cdvds	⊢ ∥
12	7	cv	⊢ 𝑛
13	10 12 11	wbr	⊢ 𝑚 ∥ 𝑛
14	13 9 5	wral	⊢ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛
15	14 7 8	crab	⊢ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 }
16		cr	⊢ ℝ
17		clt	⊢ <
18	15 16 17	cinf	⊢ inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } , ℝ , < )
19	6 4 18	cif	⊢ if ( 0 ∈ 𝑧 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } , ℝ , < ) )
20	1 3 19	cmpt	⊢ ( 𝑧 ∈ 𝒫 ℤ ↦ if ( 0 ∈ 𝑧 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } , ℝ , < ) ) )
21	0 20	wceq	⊢ lcm = ( 𝑧 ∈ 𝒫 ℤ ↦ if ( 0 ∈ 𝑧 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } , ℝ , < ) ) )