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 
|- ( ( M e. NN /\ N e. NN ) -> ( ( M lcm N ) x. ( M gcd N ) ) = ( M x. N ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( M e. NN -> M e. ZZ )
2 nnz 
 |-  ( N e. NN -> N e. ZZ )
3 lcmgcd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) x. ( M gcd N ) ) = ( abs ` ( M x. N ) ) )
4 1 2 3 syl2an 
 |-  ( ( M e. NN /\ N e. NN ) -> ( ( M lcm N ) x. ( M gcd N ) ) = ( abs ` ( M x. N ) ) )
5 nnmulcl 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M x. N ) e. NN )
6 5 nnnn0d 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M x. N ) e. NN0 )
7 nn0re 
 |-  ( ( M x. N ) e. NN0 -> ( M x. N ) e. RR )
8 nn0ge0 
 |-  ( ( M x. N ) e. NN0 -> 0 <_ ( M x. N ) )
9 7 8 jca 
 |-  ( ( M x. N ) e. NN0 -> ( ( M x. N ) e. RR /\ 0 <_ ( M x. N ) ) )
10 absid 
 |-  ( ( ( M x. N ) e. RR /\ 0 <_ ( M x. N ) ) -> ( abs ` ( M x. N ) ) = ( M x. N ) )
11 6 9 10 3syl 
 |-  ( ( M e. NN /\ N e. NN ) -> ( abs ` ( M x. N ) ) = ( M x. N ) )
12 4 11 eqtrd 
 |-  ( ( M e. NN /\ N e. NN ) -> ( ( M lcm N ) x. ( M gcd N ) ) = ( M x. N ) )