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 )