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 ) )