Theorem lcmfdvds

Description: The least common multiple of a set of integers divides any integer which is divisible by all elements of the set. (Contributed by AV, 26-Aug-2020)

	Ref	Expression
Assertion	lcmfdvds	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → ( lcm ‘ 𝑍 ) ∥ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑘 = 𝐾 → ( 𝑚 ∥ 𝑘 ↔ 𝑚 ∥ 𝐾 ) )
2	1	ralbidv	⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 ↔ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) )
3		breq2	⊢ ( 𝑘 = 𝐾 → ( ( lcm ‘ 𝑍 ) ∥ 𝑘 ↔ ( lcm ‘ 𝑍 ) ∥ 𝐾 ) )
4	2 3	imbi12d	⊢ ( 𝑘 = 𝐾 → ( ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑍 ) ∥ 𝑘 ) ↔ ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → ( lcm ‘ 𝑍 ) ∥ 𝐾 ) ) )
5	4	rspccv	⊢ ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑍 ) ∥ 𝑘 ) → ( 𝐾 ∈ ℤ → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → ( lcm ‘ 𝑍 ) ∥ 𝐾 ) ) )
6	5	adantr	⊢ ( ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑍 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑍 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑍 ) lcm 𝑛 ) ) → ( 𝐾 ∈ ℤ → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → ( lcm ‘ 𝑍 ) ∥ 𝐾 ) ) )
7		lcmfunsnlem	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ∀ 𝑘 ∈ ℤ ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → ( lcm ‘ 𝑍 ) ∥ 𝑘 ) ∧ ∀ 𝑛 ∈ ℤ ( lcm ‘ ( 𝑍 ∪ { 𝑛 } ) ) = ( ( lcm ‘ 𝑍 ) lcm 𝑛 ) ) )
8	6 7	syl11	⊢ ( 𝐾 ∈ ℤ → ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → ( lcm ‘ 𝑍 ) ∥ 𝐾 ) ) )
9	8	3impib	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → ( lcm ‘ 𝑍 ) ∥ 𝐾 ) )