Theorem lcmfunsn

Description: The _lcm function for a union of a set of integer and a singleton. (Contributed by AV, 26-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		lcmfunsnlem	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\to \left(\forall k\in \mathbb{Z}\left(\forall m\in Ym\parallel k\to \underset{\_}{\mathrm{lcm}}\left(Y\right)\parallel k\right)\wedge \forall n\in \mathbb{Z}\underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{n\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}n\right)$$
2		sneq	$$⊢n=N\to \left\{n\right\}=\left\{N\right\}$$
3	2	uneq2d	$$⊢n=N\to Y\cup \left\{n\right\}=Y\cup \left\{N\right\}$$
4	3	fveq2d	$$⊢n=N\to \underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{n\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{N\right\}\right)$$
5		oveq2	$$⊢n=N\to \underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}n=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}N$$
6	4 5	eqeq12d	$$⊢n=N\to \left(\underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{n\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}n\leftrightarrow \underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{N\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}N\right)$$
7	6	rspccv	$$⊢\forall n\in \mathbb{Z}\underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{n\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}n\to \left(N\in \mathbb{Z}\to \underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{N\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}N\right)$$
8	1 7	simpl2im	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\right)\to \left(N\in \mathbb{Z}\to \underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{N\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}N\right)$$
9	8	3impia	$$⊢\left(Y\subseteq \mathbb{Z}\wedge Y\in \mathrm{Fin}\wedge N\in \mathbb{Z}\right)\to \underset{\_}{\mathrm{lcm}}\left(Y\cup \left\{N\right\}\right)=\underset{\_}{\mathrm{lcm}}\left(Y\right)\mathrm{lcm}N$$