Metamath Proof Explorer

Theorem gcddvdslcm

Description: The greatest common divisor of two numbers divides their least common multiple. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion gcddvdslcm 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || ( M lcm N ) )

Proof

Step Hyp Ref Expression
1 gcdcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
2 1 nn0zd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. ZZ )
3 simpl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
4 lcmcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )
5 4 nn0zd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. ZZ )
6 gcddvds 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
7 6 simpld 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || M )
8 dvdslcm 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )
9 8 simpld 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M || ( M lcm N ) )
10 2 3 5 7 9 dvdstrd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || ( M lcm N ) )