| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cleq1lem 15021 | . . . . . 6
⊢ (𝑥 = ∅ → ((𝑥 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) ↔ (∅
⊆ ℤ ∧ (𝑌
⊆ ℤ ∧ 𝑌
∈ Fin)))) | 
| 2 |  | uneq2 4162 | . . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑌 ∪ 𝑥) = (𝑌 ∪ ∅)) | 
| 3 |  | un0 4394 | . . . . . . . . 9
⊢ (𝑌 ∪ ∅) = 𝑌 | 
| 4 | 2, 3 | eqtrdi 2793 | . . . . . . . 8
⊢ (𝑥 = ∅ → (𝑌 ∪ 𝑥) = 𝑌) | 
| 5 | 4 | fveq2d 6910 | . . . . . . 7
⊢ (𝑥 = ∅ →
(lcm‘(𝑌 ∪
𝑥)) =
(lcm‘𝑌)) | 
| 6 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑥 = ∅ →
(lcm‘𝑥) =
(lcm‘∅)) | 
| 7 |  | lcmf0 16671 | . . . . . . . . 9
⊢
(lcm‘∅) = 1 | 
| 8 | 6, 7 | eqtrdi 2793 | . . . . . . . 8
⊢ (𝑥 = ∅ →
(lcm‘𝑥) =
1) | 
| 9 | 8 | oveq2d 7447 | . . . . . . 7
⊢ (𝑥 = ∅ →
((lcm‘𝑌) lcm
(lcm‘𝑥)) =
((lcm‘𝑌) lcm
1)) | 
| 10 | 5, 9 | eqeq12d 2753 | . . . . . 6
⊢ (𝑥 = ∅ →
((lcm‘(𝑌 ∪
𝑥)) =
((lcm‘𝑌) lcm
(lcm‘𝑥))
↔ (lcm‘𝑌)
= ((lcm‘𝑌) lcm
1))) | 
| 11 | 1, 10 | imbi12d 344 | . . . . 5
⊢ (𝑥 = ∅ → (((𝑥 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑥)) =
((lcm‘𝑌) lcm
(lcm‘𝑥)))
↔ ((∅ ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → (lcm‘𝑌) = ((lcm‘𝑌) lcm 1)))) | 
| 12 |  | cleq1lem 15021 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) ↔ (𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)))) | 
| 13 |  | uneq2 4162 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑌 ∪ 𝑥) = (𝑌 ∪ 𝑦)) | 
| 14 | 13 | fveq2d 6910 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (lcm‘(𝑌 ∪ 𝑥)) = (lcm‘(𝑌 ∪ 𝑦))) | 
| 15 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (lcm‘𝑥) = (lcm‘𝑦)) | 
| 16 | 15 | oveq2d 7447 | . . . . . . 7
⊢ (𝑥 = 𝑦 → ((lcm‘𝑌) lcm (lcm‘𝑥)) = ((lcm‘𝑌) lcm (lcm‘𝑦))) | 
| 17 | 14, 16 | eqeq12d 2753 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((lcm‘(𝑌 ∪ 𝑥)) = ((lcm‘𝑌) lcm (lcm‘𝑥)) ↔ (lcm‘(𝑌 ∪ 𝑦)) = ((lcm‘𝑌) lcm (lcm‘𝑦)))) | 
| 18 | 12, 17 | imbi12d 344 | . . . . 5
⊢ (𝑥 = 𝑦 → (((𝑥 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑥)) =
((lcm‘𝑌) lcm
(lcm‘𝑥)))
↔ ((𝑦 ⊆ ℤ
∧ (𝑌 ⊆ ℤ
∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))))) | 
| 19 |  | cleq1lem 15021 | . . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑥 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) ↔ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)))) | 
| 20 |  | uneq2 4162 | . . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑌 ∪ 𝑥) = (𝑌 ∪ (𝑦 ∪ {𝑧}))) | 
| 21 | 20 | fveq2d 6910 | . . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (lcm‘(𝑌 ∪ 𝑥)) = (lcm‘(𝑌 ∪ (𝑦 ∪ {𝑧})))) | 
| 22 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (lcm‘𝑥) = (lcm‘(𝑦 ∪ {𝑧}))) | 
| 23 | 22 | oveq2d 7447 | . . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((lcm‘𝑌) lcm (lcm‘𝑥)) = ((lcm‘𝑌) lcm (lcm‘(𝑦 ∪ {𝑧})))) | 
| 24 | 21, 23 | eqeq12d 2753 | . . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((lcm‘(𝑌 ∪ 𝑥)) = ((lcm‘𝑌) lcm (lcm‘𝑥)) ↔ (lcm‘(𝑌 ∪ (𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm (lcm‘(𝑦 ∪ {𝑧}))))) | 
| 25 | 19, 24 | imbi12d 344 | . . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((𝑥 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑥)) =
((lcm‘𝑌) lcm
(lcm‘𝑥)))
↔ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
(𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm (lcm‘(𝑦 ∪ {𝑧})))))) | 
| 26 |  | cleq1lem 15021 | . . . . . 6
⊢ (𝑥 = 𝑍 → ((𝑥 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) ↔ (𝑍 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)))) | 
| 27 |  | uneq2 4162 | . . . . . . . 8
⊢ (𝑥 = 𝑍 → (𝑌 ∪ 𝑥) = (𝑌 ∪ 𝑍)) | 
| 28 | 27 | fveq2d 6910 | . . . . . . 7
⊢ (𝑥 = 𝑍 → (lcm‘(𝑌 ∪ 𝑥)) = (lcm‘(𝑌 ∪ 𝑍))) | 
| 29 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑥 = 𝑍 → (lcm‘𝑥) = (lcm‘𝑍)) | 
| 30 | 29 | oveq2d 7447 | . . . . . . 7
⊢ (𝑥 = 𝑍 → ((lcm‘𝑌) lcm (lcm‘𝑥)) = ((lcm‘𝑌) lcm (lcm‘𝑍))) | 
| 31 | 28, 30 | eqeq12d 2753 | . . . . . 6
⊢ (𝑥 = 𝑍 → ((lcm‘(𝑌 ∪ 𝑥)) = ((lcm‘𝑌) lcm (lcm‘𝑥)) ↔ (lcm‘(𝑌 ∪ 𝑍)) = ((lcm‘𝑌) lcm (lcm‘𝑍)))) | 
| 32 | 26, 31 | imbi12d 344 | . . . . 5
⊢ (𝑥 = 𝑍 → (((𝑥 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑥)) =
((lcm‘𝑌) lcm
(lcm‘𝑥)))
↔ ((𝑍 ⊆ ℤ
∧ (𝑌 ⊆ ℤ
∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑍)) =
((lcm‘𝑌) lcm
(lcm‘𝑍))))) | 
| 33 |  | lcmfcl 16665 | . . . . . . . . . 10
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) →
(lcm‘𝑌) ∈
ℕ0) | 
| 34 | 33 | nn0zd 12639 | . . . . . . . . 9
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) →
(lcm‘𝑌) ∈
ℤ) | 
| 35 |  | lcm1 16647 | . . . . . . . . 9
⊢
((lcm‘𝑌) ∈ ℤ →
((lcm‘𝑌) lcm
1) = (abs‘(lcm‘𝑌))) | 
| 36 | 34, 35 | syl 17 | . . . . . . . 8
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) →
((lcm‘𝑌) lcm
1) = (abs‘(lcm‘𝑌))) | 
| 37 |  | nn0re 12535 | . . . . . . . . . . 11
⊢
((lcm‘𝑌) ∈ ℕ0 →
(lcm‘𝑌) ∈
ℝ) | 
| 38 |  | nn0ge0 12551 | . . . . . . . . . . 11
⊢
((lcm‘𝑌) ∈ ℕ0 → 0 ≤
(lcm‘𝑌)) | 
| 39 | 37, 38 | jca 511 | . . . . . . . . . 10
⊢
((lcm‘𝑌) ∈ ℕ0 →
((lcm‘𝑌)
∈ ℝ ∧ 0 ≤ (lcm‘𝑌))) | 
| 40 | 33, 39 | syl 17 | . . . . . . . . 9
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) →
((lcm‘𝑌)
∈ ℝ ∧ 0 ≤ (lcm‘𝑌))) | 
| 41 |  | absid 15335 | . . . . . . . . 9
⊢
(((lcm‘𝑌) ∈ ℝ ∧ 0 ≤
(lcm‘𝑌))
→ (abs‘(lcm‘𝑌)) = (lcm‘𝑌)) | 
| 42 | 40, 41 | syl 17 | . . . . . . . 8
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) →
(abs‘(lcm‘𝑌)) = (lcm‘𝑌)) | 
| 43 | 36, 42 | eqtrd 2777 | . . . . . . 7
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) →
((lcm‘𝑌) lcm
1) = (lcm‘𝑌)) | 
| 44 | 43 | adantl 481 | . . . . . 6
⊢ ((∅
⊆ ℤ ∧ (𝑌
⊆ ℤ ∧ 𝑌
∈ Fin)) → ((lcm‘𝑌) lcm 1) = (lcm‘𝑌)) | 
| 45 | 44 | eqcomd 2743 | . . . . 5
⊢ ((∅
⊆ ℤ ∧ (𝑌
⊆ ℤ ∧ 𝑌
∈ Fin)) → (lcm‘𝑌) = ((lcm‘𝑌) lcm 1)) | 
| 46 |  | unass 4172 | . . . . . . . . . . . . . 14
⊢ ((𝑌 ∪ 𝑦) ∪ {𝑧}) = (𝑌 ∪ (𝑦 ∪ {𝑧})) | 
| 47 | 46 | eqcomi 2746 | . . . . . . . . . . . . 13
⊢ (𝑌 ∪ (𝑦 ∪ {𝑧})) = ((𝑌 ∪ 𝑦) ∪ {𝑧}) | 
| 48 | 47 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) → (𝑌 ∪ (𝑦 ∪ {𝑧})) = ((𝑌 ∪ 𝑦) ∪ {𝑧})) | 
| 49 | 48 | fveq2d 6910 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
(lcm‘(𝑌 ∪
(𝑦 ∪ {𝑧}))) = (lcm‘((𝑌 ∪ 𝑦) ∪ {𝑧}))) | 
| 50 |  | simpl 482 | . . . . . . . . . . . . . . 15
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) → 𝑌 ⊆
ℤ) | 
| 51 | 50 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → 𝑌 ⊆ ℤ) | 
| 52 |  | unss 4190 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ ℤ ∧ {𝑧} ⊆ ℤ) ↔ (𝑦 ∪ {𝑧}) ⊆ ℤ) | 
| 53 |  | simpl 482 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ ℤ ∧ {𝑧} ⊆ ℤ) → 𝑦 ⊆
ℤ) | 
| 54 | 52, 53 | sylbir 235 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∪ {𝑧}) ⊆ ℤ → 𝑦 ⊆ ℤ) | 
| 55 | 54 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → 𝑦 ⊆ ℤ) | 
| 56 | 51, 55 | unssd 4192 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → (𝑌 ∪ 𝑦) ⊆ ℤ) | 
| 57 | 56 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) → (𝑌 ∪ 𝑦) ⊆ ℤ) | 
| 58 |  | unfi 9211 | . . . . . . . . . . . . . . . 16
⊢ ((𝑌 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝑌 ∪ 𝑦) ∈ Fin) | 
| 59 | 58 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (𝑌 ∈ Fin → (𝑦 ∈ Fin → (𝑌 ∪ 𝑦) ∈ Fin)) | 
| 60 | 59 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) → (𝑦 ∈ Fin → (𝑌 ∪ 𝑦) ∈ Fin)) | 
| 61 | 60 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → (𝑦 ∈ Fin → (𝑌 ∪ 𝑦) ∈ Fin)) | 
| 62 | 61 | impcom 407 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) → (𝑌 ∪ 𝑦) ∈ Fin) | 
| 63 |  | vex 3484 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V | 
| 64 | 63 | snss 4785 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℤ ↔ {𝑧} ⊆
ℤ) | 
| 65 | 64 | biimpri 228 | . . . . . . . . . . . . . . . 16
⊢ ({𝑧} ⊆ ℤ → 𝑧 ∈
ℤ) | 
| 66 | 65 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ ℤ ∧ {𝑧} ⊆ ℤ) → 𝑧 ∈
ℤ) | 
| 67 | 52, 66 | sylbir 235 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∪ {𝑧}) ⊆ ℤ → 𝑧 ∈ ℤ) | 
| 68 | 67 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → 𝑧 ∈ ℤ) | 
| 69 | 68 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) → 𝑧 ∈ ℤ) | 
| 70 |  | lcmfunsn 16681 | . . . . . . . . . . . 12
⊢ (((𝑌 ∪ 𝑦) ⊆ ℤ ∧ (𝑌 ∪ 𝑦) ∈ Fin ∧ 𝑧 ∈ ℤ) →
(lcm‘((𝑌 ∪
𝑦) ∪ {𝑧})) = ((lcm‘(𝑌 ∪ 𝑦)) lcm 𝑧)) | 
| 71 | 57, 62, 69, 70 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
(lcm‘((𝑌 ∪
𝑦) ∪ {𝑧})) = ((lcm‘(𝑌 ∪ 𝑦)) lcm 𝑧)) | 
| 72 | 49, 71 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
(lcm‘(𝑌 ∪
(𝑦 ∪ {𝑧}))) = ((lcm‘(𝑌 ∪ 𝑦)) lcm 𝑧)) | 
| 73 | 72 | adantr 480 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) ∧ ((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))))
→ (lcm‘(𝑌
∪ (𝑦 ∪ {𝑧}))) = ((lcm‘(𝑌 ∪ 𝑦)) lcm 𝑧)) | 
| 74 | 54 | anim1i 615 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → (𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) | 
| 75 | 74 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) → (𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) | 
| 76 |  | id 22 | . . . . . . . . . . . 12
⊢ (((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦)))
→ ((𝑦 ⊆ ℤ
∧ (𝑌 ⊆ ℤ
∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦)))) | 
| 77 | 75, 76 | mpan9 506 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) ∧ ((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))))
→ (lcm‘(𝑌
∪ 𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))) | 
| 78 | 77 | oveq1d 7446 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) ∧ ((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))))
→ ((lcm‘(𝑌 ∪ 𝑦)) lcm 𝑧) = (((lcm‘𝑌) lcm (lcm‘𝑦)) lcm 𝑧)) | 
| 79 | 34 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → (lcm‘𝑌) ∈
ℤ) | 
| 80 | 79 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
(lcm‘𝑌) ∈
ℤ) | 
| 81 | 55 | anim2i 617 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) → (𝑦 ∈ Fin ∧ 𝑦 ⊆ ℤ)) | 
| 82 | 81 | ancomd 461 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) → (𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin)) | 
| 83 |  | lcmfcl 16665 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) →
(lcm‘𝑦) ∈
ℕ0) | 
| 84 | 82, 83 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
(lcm‘𝑦) ∈
ℕ0) | 
| 85 | 84 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
(lcm‘𝑦) ∈
ℤ) | 
| 86 |  | lcmass 16651 | . . . . . . . . . . . 12
⊢
(((lcm‘𝑌) ∈ ℤ ∧
(lcm‘𝑦) ∈
ℤ ∧ 𝑧 ∈
ℤ) → (((lcm‘𝑌) lcm (lcm‘𝑦)) lcm 𝑧) = ((lcm‘𝑌) lcm ((lcm‘𝑦) lcm 𝑧))) | 
| 87 | 80, 85, 69, 86 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
(((lcm‘𝑌) lcm
(lcm‘𝑦)) lcm
𝑧) =
((lcm‘𝑌) lcm
((lcm‘𝑦) lcm
𝑧))) | 
| 88 | 87 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) ∧ ((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))))
→ (((lcm‘𝑌) lcm (lcm‘𝑦)) lcm 𝑧) = ((lcm‘𝑌) lcm ((lcm‘𝑦) lcm 𝑧))) | 
| 89 | 78, 88 | eqtrd 2777 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) ∧ ((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))))
→ ((lcm‘(𝑌 ∪ 𝑦)) lcm 𝑧) = ((lcm‘𝑌) lcm ((lcm‘𝑦) lcm 𝑧))) | 
| 90 | 73, 89 | eqtrd 2777 | . . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) ∧ ((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))))
→ (lcm‘(𝑌
∪ (𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm ((lcm‘𝑦) lcm 𝑧))) | 
| 91 | 53 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ⊆ ℤ ∧ {𝑧} ⊆ ℤ) ∧ 𝑦 ∈ Fin) → 𝑦 ⊆
ℤ) | 
| 92 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ⊆ ℤ ∧ {𝑧} ⊆ ℤ) ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin) | 
| 93 | 66 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ⊆ ℤ ∧ {𝑧} ⊆ ℤ) ∧ 𝑦 ∈ Fin) → 𝑧 ∈
ℤ) | 
| 94 | 91, 92, 93 | 3jca 1129 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ⊆ ℤ ∧ {𝑧} ⊆ ℤ) ∧ 𝑦 ∈ Fin) → (𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈
ℤ)) | 
| 95 | 94 | ex 412 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ ℤ ∧ {𝑧} ⊆ ℤ) → (𝑦 ∈ Fin → (𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈
ℤ))) | 
| 96 | 52, 95 | sylbir 235 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∪ {𝑧}) ⊆ ℤ → (𝑦 ∈ Fin → (𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ))) | 
| 97 | 96 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → (𝑦 ∈ Fin → (𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ))) | 
| 98 | 97 | impcom 407 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) → (𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ)) | 
| 99 |  | lcmfunsn 16681 | . . . . . . . . . . . 12
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ ℤ) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧)) | 
| 100 | 98, 99 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
(lcm‘(𝑦 ∪
{𝑧})) =
((lcm‘𝑦) lcm
𝑧)) | 
| 101 | 100 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
((lcm‘𝑌) lcm
(lcm‘(𝑦 ∪
{𝑧}))) =
((lcm‘𝑌) lcm
((lcm‘𝑦) lcm
𝑧))) | 
| 102 | 101 | eqeq2d 2748 | . . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) →
((lcm‘(𝑌 ∪
(𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm (lcm‘(𝑦 ∪ {𝑧}))) ↔ (lcm‘(𝑌 ∪ (𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm ((lcm‘𝑦) lcm 𝑧)))) | 
| 103 | 102 | adantr 480 | . . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) ∧ ((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))))
→ ((lcm‘(𝑌 ∪ (𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm (lcm‘(𝑦 ∪ {𝑧}))) ↔ (lcm‘(𝑌 ∪ (𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm ((lcm‘𝑦) lcm 𝑧)))) | 
| 104 | 90, 103 | mpbird 257 | . . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin))) ∧ ((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦))))
→ (lcm‘(𝑌
∪ (𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm (lcm‘(𝑦 ∪ {𝑧})))) | 
| 105 | 104 | exp31 419 | . . . . . 6
⊢ (𝑦 ∈ Fin → (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) → (((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦)))
→ (lcm‘(𝑌
∪ (𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm (lcm‘(𝑦 ∪ {𝑧})))))) | 
| 106 | 105 | com23 86 | . . . . 5
⊢ (𝑦 ∈ Fin → (((𝑦 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑦)) =
((lcm‘𝑌) lcm
(lcm‘𝑦)))
→ (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
(𝑦 ∪ {𝑧}))) = ((lcm‘𝑌) lcm (lcm‘(𝑦 ∪ {𝑧})))))) | 
| 107 | 11, 18, 25, 32, 45, 106 | findcard2 9204 | . . . 4
⊢ (𝑍 ∈ Fin → ((𝑍 ⊆ ℤ ∧ (𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑍)) =
((lcm‘𝑌) lcm
(lcm‘𝑍)))) | 
| 108 | 107 | expd 415 | . . 3
⊢ (𝑍 ∈ Fin → (𝑍 ⊆ ℤ → ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) →
(lcm‘(𝑌 ∪
𝑍)) =
((lcm‘𝑌) lcm
(lcm‘𝑍))))) | 
| 109 | 108 | impcom 407 | . 2
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin) → ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) →
(lcm‘(𝑌 ∪
𝑍)) =
((lcm‘𝑌) lcm
(lcm‘𝑍)))) | 
| 110 | 109 | impcom 407 | 1
⊢ (((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin)) →
(lcm‘(𝑌 ∪
𝑍)) =
((lcm‘𝑌) lcm
(lcm‘𝑍))) |