---

Step * 2 2 of Lemma lcm-is-lcm-nat


1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. m : ℕ
4. ¬(m = 0 ∈ ℤ)
⊢ ((n | lcm(n;m)) ∧ (m | lcm(n;m))) ∧ (∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (lcm(n;m) | v)))
BY
{ (InstLemma `lcm-is-lcm` [⌜n⌝;⌜m⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mneg{}(n  =  0)
3.  m  :  \mBbbN{}
4.  \mneg{}(m  =  0)
\mvdash{}  ((n  |  lcm(n;m))  \mwedge{}  (m  |  lcm(n;m)))  \mwedge{}  (\mforall{}v:\mBbbZ{}.  ((n  |  v)  {}\mRightarrow{}  (m  |  v)  {}\mRightarrow{}  (lcm(n;m)  |  v)))


By

---

Latex:
(InstLemma  `lcm-is-lcm`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index