---

Step * 1 of Lemma lcm-assoc-nat


1. n : ℕ
2. m : ℕ
3. k : ℕ
⊢ lcm(n;lcm(m;k)) = lcm(lcm(n;m);k) ∈ ℤ
BY
{ (BLemma `lcm-unique-nat` THEN Auto THEN (Repeat (BLemma `lcm-is-lcm-nat` ⋅) THENA Auto)) }

1
1. n : ℕ
2. m : ℕ
3. k : ℕ
⊢ m | lcm(n;lcm(m;k))

2
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. lcm(n;m) | lcm(n;lcm(m;k))
⊢ k | lcm(n;lcm(m;k))

3
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. lcm(n;m) | lcm(n;lcm(m;k))
5. k | lcm(n;lcm(m;k))
6. v : ℤ@i
7. lcm(n;m) | v@i
8. k | v@i
⊢ n | v

4
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. lcm(n;m) | lcm(n;lcm(m;k))
5. k | lcm(n;lcm(m;k))
6. v : ℤ@i
7. lcm(n;m) | v@i
8. k | v@i
⊢ m | v

5
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. lcm(n;m) | lcm(n;lcm(m;k))
5. k | lcm(n;lcm(m;k))
6. v : ℤ@i
7. lcm(n;m) | v@i
8. k | v@i
⊢ k | v

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  k  :  \mBbbN{}
\mvdash{}  lcm(n;lcm(m;k))  =  lcm(lcm(n;m);k)


By

---

Latex:
(BLemma  `lcm-unique-nat`  THEN  Auto  THEN  (Repeat  (BLemma  `lcm-is-lcm-nat`  \mcdot{})  THENA  Auto))

---

Home Index