---

Step * of Lemma gcd-non-zero

∀a,b:ℤ.  ((a ≠ 0 ∨ b ≠ 0) ⇒ gcd(a;b) ≠ 0)
BY
{ (Auto
   THEN InstLemma `gcd-property` [⌜a⌝;⌜b⌝]⋅
   THEN Auto
   THEN ExRepD
   THEN Try (((D 0 THEN Auto) THEN Eliminate ⌜gcd(a;b)⌝⋅ THEN Auto'))) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    ((a  \mneq{}  0  \mvee{}  b  \mneq{}  0)  {}\mRightarrow{}  gcd(a;b)  \mneq{}  0)


By

---

Latex:
(Auto
  THEN  InstLemma  `gcd-property`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ExRepD
  THEN  Try  (((D  0  THEN  Auto)  THEN  Eliminate  \mkleeneopen{}gcd(a;b)\mkleeneclose{}\mcdot{}  THEN  Auto')))

---

Home Index