---

Step * 1 of Lemma gcd_wf


1. ∀k:ℕ. ∀a,b:ℤ.  (|b| < k ⇒ (gcd(a;b) ∈ ℤ))
⊢ ∀a,b:ℤ.  (gcd(a;b) ∈ ℤ)
BY
{ ((Auto THEN (Assert 0 ≤ |b| BY Auto)) THEN InstHyp [⌜|b| + 1⌝;⌜a⌝;⌜b⌝] 1⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}k:\mBbbN{}.  \mforall{}a,b:\mBbbZ{}.    (|b|  <  k  {}\mRightarrow{}  (gcd(a;b)  \mmember{}  \mBbbZ{}))
\mvdash{}  \mforall{}a,b:\mBbbZ{}.    (gcd(a;b)  \mmember{}  \mBbbZ{})


By

---

Latex:
((Auto  THEN  (Assert  0  \mleq{}  |b|  BY  Auto))  THEN  InstHyp  [\mkleeneopen{}|b|  +  1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  1\mcdot{}  THEN  Auto)

---

Home Index