---

Step * 1 of Lemma gcd_sat_gcd_p

.....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))
BY
{ (((Assert 0 < |b| BY ((RWO "absval_unfold" 0 THENA Auto) THEN AutoSplit)) THEN (Assert |a rem b| < |b| BY Auto))
   THEN (InstHyp [⌜d - 1⌝;⌜b⌝;⌜a rem b⌝] 2⋅ THENA Auto)⋅
   ) }

1
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 ∈ ℤ)
7. 0 < |b|
8. |a rem b| < |b|
9. GCD(b;a rem b;gcd(b;a rem b))
⊢ GCD(a;b;gcd(b;a rem b))

---

Latex:

---

Latex:
.....falsecase..... 
1.  d  :  \mBbbN{}
2.  \mforall{}d:\mBbbN{}d.  \mforall{}a,b:\mBbbZ{}.    ((|b|  \mleq{}  d)  {}\mRightarrow{}  GCD(a;b;gcd(a;b)))
3.  a  :  \mBbbZ{}
4.  b  :  \mBbbZ{}
5.  |b|  \mleq{}  d
6.  \mneg{}(b  =  0)
\mvdash{}  GCD(a;b;gcd(b;a  rem  b))


By

---

Latex:
(((Assert  0  <  |b|  BY
                  ((RWO  "absval\_unfold"  0  THENA  Auto)  THEN  AutoSplit))
    THEN  (Assert  |a  rem  b|  <  |b|  BY
                            Auto)
    )
  THEN  (InstHyp  [\mkleeneopen{}d  -  1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a  rem  b\mkleeneclose{}]  2\mcdot{}  THENA  Auto)\mcdot{}
  )

---

Home Index