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 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