Metamath Proof Explorer

Theorem lcmcl

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

Ref Expression
Assertion lcmcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N ∈ ℕ 0

Proof

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