Metamath Proof Explorer

Theorem lcmfdvds

Description: The least common multiple of a set of integers divides any integer which is divisible by all elements of the set. (Contributed by AV, 26-Aug-2020)

Ref Expression
Assertion lcmfdvds ⊢ K ∈ ℤ ∧ Z ⊆ ℤ ∧ Z ∈ Fin → ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ∥ K

Proof

Step Hyp Ref Expression
1 breq2 ⊢ k = K → m ∥ k ↔ m ∥ K
2 1 ralbidv ⊢ k = K → ∀ m ∈ Z m ∥ k ↔ ∀ m ∈ Z m ∥ K
3 breq2 ⊢ k = K → lcm _ ⁡ Z ∥ k ↔ lcm _ ⁡ Z ∥ K
4 2 3 imbi12d ⊢ k = K → ∀ m ∈ Z m ∥ k → lcm _ ⁡ Z ∥ k ↔ ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ∥ K
5 4 rspccv ⊢ ∀ k ∈ ℤ ∀ m ∈ Z m ∥ k → lcm _ ⁡ Z ∥ k → K ∈ ℤ → ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ∥ K
6 5 adantr ⊢ ∀ k ∈ ℤ ∀ m ∈ Z m ∥ k → lcm _ ⁡ Z ∥ k ∧ ∀ n ∈ ℤ lcm _ ⁡ Z ∪ n = lcm _ ⁡ Z lcm n → K ∈ ℤ → ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ∥ K
7 lcmfunsnlem ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → ∀ k ∈ ℤ ∀ m ∈ Z m ∥ k → lcm _ ⁡ Z ∥ k ∧ ∀ n ∈ ℤ lcm _ ⁡ Z ∪ n = lcm _ ⁡ Z lcm n
8 6 7 syl11 ⊢ K ∈ ℤ → Z ⊆ ℤ ∧ Z ∈ Fin → ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ∥ K
9 8 3impib ⊢ K ∈ ℤ ∧ Z ⊆ ℤ ∧ Z ∈ Fin → ∀ m ∈ Z m ∥ K → lcm _ ⁡ Z ∥ K