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