Theorem lcm1un

Description: Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Assertion	lcm1un	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2		id	$$⊢1\in \mathbb{N}\to 1\in \mathbb{N}$$
3	2	lcmfunnnd	$$⊢1\in \mathbb{N}\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1-1\right)\right)\mathrm{lcm}1$$
4	1 3	ax-mp	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1-1\right)\right)\mathrm{lcm}1$$
5		1m1e0	$$⊢1-1=0$$
6	5	oveq2i	$$⊢\left(1\dots 1-1\right)=\left(1\dots 0\right)$$
7		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
8	6 7	eqtri	$$⊢\left(1\dots 1-1\right)=\varnothing$$
9	8	fveq2i	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1-1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\varnothing \right)$$
10		lcmf0	$$⊢\underset{\_}{\mathrm{lcm}}\left(\varnothing \right)=1$$
11	9 10	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1-1\right)\right)=1$$
12	11	oveq1i	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1-1\right)\right)\mathrm{lcm}1=1\mathrm{lcm}1$$
13		1z	$$⊢1\in \mathbb{Z}$$
14		lcmid	$$⊢1\in \mathbb{Z}\to 1\mathrm{lcm}1=\left|1\right|$$
15	13 14	ax-mp	$$⊢1\mathrm{lcm}1=\left|1\right|$$
16		abs1	$$⊢\left|1\right|=1$$
17	15 16	eqtri	$$⊢1\mathrm{lcm}1=1$$
18	12 17	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1-1\right)\right)\mathrm{lcm}1=1$$
19	4 18	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 1\right)\right)=1$$