---

Step * 1 1 1 of Lemma gcd_sat_gcd_p


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))
BY
{ (SeqOnM [RWN 1 (LemmaC `rem_to_div`) 5 ;Using [`k',⌜a ÷ b⌝] (FLemma `gcd_p_shift` [5]) ;RW IntNormC 6] THENA Auto) }

1
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))

---

Latex:

---

Latex:

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


By

---

Latex:
(SeqOnM
  [RWN  1  (LemmaC  `rem\_to\_div`)  5
  ;Using  [`k',\mkleeneopen{}a  \mdiv{}  b\mkleeneclose{}]  (FLemma  `gcd\_p\_shift`  [5])
  ;RW  IntNormC  6]
  THENA  Auto
  )

---

Home Index