---

Step * 1 1 1 1 of Lemma gcd_sat_gcd_p


1. a : ℤ
2. b : ℤ
3. ¬(b = 0 ∈ ℤ)
4. 0 < |b|
5. GCD(b;a - (a ÷ b) * b;gcd(b;a rem b))
6. GCD(b;a;gcd(b;a rem b))
⊢ GCD(a;b;gcd(b;a rem b))
BY
{ (BLemma `gcd_p_sym` THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  \mneg{}(b  =  0)
4.  0  <  |b|
5.  GCD(b;a  -  (a  \mdiv{}  b)  *  b;gcd(b;a  rem  b))
6.  GCD(b;a;gcd(b;a  rem  b))
\mvdash{}  GCD(a;b;gcd(b;a  rem  b))


By

---

Latex:
(BLemma  `gcd\_p\_sym`  THEN  Auto)\mcdot{}

---

Home Index