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 ⊢ M ∈ ℤ → M lcm 0 = 0

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 lcmval ⊢ M ∈ ℤ ∧ 0 ∈ ℤ → M lcm 0 = if M = 0 ∨ 0 = 0 0 inf n ∈ ℕ | M ∥ n ∧ 0 ∥ n ℝ <
3 eqid ⊢ 0 = 0
4 3 olci ⊢ M = 0 ∨ 0 = 0
5 4 iftruei ⊢ if M = 0 ∨ 0 = 0 0 inf n ∈ ℕ | M ∥ n ∧ 0 ∥ n ℝ < = 0
6 2 5 eqtrdi ⊢ M ∈ ℤ ∧ 0 ∈ ℤ → M lcm 0 = 0
7 1 6 mpan2 ⊢ M ∈ ℤ → M lcm 0 = 0