---

Step * of Lemma gcd_sat_gcd_p

∀a,b:ℤ.  GCD(a;b;gcd(a;b))
BY
{ (InductionOn ⌜|b|⌝ CompNatInd⋅ THEN Auto THEN RecCaseSplit `gcd` THEN Auto THEN Try ((HypSubst' (-1) 0⋅ THEN Auto))) }

1
.....falsecase..... 
1. d : ℕ
2. ∀d:ℕd. ∀a,b:ℤ.  ((|b| ≤ d) ⇒ GCD(a;b;gcd(a;b)))
3. a : ℤ
4. b : ℤ
5. |b| ≤ d
6. ¬(b = 0 ∈ ℤ)
⊢ GCD(a;b;gcd(b;a rem b))

---

Latex:

---

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


By

---

Latex:
(InductionOn  \mkleeneopen{}|b|\mkleeneclose{}  CompNatInd\mcdot{}
  THEN  Auto
  THEN  RecCaseSplit  `gcd`
  THEN  Auto
  THEN  Try  ((HypSubst'  (-1)  0\mcdot{}  THEN  Auto)))

---

Home Index