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