---

Step * 1 of Lemma gcd_sq_exists_anne


1. n : @i
 m:. (g:{| GCD(m;n;g)})
BY
{ (GeneralNatInd 1 THENA Auto) }

1
1. n : @i
2. n1:n. m:.  (g:{| GCD(m;n1;g)})@i
 m:. (g:{| GCD(m;n;g)})



1.  n  :  \mBbbN{}@i
\mvdash{}  \mforall{}m:\mBbbN{}.  (\mexists{}g:\{\mBbbN{}|  GCD(m;n;g)\})


By

(GeneralNatInd  1  THENA  Auto)



Home Index