---

Step * of Lemma bezout_ident

∀a,b:ℤ.  ∃u,v:ℤ. GCD(a;b;(u * a) + (v * b))
BY
{ ((UnivCD THENM Decide ⌜0 ≤ b⌝) THENA Auto) }

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

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

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    \mexists{}u,v:\mBbbZ{}.  GCD(a;b;(u  *  a)  +  (v  *  b))


By

---

Latex:
((UnivCD  THENM  Decide  \mkleeneopen{}0  \mleq{}  b\mkleeneclose{})  THENA  Auto)

---

Home Index