---

Step * of Lemma bezout_ident_n

∀b:ℕ. ∀a:ℤ.  ∃u,v:ℤ. GCD(a;b;(u * a) + (v * b))
BY
{ (((D 0 THENM OnVar `b' CompNatInd) THENM D 0) THENA Auto) }

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

---

Latex:

---

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


By

---

Latex:
(((D  0  THENM  OnVar  `b'  CompNatInd)  THENM  D  0)  THENA  Auto)

---

Home Index