Theorem lcmn0val

Description: The value of the lcm operator when both operands are nonzero. (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 16-Sep-2020)

	Ref	Expression
Assertion	lcmn0val	$$⊢\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=sup\left(\left\{n\in \mathbb{N}|\left(M\parallel n\wedge N\parallel n\right)\right\},ℝ,<\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcmval	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to M\mathrm{lcm}N=if\left(\left(M=0\vee N=0\right),0,sup\left(\left\{n\in \mathbb{N}|\left(M\parallel n\wedge N\parallel n\right)\right\},ℝ,<\right)\right)$$
2		iffalse	$$⊢\neg \left(M=0\vee N=0\right)\to if\left(\left(M=0\vee N=0\right),0,sup\left(\left\{n\in \mathbb{N}|\left(M\parallel n\wedge N\parallel n\right)\right\},ℝ,<\right)\right)=sup\left(\left\{n\in \mathbb{N}|\left(M\parallel n\wedge N\parallel n\right)\right\},ℝ,<\right)$$
3	1 2	sylan9eq	$$⊢\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=sup\left(\left\{n\in \mathbb{N}|\left(M\parallel n\wedge N\parallel n\right)\right\},ℝ,<\right)$$