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 ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm𝑍 ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } )

Proof

Step Hyp Ref Expression
1 lcmfn0val ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm𝑍 ) = inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } , ℝ , < ) )
2 ssrab2 { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } ⊆ ℕ
3 nnuz ℕ = ( ℤ ‘ 1 )
4 2 3 sseqtri { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } ⊆ ( ℤ ‘ 1 )
5 fissn0dvdsn0 ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } ≠ ∅ )
6 infssuzcl ( ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } ⊆ ( ℤ ‘ 1 ) ∧ { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } )
7 4 5 6 sylancr ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } )
8 1 7 eqeltrd ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm𝑍 ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑛 } )