Metamath Proof Explorer

Theorem gcddvdslcm

Description: The greatest common divisor of two numbers divides their least common multiple. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion gcddvdslcm ⊢M∈ℤ∧N∈ℤ→MgcdN∥MlcmN

Proof

Step Hyp Ref Expression
1 gcdcl ⊢M∈ℤ∧N∈ℤ→MgcdN∈ℕ0
2 1 nn0zd ⊢M∈ℤ∧N∈ℤ→MgcdN∈ℤ
3 simpl ⊢M∈ℤ∧N∈ℤ→M∈ℤ
4 lcmcl ⊢M∈ℤ∧N∈ℤ→MlcmN∈ℕ0
5 4 nn0zd ⊢M∈ℤ∧N∈ℤ→MlcmN∈ℤ
6 gcddvds ⊢M∈ℤ∧N∈ℤ→MgcdN∥M∧MgcdN∥N
7 6 simpld ⊢M∈ℤ∧N∈ℤ→MgcdN∥M
8 dvdslcm ⊢M∈ℤ∧N∈ℤ→M∥MlcmN∧N∥MlcmN
9 8 simpld ⊢M∈ℤ∧N∈ℤ→M∥MlcmN
10 2 3 5 7 9 dvdstrd ⊢M∈ℤ∧N∈ℤ→MgcdN∥MlcmN