Metamath Proof Explorer

Theorem dvdslcmf

Description: The least common multiple of a set of integers is divisible by each of its elements. (Contributed by AV, 22-Aug-2020)

Ref Expression
Assertion dvdslcmf ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → ∀ x ∈ Z x ∥ lcm _ ⁡ Z

Proof

Step Hyp Ref Expression
1 ssel ⊢ Z ⊆ ℤ → x ∈ Z → x ∈ ℤ
2 1 ad2antrr ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∈ Z → x ∈ Z → x ∈ ℤ
3 2 imp ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∈ Z ∧ x ∈ Z → x ∈ ℤ
4 dvds0 ⊢ x ∈ ℤ → x ∥ 0
5 3 4 syl ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∈ Z ∧ x ∈ Z → x ∥ 0
6 lcmf0val ⊢ Z ⊆ ℤ ∧ 0 ∈ Z → lcm _ ⁡ Z = 0
7 6 ad4ant13 ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∈ Z ∧ x ∈ Z → lcm _ ⁡ Z = 0
8 5 7 breqtrrd ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∈ Z ∧ x ∈ Z → x ∥ lcm _ ⁡ Z
9 8 ralrimiva ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∈ Z → ∀ x ∈ Z x ∥ lcm _ ⁡ Z
10 df-nel ⊢ 0 ∉ Z ↔ ¬ 0 ∈ Z
11 lcmfcllem ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ n ∈ ℕ | ∀ x ∈ Z x ∥ n
12 11 3expa ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ n ∈ ℕ | ∀ x ∈ Z x ∥ n
13 10 12 sylan2br ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ ¬ 0 ∈ Z → lcm _ ⁡ Z ∈ n ∈ ℕ | ∀ x ∈ Z x ∥ n
14 lcmfn0cl ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ ℕ
15 14 3expa ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ 0 ∉ Z → lcm _ ⁡ Z ∈ ℕ
16 10 15 sylan2br ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ ¬ 0 ∈ Z → lcm _ ⁡ Z ∈ ℕ
17 breq2 ⊢ n = lcm _ ⁡ Z → x ∥ n ↔ x ∥ lcm _ ⁡ Z
18 17 ralbidv ⊢ n = lcm _ ⁡ Z → ∀ x ∈ Z x ∥ n ↔ ∀ x ∈ Z x ∥ lcm _ ⁡ Z
19 18 elrab3 ⊢ lcm _ ⁡ Z ∈ ℕ → lcm _ ⁡ Z ∈ n ∈ ℕ | ∀ x ∈ Z x ∥ n ↔ ∀ x ∈ Z x ∥ lcm _ ⁡ Z
20 16 19 syl ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ ¬ 0 ∈ Z → lcm _ ⁡ Z ∈ n ∈ ℕ | ∀ x ∈ Z x ∥ n ↔ ∀ x ∈ Z x ∥ lcm _ ⁡ Z
21 13 20 mpbid ⊢ Z ⊆ ℤ ∧ Z ∈ Fin ∧ ¬ 0 ∈ Z → ∀ x ∈ Z x ∥ lcm _ ⁡ Z
22 9 21 pm2.61dan ⊢ Z ⊆ ℤ ∧ Z ∈ Fin → ∀ x ∈ Z x ∥ lcm _ ⁡ Z