Theorem lcm7un

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

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

Proof

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