Metamath Proof Explorer


Theorem lcmeq0

Description: The lcm of two integers is zero iff either is zero. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion lcmeq0 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) = 0 ↔ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 lcmn0cl ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ )
2 1 nnne0d ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) ≠ 0 )
3 2 ex ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) → ( 𝑀 lcm 𝑁 ) ≠ 0 ) )
4 3 necon4bd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) = 0 → ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) )
5 oveq1 ( 𝑀 = 0 → ( 𝑀 lcm 𝑁 ) = ( 0 lcm 𝑁 ) )
6 0z 0 ∈ ℤ
7 lcmcom ( ( 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝑁 lcm 0 ) = ( 0 lcm 𝑁 ) )
8 6 7 mpan2 ( 𝑁 ∈ ℤ → ( 𝑁 lcm 0 ) = ( 0 lcm 𝑁 ) )
9 lcm0val ( 𝑁 ∈ ℤ → ( 𝑁 lcm 0 ) = 0 )
10 8 9 eqtr3d ( 𝑁 ∈ ℤ → ( 0 lcm 𝑁 ) = 0 )
11 5 10 sylan9eqr ( ( 𝑁 ∈ ℤ ∧ 𝑀 = 0 ) → ( 𝑀 lcm 𝑁 ) = 0 )
12 11 adantll ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝑀 lcm 𝑁 ) = 0 )
13 oveq2 ( 𝑁 = 0 → ( 𝑀 lcm 𝑁 ) = ( 𝑀 lcm 0 ) )
14 lcm0val ( 𝑀 ∈ ℤ → ( 𝑀 lcm 0 ) = 0 )
15 13 14 sylan9eqr ( ( 𝑀 ∈ ℤ ∧ 𝑁 = 0 ) → ( 𝑀 lcm 𝑁 ) = 0 )
16 15 adantlr ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( 𝑀 lcm 𝑁 ) = 0 )
17 12 16 jaodan ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) = 0 )
18 17 ex ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) → ( 𝑀 lcm 𝑁 ) = 0 ) )
19 4 18 impbid ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) = 0 ↔ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) )