| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfv 1914 | . . 3
⊢
Ⅎ𝑘(𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) | 
| 2 |  | nfra1 3284 | . . . 4
⊢
Ⅎ𝑘∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) | 
| 3 |  | nfv 1914 | . . . 4
⊢
Ⅎ𝑘∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) | 
| 4 | 2, 3 | nfan 1899 | . . 3
⊢
Ⅎ𝑘(∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)) | 
| 5 | 1, 4 | nfan 1899 | . 2
⊢
Ⅎ𝑘((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) | 
| 6 |  | breq2 5147 | . . . . . . . 8
⊢ (𝑘 = 𝑙 → (𝑚 ∥ 𝑘 ↔ 𝑚 ∥ 𝑙)) | 
| 7 | 6 | ralbidv 3178 | . . . . . . 7
⊢ (𝑘 = 𝑙 → (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 ↔ ∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙)) | 
| 8 |  | breq2 5147 | . . . . . . 7
⊢ (𝑘 = 𝑙 → ((lcm‘𝑦) ∥ 𝑘 ↔ (lcm‘𝑦) ∥ 𝑙)) | 
| 9 | 7, 8 | imbi12d 344 | . . . . . 6
⊢ (𝑘 = 𝑙 → ((∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ↔ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙))) | 
| 10 | 9 | cbvralvw 3237 | . . . . 5
⊢
(∀𝑘 ∈
ℤ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ↔ ∀𝑙 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙)) | 
| 11 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑙 = 𝑘 → (𝑚 ∥ 𝑙 ↔ 𝑚 ∥ 𝑘)) | 
| 12 | 11 | ralbidv 3178 | . . . . . . . . 9
⊢ (𝑙 = 𝑘 → (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 ↔ ∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘)) | 
| 13 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑙 = 𝑘 → ((lcm‘𝑦) ∥ 𝑙 ↔ (lcm‘𝑦) ∥ 𝑘)) | 
| 14 | 12, 13 | imbi12d 344 | . . . . . . . 8
⊢ (𝑙 = 𝑘 → ((∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙) ↔ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘))) | 
| 15 | 14 | rspcv 3618 | . . . . . . 7
⊢ (𝑘 ∈ ℤ →
(∀𝑙 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙) → (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘))) | 
| 16 | 15 | adantl 481 | . . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑙 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑙 → (lcm‘𝑦) ∥ 𝑙) → (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘))) | 
| 17 |  | sneq 4636 | . . . . . . . . . . . . 13
⊢ (𝑛 = 𝑧 → {𝑛} = {𝑧}) | 
| 18 | 17 | uneq2d 4168 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑧 → (𝑦 ∪ {𝑛}) = (𝑦 ∪ {𝑧})) | 
| 19 | 18 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑧 → (lcm‘(𝑦 ∪ {𝑛})) = (lcm‘(𝑦 ∪ {𝑧}))) | 
| 20 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑧 → ((lcm‘𝑦) lcm 𝑛) = ((lcm‘𝑦) lcm 𝑧)) | 
| 21 | 19, 20 | eqeq12d 2753 | . . . . . . . . . 10
⊢ (𝑛 = 𝑧 → ((lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) ↔ (lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧))) | 
| 22 | 21 | rspcv 3618 | . . . . . . . . 9
⊢ (𝑧 ∈ ℤ →
(∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) | 
| 23 | 22 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) | 
| 24 | 23 | adantr 480 | . . . . . . 7
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) | 
| 25 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈
ℤ) | 
| 26 |  | lcmfcl 16665 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℕ0) | 
| 27 | 26 | nn0zd 12639 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) | 
| 28 | 27 | 3adant1 1131 | . . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(lcm‘𝑦) ∈
ℤ) | 
| 30 |  | simpl1 1192 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) → 𝑧 ∈
ℤ) | 
| 31 | 25, 29, 30 | 3jca 1129 | . . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ ℤ ∧
(lcm‘𝑦) ∈
ℤ ∧ 𝑧 ∈
ℤ)) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) ∧
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) → (𝑘 ∈ ℤ ∧ (lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈
ℤ)) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → (𝑘 ∈ ℤ ∧ (lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈
ℤ)) | 
| 34 |  | ssun1 4178 | . . . . . . . . . . . . . . . 16
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) | 
| 35 |  | ssralv 4052 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → ∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘)) | 
| 36 | 34, 35 | mp1i 13 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → ∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘)) | 
| 37 | 36 | imim1d 82 | . . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
((∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘))) | 
| 38 | 37 | imp31 417 | . . . . . . . . . . . . 13
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → (lcm‘𝑦) ∥ 𝑘) | 
| 39 |  | snidg 4660 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℤ → 𝑧 ∈ {𝑧}) | 
| 40 | 39 | olcd 875 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℤ → (𝑧 ∈ 𝑦 ∨ 𝑧 ∈ {𝑧})) | 
| 41 |  | elun 4153 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑧 ∈ 𝑦 ∨ 𝑧 ∈ {𝑧})) | 
| 42 | 40, 41 | sylibr 234 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℤ → 𝑧 ∈ (𝑦 ∪ {𝑧})) | 
| 43 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑧 → (𝑚 ∥ 𝑘 ↔ 𝑧 ∥ 𝑘)) | 
| 44 | 43 | rspcv 3618 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝑦 ∪ {𝑧}) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) | 
| 45 | 42, 44 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℤ →
(∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) | 
| 46 | 45 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) | 
| 48 | 47 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) ∧
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → 𝑧 ∥ 𝑘)) | 
| 49 | 48 | imp 406 | . . . . . . . . . . . . 13
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → 𝑧 ∥ 𝑘) | 
| 50 | 38, 49 | jca 511 | . . . . . . . . . . . 12
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → ((lcm‘𝑦) ∥ 𝑘 ∧ 𝑧 ∥ 𝑘)) | 
| 51 |  | lcmdvds 16645 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧
(lcm‘𝑦) ∈
ℤ ∧ 𝑧 ∈
ℤ) → (((lcm‘𝑦) ∥ 𝑘 ∧ 𝑧 ∥ 𝑘) → ((lcm‘𝑦) lcm 𝑧) ∥ 𝑘)) | 
| 52 | 33, 50, 51 | sylc 65 | . . . . . . . . . . 11
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → ((lcm‘𝑦) lcm 𝑧) ∥ 𝑘) | 
| 53 |  | breq1 5146 | . . . . . . . . . . 11
⊢
((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → ((lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘 ↔ ((lcm‘𝑦) lcm 𝑧) ∥ 𝑘)) | 
| 54 | 52, 53 | syl5ibrcom 247 | . . . . . . . . . 10
⊢
(((((𝑧 ∈
ℤ ∧ 𝑦 ⊆
ℤ ∧ 𝑦 ∈ Fin)
∧ 𝑘 ∈ ℤ)
∧ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘) → ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘)) | 
| 55 | 54 | ex 412 | . . . . . . . . 9
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) ∧
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘))) | 
| 56 | 55 | com23 86 | . . . . . . . 8
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) ∧
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘)) → ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘))) | 
| 57 | 56 | ex 412 | . . . . . . 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 | biimtrid 242 | . . . 4
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘)))) | 
| 61 | 60 | impd 410 | . . 3
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑘 ∈ ℤ) →
((∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)) → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘))) | 
| 62 | 61 | impancom 451 | . 2
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑘 ∈ ℤ → (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘))) | 
| 63 | 5, 62 | ralrimi 3257 | 1
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → ∀𝑘 ∈ ℤ (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘)) |