---

Step * 1 1 1 2 2 of Lemma gcd_sq_exists_anne


1. n : @i
2. n1:n. m:.  (g:{| GCD(m;n1;g)})@i
3. m : @i
4. (n = 0)
5. g:{| GCD(n;m rem n;g)}
 g:{| GCD(m;n;g)}
BY
{ D 5 }

1
1. n : @i
2. n1:n. m:.  (g:{| GCD(m;n1;g)})@i
3. m : @i
4. (n = 0)
5. g : 
6. [%8] : GCD(n;m rem n;g)
 g:{| GCD(m;n;g)}



1.  n  :  \mBbbN{}@i
2.  \mforall{}n1:\mBbbN{}n.  \mforall{}m:\mBbbN{}.    (\mexists{}g:\{\mBbbN{}|  GCD(m;n1;g)\})@i
3.  m  :  \mBbbN{}@i
4.  \mneg{}(n  =  0)
5.  \mexists{}g:\{\mBbbN{}|  GCD(n;m  rem  n;g)\}
\mvdash{}  \mexists{}g:\{\mBbbN{}|  GCD(m;n;g)\}


By

D  5



Home Index