Theorem lcmfass

Description: Associative law for the _lcm function. (Contributed by AV, 27-Aug-2020)

	Ref	Expression
Assertion	lcmfass	$$⊢\left(\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\wedge \left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\right)\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\cup Z\right)=\underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcmfcl	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(Y\right)\in {\mathbb{N}}_0$$
2	1	nn0zd	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(Y\right)\in \mathbb{Z}$$
3		lcmfsn	$$⊢\underset{\_}{\mathrm{lcm}}\left(Y\right)\in \mathbb{Z}\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\right)=\left|\underset{\_}{\mathrm{lcm}}\left(Y\right)\right|$$
4	2 3	syl	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\right)=\left|\underset{\_}{\mathrm{lcm}}\left(Y\right)\right|$$
5		nn0re	$$⊢\underset{\_}{\mathrm{lcm}}\left(Y\right)\in {\mathbb{N}}_0\to \underset{\_}{\mathrm{lcm}}\left(Y\right)\in ℝ$$
6		nn0ge0	$$⊢\underset{\_}{\mathrm{lcm}}\left(Y\right)\in {\mathbb{N}}_0\to 0\le \underset{\_}{\mathrm{lcm}}\left(Y\right)$$
7	5 6	jca	$$⊢\underset{\_}{\mathrm{lcm}}\left(Y\right)\in {\mathbb{N}}_0\to \left(\underset{\_}{\mathrm{lcm}}\left(Y\right)\in ℝ\wedge 0\le \underset{\_}{\mathrm{lcm}}\left(Y\right)\right)$$
8		absid	$$⊢\left(\underset{\_}{\mathrm{lcm}}\left(Y\right)\in ℝ\wedge 0\le \underset{\_}{\mathrm{lcm}}\left(Y\right)\right)\to \left|\underset{\_}{\mathrm{lcm}}\left(Y\right)\right|=\underset{\_}{\mathrm{lcm}}\left(Y\right)$$
9	1 7 8	3syl	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\to \left|\underset{\_}{\mathrm{lcm}}\left(Y\right)\right|=\underset{\_}{\mathrm{lcm}}\left(Y\right)$$
10	4 9	eqtrd	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)$$
11		lcmfcl	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)\in {\mathbb{N}}_0$$
12	11	nn0zd	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)\in \mathbb{Z}$$
13		lcmfsn	$$⊢\underset{\_}{\mathrm{lcm}}\left(Z\right)\in \mathbb{Z}\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)=\left|\underset{\_}{\mathrm{lcm}}\left(Z\right)\right|$$
14	12 13	syl	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)=\left|\underset{\_}{\mathrm{lcm}}\left(Z\right)\right|$$
15		nn0re	$$⊢\underset{\_}{\mathrm{lcm}}\left(Z\right)\in {\mathbb{N}}_0\to \underset{\_}{\mathrm{lcm}}\left(Z\right)\in ℝ$$
16		nn0ge0	$$⊢\underset{\_}{\mathrm{lcm}}\left(Z\right)\in {\mathbb{N}}_0\to 0\le \underset{\_}{\mathrm{lcm}}\left(Z\right)$$
17	15 16	jca	$$⊢\underset{\_}{\mathrm{lcm}}\left(Z\right)\in {\mathbb{N}}_0\to \left(\underset{\_}{\mathrm{lcm}}\left(Z\right)\in ℝ\wedge 0\le \underset{\_}{\mathrm{lcm}}\left(Z\right)\right)$$
18		absid	$$⊢\left(\underset{\_}{\mathrm{lcm}}\left(Z\right)\in ℝ\wedge 0\le \underset{\_}{\mathrm{lcm}}\left(Z\right)\right)\to \left|\underset{\_}{\mathrm{lcm}}\left(Z\right)\right|=\underset{\_}{\mathrm{lcm}}\left(Z\right)$$
19	11 17 18	3syl	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \left|\underset{\_}{\mathrm{lcm}}\left(Z\right)\right|=\underset{\_}{\mathrm{lcm}}\left(Z\right)$$
20	14 19	eqtr2d	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(Z\right)=\underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)$$
21	10 20	oveqan12d	$$⊢\left(\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\wedge \left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\right)\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\right)\mathrm{lcm}\underset{\_}{\mathrm{lcm}}\left(Z\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}\underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)$$
22	2	snssd	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\to \left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\subseteq \mathbb{Z}$$
23		snfi	$$⊢\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\in \mathrm{Fin}$$
24	22 23	jctir	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\to \left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\subseteq \mathbb{Z}\wedge \left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\in \mathrm{Fin}\right)$$
25		lcmfun	$$⊢\left(\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\subseteq \mathbb{Z}\wedge \left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\in \mathrm{Fin}\right)\wedge \left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\right)\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\cup Z\right)=\underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\right)\mathrm{lcm}\underset{\_}{\mathrm{lcm}}\left(Z\right)$$
26	24 25	sylan	$$⊢\left(\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\wedge \left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\right)\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\cup Z\right)=\underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\right)\mathrm{lcm}\underset{\_}{\mathrm{lcm}}\left(Z\right)$$
27	12	snssd	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\subseteq \mathbb{Z}$$
28		snfi	$$⊢\left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\in \mathrm{Fin}$$
29	27 28	jctir	$$⊢\left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\to \left(\left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\subseteq \mathbb{Z}\wedge \left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\in \mathrm{Fin}\right)$$
30		lcmfun	$$⊢\left(\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\wedge \left(\left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\subseteq \mathbb{Z}\wedge \left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\in \mathrm{Fin}\right)\right)\to \underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}\underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)$$
31	29 30	sylan2	$$⊢\left(\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\wedge \left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\right)\to \underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}\underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)$$
32	21 26 31	3eqtr4d	$$⊢\left(\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\wedge \left(Z\subseteq \mathbb{Z}\wedge Z\in \mathrm{Fin}\right)\right)\to \underset{\_}{\mathrm{lcm}}\left(\left\{\underset{\_}{\mathrm{lcm}}\left(Y\right)\right\}\cup Z\right)=\underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{\underset{\_}{\mathrm{lcm}}\left(Z\right)\right\}\right)$$