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 \in ℕ \land N \in ℕ) \to (M lcm N) (M \gcd N) = M \cdot N$

Proof

Step	Hyp	Ref	Expression
1		nnz	$⊢ M \in ℕ \to M \in ℤ$
2		nnz	$⊢ N \in ℕ \to N \in ℤ$
3		lcmgcd	$⊢ (M \in ℤ \land N \in ℤ) \to (M lcm N) (M \gcd N) = \|M \cdot N\|$
4	1 2 3	syl2an	$⊢ (M \in ℕ \land N \in ℕ) \to (M lcm N) (M \gcd N) = \|M \cdot N\|$
5		nnmulcl	$⊢ (M \in ℕ \land N \in ℕ) \to M \cdot N \in ℕ$
6	5	nnnn0d	$⊢ (M \in ℕ \land N \in ℕ) \to M \cdot N \in ℕ_{0}$
7		nn0re	$⊢ M \cdot N \in ℕ_{0} \to M \cdot N \in ℝ$
8		nn0ge0	$⊢ M \cdot N \in ℕ_{0} \to 0 \leq M \cdot N$
9	7 8	jca	$⊢ M \cdot N \in ℕ_{0} \to (M \cdot N \in ℝ \land 0 \leq M \cdot N)$
10		absid	$⊢ (M \cdot N \in ℝ \land 0 \leq M \cdot N) \to \|M \cdot N\| = M \cdot N$
11	6 9 10	3syl	$⊢ (M \in ℕ \land N \in ℕ) \to \|M \cdot N\| = M \cdot N$
12	4 11	eqtrd	$⊢ (M \in ℕ \land N \in ℕ) \to (M lcm N) (M \gcd N) = M \cdot N$