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