---

Step * of Lemma gcd_wf

∀a,b:ℤ.  (gcd(a;b) ∈ ℤ)
BY
{ (Assert ∀k:ℕ. ∀a,b:ℤ.  (|b| < k ⇒ (gcd(a;b) ∈ ℤ)) BY
         (InductionOnNat
          THEN (Auto THEN (Assert 0 ≤ |b| BY Auto) THEN Auto)
          THEN RecUnfold `gcd` 0
          THEN AutoSplit
          THEN BackThruSomeHyp
          THEN InstLemma `rem_bounds_z` [⌜a⌝;⌜b⌝]⋅
          THEN Auto)) }

1
1. ∀k:ℕ. ∀a,b:ℤ.  (|b| < k ⇒ (gcd(a;b) ∈ ℤ))
⊢ ∀a,b:ℤ.  (gcd(a;b) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    (gcd(a;b)  \mmember{}  \mBbbZ{})


By

---

Latex:
(Assert  \mforall{}k:\mBbbN{}.  \mforall{}a,b:\mBbbZ{}.    (|b|  <  k  {}\mRightarrow{}  (gcd(a;b)  \mmember{}  \mBbbZ{}))  BY
              (InductionOnNat
                THEN  (Auto  THEN  (Assert  0  \mleq{}  |b|  BY  Auto)  THEN  Auto)
                THEN  RecUnfold  `gcd`  0
                THEN  AutoSplit
                THEN  BackThruSomeHyp
                THEN  InstLemma  `rem\_bounds\_z`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
                THEN  Auto))

---

Home Index