This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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