Step | Hyp | Ref
| Expression |
1 | | elun 3753 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ (𝑖 ∈ (𝑦 ∪ {𝑧}) ∨ 𝑖 ∈ {𝑛})) |
2 | | elun 3753 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧})) |
3 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑧 ∈
ℤ) |
4 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∈
ℤ) |
5 | 4 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑧 ∈ ℤ) |
6 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑧 → {𝑛} = {𝑧}) |
7 | 6 | uneq2d 3767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑧 → (𝑦 ∪ {𝑛}) = (𝑦 ∪ {𝑧})) |
8 | 7 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑧 → (lcm‘(𝑦 ∪ {𝑛})) = (lcm‘(𝑦 ∪ {𝑧}))) |
9 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑧 → ((lcm‘𝑦) lcm 𝑛) = ((lcm‘𝑦) lcm 𝑧)) |
10 | 8, 9 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑧 → ((lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) ↔ (lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧))) |
11 | 10 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℤ →
(∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) |
12 | 5, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) |
13 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑖 → (𝑘 ∥ (lcm‘𝑦) ↔ 𝑖 ∥ (lcm‘𝑦))) |
14 | 13 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ 𝑦 → (∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦) → 𝑖 ∥ (lcm‘𝑦))) |
15 | | dvdslcmf 15344 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦)) |
16 | 15 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦)) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦)) |
18 | 14, 17 | impel 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (lcm‘𝑦)) |
19 | | lcmfcl 15341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℕ0) |
20 | 19 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) |
21 | 20 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
(lcm‘𝑦) ∈
ℤ) |
23 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈
ℕ0) |
24 | 3, 23 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈
ℕ0) |
25 | 24 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈ ℤ) |
26 | 22, 25 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦)
∈ ℤ ∧ (𝑧 lcm
𝑛) ∈
ℤ)) |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘𝑦)
∈ ℤ ∧ (𝑧 lcm
𝑛) ∈
ℤ)) |
28 | | dvdslcm 15311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((lcm‘𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) →
((lcm‘𝑦)
∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)) ∧ (𝑧 lcm 𝑛) ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)))) |
29 | 28 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((lcm‘𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) →
(lcm‘𝑦)
∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
(lcm‘𝑦)
∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
31 | | ssel 3597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ⊆ ℤ → (𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ)) |
32 | 31 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ)) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ)) |
34 | 33 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∈ ℤ) |
35 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
(lcm‘𝑦) ∈
ℤ) |
36 | 25 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (𝑧 lcm 𝑛) ∈ ℤ) |
37 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((lcm‘𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) →
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛)) ∈
ℕ0) |
38 | 35, 36, 37 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛)) ∈
ℕ0) |
39 | 38 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛)) ∈ ℤ) |
40 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ ℤ ∧
(lcm‘𝑦) ∈
ℤ ∧ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)) ∈ ℤ) → ((𝑖 ∥ (lcm‘𝑦) ∧ (lcm‘𝑦) ∥
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛))) → 𝑖 ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)))) |
41 | 34, 35, 39, 40 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → ((𝑖 ∥ (lcm‘𝑦) ∧ (lcm‘𝑦) ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) → 𝑖 ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)))) |
42 | 18, 30, 41 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
43 | 4 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑧 ∈ ℤ) |
44 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈
ℤ) |
45 | 44 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑛 ∈ ℤ) |
46 | | lcmass 15327 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) = ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
47 | 35, 43, 45, 46 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) = ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) |
48 | 42, 47 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) |
49 | 48 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝑦 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
50 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ {𝑧} → 𝑖 = 𝑧) |
51 | 21, 3 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
((lcm‘𝑦)
∈ ℤ ∧ 𝑧
∈ ℤ)) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦)
∈ ℤ ∧ 𝑧
∈ ℤ)) |
53 | | dvdslcm 15311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
((lcm‘𝑦)
∥ ((lcm‘𝑦) lcm 𝑧) ∧ 𝑧 ∥ ((lcm‘𝑦) lcm 𝑧))) |
54 | 53 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) → 𝑧 ∥ ((lcm‘𝑦) lcm 𝑧)) |
55 | 52, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∥
((lcm‘𝑦) lcm
𝑧)) |
56 | 19 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℕ0) |
57 | 56 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) |
58 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∈
ℕ0) |
59 | 57, 3, 58 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
((lcm‘𝑦) lcm
𝑧) ∈
ℕ0) |
60 | 59 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
((lcm‘𝑦) lcm
𝑧) ∈
ℤ) |
61 | | dvdslcm 15311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((lcm‘𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∧ 𝑛 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
62 | 61 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((lcm‘𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) |
63 | 60, 62 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) |
64 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∈
ℤ) |
65 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((lcm‘𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈
ℕ0) |
66 | 60, 65 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈
ℕ0) |
67 | 66 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈ ℤ) |
68 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧
((lcm‘𝑦) lcm
𝑧) ∈ ℤ ∧
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈ ℤ) → ((𝑧 ∥ ((lcm‘𝑦) lcm 𝑧) ∧ ((lcm‘𝑦) lcm 𝑧) ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) → 𝑧 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
69 | 4, 64, 67, 68 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑧 ∥
((lcm‘𝑦) lcm
𝑧) ∧
((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) → 𝑧 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
70 | 55, 63, 69 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) |
71 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑧 → (𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛) ↔ 𝑧 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
72 | 70, 71 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑧 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
73 | 50, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ {𝑧} → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
74 | 49, 73 | jaoi 394 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
75 | 74 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) |
76 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢
((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) |
77 | 76 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
⊢
((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ↔ 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) |
78 | 75, 77 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛))) |
79 | 12, 78 | syld 47 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛))) |
80 | 79 | ex 450 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
81 | 2, 80 | sylbi 207 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑦 ∪ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
82 | | elsni 4194 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ {𝑛} → 𝑖 = 𝑛) |
83 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ⊆
ℤ) |
84 | | snssi 4339 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ ℤ → {𝑧} ⊆
ℤ) |
85 | 84 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → {𝑧} ⊆
ℤ) |
86 | 83, 85 | unssd 3789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ⊆ ℤ) |
87 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin) |
88 | | snfi 8038 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑧} ∈ Fin |
89 | | unfi 8227 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
90 | 87, 88, 89 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
91 | | lcmfcl 15341 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑦 ∪ {𝑧}) ∈ Fin) →
(lcm‘(𝑦 ∪
{𝑧})) ∈
ℕ0) |
92 | 86, 90, 91 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘(𝑦 ∪
{𝑧})) ∈
ℕ0) |
93 | 92 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘(𝑦 ∪
{𝑧})) ∈
ℤ) |
94 | 93 | anim1i 592 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘(𝑦 ∪
{𝑧})) ∈ ℤ ∧
𝑛 ∈
ℤ)) |
95 | 94 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧
∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) →
((lcm‘(𝑦 ∪
{𝑧})) ∈ ℤ ∧
𝑛 ∈
ℤ)) |
96 | | dvdslcm 15311 |
. . . . . . . . . . . . . . . . . 18
⊢
(((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((lcm‘(𝑦 ∪
{𝑧})) ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛) ∧ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧
∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) →
((lcm‘(𝑦 ∪
{𝑧})) ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛) ∧ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
98 | 97 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧
∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) → 𝑛 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)) |
99 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑛 → (𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ↔ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
100 | 98, 99 | syl5ibr 236 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ ∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛))) |
101 | 100 | expd 452 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
102 | 82, 101 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ {𝑛} → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
103 | 81, 102 | jaoi 394 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ (𝑦 ∪ {𝑧}) ∨ 𝑖 ∈ {𝑛}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
104 | 1, 103 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) |
105 | 104 | com13 88 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))) |
106 | 105 | expd 452 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))) |
107 | 106 | adantl 482 |
. . . . . . . 8
⊢
((∀𝑘 ∈
ℤ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)) → ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))) |
108 | 107 | impcom 446 |
. . . . . . 7
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))) |
109 | 108 | impcom 446 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)))) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
110 | 109 | adantl 482 |
. . . . 5
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) |
111 | 110 | ralrimiv 2965 |
. . . 4
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)) |
112 | | lcmfunsnlem2lem1 15351 |
. . . 4
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)) |
113 | 111, 112 | jca 554 |
. . 3
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘))) |
114 | 94 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ)) |
115 | 86 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑦 ∪ {𝑧}) ⊆ ℤ) |
116 | 115 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (𝑦 ∪ {𝑧}) ⊆ ℤ) |
117 | 90 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑦 ∪ {𝑧}) ∈ Fin) |
118 | 117 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (𝑦 ∪ {𝑧}) ∈ Fin) |
119 | | df-nel 2898 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0
∉ 𝑦 ↔ ¬ 0
∈ 𝑦) |
120 | 119 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0
∉ 𝑦 → ¬ 0
∈ 𝑦) |
121 | 120 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ 𝑦) |
122 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
{𝑧} → 0 = 𝑧) |
123 | 122 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
{𝑧} → 𝑧 = 0) |
124 | 123 | necon3ai 2819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ≠ 0 → ¬ 0 ∈
{𝑧}) |
125 | 124 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ {𝑧}) |
126 | | ioran 511 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬ (0
∈ 𝑦 ∨ 0 ∈
{𝑧}) ↔ (¬ 0 ∈
𝑦 ∧ ¬ 0 ∈
{𝑧})) |
127 | 121, 125,
126 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧})) |
128 | | elun 3753 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
(𝑦 ∪ {𝑧}) ↔ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧})) |
129 | 127, 128 | sylnibr 319 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ (𝑦 ∪ {𝑧})) |
130 | | df-nel 2898 |
. . . . . . . . . . . . . . . . 17
⊢ (0
∉ (𝑦 ∪ {𝑧}) ↔ ¬ 0 ∈ (𝑦 ∪ {𝑧})) |
131 | 129, 130 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → 0 ∉ (𝑦 ∪ {𝑧})) |
132 | 131 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → 0 ∉ (𝑦 ∪ {𝑧})) |
133 | | lcmfn0cl 15339 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑦 ∪ {𝑧}) ∈ Fin ∧ 0 ∉ (𝑦 ∪ {𝑧})) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ) |
134 | 116, 118,
132, 133 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ) |
135 | 134 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (lcm‘(𝑦 ∪ {𝑧})) ≠ 0) |
136 | 135 | neneqd 2799 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬
(lcm‘(𝑦 ∪
{𝑧})) = 0) |
137 | | df-ne 2795 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ≠ 0 ↔ ¬ 𝑛 = 0) |
138 | 137 | biimpi 206 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ≠ 0 → ¬ 𝑛 = 0) |
139 | 138 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 𝑛 = 0) |
140 | 139 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬ 𝑛 = 0) |
141 | | ioran 511 |
. . . . . . . . . . . 12
⊢ (¬
((lcm‘(𝑦 ∪
{𝑧})) = 0 ∨ 𝑛 = 0) ↔ (¬
(lcm‘(𝑦 ∪
{𝑧})) = 0 ∧ ¬ 𝑛 = 0)) |
142 | 136, 140,
141 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬
((lcm‘(𝑦 ∪
{𝑧})) = 0 ∨ 𝑛 = 0)) |
143 | | lcmn0cl 15310 |
. . . . . . . . . . 11
⊢
((((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬
((lcm‘(𝑦 ∪
{𝑧})) = 0 ∨ 𝑛 = 0)) →
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛) ∈
ℕ) |
144 | 114, 142,
143 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ) |
145 | | snssi 4339 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → {𝑛} ⊆
ℤ) |
146 | 145 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → {𝑛} ⊆
ℤ) |
147 | 115, 146 | unssd 3789 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ) |
148 | 147 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ) |
149 | 88, 89 | mpan2 707 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ Fin → (𝑦 ∪ {𝑧}) ∈ Fin) |
150 | | snfi 8038 |
. . . . . . . . . . . . . . 15
⊢ {𝑛} ∈ Fin |
151 | | unfi 8227 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ {𝑛} ∈ Fin) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
152 | 149, 150,
151 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
153 | 152 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
154 | 153 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
155 | 154 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) |
156 | | elun 3753 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ (0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛})) |
157 | | nnel 2906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬ 0
∉ 𝑦 ↔ 0 ∈
𝑦) |
158 | 157 | biimpri 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
𝑦 → ¬ 0 ∉
𝑦) |
159 | 158 | 3mix1d 1236 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
𝑦 → (¬ 0 ∉
𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
160 | | nne 2798 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑧 ≠ 0 ↔ 𝑧 = 0) |
161 | 123, 160 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
{𝑧} → ¬ 𝑧 ≠ 0) |
162 | 161 | 3mix2d 1237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
{𝑧} → (¬ 0 ∉
𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
163 | 159, 162 | jaoi 394 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ 𝑦 ∨ 0 ∈
{𝑧}) → (¬ 0
∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
164 | 128, 163 | sylbi 207 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
(𝑦 ∪ {𝑧}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
165 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
{𝑛} → 0 = 𝑛) |
166 | 165 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
{𝑛} → 𝑛 = 0) |
167 | | nne 2798 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑛 ≠ 0 ↔ 𝑛 = 0) |
168 | 166, 167 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
{𝑛} → ¬ 𝑛 ≠ 0) |
169 | 168 | 3mix3d 1238 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
{𝑛} → (¬ 0 ∉
𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
170 | 164, 169 | jaoi 394 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
171 | 156, 170 | sylbi 207 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
((𝑦 ∪ {𝑧}) ∪ {𝑛}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
172 | | 3ianor 1055 |
. . . . . . . . . . . . . . 15
⊢ (¬ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ↔ (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) |
173 | 171, 172 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
((𝑦 ∪ {𝑧}) ∪ {𝑛}) → ¬ (0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) |
174 | 173 | con2i 134 |
. . . . . . . . . . . . 13
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) |
175 | | df-nel 2898 |
. . . . . . . . . . . . 13
⊢ (0
∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ ¬ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) |
176 | 174, 175 | sylibr 224 |
. . . . . . . . . . . 12
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) |
177 | 176 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) |
178 | 148, 155,
177 | 3jca 1242 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))) |
179 | 144, 178 | jca 554 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))) |
180 | 179 | ex 450 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))) |
181 | 180 | ex 450 |
. . . . . . 7
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))))) |
182 | 181 | adantr 481 |
. . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑛 ∈ ℤ → ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))))) |
183 | 182 | impcom 446 |
. . . . 5
⊢ ((𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)))) → ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))) |
184 | 183 | impcom 446 |
. . . 4
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))) |
185 | | lcmf 15346 |
. . . 4
⊢
((((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) ↔ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)))) |
186 | 184, 185 | syl 17 |
. . 3
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) ↔ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)))) |
187 | 113, 186 | mpbird 247 |
. 2
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛}))) |
188 | 187 | eqcomd 2628 |
1
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)) |