Metamath Proof Explorer

Theorem lcmfass

Description: Associative law for the _lcm function. (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion lcmfass ⊢Y⊆ℤ∧Y∈Fin∧Z⊆ℤ∧Z∈Fin→lcm_⁡lcm_⁡Y∪Z=lcm_⁡Y∪lcm_⁡Z

Proof

Step Hyp Ref Expression
1 lcmfcl ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡Y∈ℕ0
2 1 nn0zd ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡Y∈ℤ
3 lcmfsn ⊢lcm_⁡Y∈ℤ→lcm_⁡lcm_⁡Y=lcm_⁡Y
4 2 3 syl ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡lcm_⁡Y=lcm_⁡Y
5 nn0re ⊢lcm_⁡Y∈ℕ0→lcm_⁡Y∈ℝ
6 nn0ge0 ⊢lcm_⁡Y∈ℕ0→0≤lcm_⁡Y
7 5 6 jca ⊢lcm_⁡Y∈ℕ0→lcm_⁡Y∈ℝ∧0≤lcm_⁡Y
8 absid ⊢lcm_⁡Y∈ℝ∧0≤lcm_⁡Y→lcm_⁡Y=lcm_⁡Y
9 1 7 8 3syl ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡Y=lcm_⁡Y
10 4 9 eqtrd ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡lcm_⁡Y=lcm_⁡Y
11 lcmfcl ⊢Z⊆ℤ∧Z∈Fin→lcm_⁡Z∈ℕ0
12 11 nn0zd ⊢Z⊆ℤ∧Z∈Fin→lcm_⁡Z∈ℤ
13 lcmfsn ⊢lcm_⁡Z∈ℤ→lcm_⁡lcm_⁡Z=lcm_⁡Z
14 12 13 syl ⊢Z⊆ℤ∧Z∈Fin→lcm_⁡lcm_⁡Z=lcm_⁡Z
15 nn0re ⊢lcm_⁡Z∈ℕ0→lcm_⁡Z∈ℝ
16 nn0ge0 ⊢lcm_⁡Z∈ℕ0→0≤lcm_⁡Z
17 15 16 jca ⊢lcm_⁡Z∈ℕ0→lcm_⁡Z∈ℝ∧0≤lcm_⁡Z
18 absid ⊢lcm_⁡Z∈ℝ∧0≤lcm_⁡Z→lcm_⁡Z=lcm_⁡Z
19 11 17 18 3syl ⊢Z⊆ℤ∧Z∈Fin→lcm_⁡Z=lcm_⁡Z
20 14 19 eqtr2d ⊢Z⊆ℤ∧Z∈Fin→lcm_⁡Z=lcm_⁡lcm_⁡Z
21 10 20 oveqan12d ⊢Y⊆ℤ∧Y∈Fin∧Z⊆ℤ∧Z∈Fin→lcm_⁡lcm_⁡Ylcmlcm_⁡Z=lcm_⁡Ylcmlcm_⁡lcm_⁡Z
22 2 snssd ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡Y⊆ℤ
23 snfi ⊢lcm_⁡Y∈Fin
24 22 23 jctir ⊢Y⊆ℤ∧Y∈Fin→lcm_⁡Y⊆ℤ∧lcm_⁡Y∈Fin
25 lcmfun ⊢lcm_⁡Y⊆ℤ∧lcm_⁡Y∈Fin∧Z⊆ℤ∧Z∈Fin→lcm_⁡lcm_⁡Y∪Z=lcm_⁡lcm_⁡Ylcmlcm_⁡Z
26 24 25 sylan ⊢Y⊆ℤ∧Y∈Fin∧Z⊆ℤ∧Z∈Fin→lcm_⁡lcm_⁡Y∪Z=lcm_⁡lcm_⁡Ylcmlcm_⁡Z
27 12 snssd ⊢Z⊆ℤ∧Z∈Fin→lcm_⁡Z⊆ℤ
28 snfi ⊢lcm_⁡Z∈Fin
29 27 28 jctir ⊢Z⊆ℤ∧Z∈Fin→lcm_⁡Z⊆ℤ∧lcm_⁡Z∈Fin
30 lcmfun ⊢Y⊆ℤ∧Y∈Fin∧lcm_⁡Z⊆ℤ∧lcm_⁡Z∈Fin→lcm_⁡Y∪lcm_⁡Z=lcm_⁡Ylcmlcm_⁡lcm_⁡Z
31 29 30 sylan2 ⊢Y⊆ℤ∧Y∈Fin∧Z⊆ℤ∧Z∈Fin→lcm_⁡Y∪lcm_⁡Z=lcm_⁡Ylcmlcm_⁡lcm_⁡Z
32 21 26 31 3eqtr4d ⊢Y⊆ℤ∧Y∈Fin∧Z⊆ℤ∧Z∈Fin→lcm_⁡lcm_⁡Y∪Z=lcm_⁡Y∪lcm_⁡Z