This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )