Metamath Proof Explorer


Theorem lcm0val

Description: The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcm0val ( 𝑀 ∈ ℤ → ( 𝑀 lcm 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 0z 0 ∈ ℤ
2 lcmval ( ( 𝑀 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝑀 lcm 0 ) = if ( ( 𝑀 = 0 ∨ 0 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀𝑛 ∧ 0 ∥ 𝑛 ) } , ℝ , < ) ) )
3 eqid 0 = 0
4 3 olci ( 𝑀 = 0 ∨ 0 = 0 )
5 4 iftruei if ( ( 𝑀 = 0 ∨ 0 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀𝑛 ∧ 0 ∥ 𝑛 ) } , ℝ , < ) ) = 0
6 2 5 eqtrdi ( ( 𝑀 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝑀 lcm 0 ) = 0 )
7 1 6 mpan2 ( 𝑀 ∈ ℤ → ( 𝑀 lcm 0 ) = 0 )