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 ∈ ℤ → M gcd N ∥ M lcm N

Proof

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