---

Step * 1 1 of Lemma gcd_sat_gcd_p


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))
BY
{ (ThinVar `d' THEN Thin (-2)) }

1
1. a : ℤ
2. b : ℤ
3. ¬(b = 0 ∈ ℤ)
4. 0 < |b|
5. GCD(b;a rem b;gcd(b;a rem b))
⊢ GCD(a;b;gcd(b;a rem b))

---

Latex:

---

Latex:

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)
7.  0  <  |b|
8.  |a  rem  b|  <  |b|
9.  GCD(b;a  rem  b;gcd(b;a  rem  b))
\mvdash{}  GCD(a;b;gcd(b;a  rem  b))


By

---

Latex:
(ThinVar  `d'  THEN  Thin  (-2))

---

Home Index