---

Step * of Lemma bezout_sq_exists_anne

n,m:.  (p:{  | let x,y = p in GCD(m;n;(x * m) + (y * n))})
BY
{ (D 0 THENA Auto) }

1
1. n : @i
 m:. (p:{  | let x,y = p in GCD(m;n;(x * m) + (y * n))})


\mforall{}n,m:\mBbbN{}.    (\mexists{}p:\{\mBbbZ{}  \mtimes{}  \mBbbZ{}|  let  x,y  =  p  in  GCD(m;n;(x  *  m)  +  (y  *  n))\})


By

(D  0  THENA  Auto)



Home Index