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

Metamath Proof Explorer

Theorem lcmfval

Description: Value of the _lcm function. ( _lcmZ ) is the least common multiple of the integers contained in the finite subset of integers Z . If at least one of the elements of Z is 0 , the result is defined conventionally as 0 . (Contributed by AV, 21-Apr-2020) (Revised by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfval 
|- ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) = if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) )

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 zex 
 |-  ZZ e. _V
8 7 ssex 
 |-  ( Z C_ ZZ -> Z e. _V )
9 elpwg 
 |-  ( Z e. _V -> ( Z e. ~P ZZ <-> Z C_ ZZ ) )
10 8 9 syl 
 |-  ( Z C_ ZZ -> ( Z e. ~P ZZ <-> Z C_ ZZ ) )
11 10 ibir 
 |-  ( Z C_ ZZ -> Z e. ~P ZZ )
12 11 adantr 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> Z e. ~P ZZ )
13 0nn0 
 |-  0 e. NN0
14 13 a1i 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e. Z ) -> 0 e. NN0 )
15 df-nel 
 |-  ( 0 e/ Z <-> -. 0 e. Z )
16 ssrab2 
 |-  { n e. NN | A. m e. Z m || n } C_ NN
17 nnssnn0 
 |-  NN C_ NN0
18 16 17 sstri 
 |-  { n e. NN | A. m e. Z m || n } C_ NN0
19 nnuz 
 |-  NN = ( ZZ>= ` 1 )
20 16 19 sseqtri 
 |-  { n e. NN | A. m e. Z m || n } C_ ( ZZ>= ` 1 )
21 fissn0dvdsn0 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> { n e. NN | A. m e. Z m || n } =/= (/) )
22 21 3expa 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e/ Z ) -> { n e. NN | A. m e. Z m || n } =/= (/) )
23 infssuzcl 
 |-  ( ( { n e. NN | A. m e. Z m || n } C_ ( ZZ>= ` 1 ) /\ { n e. NN | A. m e. Z m || n } =/= (/) ) -> inf ( { n e. NN | A. m e. Z m || n } , RR , < ) e. { n e. NN | A. m e. Z m || n } )
24 20 22 23 sylancr 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e/ Z ) -> inf ( { n e. NN | A. m e. Z m || n } , RR , < ) e. { n e. NN | A. m e. Z m || n } )
25 18 24 sselid 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e/ Z ) -> inf ( { n e. NN | A. m e. Z m || n } , RR , < ) e. NN0 )
26 15 25 sylan2br 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ -. 0 e. Z ) -> inf ( { n e. NN | A. m e. Z m || n } , RR , < ) e. NN0 )
27 14 26 ifclda 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) e. NN0 )
28 1 6 12 27 fvmptd3 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) = if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) )