This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ‘ 𝑀 ) )