---

Step * of Lemma lcm-is-lcm

∀n,m:ℕ+.  (((n | lcm(n;m)) ∧ (m | lcm(n;m))) ∧ (∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (lcm(n;m) | v))))
BY
{ (Auto THEN (InstLemma `lcm-property` [⌜n⌝;⌜m⌝]⋅ THENA Auto) THEN ExRepD) }

1
1. n : ℕ+
2. m : ℕ+
3. a : ℤ
4. b : ℤ
5. CoPrime(a,b)
6. (n * b) = lcm(n;m) ∈ ℤ
7. (m * a) = lcm(n;m) ∈ ℤ
⊢ n | lcm(n;m)

2
1. n : ℕ+
2. m : ℕ+
3. n | lcm(n;m)
4. a : ℤ
5. b : ℤ
6. CoPrime(a,b)
7. (n * b) = lcm(n;m) ∈ ℤ
8. (m * a) = lcm(n;m) ∈ ℤ
⊢ m | lcm(n;m)

3
1. n : ℕ+
2. m : ℕ+
3. n | lcm(n;m)
4. m | lcm(n;m)
5. v : ℤ
6. n | v
7. m | v
8. a : ℤ
9. b : ℤ
10. CoPrime(a,b)
11. (n * b) = lcm(n;m) ∈ ℤ
12. (m * a) = lcm(n;m) ∈ ℤ
⊢ lcm(n;m) | v

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbN{}\msupplus{}.    (((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:
(Auto  THEN  (InstLemma  `lcm-property`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index