---

Step * of Lemma lcm-is-lcm-nat

∀n,m:ℕ.  (((n | lcm(n;m)) ∧ (m | lcm(n;m))) ∧ (∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (lcm(n;m) | v))))
BY
{ ((D 0 THENA Auto) THEN CaseNat 0 `n') }

1
1. n : ℕ
2. n = 0 ∈ ℤ
⊢ ∀m:ℕ. (((0 | lcm(0;m)) ∧ (m | lcm(0;m))) ∧ (∀v:ℤ. ((0 | v) ⇒ (m | v) ⇒ (lcm(0;m) | v))))

2
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
⊢ ∀m:ℕ. (((n | lcm(n;m)) ∧ (m | lcm(n;m))) ∧ (∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (lcm(n;m) | v))))

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbN{}.    (((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:
((D  0  THENA  Auto)  THEN  CaseNat  0  `n')

---

Home Index