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

Metamath Proof Explorer

Theorem lcmfunsn

Description: The _lcm function for a union of a set of integer and a singleton. (Contributed by AV, 26-Aug-2020)

Ref Expression
Assertion lcmfunsn ⊢ Y ⊆ ℤ ∧ Y ∈ Fin ∧ N ∈ ℤ → lcm _ ⁡ Y ∪ N = lcm _ ⁡ Y lcm N

Proof

Step Hyp Ref Expression
1 lcmfunsnlem ⊢ Y ⊆ ℤ ∧ Y ∈ Fin → ∀ k ∈ ℤ ∀ m ∈ Y m ∥ k → lcm _ ⁡ Y ∥ k ∧ ∀ n ∈ ℤ lcm _ ⁡ Y ∪ n = lcm _ ⁡ Y lcm n
2 sneq ⊢ n = N → n = N
3 2 uneq2d ⊢ n = N → Y ∪ n = Y ∪ N
4 3 fveq2d ⊢ n = N → lcm _ ⁡ Y ∪ n = lcm _ ⁡ Y ∪ N
5 oveq2 ⊢ n = N → lcm _ ⁡ Y lcm n = lcm _ ⁡ Y lcm N
6 4 5 eqeq12d ⊢ n = N → lcm _ ⁡ Y ∪ n = lcm _ ⁡ Y lcm n ↔ lcm _ ⁡ Y ∪ N = lcm _ ⁡ Y lcm N
7 6 rspccv ⊢ ∀ n ∈ ℤ lcm _ ⁡ Y ∪ n = lcm _ ⁡ Y lcm n → N ∈ ℤ → lcm _ ⁡ Y ∪ N = lcm _ ⁡ Y lcm N
8 1 7 simpl2im ⊢ Y ⊆ ℤ ∧ Y ∈ Fin → N ∈ ℤ → lcm _ ⁡ Y ∪ N = lcm _ ⁡ Y lcm N
9 8 3impia ⊢ Y ⊆ ℤ ∧ Y ∈ Fin ∧ N ∈ ℤ → lcm _ ⁡ Y ∪ N = lcm _ ⁡ Y lcm N