Metamath Proof Explorer

Theorem lcmeq0

Description: The lcm of two integers is zero iff either is zero. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion lcmeq0 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) = 0 <-> ( M = 0 \/ N = 0 ) ) )

Proof

Step Hyp Ref Expression
1 lcmn0cl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. NN )
2 1 nnne0d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) =/= 0 )
3 2 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 \/ N = 0 ) -> ( M lcm N ) =/= 0 ) )
4 3 necon4bd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) = 0 -> ( M = 0 \/ N = 0 ) ) )
5 oveq1 
 |-  ( M = 0 -> ( M lcm N ) = ( 0 lcm N ) )
6 0z 
 |-  0 e. ZZ
7 lcmcom 
 |-  ( ( N e. ZZ /\ 0 e. ZZ ) -> ( N lcm 0 ) = ( 0 lcm N ) )
8 6 7 mpan2 
 |-  ( N e. ZZ -> ( N lcm 0 ) = ( 0 lcm N ) )
9 lcm0val 
 |-  ( N e. ZZ -> ( N lcm 0 ) = 0 )
10 8 9 eqtr3d 
 |-  ( N e. ZZ -> ( 0 lcm N ) = 0 )
11 5 10 sylan9eqr 
 |-  ( ( N e. ZZ /\ M = 0 ) -> ( M lcm N ) = 0 )
12 11 adantll 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M = 0 ) -> ( M lcm N ) = 0 )
13 oveq2 
 |-  ( N = 0 -> ( M lcm N ) = ( M lcm 0 ) )
14 lcm0val 
 |-  ( M e. ZZ -> ( M lcm 0 ) = 0 )
15 13 14 sylan9eqr 
 |-  ( ( M e. ZZ /\ N = 0 ) -> ( M lcm N ) = 0 )
16 15 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( M lcm N ) = 0 )
17 12 16 jaodan 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = 0 )
18 17 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M = 0 \/ N = 0 ) -> ( M lcm N ) = 0 ) )
19 4 18 impbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) = 0 <-> ( M = 0 \/ N = 0 ) ) )