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 = sup k ∈ ℕ | ∀ m ∈ Z m ∥ k ℝ <
2 1 adantr ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z = sup 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 simpr ⊢ Z ⊆ ℤ ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K
7 breq2 ⊢ k = K → m ∥ k ↔ m ∥ K
8 7 ralbidv ⊢ k = K → ∀ m ∈ Z m ∥ k ↔ ∀ m ∈ Z m ∥ K
9 8 elrab ⊢ K ∈ k ∈ ℕ | ∀ m ∈ Z m ∥ k ↔ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K
10 6 9 sylibr ⊢ Z ⊆ ℤ ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → K ∈ k ∈ ℕ | ∀ m ∈ Z m ∥ k
11 infssuzle ⊢ k ∈ ℕ | ∀ m ∈ Z m ∥ k ⊆ ℤ ≥ 1 ∧ K ∈ k ∈ ℕ | ∀ m ∈ Z m ∥ k → sup k ∈ ℕ | ∀ m ∈ Z m ∥ k ℝ < ≤ K
12 5 10 11 sylancr ⊢ Z ⊆ ℤ ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → sup k ∈ ℕ | ∀ m ∈ Z m ∥ k ℝ < ≤ K
13 12 3ad2antl1 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → sup k ∈ ℕ | ∀ m ∈ Z m ∥ k ℝ < ≤ K
14 2 13 eqbrtrd ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z ∧ K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ≤ K
15 14 ex ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → K ∈ ℕ ∧ ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ≤ K