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