Step
*
1
of Lemma
bezout_sq_exists_anne
1. n :
@i
m:
. (
p:{
| let x,y = p in GCD(m;n;(x * m) + (y * n))})
BY
{ (GeneralNatInd 1 THENA Auto) }
1
1. n :
@i
2.
n1:
n.
m:
. (
p:{
| let x,y = p in GCD(m;n1;(x * m) + (y * n1))})@i
m:
. (
p:{
| let x,y = p in GCD(m;n;(x * m) + (y * n))})
1. n : \mBbbN{}@i
\mvdash{} \mforall{}m:\mBbbN{}. (\mexists{}p:\{\mBbbZ{} \mtimes{} \mBbbZ{}| let x,y = p in GCD(m;n;(x * m) + (y * n))\})
By
(GeneralNatInd 1 THENA Auto)
Home
Index