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

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