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	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		fissn0dvds	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 )
2		rabn0	⊢ ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ≠ ∅ ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 )
3	1 2	sylibr	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ≠ ∅ )