Theorem lcm8un

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

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

Proof

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