Theorem lcmfsn

Description: The least common multiple of a singleton is its absolute value. (Contributed by AV, 22-Aug-2020)

	Ref	Expression
Assertion	lcmfsn	$$⊢M\in \mathbb{Z}\to \underset{\_}{\mathrm{lcm}}\left(\left\{M\right\}\right)=\left|M\right|$$

Proof

Step	Hyp	Ref	Expression
1		dfsn2	$$⊢\left\{M\right\}=\left\{M,M\right\}$$
2	1	a1i	$$⊢M\in \mathbb{Z}\to \left\{M\right\}=\left\{M,M\right\}$$
3	2	fveq2d	$$⊢M\in \mathbb{Z}\to \underset{\_}{\mathrm{lcm}}\left(\left\{M\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(\left\{M,M\right\}\right)$$
4		lcmfpr	$$⊢\left(M\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \underset{\_}{\mathrm{lcm}}\left(\left\{M,M\right\}\right)=M\mathrm{lcm}M$$
5	4	anidms	$$⊢M\in \mathbb{Z}\to \underset{\_}{\mathrm{lcm}}\left(\left\{M,M\right\}\right)=M\mathrm{lcm}M$$
6		lcmid	$$⊢M\in \mathbb{Z}\to M\mathrm{lcm}M=\left|M\right|$$
7	3 5 6	3eqtrd	$$⊢M\in \mathbb{Z}\to \underset{\_}{\mathrm{lcm}}\left(\left\{M\right\}\right)=\left|M\right|$$