---

Step * of Lemma gcd-lcm-absorption

∀[n,m:ℕ].  (gcd(n;lcm(n;m)) = n ∈ ℤ)
BY
{ (Auto THEN Symmetry THEN BLemma `gcd-unique-nat` THEN Auto) }

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

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].    (gcd(n;lcm(n;m))  =  n)


By

---

Latex:
(Auto  THEN  Symmetry  THEN  BLemma  `gcd-unique-nat`  THEN  Auto)

---

Home Index