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

Metamath Proof Explorer

Theorem lcmfeq0b

Description: The least common multiple of a set of integers is 0 iff at least one of its element is 0. (Contributed by AV, 21-Aug-2020)

Ref Expression
Assertion lcmfeq0b 
|- ( ( Z C_ ZZ /\ Z e. Fin ) -> ( ( _lcm ` Z ) = 0 <-> 0 e. Z ) )

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( 0 e/ Z <-> -. 0 e. Z )
2 lcmfn0cl 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. NN )
3 2 nnne0d 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) =/= 0 )
4 3 3expia 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( 0 e/ Z -> ( _lcm ` Z ) =/= 0 ) )
5 1 4 biimtrrid 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( -. 0 e. Z -> ( _lcm ` Z ) =/= 0 ) )
6 5 necon4bd 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( ( _lcm ` Z ) = 0 -> 0 e. Z ) )
7 lcmf0val 
 |-  ( ( Z C_ ZZ /\ 0 e. Z ) -> ( _lcm ` Z ) = 0 )
8 7 ex 
 |-  ( Z C_ ZZ -> ( 0 e. Z -> ( _lcm ` Z ) = 0 ) )
9 8 adantr 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( 0 e. Z -> ( _lcm ` Z ) = 0 ) )
10 6 9 impbid 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( ( _lcm ` Z ) = 0 <-> 0 e. Z ) )