This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ELEMENTARY NUMBER THEORY Elementary properties of divisibility The least common multiple 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 ∉ 𝑍 ) → { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ≠ ∅ )