Metamath Proof Explorer

Theorem lcmid

Description: The lcm of an integer and itself is its absolute value. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion lcmid ⊢M∈ℤ→MlcmM=M

Proof

Step Hyp Ref Expression
1 oveq2 ⊢M=0→MlcmM=Mlcm0
2 fveq2 ⊢M=0→M=0
3 abs0 ⊢0=0
4 2 3 eqtrdi ⊢M=0→M=0
5 1 4 eqeq12d ⊢M=0→MlcmM=M↔Mlcm0=0
6 lcmcl ⊢M∈ℤ∧M∈ℤ→MlcmM∈ℕ0
7 6 nn0cnd ⊢M∈ℤ∧M∈ℤ→MlcmM∈ℂ
8 7 anidms ⊢M∈ℤ→MlcmM∈ℂ
9 8 adantr ⊢M∈ℤ∧M≠0→MlcmM∈ℂ
10 zabscl ⊢M∈ℤ→M∈ℤ
11 10 zcnd ⊢M∈ℤ→M∈ℂ
12 11 adantr ⊢M∈ℤ∧M≠0→M∈ℂ
13 zcn ⊢M∈ℤ→M∈ℂ
14 13 adantr ⊢M∈ℤ∧M≠0→M∈ℂ
15 simpr ⊢M∈ℤ∧M≠0→M≠0
16 14 15 absne0d ⊢M∈ℤ∧M≠0→M≠0
17 lcmgcd ⊢M∈ℤ∧M∈ℤ→MlcmM⁢MgcdM= M⋅ M
18 17 anidms ⊢M∈ℤ→MlcmM⁢MgcdM= M⋅ M
19 gcdid ⊢M∈ℤ→MgcdM=M
20 19 oveq2d ⊢M∈ℤ→MlcmM⁢MgcdM=MlcmM⁢M
21 13 13 absmuld ⊢M∈ℤ→ M⋅ M=M⁢M
22 18 20 21 3eqtr3d ⊢M∈ℤ→MlcmM⁢M=M⁢M
23 22 adantr ⊢M∈ℤ∧M≠0→MlcmM⁢M=M⁢M
24 9 12 12 16 23 mulcan2ad ⊢M∈ℤ∧M≠0→MlcmM=M
25 lcm0val ⊢M∈ℤ→Mlcm0=0
26 5 24 25 pm2.61ne ⊢M∈ℤ→MlcmM=M