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

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → Z ⊆ ℤ
2 simp2 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → Z ∈ Fin
3 eqid ⊢ ∏ k ∈ Z k = ∏ k ∈ Z k
4 simp3 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → 0 ∉ Z
5 1 2 3 4 absprodnn ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → ∏ k ∈ Z k ∈ ℕ
6 breq2 ⊢ n = ∏ k ∈ Z k → m ∥ n ↔ m ∥ ∏ k ∈ Z k
7 6 ralbidv ⊢ n = ∏ k ∈ Z k → ∀ m ∈ Z m ∥ n ↔ ∀ m ∈ Z m ∥ ∏ k ∈ Z k
8 7 adantl ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z ∧ n = ∏ k ∈ Z k → ∀ m ∈ Z m ∥ n ↔ ∀ m ∈ Z m ∥ ∏ k ∈ Z k
9 1 2 3 absproddvds ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → ∀ m ∈ Z m ∥ ∏ k ∈ Z k
10 5 8 9 rspcedvd ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → ∃ n ∈ ℕ ∀ m ∈ Z m ∥ n