---

Step * of Lemma lcm-unique-nat

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

1
1. n : ℕ
2. m : ℕ
3. l : ℕ
4. n | l
5. m | l
6. ∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (l | v))
7. n = 0 ∈ ℤ
⊢ l = lcm(0;m) ∈ ℤ

2
1. n : ℕ
2. m : ℕ
3. l : ℕ
4. n | l
5. m | l
6. ∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (l | v))
7. ¬(n = 0 ∈ ℤ)
⊢ l = lcm(n;m) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}n,m,l:\mBbbN{}.    ((((n  |  l)  \mwedge{}  (m  |  l))  \mwedge{}  (\mforall{}v:\mBbbZ{}.  ((n  |  v)  {}\mRightarrow{}  (m  |  v)  {}\mRightarrow{}  (l  |  v))))  {}\mRightarrow{}  (l  =  lcm(n;m)))


By

---

Latex:
(Auto  THEN  CaseNat  0  `n')

---

Home Index