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\in \mathbb{Z}\to M\mathrm{lcm}0=0$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		lcmval	$$⊢\left(M\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to M\mathrm{lcm}0=if\left(\left(M=0\vee 0=0\right),0,sup\left(\left\{n\in \mathbb{N}|\left(M\parallel n\wedge 0\parallel n\right)\right\},ℝ,<\right)\right)$$
3		eqid	$$⊢0=0$$
4	3	olci	$$⊢\left(M=0\vee 0=0\right)$$
5	4	iftruei	$$⊢if\left(\left(M=0\vee 0=0\right),0,sup\left(\left\{n\in \mathbb{N}|\left(M\parallel n\wedge 0\parallel n\right)\right\},ℝ,<\right)\right)=0$$
6	2 5	eqtrdi	$$⊢\left(M\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to M\mathrm{lcm}0=0$$
7	1 6	mpan2	$$⊢M\in \mathbb{Z}\to M\mathrm{lcm}0=0$$