Metamath Proof Explorer

Theorem lcmfledvds

Description: A positive integer which is divisible by all elements of a set of integers bounds the least common multiple of the set. (Contributed by AV, 22-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfledvds ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ≤ K

Proof

Step Hyp Ref Expression
1 lcmfn0val ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z = inf k ∈ ℕ | ∀ m ∈ Z m ∥ k ℝ <
2 1 adantr ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z = inf k ∈ ℕ | ∀ m ∈ Z m ∥ k ℝ <
3 ssrab2 ⊢ k ∈ ℕ | ∀ m ∈ Z m ∥ k ⊆ ℕ
4 nnuz ⊢ ℕ = ℤ ≥ 1
5 3 4 sseqtri ⊢ k ∈ ℕ | ∀ m ∈ Z m ∥ k ⊆ ℤ ≥ 1
6 breq2 ⊢ k = K → m ∥ k ↔ m ∥ K
7 6 ralbidv ⊢ k = K → ∀ m ∈ Z m ∥ k ↔ ∀ m ∈ Z m ∥ K
8 7 elrab ⊢ K ∈ k ∈ ℕ | ∀ m ∈ Z m ∥ k ↔ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K
9 8 bilanri ⊢ Z ⊆ ℤ ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → K ∈ k ∈ ℕ | ∀ m ∈ Z m ∥ k
10 infssuzle ⊢ k ∈ ℕ | ∀ m ∈ Z m ∥ k ⊆ ℤ ≥ 1 ∧ K ∈ k ∈ ℕ | ∀ m ∈ Z m ∥ k → inf k ∈ ℕ | ∀ m ∈ Z m ∥ k ℝ < ≤ K
11 5 9 10 sylancr ⊢ Z ⊆ ℤ ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → inf k ∈ ℕ | ∀ m ∈ Z m ∥ k ℝ < ≤ K
12 11 3ad2antl1 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → inf k ∈ ℕ | ∀ m ∈ Z m ∥ k ℝ < ≤ K
13 2 12 eqbrtrd ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ≤ K
14 13 ex ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ≤ K