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	syl5bir	|- ( ( 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 ) )