Theorem fissn0dvdsn0

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	fissn0dvdsn0	|- ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> { n e. NN | A. m e. Z m || n } =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		fissn0dvds	|- ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> E. n e. NN A. m e. Z m || n )
2		rabn0	|- ( { n e. NN | A. m e. Z m || n } =/= (/) <-> E. n e. NN A. m e. Z m || n )
3	1 2	sylibr	|- ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> { n e. NN | A. m e. Z m || n } =/= (/) )