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 ∈ ℤ → M lcm 1 = M

Proof

Step Hyp Ref Expression
1 gcd1 ⊢ M ∈ ℤ → M gcd 1 = 1
2 1 oveq2d ⊢ M ∈ ℤ → M lcm 1 ⁢ M gcd 1 = M lcm 1 ⋅ 1
3 1z ⊢ 1 ∈ ℤ
4 lcmcl ⊢ M ∈ ℤ ∧ 1 ∈ ℤ → M lcm 1 ∈ ℕ 0
5 3 4 mpan2 ⊢ M ∈ ℤ → M lcm 1 ∈ ℕ 0
6 5 nn0cnd ⊢ M ∈ ℤ → M lcm 1 ∈ ℂ
7 6 mulridd ⊢ M ∈ ℤ → M lcm 1 ⋅ 1 = M lcm 1
8 2 7 eqtr2d ⊢ M ∈ ℤ → M lcm 1 = M lcm 1 ⁢ M gcd 1
9 lcmgcd ⊢ M ∈ ℤ ∧ 1 ∈ ℤ → M lcm 1 ⁢ M gcd 1 = M ⋅ 1
10 3 9 mpan2 ⊢ M ∈ ℤ → M lcm 1 ⁢ M gcd 1 = M ⋅ 1
11 zcn ⊢ M ∈ ℤ → M ∈ ℂ
12 11 mulridd ⊢ M ∈ ℤ → M ⋅ 1 = M
13 12 fveq2d ⊢ M ∈ ℤ → M ⋅ 1 = M
14 8 10 13 3eqtrd ⊢ M ∈ ℤ → M lcm 1 = M