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∈Zx∥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∈Zx∥lcm_⁡Z
10 df-nel ⊢0∉Z↔¬0∈Z
11 lcmfcllem ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→lcm_⁡Z∈n∈ℕ|∀x∈Zx∥n
12 11 3expa ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→lcm_⁡Z∈n∈ℕ|∀x∈Zx∥n
13 10 12 sylan2br ⊢Z⊆ℤ∧Z∈Fin∧¬0∈Z→lcm_⁡Z∈n∈ℕ|∀x∈Zx∥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∈Zx∥n↔∀x∈Zx∥lcm_⁡Z
19 18 elrab3 ⊢lcm_⁡Z∈ℕ→lcm_⁡Z∈n∈ℕ|∀x∈Zx∥n↔∀x∈Zx∥lcm_⁡Z
20 16 19 syl ⊢Z⊆ℤ∧Z∈Fin∧¬0∈Z→lcm_⁡Z∈n∈ℕ|∀x∈Zx∥n↔∀x∈Zx∥lcm_⁡Z
21 13 20 mpbid ⊢Z⊆ℤ∧Z∈Fin∧¬0∈Z→∀x∈Zx∥lcm_⁡Z
22 9 21 pm2.61dan ⊢Z⊆ℤ∧Z∈Fin→∀x∈Zx∥lcm_⁡Z