---

Step * 1 1 1 2 2 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)
5. p:{  | let x,y = p 
              in GCD(n;m rem n;(x * n) + (y * (m rem n)))}
 p:{  | let x,y = p 
             in GCD(m;n;(x * m) + (y * n))}
BY
{ D 5 }

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)
5. p :   
6. [%8] : let x,y = p 
          in GCD(n;m rem n;(x * n) + (y * (m rem n)))
 p:{  | let x,y = p 
             in GCD(m;n;(x * m) + (y * n))}



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.  \mneg{}(n  =  0)
5.  \mexists{}p:\{\mBbbZ{}  \mtimes{}  \mBbbZ{}|  let  x,y  =  p 
                            in  GCD(n;m  rem  n;(x  *  n)  +  (y  *  (m  rem  n)))\}
\mvdash{}  \mexists{}p:\{\mBbbZ{}  \mtimes{}  \mBbbZ{}|  let  x,y  =  p 
                          in  GCD(m;n;(x  *  m)  +  (y  *  n))\}


By

D  5



Home Index