Metamath Proof Explorer

Theorem lcmfcllem

Description: Lemma for lcmfn0cl and dvdslcmf . (Contributed by AV, 21-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfcllem ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→lcm_⁡Z∈n∈ℕ|∀m∈Zm∥n

Proof

Step Hyp Ref Expression
1 lcmfn0val ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→lcm_⁡Z=supn∈ℕ|∀m∈Zm∥nℝ<
2 ssrab2 ⊢n∈ℕ|∀m∈Zm∥n⊆ℕ
3 nnuz ⊢ℕ=ℤ≥1
4 2 3 sseqtri ⊢n∈ℕ|∀m∈Zm∥n⊆ℤ≥1
5 fissn0dvdsn0 ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→n∈ℕ|∀m∈Zm∥n≠∅
6 infssuzcl ⊢n∈ℕ|∀m∈Zm∥n⊆ℤ≥1∧n∈ℕ|∀m∈Zm∥n≠∅→supn∈ℕ|∀m∈Zm∥nℝ<∈n∈ℕ|∀m∈Zm∥n
7 4 5 6 sylancr ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→supn∈ℕ|∀m∈Zm∥nℝ<∈n∈ℕ|∀m∈Zm∥n
8 1 7 eqeltrd ⊢Z⊆ℤ∧Z∈Fin∧0∉Z→lcm_⁡Z∈n∈ℕ|∀m∈Zm∥n