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	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 lcm 𝑀 ) = ( abs ‘ 𝑀 ) )

Proof

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