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 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