<abstract xmlns="http://www.w3.org/1999/xhtml">The article is the next in a series aiming to formalize the MDPR-theorem using the Mizar proof assistant [3], [6], [4]. We analyze four equations from the Diophantine standpoint that are crucial in the bounded quantifier theorem, that is used in one of the approaches to solve the problem.Based on our previous work [1], 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<disp-formula><alternatives><graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2019-0019_eq_001.png"></graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mrow><mi>z</mi><mo>=</mo><munderover><mo>∏</mo><mrow><mi>i</mi><mo>=</mo><mn>1</mn></mrow><mi>x</mi></munderover><mrow><mrow><mo>(</mo><mrow><mn>1</mn><mo>+</mo><mi>i</mi><mo>⋅</mo><mi>y</mi></mrow><mo>)</mo></mrow><mo>,</mo><mi> </mi><mi> </mi><mi> </mi><mi> </mi><mi> </mi><mi> </mi><mi> </mi><mi> </mi></mrow><mi>z</mi><mo>=</mo><munderover><mo>∏</mo><mrow><mi>i</mi><mo>=</mo><mn>1</mn></mrow><mi>x</mi></munderover><mrow><mrow><mo>(</mo><mrow><mi>y</mi><mo>+</mo><mn>1</mn><mo>-</mo><mi>j</mi></mrow><mo>)</mo></mrow><mo>,</mo><mi> </mi><mi> </mi><mi> </mi><mi> </mi><mi> </mi><mi> </mi><mo>(</mo><mn>0.1</mn><mo>)</mo></mrow></mrow></math><tex-math>$$z = \prod\limits_{i = 1}^x {\left( {1 + i \cdot y} \right),\,\,\,\,\,\,\,\,} z = \prod\limits_{i = 1}^x {\left( {y + 1 - j} \right),\,\,\,\,\,\,(0.1)} $$</tex-math></alternatives></disp-formula>where <italic>y > x</italic> are Diophantine.The formalization follows [10], Z. Adamowicz, P. Zbierski [2] as well as M. Davis [5].</abstract>

The article is the next in a series aiming to formalize the MDPR-theorem using the Mizar proof assistant [3], [6], [4]. We analyze four equations from the Diophantine standpoint that are crucial in the bounded quantifier theorem, that is used in one of the approaches to solve the problem.Based on our previous work [1], 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 productsz=∏i=1x(1+i⋅y),        z=∏i=1x(y+1-j),      (0.1)$$z = \prod\limits_{i = 1}^x {\left( {1 + i \cdot y} \right),\,\,\,\,\,\,\,\,} z = \prod\limits_{i = 1}^x {\left( {y + 1 - j} \right),\,\,\,\,\,\,(0.1)} $$where y > x are Diophantine.The formalization follows [10], Z. Adamowicz, P. Zbierski [2] as well as M. Davis [5].

Diophantine Sets. Part II

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

{"article-title":"Diophantine Sets. Part II"}

The article is the next in a series aiming to formalize the MDPR-theorem using the Mizar proof assistant [3], [6], [4]. We analyze four equations from the...

Diophantine Sets. Part II

Publicado en línea: 20 jul 2019

Páginas: 197 - 208

Aceptado: 27 may 2019

DOI: https://doi.org/10.2478/forma-2019-0019

Palabras clave
Hilbert’s 10th problem, Diophantine relations

© 2019 Karol Pąk, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Diophantine Sets. Part II

Publicado en línea: 20 jul 2019

Páginas: 197 - 208

Aceptado: 27 may 2019

DOI: https://doi.org/10.2478/forma-2019-0019

Palabras claveHilbert’s 10th problem, Diophantine relations

© 2019 Karol Pąk, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Palabras clave
Hilbert’s 10th problem, Diophantine relations