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 ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → 𝑍 ⊆ ℤ )
2 simp2 ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → 𝑍 ∈ Fin )
3 eqid ⊢ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) = ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 )
4 simp3 ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → 0 ∉ 𝑍 )
5 1 2 3 4 absprodnn ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ∈ ℕ )
6 breq2 ⊢ ( 𝑛 = ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) → ( 𝑚 ∥ 𝑛 ↔ 𝑚 ∥ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ) )
7 6 ralbidv ⊢ ( 𝑛 = ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 ↔ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ) )
8 7 adantl ⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ 𝑛 = ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 ↔ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) ) )
9 1 2 3 absproddvds ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ∀ 𝑚 ∈ 𝑍 𝑚 ∥ ( abs ‘ ∏ 𝑘 ∈ 𝑍 𝑘 ) )
10 5 8 9 rspcedvd ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 )