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

Proof

Step Hyp Ref Expression
1 gcd1 ⊢M∈ℤ→Mgcd1=1
2 1 oveq2d ⊢M∈ℤ→Mlcm1⁢Mgcd1=Mlcm1⋅1
3 1z ⊢1∈ℤ
4 lcmcl ⊢M∈ℤ∧1∈ℤ→Mlcm1∈ℕ0
5 3 4 mpan2 ⊢M∈ℤ→Mlcm1∈ℕ0
6 5 nn0cnd ⊢M∈ℤ→Mlcm1∈ℂ
7 6 mulridd ⊢M∈ℤ→Mlcm1⋅1=Mlcm1
8 2 7 eqtr2d ⊢M∈ℤ→Mlcm1=Mlcm1⁢Mgcd1
9 lcmgcd ⊢M∈ℤ∧1∈ℤ→Mlcm1⁢Mgcd1= M⋅1
10 3 9 mpan2 ⊢M∈ℤ→Mlcm1⁢Mgcd1= 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∈ℤ→Mlcm1=M