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

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