Metamath Proof Explorer

Theorem lcmcl

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

Ref Expression
Assertion lcmcl 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )

Proof

Step Hyp Ref Expression
1 lcmcom 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = ( N lcm M ) )
2 1 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M = 0 ) -> ( M lcm N ) = ( N lcm M ) )
3 oveq2 
 |-  ( M = 0 -> ( N lcm M ) = ( N lcm 0 ) )
4 lcm0val 
 |-  ( N e. ZZ -> ( N lcm 0 ) = 0 )
5 3 4 sylan9eqr 
 |-  ( ( N e. ZZ /\ M = 0 ) -> ( N lcm M ) = 0 )
6 5 adantll 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M = 0 ) -> ( N lcm M ) = 0 )
7 2 6 eqtrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M = 0 ) -> ( M lcm N ) = 0 )
8 oveq2 
 |-  ( N = 0 -> ( M lcm N ) = ( M lcm 0 ) )
9 lcm0val 
 |-  ( M e. ZZ -> ( M lcm 0 ) = 0 )
10 8 9 sylan9eqr 
 |-  ( ( M e. ZZ /\ N = 0 ) -> ( M lcm N ) = 0 )
11 10 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( M lcm N ) = 0 )
12 7 11 jaodan 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = 0 )
13 0nn0 
 |-  0 e. NN0
14 12 13 eqeltrdi 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. NN0 )
15 lcmn0cl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. NN )
16 15 nnnn0d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. NN0 )
17 14 16 pm2.61dan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )