Database
ELEMENTARY NUMBER THEORY
Elementary properties of divisibility
The least common multiple
lcm0val
Metamath Proof Explorer
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 sup 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 sup 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