---

Step * 1 1 1 1 1 1 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
 GCD(m;0;m)
BY
{ (InstLemma `gcd_p_zero` [m] THENA Auto) }

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



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.  n  =  0
\mvdash{}  GCD(m;0;m)


By

(InstLemma  `gcd\_p\_zero`  [\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)



Home Index