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	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( 𝑀 · 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
2		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3		lcmgcd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( abs ‘ ( 𝑀 · 𝑁 ) ) )
4	1 2 3	syl2an	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( abs ‘ ( 𝑀 · 𝑁 ) ) )
5		nnmulcl	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 · 𝑁 ) ∈ ℕ )
6	5	nnnn0d	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 · 𝑁 ) ∈ ℕ0 )
7		nn0re	⊢ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 → ( 𝑀 · 𝑁 ) ∈ ℝ )
8		nn0ge0	⊢ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 → 0 ≤ ( 𝑀 · 𝑁 ) )
9	7 8	jca	⊢ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 → ( ( 𝑀 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝑀 · 𝑁 ) ) )
10		absid	⊢ ( ( ( 𝑀 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝑀 · 𝑁 ) ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) = ( 𝑀 · 𝑁 ) )
11	6 9 10	3syl	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) = ( 𝑀 · 𝑁 ) )
12	4 11	eqtrd	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( 𝑀 · 𝑁 ) )