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