@MISC{HILB10_4.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {Diophantine Sets -- Preliminaries},
   SECTION1 = {Product of zero based finite sequences},
  SECTION2 = {Binomial is Diophantin}
  SECTION3 = {Factorial is Diophantin},
  SECTION4 = {Diophanticity of selected products},
  SECTION5 = {Selected subsets of zero based finite sequences of $\mathbb{N}$ as diophantine sets},
  DAY = {27},
  MONTH = {May},
  YEAR = {2019},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {The article is the next in a series aiming to formalize
  the MDPR-theorem using the Mizar proof assistant.
  We analyze four equations from the diophantine standpoint that are crucial in the bounded quantifier   theorem,
  that is used in one of approaches to solve the problem.
  \par
  Based on our previous work \cite{HILB10_3.ABS}, we prove that
  the value of a given binomial coefficient and factorial
  can be determined by its arguments in a diophantine way.
  Then we prove that two products \begin{equation}z = \displaystyle\prod_{i=1}^{x}(1+i\cdot y),
  \mkern50mu
  z = \displaystyle\prod_{i=1}^{x}(y +1 -j),\end{equation} where $y>x$ are Diophantin.
  \par The formalization follows Z. Adamowicz, P. Zbierski
   \cite{AdamowiczZbierski} as well as M. Davis \cite{Hilbert10}.}
  }
