Theorem lcmcl

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

	Ref	Expression
Assertion	lcmcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		lcmcom	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) = ( 𝑁 lcm 𝑀 ) )
2	1	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝑀 lcm 𝑁 ) = ( 𝑁 lcm 𝑀 ) )
3		oveq2	⊢ ( 𝑀 = 0 → ( 𝑁 lcm 𝑀 ) = ( 𝑁 lcm 0 ) )
4		lcm0val	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 lcm 0 ) = 0 )
5	3 4	sylan9eqr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 = 0 ) → ( 𝑁 lcm 𝑀 ) = 0 )
6	5	adantll	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝑁 lcm 𝑀 ) = 0 )
7	2 6	eqtrd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝑀 lcm 𝑁 ) = 0 )
8		oveq2	⊢ ( 𝑁 = 0 → ( 𝑀 lcm 𝑁 ) = ( 𝑀 lcm 0 ) )
9		lcm0val	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 lcm 0 ) = 0 )
10	8 9	sylan9eqr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 = 0 ) → ( 𝑀 lcm 𝑁 ) = 0 )
11	10	adantlr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( 𝑀 lcm 𝑁 ) = 0 )
12	7 11	jaodan	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) = 0 )
13		0nn0	⊢ 0 ∈ ℕ0
14	12 13	eqeltrdi	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )
15		lcmn0cl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ )
16	15	nnnn0d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )
17	14 16	pm2.61dan	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )