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

Metamath Proof Explorer

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