Metamath Proof Explorer

Theorem 60lcm6e60

Description: The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Assertion 60lcm6e60 
|- ( ; 6 0 lcm 6 ) = ; 6 0

Proof

Step Hyp Ref Expression
1 6nn 
 |-  6 e. NN
2 1 decnncl2 
 |-  ; 6 0 e. NN
3 60gcd6e6 
 |-  ( ; 6 0 gcd 6 ) = 6
4 eqid 
 |-  ( 6 x. ; 6 0 ) = ( 6 x. ; 6 0 )
5 2 1 mulcomnni 
 |-  ( ; 6 0 x. 6 ) = ( 6 x. ; 6 0 )
6 2 1 1 2 3 4 5 lcmeprodgcdi 
 |-  ( ; 6 0 lcm 6 ) = ; 6 0