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∈Zm∥K→lcm_⁡Z∥K

Proof

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