---

Step * 1 2 of Lemma lcm-assoc-nat


1. n : ℕ
2. m : ℕ
3. k : ℕ
4. lcm(n;m) | lcm(n;lcm(m;k))
⊢ k | lcm(n;lcm(m;k))
BY
{ (UseTrans ⌜lcm(m;k)⌝⋅ THEN Auto THEN BLemma `lcm-is-lcm-nat` ⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  k  :  \mBbbN{}
4.  lcm(n;m)  |  lcm(n;lcm(m;k))
\mvdash{}  k  |  lcm(n;lcm(m;k))


By

---

Latex:
(UseTrans  \mkleeneopen{}lcm(m;k)\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  BLemma  `lcm-is-lcm-nat`  \mcdot{}  THEN  Auto)

---

Home Index