Metamath Proof Explorer

Theorem lcmgcdnn

Description: The product of two positive integers' least common multiple and greatest common divisor is the product of the two integers. (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion lcmgcdnn ⊢ M ∈ ℕ ∧ N ∈ ℕ → M lcm N ⁢ M gcd N = M ⋅ N

Proof

Step Hyp Ref Expression
1 nnz ⊢ M ∈ ℕ → M ∈ ℤ
2 nnz ⊢ N ∈ ℕ → N ∈ ℤ
3 lcmgcd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N ⁢ M gcd N = M ⋅ N
4 1 2 3 syl2an ⊢ M ∈ ℕ ∧ N ∈ ℕ → M lcm N ⁢ M gcd N = M ⋅ N
5 nnmulcl ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ⋅ N ∈ ℕ
6 5 nnnn0d ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ⋅ N ∈ ℕ 0
7 nn0re ⊢ M ⋅ N ∈ ℕ 0 → M ⋅ N ∈ ℝ
8 nn0ge0 ⊢ M ⋅ N ∈ ℕ 0 → 0 ≤ M ⋅ N
9 7 8 jca ⊢ M ⋅ N ∈ ℕ 0 → M ⋅ N ∈ ℝ ∧ 0 ≤ M ⋅ N
10 absid ⊢ M ⋅ N ∈ ℝ ∧ 0 ≤ M ⋅ N → M ⋅ N = M ⋅ N
11 6 9 10 3syl ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ⋅ N = M ⋅ N
12 4 11 eqtrd ⊢ M ∈ ℕ ∧ N ∈ ℕ → M lcm N ⁢ M gcd N = M ⋅ N