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

Metamath Proof Explorer

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 )