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 ⊢ 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 ≠ ∅