Theorem lcmn0cl

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

	Ref	Expression
Assertion	lcmn0cl	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		ssrab2	|- { n e. NN | ( M || n /\ N || n ) } C_ NN
2		lcmcllem	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. { n e. NN | ( M || n /\ N || n ) } )
3	1 2	sselid	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. NN )