This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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