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 breq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑚 ∥ 𝑘 ↔ 𝑚 ∥ 𝐾 ) )
7 6 ralbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 ↔ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) )
8 7 elrab ⊢ ( 𝐾 ∈ { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } ↔ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) )
9 8 bilanri ⊢ ( ( 𝑍 ⊆ ℤ ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → 𝐾 ∈ { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } )
10 infssuzle ⊢ ( ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝐾 ∈ { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } ) → inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } , ℝ , < ) ≤ 𝐾 )
11 5 9 10 sylancr ⊢ ( ( 𝑍 ⊆ ℤ ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } , ℝ , < ) ≤ 𝐾 )
12 11 3ad2antl1 ⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → inf ( { 𝑘 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 } , ℝ , < ) ≤ 𝐾 )
13 2 12 eqbrtrd ⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) ∧ ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) ) → ( lcm ‘ 𝑍 ) ≤ 𝐾 )
14 13 ex ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → ( ( 𝐾 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) → ( lcm ‘ 𝑍 ) ≤ 𝐾 ) )