---

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


1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
⊢ ∀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 `m') }

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

2
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)))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mneg{}(n  =  0)
\mvdash{}  \mforall{}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  `m')

---

Home Index