Theorem lcmfunnnd

Description: Useful equation to calculate the least common multiple of 1 to n. (Contributed by metakunt, 29-Apr-2024)

	Ref	Expression
Hypothesis	lcmfunnnd.1	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	lcmfunnnd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N-1\right)\right)\mathrm{lcm}N$$

Proof

Step	Hyp	Ref	Expression
1		lcmfunnnd.1	$$⊢\phi \to N\in \mathbb{N}$$
2	1	nncnd	$$⊢\phi \to N\in ℂ$$
3		1cnd	$$⊢\phi \to 1\in ℂ$$
4	2 3	npcand	$$⊢\phi \to N-1+1=N$$
5	4	oveq2d	$$⊢\phi \to \left(1\dots N-1+1\right)=\left(1\dots N\right)$$
6		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
7	1 6	syl	$$⊢\phi \to N-1\in {\mathbb{N}}_0$$
8		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
9	8	eleq2i	$$⊢N-1\in {\mathbb{N}}_0\leftrightarrow N-1\in {\mathbb{Z}}_{\ge 0}$$
10	7 9	sylib	$$⊢\phi \to N-1\in {\mathbb{Z}}_{\ge 0}$$
11		1m1e0	$$⊢1-1=0$$
12	11	fveq2i	$$⊢{\mathbb{Z}}_{\ge \left(1-1\right)}={\mathbb{Z}}_{\ge 0}$$
13	12	eleq2i	$$⊢N-1\in {\mathbb{Z}}_{\ge \left(1-1\right)}\leftrightarrow N-1\in {\mathbb{Z}}_{\ge 0}$$
14	13	a1i	$$⊢\phi \to \left(N-1\in {\mathbb{Z}}_{\ge \left(1-1\right)}\leftrightarrow N-1\in {\mathbb{Z}}_{\ge 0}\right)$$
15	10 14	mpbird	$$⊢\phi \to N-1\in {\mathbb{Z}}_{\ge \left(1-1\right)}$$
16		1z	$$⊢1\in \mathbb{Z}$$
17		fzsuc2	$$⊢\left(1\in \mathbb{Z}\wedge N-1\in {\mathbb{Z}}_{\ge \left(1-1\right)}\right)\to \left(1\dots N-1+1\right)=\left(1\dots N-1\right)\cup \left\{N-1+1\right\}$$
18	16 17	mpan	$$⊢N-1\in {\mathbb{Z}}_{\ge \left(1-1\right)}\to \left(1\dots N-1+1\right)=\left(1\dots N-1\right)\cup \left\{N-1+1\right\}$$
19	15 18	syl	$$⊢\phi \to \left(1\dots N-1+1\right)=\left(1\dots N-1\right)\cup \left\{N-1+1\right\}$$
20	5 19	eqtr3d	$$⊢\phi \to \left(1\dots N\right)=\left(1\dots N-1\right)\cup \left\{N-1+1\right\}$$
21	4	sneqd	$$⊢\phi \to \left\{N-1+1\right\}=\left\{N\right\}$$
22	21	uneq2d	$$⊢\phi \to \left(1\dots N-1\right)\cup \left\{N-1+1\right\}=\left(1\dots N-1\right)\cup \left\{N\right\}$$
23	20 22	eqtrd	$$⊢\phi \to \left(1\dots N\right)=\left(1\dots N-1\right)\cup \left\{N\right\}$$
24	23	fveq2d	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N-1\right)\cup \left\{N\right\}\right)$$
25		fzssz	$$⊢\left(1\dots N-1\right)\subseteq \mathbb{Z}$$
26	25	a1i	$$⊢\phi \to \left(1\dots N-1\right)\subseteq \mathbb{Z}$$
27		fzfi	$$⊢\left(1\dots N-1\right)\in \mathrm{Fin}$$
28	27	a1i	$$⊢\phi \to \left(1\dots N-1\right)\in \mathrm{Fin}$$
29		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
30	1 29	syl	$$⊢\phi \to N\in \mathbb{Z}$$
31	26 28 30	3jca	$$⊢\phi \to \left(\left(1\dots N-1\right)\subseteq \mathbb{Z}\wedge \left(1\dots N-1\right)\in \mathrm{Fin}\wedge N\in \mathbb{Z}\right)$$
32		lcmfunsn	$$⊢\left(\left(1\dots N-1\right)\subseteq \mathbb{Z}\wedge \left(1\dots N-1\right)\in \mathrm{Fin}\wedge N\in \mathbb{Z}\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N-1\right)\cup \left\{N\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N-1\right)\right)\mathrm{lcm}N$$
33	31 32	syl	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N-1\right)\cup \left\{N\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N-1\right)\right)\mathrm{lcm}N$$
34	24 33	eqtrd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N-1\right)\right)\mathrm{lcm}N$$