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

Proof

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