Metamath Proof Explorer

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 ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → n ∈ ℕ | ∀ m ∈ Z m ∥ n ≠ ∅

Proof

Step Hyp Ref Expression
1 fissn0dvds ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → ∃ n ∈ ℕ ∀ m ∈ Z m ∥ n
2 rabn0 ⊢ n ∈ ℕ | ∀ m ∈ Z m ∥ n ≠ ∅ ↔ ∃ n ∈ ℕ ∀ m ∈ Z m ∥ n
3 1 2 sylibr ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → n ∈ ℕ | ∀ m ∈ Z m ∥ n ≠ ∅