Step | Hyp | Ref
| Expression |
1 | | nfv 1921 |
. . 3
⊢
Ⅎ𝑘(𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) |
2 | | nfra1 3145 |
. . . 4
⊢
Ⅎ𝑘∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) |
3 | | nfv 1921 |
. . . 4
⊢
Ⅎ𝑘∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) |
4 | 2, 3 | nfan 1906 |
. . 3
⊢
Ⅎ𝑘(∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)) |
5 | 1, 4 | nfan 1906 |
. 2
⊢
Ⅎ𝑘((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) |
6 | | breq2 5083 |
. . . . . . . 8
⊢ (𝑘 = 𝑙 → (𝑚 ∥ 𝑘 ↔ 𝑚 ∥ 𝑙)) |
7 | 6 | ralbidv 3123 |
. . . . . . 7
⊢ (𝑘 = 𝑙 → (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 ↔ ∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙)) |
8 | | breq2 5083 |
. . . . . . 7
⊢ (𝑘 = 𝑙 → ((lcm‘𝑦) ∥ 𝑘 ↔ (lcm‘𝑦) ∥ 𝑙)) |
9 | 7, 8 | imbi12d 345 |
. . . . . 6
⊢ (𝑘 = 𝑙 → ((∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ↔ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙))) |
10 | 9 | cbvralvw 3381 |
. . . . 5
⊢
(∀𝑘 ∈
ℤ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ↔ ∀𝑙 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙)) |
11 | | breq2 5083 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → (𝑚 ∥ 𝑙 ↔ 𝑚 ∥ 𝑘)) |
12 | 11 | ralbidv 3123 |
. . . . . . . . 9
⊢ (𝑙 = 𝑘 → (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 ↔ ∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘)) |
13 | | breq2 5083 |
. . . . . . . . 9
⊢ (𝑙 = 𝑘 → ((lcm‘𝑦) ∥ 𝑙 ↔ (lcm‘𝑦) ∥ 𝑘)) |
14 | 12, 13 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑙 = 𝑘 → ((∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙) ↔ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘))) |
15 | 14 | rspcv 3556 |
. . . . . . 7
⊢ (𝑘 ∈ ℤ →
(∀𝑙 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙) → (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘))) |
16 | 15 | adantl 482 |
. . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑙 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙) → (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘))) |
17 | | sneq 4577 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑧 → {𝑛} = {𝑧}) |
18 | 17 | uneq2d 4102 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑧 → (𝑦 ∪ {𝑛}) = (𝑦 ∪ {𝑧})) |
19 | 18 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑧 → (lcm‘(𝑦 ∪ {𝑛})) = (lcm‘(𝑦 ∪ {𝑧}))) |
20 | | oveq2 7279 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑧 → ((lcm‘𝑦) lcm 𝑛) = ((lcm‘𝑦) lcm 𝑧)) |
21 | 19, 20 | eqeq12d 2756 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑧 → ((lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) ↔ (lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧))) |
22 | 21 | rspcv 3556 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ →
(∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) |
23 | 22 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) |
24 | 23 | adantr 481 |
. . . . . . 7
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) |
25 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈
ℤ) |
26 | | lcmfcl 16331 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℕ0) |
27 | 26 | nn0zd 12423 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) |
28 | 27 | 3adant1 1129 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(lcm‘𝑦) ∈
ℤ) |
30 | | simpl1 1190 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) → 𝑧 ∈
ℤ) |
31 | 25, 29, 30 | 3jca 1127 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ ℤ ∧
(lcm‘𝑦) ∈
ℤ ∧ 𝑧 ∈
ℤ)) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) ∧
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) → (𝑘 ∈ ℤ ∧ (lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈
ℤ)) |
33 | 32 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → (𝑘 ∈ ℤ ∧ (lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈
ℤ)) |
34 | | ssun1 4111 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
35 | | ssralv 3992 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → ∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘)) |
36 | 34, 35 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → ∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘)) |
37 | 36 | imim1d 82 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
((∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘))) |
38 | 37 | imp31 418 |
. . . . . . . . . . . . 13
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → (lcm‘𝑦) ∥ 𝑘) |
39 | | snidg 4601 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℤ → 𝑧 ∈ {𝑧}) |
40 | 39 | olcd 871 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℤ → (𝑧 ∈ 𝑦 ∨ 𝑧 ∈ {𝑧})) |
41 | | elun 4088 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑧 ∈ 𝑦 ∨ 𝑧 ∈ {𝑧})) |
42 | 40, 41 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℤ → 𝑧 ∈ (𝑦 ∪ {𝑧})) |
43 | | breq1 5082 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑧 → (𝑚 ∥ 𝑘 ↔ 𝑧 ∥ 𝑘)) |
44 | 43 | rspcv 3556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝑦 ∪ {𝑧}) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) |
45 | 42, 44 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℤ →
(∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) |
46 | 45 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) |
48 | 47 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) ∧
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) |
49 | 48 | imp 407 |
. . . . . . . . . . . . 13
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → 𝑧 ∥ 𝑘) |
50 | 38, 49 | jca 512 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → ((lcm‘𝑦) ∥ 𝑘 ∧ 𝑧 ∥ 𝑘)) |
51 | | lcmdvds 16311 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧
(lcm‘𝑦) ∈
ℤ ∧ 𝑧 ∈
ℤ) → (((lcm‘𝑦) ∥ 𝑘 ∧ 𝑧 ∥ 𝑘) → ((lcm‘𝑦) lcm 𝑧) ∥ 𝑘)) |
52 | 33, 50, 51 | sylc 65 |
. . . . . . . . . . 11
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → ((lcm‘𝑦) lcm 𝑧) ∥ 𝑘) |
53 | | breq1 5082 |
. . . . . . . . . . 11
⊢
((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → ((lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘 ↔ ((lcm‘𝑦) lcm 𝑧) ∥ 𝑘)) |
54 | 52, 53 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘)) |
55 | 54 | ex 413 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) ∧
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘))) |
56 | 55 | com23 86 |
. . . . . . . 8
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) ∧
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) → ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘))) |
57 | 56 | ex 413 |
. . . . . . 7
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
((∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) → ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘)))) |
58 | 24, 57 | syl5d 73 |
. . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
((∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘)))) |
59 | 16, 58 | syld 47 |
. . . . 5
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑙 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘)))) |
60 | 10, 59 | syl5bi 241 |
. . . 4
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘)))) |
61 | 60 | impd 411 |
. . 3
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
((∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘))) |
62 | 61 | impancom 452 |
. 2
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑘 ∈ ℤ → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘))) |
63 | 5, 62 | ralrimi 3142 |
1
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → ∀𝑘 ∈ ℤ (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘)) |