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 ∈ Z m ∥ n

Proof

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