Theorem lcm5un

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

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

Proof

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