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 ‘ 𝑍 ) } ) ) )