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	mulridd	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 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	mulridd	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 · 1 ) = 𝑀 )
13	12	fveq2d	⊢ ( 𝑀 ∈ ℤ → ( abs ‘ ( 𝑀 · 1 ) ) = ( abs ‘ 𝑀 ) )
14	8 10 13	3eqtrd	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 lcm 1 ) = ( abs ‘ 𝑀 ) )