Metamath Proof Explorer

Theorem lcmn0cl

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

Ref Expression
Assertion lcmn0cl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N ∈ ℕ

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ n ∈ ℕ | M ∥ n ∧ N ∥ n ⊆ ℕ
2 lcmcllem ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N ∈ n ∈ ℕ | M ∥ n ∧ N ∥ n
3 1 2 sseldi ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N ∈ ℕ