Metamath Proof Explorer


Theorem lcmfledvds

Description: A positive integer which is divisible by all elements of a set of integers bounds the least common multiple of the set. (Contributed by AV, 22-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfledvds ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) → ( lcm𝑍 ) ≤ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 lcmfn0val ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( lcm𝑍 ) = inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } , ℝ , < ) )
2 1 adantr ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) ) → ( lcm𝑍 ) = inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } , ℝ , < ) )
3 ssrab2 { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } ⊆ ℕ
4 nnuz ℕ = ( ℤ ‘ 1 )
5 3 4 sseqtri { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } ⊆ ( ℤ ‘ 1 )
6 simpr ( ( 𝑍 ⊆ ℤ ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) ) → ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) )
7 breq2 ( 𝑘 = 𝐾 → ( 𝑚𝑘𝑚𝐾 ) )
8 7 ralbidv ( 𝑘 = 𝐾 → ( ∀ 𝑚𝑍 𝑚𝑘 ↔ ∀ 𝑚𝑍 𝑚𝐾 ) )
9 8 elrab ( 𝐾 ∈ { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } ↔ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) )
10 6 9 sylibr ( ( 𝑍 ⊆ ℤ ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) ) → 𝐾 ∈ { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } )
11 infssuzle ( ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } ⊆ ( ℤ ‘ 1 ) ∧ 𝐾 ∈ { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } ) → inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } , ℝ , < ) ≤ 𝐾 )
12 5 10 11 sylancr ( ( 𝑍 ⊆ ℤ ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) ) → inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } , ℝ , < ) ≤ 𝐾 )
13 12 3ad2antl1 ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) ) → inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚𝑍 𝑚𝑘 } , ℝ , < ) ≤ 𝐾 )
14 2 13 eqbrtrd ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) ) → ( lcm𝑍 ) ≤ 𝐾 )
15 14 ex ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( ( 𝐾 ∈ ℕ ∧ ∀ 𝑚𝑍 𝑚𝐾 ) → ( lcm𝑍 ) ≤ 𝐾 ) )