---

Step * 1 1 1 1 1 1 of Lemma bezout_sq_exists_anne


1. n : @i
2. n1:n. m:.  (p:{  | let x,y = p in GCD(m;n1;(x * m) + (y * n1))})@i
3. m : @i
4. n = 0
 let x,y = <1, 0> 
  in GCD(m;0;(x * m) + (y * 0))
BY
{ Reduce 0 }

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



1.  n  :  \mBbbN{}@i
2.  \mforall{}n1:\mBbbN{}n.  \mforall{}m:\mBbbN{}.    (\mexists{}p:\{\mBbbZ{}  \mtimes{}  \mBbbZ{}|  let  x,y  =  p  in  GCD(m;n1;(x  *  m)  +  (y  *  n1))\})@i
3.  m  :  \mBbbN{}@i
4.  n  =  0
\mvdash{}  let  x,y  =  ə,  0> 
    in  GCD(m;0;(x  *  m)  +  (y  *  0))


By

Reduce  0



Home Index