Theorem lcmf0val

Description: The value, by convention, of the least common multiple for a set containing 0 is 0. (Contributed by AV, 21-Apr-2020) (Proof shortened by AV, 16-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		df-lcmf	|- _lcm = ( z e. ~P ZZ |-> if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) ) )
2		eleq2	|- ( z = Z -> ( 0 e. z <-> 0 e. Z ) )
3		raleq	|- ( z = Z -> ( A. m e. z m || n <-> A. m e. Z m || n ) )
4	3	rabbidv	|- ( z = Z -> { n e. NN | A. m e. z m || n } = { n e. NN | A. m e. Z m || n } )
5	4	infeq1d	|- ( z = Z -> inf ( { n e. NN | A. m e. z m || n } , RR , < ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )
6	2 5	ifbieq2d	|- ( z = Z -> if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) ) = if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) )
7		iftrue	|- ( 0 e. Z -> if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) = 0 )
8	7	adantl	|- ( ( Z C_ ZZ /\ 0 e. Z ) -> if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) = 0 )
9	6 8	sylan9eqr	|- ( ( ( Z C_ ZZ /\ 0 e. Z ) /\ z = Z ) -> if ( 0 e. z , 0 , inf ( { n e. NN | A. m e. z m || n } , RR , < ) ) = 0 )
10		zex	|- ZZ e. _V
11	10	ssex	|- ( Z C_ ZZ -> Z e. _V )
12		elpwg	|- ( Z e. _V -> ( Z e. ~P ZZ <-> Z C_ ZZ ) )
13	11 12	syl	|- ( Z C_ ZZ -> ( Z e. ~P ZZ <-> Z C_ ZZ ) )
14	13	ibir	|- ( Z C_ ZZ -> Z e. ~P ZZ )
15	14	adantr	|- ( ( Z C_ ZZ /\ 0 e. Z ) -> Z e. ~P ZZ )
16		simpr	|- ( ( Z C_ ZZ /\ 0 e. Z ) -> 0 e. Z )
17	1 9 15 16	fvmptd2	|- ( ( Z C_ ZZ /\ 0 e. Z ) -> ( _lcm ` Z ) = 0 )