Step * of Lemma bezout_ident_n

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

1
1. : ℕ
2. ∀b:ℕb. ∀a:ℤ.  ∃u,v:ℤGCD(a;b;(u a) (v b))
3. : ℤ@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