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 ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ∀ 𝑥𝑍 𝑥 ∥ ( lcm𝑍 ) )

Proof

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