Metamath Proof Explorer

Theorem lcm1

Description: The lcm of an integer and 1 is the absolute value of the integer. (Contributed by AV, 23-Aug-2020)

Ref Expression
Assertion lcm1 
|- ( M e. ZZ -> ( M lcm 1 ) = ( abs ` M ) )

Proof

Step Hyp Ref Expression
1 gcd1 
 |-  ( M e. ZZ -> ( M gcd 1 ) = 1 )
2 1 oveq2d 
 |-  ( M e. ZZ -> ( ( M lcm 1 ) x. ( M gcd 1 ) ) = ( ( M lcm 1 ) x. 1 ) )
3 1z 
 |-  1 e. ZZ
4 lcmcl 
 |-  ( ( M e. ZZ /\ 1 e. ZZ ) -> ( M lcm 1 ) e. NN0 )
5 3 4 mpan2 
 |-  ( M e. ZZ -> ( M lcm 1 ) e. NN0 )
6 5 nn0cnd 
 |-  ( M e. ZZ -> ( M lcm 1 ) e. CC )
7 6 mulridd 
 |-  ( M e. ZZ -> ( ( M lcm 1 ) x. 1 ) = ( M lcm 1 ) )
8 2 7 eqtr2d 
 |-  ( M e. ZZ -> ( M lcm 1 ) = ( ( M lcm 1 ) x. ( M gcd 1 ) ) )
9 lcmgcd 
 |-  ( ( M e. ZZ /\ 1 e. ZZ ) -> ( ( M lcm 1 ) x. ( M gcd 1 ) ) = ( abs ` ( M x. 1 ) ) )
10 3 9 mpan2 
 |-  ( M e. ZZ -> ( ( M lcm 1 ) x. ( M gcd 1 ) ) = ( abs ` ( M x. 1 ) ) )
11 zcn 
 |-  ( M e. ZZ -> M e. CC )
12 11 mulridd 
 |-  ( M e. ZZ -> ( M x. 1 ) = M )
13 12 fveq2d 
 |-  ( M e. ZZ -> ( abs ` ( M x. 1 ) ) = ( abs ` M ) )
14 8 10 13 3eqtrd 
 |-  ( M e. ZZ -> ( M lcm 1 ) = ( abs ` M ) )