Metamath Proof Explorer

Theorem fissn0dvds

Description: For each finite subset of the integers not containing 0 there is a positive integer which is divisible by each element of this subset. (Contributed by AV, 21-Aug-2020)

Ref Expression
Assertion fissn0dvds 
|- ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> E. n e. NN A. m e. Z m || n )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> Z C_ ZZ )
2 simp2 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> Z e. Fin )
3 eqid 
 |-  ( abs ` prod_ k e. Z k ) = ( abs ` prod_ k e. Z k )
4 simp3 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> 0 e/ Z )
5 1 2 3 4 absprodnn 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( abs ` prod_ k e. Z k ) e. NN )
6 breq2 
 |-  ( n = ( abs ` prod_ k e. Z k ) -> ( m || n <-> m || ( abs ` prod_ k e. Z k ) ) )
7 6 ralbidv 
 |-  ( n = ( abs ` prod_ k e. Z k ) -> ( A. m e. Z m || n <-> A. m e. Z m || ( abs ` prod_ k e. Z k ) ) )
8 7 adantl 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) /\ n = ( abs ` prod_ k e. Z k ) ) -> ( A. m e. Z m || n <-> A. m e. Z m || ( abs ` prod_ k e. Z k ) ) )
9 1 2 3 absproddvds 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> A. m e. Z m || ( abs ` prod_ k e. Z k ) )
10 5 8 9 rspcedvd 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> E. n e. NN A. m e. Z m || n )