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 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = 0 ↔ M = 0 ∨ N = 0

Proof

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