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 ( 𝑀 ∈ ℤ → ( 𝑀 lcm 1 ) = ( abs ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 gcd1 ( 𝑀 ∈ ℤ → ( 𝑀 gcd 1 ) = 1 )
2 1 oveq2d ( 𝑀 ∈ ℤ → ( ( 𝑀 lcm 1 ) · ( 𝑀 gcd 1 ) ) = ( ( 𝑀 lcm 1 ) · 1 ) )
3 1z 1 ∈ ℤ
4 lcmcl ( ( 𝑀 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑀 lcm 1 ) ∈ ℕ0 )
5 3 4 mpan2 ( 𝑀 ∈ ℤ → ( 𝑀 lcm 1 ) ∈ ℕ0 )
6 5 nn0cnd ( 𝑀 ∈ ℤ → ( 𝑀 lcm 1 ) ∈ ℂ )
7 6 mulid1d ( 𝑀 ∈ ℤ → ( ( 𝑀 lcm 1 ) · 1 ) = ( 𝑀 lcm 1 ) )
8 2 7 eqtr2d ( 𝑀 ∈ ℤ → ( 𝑀 lcm 1 ) = ( ( 𝑀 lcm 1 ) · ( 𝑀 gcd 1 ) ) )
9 lcmgcd ( ( 𝑀 ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝑀 lcm 1 ) · ( 𝑀 gcd 1 ) ) = ( abs ‘ ( 𝑀 · 1 ) ) )
10 3 9 mpan2 ( 𝑀 ∈ ℤ → ( ( 𝑀 lcm 1 ) · ( 𝑀 gcd 1 ) ) = ( abs ‘ ( 𝑀 · 1 ) ) )
11 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
12 11 mulid1d ( 𝑀 ∈ ℤ → ( 𝑀 · 1 ) = 𝑀 )
13 12 fveq2d ( 𝑀 ∈ ℤ → ( abs ‘ ( 𝑀 · 1 ) ) = ( abs ‘ 𝑀 ) )
14 8 10 13 3eqtrd ( 𝑀 ∈ ℤ → ( 𝑀 lcm 1 ) = ( abs ‘ 𝑀 ) )