Theorem lcmn0cl

Description: Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020)

	Ref	Expression
Assertion	lcmn0cl	$$⊢\left(\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\wedge \neg \left(M=0\vee N=0\right)\right)\to M\mathrm{lcm}N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$$⊢\left\{n\in \mathbb{N}|\left(M\parallel n\wedge N\parallel n\right)\right\}\subseteq \mathbb{N}$$
2		lcmcllem	$$⊢\left(\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\wedge \neg \left(M=0\vee N=0\right)\right)\to M\mathrm{lcm}N\in \left\{n\in \mathbb{N}|\left(M\parallel n\wedge N\parallel n\right)\right\}$$
3	1 2	sselid	$$⊢\left(\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\wedge \neg \left(M=0\vee N=0\right)\right)\to M\mathrm{lcm}N\in \mathbb{N}$$