---

Step * 2 of Lemma bezout_ident


1. a : ℤ@i
2. b : ℤ@i
3. ¬(0 ≤ b)
⊢ ∃u,v:ℤ. GCD(a;b;(u * a) + (v * b))
BY
{ ((InstLemma `bezout_ident_n` [⌜-b⌝;⌜a⌝] THENM ExRepD) THEN Auto) }

1
1. a : ℤ@i
2. b : ℤ@i
3. ¬(0 ≤ b)
4. u : ℤ
5. v : ℤ
6. GCD(a;-b;(u * a) + (v * (-b)))
⊢ ∃u,v:ℤ. GCD(a;b;(u * a) + (v * b))

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  b  :  \mBbbZ{}@i
3.  \mneg{}(0  \mleq{}  b)
\mvdash{}  \mexists{}u,v:\mBbbZ{}.  GCD(a;b;(u  *  a)  +  (v  *  b))


By

---

Latex:
((InstLemma  `bezout\_ident\_n`  [\mkleeneopen{}-b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  THENM  ExRepD)  THEN  Auto)

---

Home Index