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

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ M = 0 → M lcm M = M lcm 0
2 fveq2 ⊢ M = 0 → M = 0
3 abs0 ⊢ 0 = 0
4 2 3 eqtrdi ⊢ M = 0 → M = 0
5 1 4 eqeq12d ⊢ M = 0 → M lcm M = M ↔ M lcm 0 = 0
6 lcmcl ⊢ M ∈ ℤ ∧ M ∈ ℤ → M lcm M ∈ ℕ 0
7 6 nn0cnd ⊢ M ∈ ℤ ∧ M ∈ ℤ → M lcm M ∈ ℂ
8 7 anidms ⊢ M ∈ ℤ → M lcm M ∈ ℂ
9 8 adantr ⊢ M ∈ ℤ ∧ M ≠ 0 → M lcm M ∈ ℂ
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 ∈ ℤ → M lcm M ⁢ M gcd M = M ⋅ M
18 17 anidms ⊢ M ∈ ℤ → M lcm M ⁢ M gcd M = M ⋅ M
19 gcdid ⊢ M ∈ ℤ → M gcd M = M
20 19 oveq2d ⊢ M ∈ ℤ → M lcm M ⁢ M gcd M = M lcm M ⁢ M
21 13 13 absmuld ⊢ M ∈ ℤ → M ⋅ M = M ⁢ M
22 18 20 21 3eqtr3d ⊢ M ∈ ℤ → M lcm M ⁢ M = M ⁢ M
23 22 adantr ⊢ M ∈ ℤ ∧ M ≠ 0 → M lcm M ⁢ M = M ⁢ M
24 9 12 12 16 23 mulcan2ad ⊢ M ∈ ℤ ∧ M ≠ 0 → M lcm M = M
25 lcm0val ⊢ M ∈ ℤ → M lcm 0 = 0
26 5 24 25 pm2.61ne ⊢ M ∈ ℤ → M lcm M = M