Step | Hyp | Ref
| Expression |
1 | | elun 4125 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ (𝑖 ∈ (𝑦 ∪ {𝑧}) ∨ 𝑖 ∈ {𝑛})) |
2 | | elun 4125 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧})) |
3 | | simp1 1132 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑧 ∈
ℤ) |
4 | 3 | adantr 483 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∈
ℤ) |
5 | 4 | adantl 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑧 ∈ ℤ) |
6 | | sneq 4577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑧 → {𝑛} = {𝑧}) |
7 | 6 | uneq2d 4139 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑧 → (𝑦 ∪ {𝑛}) = (𝑦 ∪ {𝑧})) |
8 | 7 | fveq2d 6674 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑧 → (lcm‘(𝑦 ∪ {𝑛})) = (lcm‘(𝑦 ∪ {𝑧}))) |
9 | | oveq2 7164 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑧 → ((lcm‘𝑦) lcm 𝑛) = ((lcm‘𝑦) lcm 𝑧)) |
10 | 8, 9 | eqeq12d 2837 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑧 → ((lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) ↔ (lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧))) |
11 | 10 | rspcv 3618 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ℤ →
(∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) |
12 | 5, 11 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) |
13 | | breq1 5069 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑖 → (𝑘 ∥ (lcm‘𝑦) ↔ 𝑖 ∥ (lcm‘𝑦))) |
14 | 13 | rspcv 3618 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ 𝑦 → (∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦) → 𝑖 ∥ (lcm‘𝑦))) |
15 | | dvdslcmf 15975 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦)) |
16 | 15 | 3adant1 1126 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦)) |
17 | 16 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦)) |
18 | 14, 17 | impel 508 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (lcm‘𝑦)) |
19 | | lcmfcl 15972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℕ0) |
20 | 19 | nn0zd 12086 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) |
21 | 20 | 3adant1 1126 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) |
22 | 21 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
(lcm‘𝑦) ∈
ℤ) |
23 | | lcmcl 15945 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈
ℕ0) |
24 | 3, 23 | sylan 582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈
ℕ0) |
25 | 24 | nn0zd 12086 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈ ℤ) |
26 | 22, 25 | jca 514 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦)
∈ ℤ ∧ (𝑧 lcm
𝑛) ∈
ℤ)) |
27 | 26 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘𝑦)
∈ ℤ ∧ (𝑧 lcm
𝑛) ∈
ℤ)) |
28 | | dvdslcm 15942 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((lcm‘𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) →
((lcm‘𝑦)
∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)) ∧ (𝑧 lcm 𝑛) ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)))) |
29 | 28 | simpld 497 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((lcm‘𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) →
(lcm‘𝑦)
∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
(lcm‘𝑦)
∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
31 | | ssel 3961 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ⊆ ℤ → (𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ)) |
32 | 31 | 3ad2ant2 1130 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ)) |
33 | 32 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ)) |
34 | 33 | impcom 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∈ ℤ) |
35 | 22 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
(lcm‘𝑦) ∈
ℤ) |
36 | 25 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (𝑧 lcm 𝑛) ∈ ℤ) |
37 | | lcmcl 15945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((lcm‘𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) →
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛)) ∈
ℕ0) |
38 | 35, 36, 37 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛)) ∈
ℕ0) |
39 | 38 | nn0zd 12086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛)) ∈ ℤ) |
40 | | dvdstr 15646 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℤ ∧
(lcm‘𝑦) ∈
ℤ ∧ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)) ∈ ℤ) → ((𝑖 ∥ (lcm‘𝑦) ∧ (lcm‘𝑦) ∥
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛))) → 𝑖 ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)))) |
41 | 34, 35, 39, 40 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → ((𝑖 ∥ (lcm‘𝑦) ∧ (lcm‘𝑦) ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) → 𝑖 ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)))) |
42 | 18, 30, 41 | mp2and 697 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
43 | 4 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑧 ∈ ℤ) |
44 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑛 ∈ ℤ) |
45 | | lcmass 15958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) = ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
46 | 35, 43, 44, 45 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) = ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
47 | 42, 46 | breqtrrd 5094 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) |
48 | 47 | ex 415 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ 𝑦 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
49 | | elsni 4584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ {𝑧} → 𝑖 = 𝑧) |
50 | 21, 3 | jca 514 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
((lcm‘𝑦)
∈ ℤ ∧ 𝑧
∈ ℤ)) |
51 | 50 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦)
∈ ℤ ∧ 𝑧
∈ ℤ)) |
52 | | dvdslcm 15942 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
((lcm‘𝑦)
∥ ((lcm‘𝑦) lcm 𝑧) ∧ 𝑧 ∥ ((lcm‘𝑦) lcm 𝑧))) |
53 | 52 | simprd 498 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) → 𝑧 ∥ ((lcm‘𝑦) lcm 𝑧)) |
54 | 51, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∥
((lcm‘𝑦) lcm
𝑧)) |
55 | 19 | 3adant1 1126 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℕ0) |
56 | 55 | nn0zd 12086 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) |
57 | | lcmcl 15945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∈
ℕ0) |
58 | 56, 3, 57 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
((lcm‘𝑦) lcm
𝑧) ∈
ℕ0) |
59 | 58 | nn0zd 12086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
((lcm‘𝑦) lcm
𝑧) ∈
ℤ) |
60 | | dvdslcm 15942 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((lcm‘𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∧ 𝑛 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
61 | 60 | simpld 497 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((lcm‘𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) |
62 | 59, 61 | sylan 582 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) |
63 | 59 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∈
ℤ) |
64 | | lcmcl 15945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((lcm‘𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈
ℕ0) |
65 | 59, 64 | sylan 582 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈
ℕ0) |
66 | 65 | nn0zd 12086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈ ℤ) |
67 | | dvdstr 15646 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧
((lcm‘𝑦) lcm
𝑧) ∈ ℤ ∧
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈ ℤ) → ((𝑧 ∥ ((lcm‘𝑦) lcm 𝑧) ∧ ((lcm‘𝑦) lcm 𝑧) ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) → 𝑧 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
68 | 4, 63, 66, 67 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑧 ∥
((lcm‘𝑦) lcm
𝑧) ∧
((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) → 𝑧 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
69 | 54, 62, 68 | mp2and 697 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) |
70 | | breq1 5069 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑧 → (𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛) ↔ 𝑧 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
71 | 69, 70 | syl5ibr 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑧 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
72 | 49, 71 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ {𝑧} → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
73 | 48, 72 | jaoi 853 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
74 | 73 | imp 409 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) |
75 | | oveq1 7163 |
. . . . . . . . . . . . . . . . 17
⊢
((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) |
76 | 75 | breq2d 5078 |
. . . . . . . . . . . . . . . 16
⊢
((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ↔ 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
77 | 74, 76 | syl5ibrcom 249 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛))) |
78 | 12, 77 | syld 47 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛))) |
79 | 78 | ex 415 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
80 | 2, 79 | sylbi 219 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (𝑦 ∪ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
81 | | elsni 4584 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ {𝑛} → 𝑖 = 𝑛) |
82 | | simp2 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ⊆
ℤ) |
83 | | snssi 4741 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ ℤ → {𝑧} ⊆
ℤ) |
84 | 83 | 3ad2ant1 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → {𝑧} ⊆
ℤ) |
85 | 82, 84 | unssd 4162 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ⊆ ℤ) |
86 | | simp3 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin) |
87 | | snfi 8594 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {𝑧} ∈ Fin |
88 | | unfi 8785 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
89 | 86, 87, 88 | sylancl 588 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
90 | | lcmfcl 15972 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑦 ∪ {𝑧}) ∈ Fin) →
(lcm‘(𝑦 ∪
{𝑧})) ∈
ℕ0) |
91 | 85, 89, 90 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘(𝑦 ∪
{𝑧})) ∈
ℕ0) |
92 | 91 | nn0zd 12086 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘(𝑦 ∪
{𝑧})) ∈
ℤ) |
93 | 92 | anim1i 616 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘(𝑦 ∪
{𝑧})) ∈ ℤ ∧
𝑛 ∈
ℤ)) |
94 | 93 | adantr 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧
∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) →
((lcm‘(𝑦 ∪
{𝑧})) ∈ ℤ ∧
𝑛 ∈
ℤ)) |
95 | | dvdslcm 15942 |
. . . . . . . . . . . . . . . . 17
⊢
(((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((lcm‘(𝑦 ∪
{𝑧})) ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛) ∧ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧
∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) →
((lcm‘(𝑦 ∪
{𝑧})) ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛) ∧ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
97 | 96 | simprd 498 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧
∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) → 𝑛 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)) |
98 | | breq1 5069 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → (𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ↔ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
99 | 97, 98 | syl5ibr 248 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ ∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛))) |
100 | 99 | expd 418 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
101 | 81, 100 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ {𝑛} → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
102 | 80, 101 | jaoi 853 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ (𝑦 ∪ {𝑧}) ∨ 𝑖 ∈ {𝑛}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
103 | 1, 102 | sylbi 219 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
104 | 103 | com13 88 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))) |
105 | 104 | expd 418 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))) |
106 | 105 | adantl 484 |
. . . . . . 7
⊢
((∀𝑘 ∈
ℤ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)) → ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))) |
107 | 106 | impcom 410 |
. . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))) |
108 | 107 | impcom 410 |
. . . . 5
⊢ ((𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)))) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
109 | 108 | adantl 484 |
. . . 4
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
110 | 109 | ralrimiv 3181 |
. . 3
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)) |
111 | | lcmfunsnlem2lem1 15982 |
. . 3
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)) |
112 | 93 | adantr 483 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ)) |
113 | 85 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑦 ∪ {𝑧}) ⊆ ℤ) |
114 | 89 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑦 ∪ {𝑧}) ∈ Fin) |
115 | | df-nel 3124 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0
∉ 𝑦 ↔ ¬ 0
∈ 𝑦) |
116 | 115 | biimpi 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0
∉ 𝑦 → ¬ 0
∈ 𝑦) |
117 | 116 | 3ad2ant1 1129 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ 𝑦) |
118 | | elsni 4584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
{𝑧} → 0 = 𝑧) |
119 | 118 | eqcomd 2827 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
{𝑧} → 𝑧 = 0) |
120 | 119 | necon3ai 3041 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ≠ 0 → ¬ 0 ∈
{𝑧}) |
121 | 120 | 3ad2ant2 1130 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ {𝑧}) |
122 | | ioran 980 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬ (0
∈ 𝑦 ∨ 0 ∈
{𝑧}) ↔ (¬ 0 ∈
𝑦 ∧ ¬ 0 ∈
{𝑧})) |
123 | 117, 121,
122 | sylanbrc 585 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧})) |
124 | | elun 4125 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
(𝑦 ∪ {𝑧}) ↔ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧})) |
125 | 123, 124 | sylnibr 331 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ (𝑦 ∪ {𝑧})) |
126 | | df-nel 3124 |
. . . . . . . . . . . . . . . 16
⊢ (0
∉ (𝑦 ∪ {𝑧}) ↔ ¬ 0 ∈ (𝑦 ∪ {𝑧})) |
127 | 125, 126 | sylibr 236 |
. . . . . . . . . . . . . . 15
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → 0 ∉ (𝑦 ∪ {𝑧})) |
128 | | lcmfn0cl 15970 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑦 ∪ {𝑧}) ∈ Fin ∧ 0 ∉ (𝑦 ∪ {𝑧})) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ) |
129 | 113, 114,
127, 128 | syl2an3an 1418 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ) |
130 | 129 | nnne0d 11688 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (lcm‘(𝑦 ∪ {𝑧})) ≠ 0) |
131 | 130 | neneqd 3021 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬
(lcm‘(𝑦 ∪
{𝑧})) = 0) |
132 | | neneq 3022 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ≠ 0 → ¬ 𝑛 = 0) |
133 | 132 | 3ad2ant3 1131 |
. . . . . . . . . . . . 13
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 𝑛 = 0) |
134 | 133 | adantl 484 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬ 𝑛 = 0) |
135 | | ioran 980 |
. . . . . . . . . . . 12
⊢ (¬
((lcm‘(𝑦 ∪
{𝑧})) = 0 ∨ 𝑛 = 0) ↔ (¬
(lcm‘(𝑦 ∪
{𝑧})) = 0 ∧ ¬ 𝑛 = 0)) |
136 | 131, 134,
135 | sylanbrc 585 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬
((lcm‘(𝑦 ∪
{𝑧})) = 0 ∨ 𝑛 = 0)) |
137 | | lcmn0cl 15941 |
. . . . . . . . . . 11
⊢
((((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬
((lcm‘(𝑦 ∪
{𝑧})) = 0 ∨ 𝑛 = 0)) →
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛) ∈
ℕ) |
138 | 112, 136,
137 | syl2anc 586 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ) |
139 | | snssi 4741 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → {𝑛} ⊆
ℤ) |
140 | 139 | adantl 484 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → {𝑛} ⊆
ℤ) |
141 | 113, 140 | unssd 4162 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ) |
142 | 141 | adantr 483 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ) |
143 | 87, 88 | mpan2 689 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ Fin → (𝑦 ∪ {𝑧}) ∈ Fin) |
144 | | snfi 8594 |
. . . . . . . . . . . . . . 15
⊢ {𝑛} ∈ Fin |
145 | | unfi 8785 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ {𝑛} ∈ Fin) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
146 | 143, 144,
145 | sylancl 588 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
147 | 146 | 3ad2ant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
148 | 147 | adantr 483 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
149 | 148 | adantr 483 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
150 | | elun 4125 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ (0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛})) |
151 | | nnel 3132 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬ 0
∉ 𝑦 ↔ 0 ∈
𝑦) |
152 | 151 | biimpri 230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
𝑦 → ¬ 0 ∉
𝑦) |
153 | 152 | 3mix1d 1332 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
𝑦 → (¬ 0 ∉
𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
154 | | nne 3020 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑧 ≠ 0 ↔ 𝑧 = 0) |
155 | 119, 154 | sylibr 236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
{𝑧} → ¬ 𝑧 ≠ 0) |
156 | 155 | 3mix2d 1333 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
{𝑧} → (¬ 0 ∉
𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
157 | 153, 156 | jaoi 853 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ 𝑦 ∨ 0 ∈
{𝑧}) → (¬ 0
∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
158 | 124, 157 | sylbi 219 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
(𝑦 ∪ {𝑧}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
159 | | elsni 4584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
{𝑛} → 0 = 𝑛) |
160 | 159 | eqcomd 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
{𝑛} → 𝑛 = 0) |
161 | | nne 3020 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑛 ≠ 0 ↔ 𝑛 = 0) |
162 | 160, 161 | sylibr 236 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
{𝑛} → ¬ 𝑛 ≠ 0) |
163 | 162 | 3mix3d 1334 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
{𝑛} → (¬ 0 ∉
𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
164 | 158, 163 | jaoi 853 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
165 | 150, 164 | sylbi 219 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
((𝑦 ∪ {𝑧}) ∪ {𝑛}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
166 | | 3ianor 1103 |
. . . . . . . . . . . . . . 15
⊢ (¬ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ↔ (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
167 | 165, 166 | sylibr 236 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
((𝑦 ∪ {𝑧}) ∪ {𝑛}) → ¬ (0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) |
168 | 167 | con2i 141 |
. . . . . . . . . . . . 13
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) |
169 | | df-nel 3124 |
. . . . . . . . . . . . 13
⊢ (0
∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ ¬ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) |
170 | 168, 169 | sylibr 236 |
. . . . . . . . . . . 12
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) |
171 | 170 | adantl 484 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) |
172 | 142, 149,
171 | 3jca 1124 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))) |
173 | 138, 172 | jca 514 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))) |
174 | 173 | ex 415 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))) |
175 | 174 | ex 415 |
. . . . . . 7
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))))) |
176 | 175 | adantr 483 |
. . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑛 ∈ ℤ → ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))))) |
177 | 176 | impcom 410 |
. . . . 5
⊢ ((𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)))) → ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))) |
178 | 177 | impcom 410 |
. . . 4
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))) |
179 | | lcmf 15977 |
. . . 4
⊢
((((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) ↔ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)))) |
180 | 178, 179 | syl 17 |
. . 3
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) ↔ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)))) |
181 | 110, 111,
180 | mpbir2and 711 |
. 2
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛}))) |
182 | 181 | eqcomd 2827 |
1
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)) |