Metamath Proof Explorer

Theorem lcmcl

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

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

Proof

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