Theorem lcm4un

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

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

Proof

Step	Hyp	Ref	Expression
1		4nn	$$⊢4\in \mathbb{N}$$
2		id	$$⊢4\in \mathbb{N}\to 4\in \mathbb{N}$$
3	2	lcmfunnnd	$$⊢4\in \mathbb{N}\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 4\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 4-1\right)\right)\mathrm{lcm}4$$
4	1 3	ax-mp	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 4\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 4-1\right)\right)\mathrm{lcm}4$$
5		4m1e3	$$⊢4-1=3$$
6	5	oveq2i	$$⊢\left(1\dots 4-1\right)=\left(1\dots 3\right)$$
7	6	fveq2i	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 4-1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3\right)\right)$$
8		lcm3un	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 3\right)\right)=6$$
9	7 8	eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 4-1\right)\right)=6$$
10	9	oveq1i	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 4-1\right)\right)\mathrm{lcm}4=6\mathrm{lcm}4$$
11		6lcm4e12	$$⊢6\mathrm{lcm}4=12$$
12	4 10 11	3eqtri	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 4\right)\right)=12$$