---

Step * 1 2 1 1 of Lemma div_rem_gcd_anne


1. m : @i
2. n : @i
3. g : @i
4. (g | n)  (g | (m rem n))  (z:. (((z | n)  (z | (m rem n)))  (z | g)))@i
 (g | m)  (g | n)  (z:. (((z | m)  (z | n))  (z | g)))
BY
{ D 4 }

1
1. m : @i
2. n : @i
3. g : @i
4. g | n@i
5. (g | (m rem n))  (z:. (((z | n)  (z | (m rem n)))  (z | g)))@i
 (g | m)  (g | n)  (z:. (((z | m)  (z | n))  (z | g)))



1.  m  :  \mBbbZ{}@i
2.  n  :  \mBbbZ{}\msupminus{}\msupzero{}@i
3.  g  :  \mBbbZ{}@i
4.  (g  |  n)  \mwedge{}  (g  |  (m  rem  n))  \mwedge{}  (\mforall{}z:\mBbbZ{}.  (((z  |  n)  \mwedge{}  (z  |  (m  rem  n)))  {}\mRightarrow{}  (z  |  g)))@i
\mvdash{}  (g  |  m)  \mwedge{}  (g  |  n)  \mwedge{}  (\mforall{}z:\mBbbZ{}.  (((z  |  m)  \mwedge{}  (z  |  n))  {}\mRightarrow{}  (z  |  g)))


By

D  4



Home Index