| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elun 4152 | . . . . . . . . . . 11
⊢ (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ (𝑖 ∈ (𝑦 ∪ {𝑧}) ∨ 𝑖 ∈ {𝑛})) | 
| 2 |  | elun 4152 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧})) | 
| 3 |  | simp1 1136 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑧 ∈
ℤ) | 
| 4 | 3 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∈
ℤ) | 
| 5 | 4 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑧 ∈ ℤ) | 
| 6 |  | sneq 4635 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑧 → {𝑛} = {𝑧}) | 
| 7 | 6 | uneq2d 4167 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑧 → (𝑦 ∪ {𝑛}) = (𝑦 ∪ {𝑧})) | 
| 8 | 7 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑧 → (lcm‘(𝑦 ∪ {𝑛})) = (lcm‘(𝑦 ∪ {𝑧}))) | 
| 9 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑧 → ((lcm‘𝑦) lcm 𝑛) = ((lcm‘𝑦) lcm 𝑧)) | 
| 10 | 8, 9 | eqeq12d 2752 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑧 → ((lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) ↔ (lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧))) | 
| 11 | 10 | rspcv 3617 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ℤ →
(∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) | 
| 12 | 5, 11 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧))) | 
| 13 |  | ssel 3976 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ⊆ ℤ → (𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ)) | 
| 14 | 13 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ)) | 
| 15 | 14 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑖 ∈ 𝑦 → 𝑖 ∈ ℤ)) | 
| 16 | 15 | impcom 407 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∈ ℤ) | 
| 17 |  | lcmfcl 16666 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℕ0) | 
| 18 | 17 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) | 
| 19 | 18 | 3adant1 1130 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) | 
| 20 | 19 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
(lcm‘𝑦) ∈
ℤ) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
(lcm‘𝑦) ∈
ℤ) | 
| 22 |  | lcmcl 16639 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈
ℕ0) | 
| 23 | 3, 22 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈
ℕ0) | 
| 24 | 23 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈ ℤ) | 
| 25 | 24 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (𝑧 lcm 𝑛) ∈ ℤ) | 
| 26 |  | lcmcl 16639 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((lcm‘𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) →
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛)) ∈
ℕ0) | 
| 27 | 21, 25, 26 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛)) ∈
ℕ0) | 
| 28 | 27 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘𝑦) lcm
(𝑧 lcm 𝑛)) ∈ ℤ) | 
| 29 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑖 → (𝑘 ∥ (lcm‘𝑦) ↔ 𝑖 ∥ (lcm‘𝑦))) | 
| 30 | 29 | rspcv 3617 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ 𝑦 → (∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦) → 𝑖 ∥ (lcm‘𝑦))) | 
| 31 |  | dvdslcmf 16669 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦)) | 
| 32 | 31 | 3adant1 1130 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦)) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
∀𝑘 ∈ 𝑦 𝑘 ∥ (lcm‘𝑦)) | 
| 34 | 30, 33 | impel 505 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (lcm‘𝑦)) | 
| 35 | 20, 24 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦)
∈ ℤ ∧ (𝑧 lcm
𝑛) ∈
ℤ)) | 
| 36 | 35 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘𝑦)
∈ ℤ ∧ (𝑧 lcm
𝑛) ∈
ℤ)) | 
| 37 |  | dvdslcm 16636 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((lcm‘𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) →
((lcm‘𝑦)
∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)) ∧ (𝑧 lcm 𝑛) ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛)))) | 
| 38 | 37 | simpld 494 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((lcm‘𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) →
(lcm‘𝑦)
∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) | 
| 39 | 36, 38 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
(lcm‘𝑦)
∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) | 
| 40 | 16, 21, 28, 34, 39 | dvdstrd 16333 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) | 
| 41 | 4 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑧 ∈ ℤ) | 
| 42 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑛 ∈ ℤ) | 
| 43 |  | lcmass 16652 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) = ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) | 
| 44 | 21, 41, 42, 43 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) = ((lcm‘𝑦) lcm (𝑧 lcm 𝑛))) | 
| 45 | 40, 44 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ 𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) | 
| 46 | 45 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ 𝑦 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) | 
| 47 |  | elsni 4642 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ {𝑧} → 𝑖 = 𝑧) | 
| 48 | 17 | 3adant1 1130 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℕ0) | 
| 49 | 48 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℤ) | 
| 50 |  | lcmcl 16639 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∈
ℕ0) | 
| 51 | 49, 3, 50 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
((lcm‘𝑦) lcm
𝑧) ∈
ℕ0) | 
| 52 | 51 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
((lcm‘𝑦) lcm
𝑧) ∈
ℤ) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∈
ℤ) | 
| 54 |  | lcmcl 16639 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((lcm‘𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈
ℕ0) | 
| 55 | 52, 54 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈
ℕ0) | 
| 56 | 55 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∈ ℤ) | 
| 57 | 19, 3 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
((lcm‘𝑦)
∈ ℤ ∧ 𝑧
∈ ℤ)) | 
| 58 | 57 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦)
∈ ℤ ∧ 𝑧
∈ ℤ)) | 
| 59 |  | dvdslcm 16636 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
((lcm‘𝑦)
∥ ((lcm‘𝑦) lcm 𝑧) ∧ 𝑧 ∥ ((lcm‘𝑦) lcm 𝑧))) | 
| 60 | 59 | simprd 495 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((lcm‘𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) → 𝑧 ∥ ((lcm‘𝑦) lcm 𝑧)) | 
| 61 | 58, 60 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∥
((lcm‘𝑦) lcm
𝑧)) | 
| 62 |  | dvdslcm 16636 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((lcm‘𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛) ∧ 𝑛 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) | 
| 63 | 62 | simpld 494 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((lcm‘𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) | 
| 64 | 52, 63 | sylan 580 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘𝑦) lcm
𝑧) ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) | 
| 65 | 4, 53, 56, 61, 64 | dvdstrd 16333 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∥
(((lcm‘𝑦) lcm
𝑧) lcm 𝑛)) | 
| 66 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑧 → (𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛) ↔ 𝑧 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) | 
| 67 | 65, 66 | imbitrrid 246 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑧 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) | 
| 68 | 47, 67 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ {𝑧} → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) | 
| 69 | 46, 68 | jaoi 857 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) | 
| 70 | 69 | imp 406 | . . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) | 
| 71 |  | oveq1 7439 | . . . . . . . . . . . . . . . . 17
⊢
((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (((lcm‘𝑦) lcm 𝑧) lcm 𝑛)) | 
| 72 | 71 | breq2d 5154 | . . . . . . . . . . . . . . . 16
⊢
((lcm‘(𝑦 ∪ {𝑧})) = ((lcm‘𝑦) lcm 𝑧) → (𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ↔ 𝑖 ∥ (((lcm‘𝑦) lcm 𝑧) lcm 𝑛))) | 
| 73 | 70, 72 | syl5ibrcom 247 | . . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) →
((lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛))) | 
| 74 | 12, 73 | syld 47 | . . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛))) | 
| 75 | 74 | ex 412 | . . . . . . . . . . . . 13
⊢ ((𝑖 ∈ 𝑦 ∨ 𝑖 ∈ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) | 
| 76 | 2, 75 | sylbi 217 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (𝑦 ∪ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) | 
| 77 |  | elsni 4642 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ {𝑛} → 𝑖 = 𝑛) | 
| 78 |  | simp2 1137 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ⊆
ℤ) | 
| 79 |  | snssi 4807 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ ℤ → {𝑧} ⊆
ℤ) | 
| 80 | 79 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → {𝑧} ⊆
ℤ) | 
| 81 | 78, 80 | unssd 4191 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ⊆ ℤ) | 
| 82 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin) | 
| 83 |  | snfi 9084 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ {𝑧} ∈ Fin | 
| 84 |  | unfi 9212 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 85 | 82, 83, 84 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 86 |  | lcmfcl 16666 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑦 ∪ {𝑧}) ∈ Fin) →
(lcm‘(𝑦 ∪
{𝑧})) ∈
ℕ0) | 
| 87 | 81, 85, 86 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘(𝑦 ∪
{𝑧})) ∈
ℕ0) | 
| 88 | 87 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘(𝑦 ∪
{𝑧})) ∈
ℤ) | 
| 89 | 88 | anim1i 615 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) →
((lcm‘(𝑦 ∪
{𝑧})) ∈ ℤ ∧
𝑛 ∈
ℤ)) | 
| 90 | 89 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧
∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) →
((lcm‘(𝑦 ∪
{𝑧})) ∈ ℤ ∧
𝑛 ∈
ℤ)) | 
| 91 |  | dvdslcm 16636 | . . . . . . . . . . . . . . . . 17
⊢
(((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((lcm‘(𝑦 ∪
{𝑧})) ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛) ∧ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) | 
| 92 | 90, 91 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧
∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) →
((lcm‘(𝑦 ∪
{𝑧})) ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛) ∧ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) | 
| 93 | 92 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧
∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) → 𝑛 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)) | 
| 94 |  | breq1 5145 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → (𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ↔ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) | 
| 95 | 93, 94 | imbitrrid 246 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ ∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛)) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛))) | 
| 96 | 95 | expd 415 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) | 
| 97 | 77, 96 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ {𝑛} → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) | 
| 98 | 76, 97 | jaoi 857 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (𝑦 ∪ {𝑧}) ∨ 𝑖 ∈ {𝑛}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) | 
| 99 | 1, 98 | sylbi 217 | . . . . . . . . . 10
⊢ (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ
(lcm‘(𝑦 ∪
{𝑛})) =
((lcm‘𝑦) lcm
𝑛) → 𝑖 ∥
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛)))) | 
| 100 | 99 | com13 88 | . . . . . . . . 9
⊢
(∀𝑛 ∈
ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))) | 
| 101 | 100 | expd 415 | . . . . . . . 8
⊢
(∀𝑛 ∈
ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛) → ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))) | 
| 102 | 101 | adantl 481 | . . . . . . 7
⊢
((∀𝑘 ∈
ℤ (∀𝑚 ∈
𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)) → ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))) | 
| 103 | 102 | impcom 407 | . . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))) | 
| 104 | 103 | impcom 407 | . . . . 5
⊢ ((𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)))) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) | 
| 105 | 104 | adantl 481 | . . . 4
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))) | 
| 106 | 105 | ralrimiv 3144 | . . 3
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)) | 
| 107 |  | lcmfunsnlem2lem1 16676 | . . 3
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)) | 
| 108 | 89 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ)) | 
| 109 | 81 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑦 ∪ {𝑧}) ⊆ ℤ) | 
| 110 | 85 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 111 |  | df-nel 3046 | . . . . . . . . . . . . . . . . . . . 20
⊢ (0
∉ 𝑦 ↔ ¬ 0
∈ 𝑦) | 
| 112 | 111 | biimpi 216 | . . . . . . . . . . . . . . . . . . 19
⊢ (0
∉ 𝑦 → ¬ 0
∈ 𝑦) | 
| 113 | 112 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . 18
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ 𝑦) | 
| 114 |  | elsni 4642 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
{𝑧} → 0 = 𝑧) | 
| 115 | 114 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
{𝑧} → 𝑧 = 0) | 
| 116 | 115 | necon3ai 2964 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ≠ 0 → ¬ 0 ∈
{𝑧}) | 
| 117 | 116 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . 18
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ {𝑧}) | 
| 118 |  | ioran 985 | . . . . . . . . . . . . . . . . . 18
⊢ (¬ (0
∈ 𝑦 ∨ 0 ∈
{𝑧}) ↔ (¬ 0 ∈
𝑦 ∧ ¬ 0 ∈
{𝑧})) | 
| 119 | 113, 117,
118 | sylanbrc 583 | . . . . . . . . . . . . . . . . 17
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧})) | 
| 120 |  | elun 4152 | . . . . . . . . . . . . . . . . 17
⊢ (0 ∈
(𝑦 ∪ {𝑧}) ↔ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧})) | 
| 121 | 119, 120 | sylnibr 329 | . . . . . . . . . . . . . . . 16
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ (𝑦 ∪ {𝑧})) | 
| 122 |  | df-nel 3046 | . . . . . . . . . . . . . . . 16
⊢ (0
∉ (𝑦 ∪ {𝑧}) ↔ ¬ 0 ∈ (𝑦 ∪ {𝑧})) | 
| 123 | 121, 122 | sylibr 234 | . . . . . . . . . . . . . . 15
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → 0 ∉ (𝑦 ∪ {𝑧})) | 
| 124 |  | lcmfn0cl 16664 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑦 ∪ {𝑧}) ∈ Fin ∧ 0 ∉ (𝑦 ∪ {𝑧})) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ) | 
| 125 | 109, 110,
123, 124 | syl2an3an 1423 | . . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ) | 
| 126 | 125 | nnne0d 12317 | . . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (lcm‘(𝑦 ∪ {𝑧})) ≠ 0) | 
| 127 | 126 | neneqd 2944 | . . . . . . . . . . . 12
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬
(lcm‘(𝑦 ∪
{𝑧})) = 0) | 
| 128 |  | neneq 2945 | . . . . . . . . . . . . . 14
⊢ (𝑛 ≠ 0 → ¬ 𝑛 = 0) | 
| 129 | 128 | 3ad2ant3 1135 | . . . . . . . . . . . . 13
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 𝑛 = 0) | 
| 130 | 129 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬ 𝑛 = 0) | 
| 131 |  | ioran 985 | . . . . . . . . . . . 12
⊢ (¬
((lcm‘(𝑦 ∪
{𝑧})) = 0 ∨ 𝑛 = 0) ↔ (¬
(lcm‘(𝑦 ∪
{𝑧})) = 0 ∧ ¬ 𝑛 = 0)) | 
| 132 | 127, 130,
131 | sylanbrc 583 | . . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬
((lcm‘(𝑦 ∪
{𝑧})) = 0 ∨ 𝑛 = 0)) | 
| 133 |  | lcmn0cl 16635 | . . . . . . . . . . 11
⊢
((((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬
((lcm‘(𝑦 ∪
{𝑧})) = 0 ∨ 𝑛 = 0)) →
((lcm‘(𝑦 ∪
{𝑧})) lcm 𝑛) ∈
ℕ) | 
| 134 | 108, 132,
133 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ) | 
| 135 |  | snssi 4807 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → {𝑛} ⊆
ℤ) | 
| 136 | 135 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → {𝑛} ⊆
ℤ) | 
| 137 | 109, 136 | unssd 4191 | . . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ) | 
| 138 | 137 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ) | 
| 139 | 83, 84 | mpan2 691 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ Fin → (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 140 |  | snfi 9084 | . . . . . . . . . . . . . . 15
⊢ {𝑛} ∈ Fin | 
| 141 |  | unfi 9212 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ {𝑛} ∈ Fin) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) | 
| 142 | 139, 140,
141 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) | 
| 143 | 142 | 3ad2ant3 1135 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) | 
| 144 | 143 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) | 
| 145 | 144 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin) | 
| 146 |  | elun 4152 | . . . . . . . . . . . . . . . 16
⊢ (0 ∈
((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ (0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛})) | 
| 147 |  | nnel 3055 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (¬ 0
∉ 𝑦 ↔ 0 ∈
𝑦) | 
| 148 | 147 | biimpri 228 | . . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
𝑦 → ¬ 0 ∉
𝑦) | 
| 149 | 148 | 3mix1d 1336 | . . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
𝑦 → (¬ 0 ∉
𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) | 
| 150 |  | nne 2943 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑧 ≠ 0 ↔ 𝑧 = 0) | 
| 151 | 115, 150 | sylibr 234 | . . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
{𝑧} → ¬ 𝑧 ≠ 0) | 
| 152 | 151 | 3mix2d 1337 | . . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
{𝑧} → (¬ 0 ∉
𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) | 
| 153 | 149, 152 | jaoi 857 | . . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ 𝑦 ∨ 0 ∈
{𝑧}) → (¬ 0
∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) | 
| 154 | 120, 153 | sylbi 217 | . . . . . . . . . . . . . . . . 17
⊢ (0 ∈
(𝑦 ∪ {𝑧}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) | 
| 155 |  | elsni 4642 | . . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
{𝑛} → 0 = 𝑛) | 
| 156 | 155 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
{𝑛} → 𝑛 = 0) | 
| 157 |  | nne 2943 | . . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑛 ≠ 0 ↔ 𝑛 = 0) | 
| 158 | 156, 157 | sylibr 234 | . . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
{𝑛} → ¬ 𝑛 ≠ 0) | 
| 159 | 158 | 3mix3d 1338 | . . . . . . . . . . . . . . . . 17
⊢ (0 ∈
{𝑛} → (¬ 0 ∉
𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) | 
| 160 | 154, 159 | jaoi 857 | . . . . . . . . . . . . . . . 16
⊢ ((0
∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) | 
| 161 | 146, 160 | sylbi 217 | . . . . . . . . . . . . . . 15
⊢ (0 ∈
((𝑦 ∪ {𝑧}) ∪ {𝑛}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) | 
| 162 |  | 3ianor 1106 | . . . . . . . . . . . . . . 15
⊢ (¬ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ↔ (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0)) | 
| 163 | 161, 162 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ (0 ∈
((𝑦 ∪ {𝑧}) ∪ {𝑛}) → ¬ (0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) | 
| 164 | 163 | con2i 139 | . . . . . . . . . . . . 13
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) | 
| 165 |  | df-nel 3046 | . . . . . . . . . . . . 13
⊢ (0
∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ ¬ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) | 
| 166 | 164, 165 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) | 
| 167 | 166 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})) | 
| 168 | 138, 145,
167 | 3jca 1128 | . . . . . . . . . 10
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))) | 
| 169 | 134, 168 | jca 511 | . . . . . . . . 9
⊢ ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))) | 
| 170 | 169 | ex 412 | . . . . . . . 8
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))) | 
| 171 | 170 | ex 412 | . . . . . . 7
⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → ((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))))) | 
| 172 | 171 | adantr 480 | . . . . . 6
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → (𝑛 ∈ ℤ → ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))))) | 
| 173 | 172 | impcom 407 | . . . . 5
⊢ ((𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧
(∀𝑘 ∈ ℤ
(∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛)))) → ((0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))) | 
| 174 | 173 | impcom 407 | . . . 4
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))) | 
| 175 |  | lcmf 16671 | . . . 4
⊢
((((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) ↔ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)))) | 
| 176 | 174, 175 | syl 17 | . . 3
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) ↔ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)))) | 
| 177 | 106, 107,
176 | mpbir2and 713 | . 2
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛}))) | 
| 178 | 177 | eqcomd 2742 | 1
⊢ (((0
∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)) |