Step * 2 1 2 of Lemma divides-iff-gcd-assoced


1. : ℤ@i
2. : ℤ@i
3. gcd(x;y) x@i
4. gcd(x;y)@i
5. gcd(x;y) y
⊢ y
BY
(RelRST THEN Auto) }


Latex:


Latex:

1.  x  :  \mBbbZ{}@i
2.  y  :  \mBbbZ{}@i
3.  gcd(x;y)  |  x@i
4.  x  |  gcd(x;y)@i
5.  gcd(x;y)  |  y
\mvdash{}  x  |  y


By


Latex:
(RelRST  THEN  Auto)




Home Index