Metamath Proof Explorer


Theorem lcmfass

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

Ref Expression
Assertion lcmfass ( ( ( 𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ) ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ) → ( lcm ‘ ( { ( lcm𝑌 ) } ∪ 𝑍 ) ) = ( lcm ‘ ( 𝑌 ∪ { ( lcm𝑍 ) } ) ) )

Proof

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