MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lcmfunsnlem2lem2 Structured version   Visualization version   GIF version

Theorem lcmfunsnlem2lem2 15560
Description: Lemma 2 for lcmfunsnlem2 15561. (Contributed by AV, 26-Aug-2020.)
Assertion
Ref Expression
lcmfunsnlem2lem2 (((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
Distinct variable groups:   𝑦,𝑚,𝑧   𝑘,𝑛,𝑦,𝑧,𝑚

Proof of Theorem lcmfunsnlem2lem2
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 elun 3904 . . . . . . . . . . . 12 (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ (𝑖 ∈ (𝑦 ∪ {𝑧}) ∨ 𝑖 ∈ {𝑛}))
2 elun 3904 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑖𝑦𝑖 ∈ {𝑧}))
3 simp1 1130 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑧 ∈ ℤ)
43adantr 466 . . . . . . . . . . . . . . . . . 18 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∈ ℤ)
54adantl 467 . . . . . . . . . . . . . . . . 17 (((𝑖𝑦𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑧 ∈ ℤ)
6 sneq 4326 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑧 → {𝑛} = {𝑧})
76uneq2d 3918 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑧 → (𝑦 ∪ {𝑛}) = (𝑦 ∪ {𝑧}))
87fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑧 → (lcm‘(𝑦 ∪ {𝑛})) = (lcm‘(𝑦 ∪ {𝑧})))
9 oveq2 6801 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑧 → ((lcm𝑦) lcm 𝑛) = ((lcm𝑦) lcm 𝑧))
108, 9eqeq12d 2786 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑧 → ((lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) ↔ (lcm‘(𝑦 ∪ {𝑧})) = ((lcm𝑦) lcm 𝑧)))
1110rspcv 3456 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℤ → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → (lcm‘(𝑦 ∪ {𝑧})) = ((lcm𝑦) lcm 𝑧)))
125, 11syl 17 . . . . . . . . . . . . . . . 16 (((𝑖𝑦𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → (lcm‘(𝑦 ∪ {𝑧})) = ((lcm𝑦) lcm 𝑧)))
13 breq1 4789 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → (𝑘 ∥ (lcm𝑦) ↔ 𝑖 ∥ (lcm𝑦)))
1413rspcv 3456 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖𝑦 → (∀𝑘𝑦 𝑘 ∥ (lcm𝑦) → 𝑖 ∥ (lcm𝑦)))
15 dvdslcmf 15552 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ∀𝑘𝑦 𝑘 ∥ (lcm𝑦))
16153adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ∀𝑘𝑦 𝑘 ∥ (lcm𝑦))
1716adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ∀𝑘𝑦 𝑘 ∥ (lcm𝑦))
1814, 17impel 495 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (lcm𝑦))
19 lcmfcl 15549 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm𝑦) ∈ ℕ0)
2019nn0zd 11682 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm𝑦) ∈ ℤ)
21203adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm𝑦) ∈ ℤ)
2221adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (lcm𝑦) ∈ ℤ)
23 lcmcl 15522 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈ ℕ0)
243, 23sylan 569 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈ ℕ0)
2524nn0zd 11682 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑧 lcm 𝑛) ∈ ℤ)
2622, 25jca 501 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((lcm𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ))
2726adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → ((lcm𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ))
28 dvdslcm 15519 . . . . . . . . . . . . . . . . . . . . . . . 24 (((lcm𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) → ((lcm𝑦) ∥ ((lcm𝑦) lcm (𝑧 lcm 𝑛)) ∧ (𝑧 lcm 𝑛) ∥ ((lcm𝑦) lcm (𝑧 lcm 𝑛))))
2928simpld 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((lcm𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) → (lcm𝑦) ∥ ((lcm𝑦) lcm (𝑧 lcm 𝑛)))
3027, 29syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (lcm𝑦) ∥ ((lcm𝑦) lcm (𝑧 lcm 𝑛)))
31 ssel 3746 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ⊆ ℤ → (𝑖𝑦𝑖 ∈ ℤ))
32313ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑖𝑦𝑖 ∈ ℤ))
3332adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑖𝑦𝑖 ∈ ℤ))
3433impcom 394 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∈ ℤ)
3522adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (lcm𝑦) ∈ ℤ)
3625adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (𝑧 lcm 𝑛) ∈ ℤ)
37 lcmcl 15522 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((lcm𝑦) ∈ ℤ ∧ (𝑧 lcm 𝑛) ∈ ℤ) → ((lcm𝑦) lcm (𝑧 lcm 𝑛)) ∈ ℕ0)
3835, 36, 37syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → ((lcm𝑦) lcm (𝑧 lcm 𝑛)) ∈ ℕ0)
3938nn0zd 11682 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → ((lcm𝑦) lcm (𝑧 lcm 𝑛)) ∈ ℤ)
40 dvdstr 15227 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ℤ ∧ (lcm𝑦) ∈ ℤ ∧ ((lcm𝑦) lcm (𝑧 lcm 𝑛)) ∈ ℤ) → ((𝑖 ∥ (lcm𝑦) ∧ (lcm𝑦) ∥ ((lcm𝑦) lcm (𝑧 lcm 𝑛))) → 𝑖 ∥ ((lcm𝑦) lcm (𝑧 lcm 𝑛))))
4134, 35, 39, 40syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → ((𝑖 ∥ (lcm𝑦) ∧ (lcm𝑦) ∥ ((lcm𝑦) lcm (𝑧 lcm 𝑛))) → 𝑖 ∥ ((lcm𝑦) lcm (𝑧 lcm 𝑛))))
4218, 30, 41mp2and 679 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ ((lcm𝑦) lcm (𝑧 lcm 𝑛)))
434adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑧 ∈ ℤ)
44 simpr 471 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
4544adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑛 ∈ ℤ)
46 lcmass 15535 . . . . . . . . . . . . . . . . . . . . . 22 (((lcm𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((lcm𝑦) lcm 𝑧) lcm 𝑛) = ((lcm𝑦) lcm (𝑧 lcm 𝑛)))
4735, 43, 45, 46syl3anc 1476 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (((lcm𝑦) lcm 𝑧) lcm 𝑛) = ((lcm𝑦) lcm (𝑧 lcm 𝑛)))
4842, 47breqtrrd 4814 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑦 ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛))
4948ex 397 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑦 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)))
50 elsni 4333 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ {𝑧} → 𝑖 = 𝑧)
5121, 3jca 501 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ((lcm𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ))
5251adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((lcm𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ))
53 dvdslcm 15519 . . . . . . . . . . . . . . . . . . . . . . . 24 (((lcm𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((lcm𝑦) ∥ ((lcm𝑦) lcm 𝑧) ∧ 𝑧 ∥ ((lcm𝑦) lcm 𝑧)))
5453simprd 483 . . . . . . . . . . . . . . . . . . . . . . 23 (((lcm𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) → 𝑧 ∥ ((lcm𝑦) lcm 𝑧))
5552, 54syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∥ ((lcm𝑦) lcm 𝑧))
56193adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm𝑦) ∈ ℕ0)
5756nn0zd 11682 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm𝑦) ∈ ℤ)
58 lcmcl 15522 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((lcm𝑦) ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((lcm𝑦) lcm 𝑧) ∈ ℕ0)
5957, 3, 58syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ((lcm𝑦) lcm 𝑧) ∈ ℕ0)
6059nn0zd 11682 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ((lcm𝑦) lcm 𝑧) ∈ ℤ)
61 dvdslcm 15519 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((lcm𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((lcm𝑦) lcm 𝑧) ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛) ∧ 𝑛 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)))
6261simpld 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((lcm𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((lcm𝑦) lcm 𝑧) ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛))
6360, 62sylan 569 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((lcm𝑦) lcm 𝑧) ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛))
6460adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((lcm𝑦) lcm 𝑧) ∈ ℤ)
65 lcmcl 15522 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((lcm𝑦) lcm 𝑧) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((lcm𝑦) lcm 𝑧) lcm 𝑛) ∈ ℕ0)
6660, 65sylan 569 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (((lcm𝑦) lcm 𝑧) lcm 𝑛) ∈ ℕ0)
6766nn0zd 11682 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (((lcm𝑦) lcm 𝑧) lcm 𝑛) ∈ ℤ)
68 dvdstr 15227 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ ℤ ∧ ((lcm𝑦) lcm 𝑧) ∈ ℤ ∧ (((lcm𝑦) lcm 𝑧) lcm 𝑛) ∈ ℤ) → ((𝑧 ∥ ((lcm𝑦) lcm 𝑧) ∧ ((lcm𝑦) lcm 𝑧) ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)) → 𝑧 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)))
694, 64, 67, 68syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑧 ∥ ((lcm𝑦) lcm 𝑧) ∧ ((lcm𝑦) lcm 𝑧) ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)) → 𝑧 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)))
7055, 63, 69mp2and 679 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑧 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛))
71 breq1 4789 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑧 → (𝑖 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛) ↔ 𝑧 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)))
7270, 71syl5ibr 236 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑧 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)))
7350, 72syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ {𝑧} → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)))
7449, 73jaoi 844 . . . . . . . . . . . . . . . . . 18 ((𝑖𝑦𝑖 ∈ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → 𝑖 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)))
7574imp 393 . . . . . . . . . . . . . . . . 17 (((𝑖𝑦𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → 𝑖 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛))
76 oveq1 6800 . . . . . . . . . . . . . . . . . 18 ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm𝑦) lcm 𝑧) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (((lcm𝑦) lcm 𝑧) lcm 𝑛))
7776breq2d 4798 . . . . . . . . . . . . . . . . 17 ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm𝑦) lcm 𝑧) → (𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ↔ 𝑖 ∥ (((lcm𝑦) lcm 𝑧) lcm 𝑛)))
7875, 77syl5ibrcom 237 . . . . . . . . . . . . . . . 16 (((𝑖𝑦𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → ((lcm‘(𝑦 ∪ {𝑧})) = ((lcm𝑦) lcm 𝑧) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
7912, 78syld 47 . . . . . . . . . . . . . . 15 (((𝑖𝑦𝑖 ∈ {𝑧}) ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ)) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
8079ex 397 . . . . . . . . . . . . . 14 ((𝑖𝑦𝑖 ∈ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
812, 80sylbi 207 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑦 ∪ {𝑧}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
82 elsni 4333 . . . . . . . . . . . . . 14 (𝑖 ∈ {𝑛} → 𝑖 = 𝑛)
83 simp2 1131 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ⊆ ℤ)
84 snssi 4474 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℤ → {𝑧} ⊆ ℤ)
85843ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → {𝑧} ⊆ ℤ)
8683, 85unssd 3940 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ⊆ ℤ)
87 simp3 1132 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin)
88 snfi 8194 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑧} ∈ Fin
89 unfi 8383 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
9087, 88, 89sylancl 574 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
91 lcmfcl 15549 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑦 ∪ {𝑧}) ∈ Fin) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
9286, 90, 91syl2anc 573 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
9392nn0zd 11682 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ)
9493anim1i 602 . . . . . . . . . . . . . . . . . . 19 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ))
9594adantr 466 . . . . . . . . . . . . . . . . . 18 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛)) → ((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ))
96 dvdslcm 15519 . . . . . . . . . . . . . . . . . 18 (((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((lcm‘(𝑦 ∪ {𝑧})) ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
9795, 96syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛)) → ((lcm‘(𝑦 ∪ {𝑧})) ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
9897simprd 483 . . . . . . . . . . . . . . . 16 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛)) → 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
99 breq1 4789 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → (𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ↔ 𝑛 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
10098, 99syl5ibr 236 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛)) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
101100expd 400 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
10282, 101syl 17 . . . . . . . . . . . . 13 (𝑖 ∈ {𝑛} → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
10381, 102jaoi 844 . . . . . . . . . . . 12 ((𝑖 ∈ (𝑦 ∪ {𝑧}) ∨ 𝑖 ∈ {𝑛}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
1041, 103sylbi 207 . . . . . . . . . . 11 (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
105104com13 88 . . . . . . . . . 10 (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
106105expd 400 . . . . . . . . 9 (∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛) → ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))))
107106adantl 467 . . . . . . . 8 ((∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛)) → ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))))
108107impcom 394 . . . . . . 7 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))) → (𝑛 ∈ ℤ → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))))
109108impcom 394 . . . . . 6 ((𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛)))) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
110109adantl 467 . . . . 5 (((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))))) → (𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → 𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛)))
111110ralrimiv 3114 . . . 4 (((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))))) → ∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
112 lcmfunsnlem2lem1 15559 . . . 4 (((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))))) → ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘))
113111, 112jca 501 . . 3 (((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))))) → (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘)))
11494adantr 466 . . . . . . . . . . 11 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ))
11586adantr 466 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑦 ∪ {𝑧}) ⊆ ℤ)
116115adantr 466 . . . . . . . . . . . . . . 15 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (𝑦 ∪ {𝑧}) ⊆ ℤ)
11790adantr 466 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → (𝑦 ∪ {𝑧}) ∈ Fin)
118117adantr 466 . . . . . . . . . . . . . . 15 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (𝑦 ∪ {𝑧}) ∈ Fin)
119 df-nel 3047 . . . . . . . . . . . . . . . . . . . . 21 (0 ∉ 𝑦 ↔ ¬ 0 ∈ 𝑦)
120119biimpi 206 . . . . . . . . . . . . . . . . . . . 20 (0 ∉ 𝑦 → ¬ 0 ∈ 𝑦)
1211203ad2ant1 1127 . . . . . . . . . . . . . . . . . . 19 ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ 𝑦)
122 elsni 4333 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ {𝑧} → 0 = 𝑧)
123122eqcomd 2777 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ {𝑧} → 𝑧 = 0)
124123necon3ai 2968 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ≠ 0 → ¬ 0 ∈ {𝑧})
1251243ad2ant2 1128 . . . . . . . . . . . . . . . . . . 19 ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ {𝑧})
126 ioran 964 . . . . . . . . . . . . . . . . . . 19 (¬ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧}) ↔ (¬ 0 ∈ 𝑦 ∧ ¬ 0 ∈ {𝑧}))
127121, 125, 126sylanbrc 572 . . . . . . . . . . . . . . . . . 18 ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧}))
128 elun 3904 . . . . . . . . . . . . . . . . . 18 (0 ∈ (𝑦 ∪ {𝑧}) ↔ (0 ∈ 𝑦 ∨ 0 ∈ {𝑧}))
129127, 128sylnibr 318 . . . . . . . . . . . . . . . . 17 ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ (𝑦 ∪ {𝑧}))
130 df-nel 3047 . . . . . . . . . . . . . . . . 17 (0 ∉ (𝑦 ∪ {𝑧}) ↔ ¬ 0 ∈ (𝑦 ∪ {𝑧}))
131129, 130sylibr 224 . . . . . . . . . . . . . . . 16 ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → 0 ∉ (𝑦 ∪ {𝑧}))
132131adantl 467 . . . . . . . . . . . . . . 15 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → 0 ∉ (𝑦 ∪ {𝑧}))
133 lcmfn0cl 15547 . . . . . . . . . . . . . . 15 (((𝑦 ∪ {𝑧}) ⊆ ℤ ∧ (𝑦 ∪ {𝑧}) ∈ Fin ∧ 0 ∉ (𝑦 ∪ {𝑧})) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ)
134116, 118, 132, 133syl3anc 1476 . . . . . . . . . . . . . 14 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (lcm‘(𝑦 ∪ {𝑧})) ∈ ℕ)
135134nnne0d 11267 . . . . . . . . . . . . 13 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (lcm‘(𝑦 ∪ {𝑧})) ≠ 0)
136135neneqd 2948 . . . . . . . . . . . 12 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬ (lcm‘(𝑦 ∪ {𝑧})) = 0)
137 df-ne 2944 . . . . . . . . . . . . . . 15 (𝑛 ≠ 0 ↔ ¬ 𝑛 = 0)
138137biimpi 206 . . . . . . . . . . . . . 14 (𝑛 ≠ 0 → ¬ 𝑛 = 0)
1391383ad2ant3 1129 . . . . . . . . . . . . 13 ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 𝑛 = 0)
140139adantl 467 . . . . . . . . . . . 12 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬ 𝑛 = 0)
141 ioran 964 . . . . . . . . . . . 12 (¬ ((lcm‘(𝑦 ∪ {𝑧})) = 0 ∨ 𝑛 = 0) ↔ (¬ (lcm‘(𝑦 ∪ {𝑧})) = 0 ∧ ¬ 𝑛 = 0))
142136, 140, 141sylanbrc 572 . . . . . . . . . . 11 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ¬ ((lcm‘(𝑦 ∪ {𝑧})) = 0 ∨ 𝑛 = 0))
143 lcmn0cl 15518 . . . . . . . . . . 11 ((((lcm‘(𝑦 ∪ {𝑧})) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ ¬ ((lcm‘(𝑦 ∪ {𝑧})) = 0 ∨ 𝑛 = 0)) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ)
144114, 142, 143syl2anc 573 . . . . . . . . . 10 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ)
145 snssi 4474 . . . . . . . . . . . . . 14 (𝑛 ∈ ℤ → {𝑛} ⊆ ℤ)
146145adantl 467 . . . . . . . . . . . . 13 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → {𝑛} ⊆ ℤ)
147115, 146unssd 3940 . . . . . . . . . . . 12 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ)
148147adantr 466 . . . . . . . . . . 11 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ)
14988, 89mpan2 671 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (𝑦 ∪ {𝑧}) ∈ Fin)
150 snfi 8194 . . . . . . . . . . . . . . 15 {𝑛} ∈ Fin
151 unfi 8383 . . . . . . . . . . . . . . 15 (((𝑦 ∪ {𝑧}) ∈ Fin ∧ {𝑛} ∈ Fin) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin)
152149, 150, 151sylancl 574 . . . . . . . . . . . . . 14 (𝑦 ∈ Fin → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin)
1531523ad2ant3 1129 . . . . . . . . . . . . 13 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin)
154153adantr 466 . . . . . . . . . . . 12 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin)
155154adantr 466 . . . . . . . . . . 11 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin)
156 elun 3904 . . . . . . . . . . . . . . . 16 (0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ (0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛}))
157 nnel 3055 . . . . . . . . . . . . . . . . . . . . 21 (¬ 0 ∉ 𝑦 ↔ 0 ∈ 𝑦)
158157biimpri 218 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ 𝑦 → ¬ 0 ∉ 𝑦)
1591583mix1d 1420 . . . . . . . . . . . . . . . . . . 19 (0 ∈ 𝑦 → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0))
160 nne 2947 . . . . . . . . . . . . . . . . . . . . 21 𝑧 ≠ 0 ↔ 𝑧 = 0)
161123, 160sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ {𝑧} → ¬ 𝑧 ≠ 0)
1621613mix2d 1421 . . . . . . . . . . . . . . . . . . 19 (0 ∈ {𝑧} → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0))
163159, 162jaoi 844 . . . . . . . . . . . . . . . . . 18 ((0 ∈ 𝑦 ∨ 0 ∈ {𝑧}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0))
164128, 163sylbi 207 . . . . . . . . . . . . . . . . 17 (0 ∈ (𝑦 ∪ {𝑧}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0))
165 elsni 4333 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ {𝑛} → 0 = 𝑛)
166165eqcomd 2777 . . . . . . . . . . . . . . . . . . 19 (0 ∈ {𝑛} → 𝑛 = 0)
167 nne 2947 . . . . . . . . . . . . . . . . . . 19 𝑛 ≠ 0 ↔ 𝑛 = 0)
168166, 167sylibr 224 . . . . . . . . . . . . . . . . . 18 (0 ∈ {𝑛} → ¬ 𝑛 ≠ 0)
1691683mix3d 1422 . . . . . . . . . . . . . . . . 17 (0 ∈ {𝑛} → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0))
170164, 169jaoi 844 . . . . . . . . . . . . . . . 16 ((0 ∈ (𝑦 ∪ {𝑧}) ∨ 0 ∈ {𝑛}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0))
171156, 170sylbi 207 . . . . . . . . . . . . . . 15 (0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0))
172 3ianor 1096 . . . . . . . . . . . . . . 15 (¬ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ↔ (¬ 0 ∉ 𝑦 ∨ ¬ 𝑧 ≠ 0 ∨ ¬ 𝑛 ≠ 0))
173171, 172sylibr 224 . . . . . . . . . . . . . 14 (0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) → ¬ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0))
174173con2i 136 . . . . . . . . . . . . 13 ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → ¬ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))
175 df-nel 3047 . . . . . . . . . . . . 13 (0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ↔ ¬ 0 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))
176174, 175sylibr 224 . . . . . . . . . . . 12 ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))
177176adantl 467 . . . . . . . . . . 11 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))
178148, 155, 1773jca 1122 . . . . . . . . . 10 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))
179144, 178jca 501 . . . . . . . . 9 ((((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) ∧ (0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0)) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))
180179ex 397 . . . . . . . 8 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑛 ∈ ℤ) → ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))))
181180ex 397 . . . . . . 7 ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) → (𝑛 ∈ ℤ → ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))))
182181adantr 466 . . . . . 6 (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))) → (𝑛 ∈ ℤ → ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))))
183182impcom 394 . . . . 5 ((𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛)))) → ((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛})))))
184183impcom 394 . . . 4 (((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))))
185 lcmf 15554 . . . 4 ((((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∈ ℕ ∧ (((𝑦 ∪ {𝑧}) ∪ {𝑛}) ⊆ ℤ ∧ ((𝑦 ∪ {𝑧}) ∪ {𝑛}) ∈ Fin ∧ 0 ∉ ((𝑦 ∪ {𝑧}) ∪ {𝑛}))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) ↔ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘))))
186184, 185syl 17 . . 3 (((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))))) → (((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) ↔ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ∧ ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘))))
187113, 186mpbird 247 . 2 (((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))))) → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) = (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})))
188187eqcomd 2777 1 (((0 ∉ 𝑦𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚𝑦 𝑚𝑘 → (lcm𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm𝑦) lcm 𝑛))))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 834  w3o 1070  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wnel 3046  wral 3061  cun 3721  wss 3723  {csn 4316   class class class wbr 4786  cfv 6031  (class class class)co 6793  Fincfn 8109  0cc0 10138  cle 10277  cn 11222  0cn0 11494  cz 11579  cdvds 15189   lcm clcm 15509  lcmclcmf 15510
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-rp 12036  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-prod 14843  df-dvds 15190  df-gcd 15425  df-lcm 15511  df-lcmf 15512
This theorem is referenced by:  lcmfunsnlem2  15561
  Copyright terms: Public domain W3C validator