This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑍 ) )