http://hdl.handle.net/11320/11406 2026-06-01T20:20:21Z http://hdl.handle.net/11320/11413 Tytuł: Elementary Number Theory Problems. Part II Autorzy: Korniłowicz, Artur; Surowik, Dariusz Abstrakt: In this paper problems 14, 15, 29, 30, 34, 78, 83, 97, and 116 from [6] are formalized, using the Mizar formalism [1], [2], [3]. Some properties related to the divisibility of prime numbers were proved. It has been shown that the equation of the form p2 + 1 = q2 + r2, where p, q, r are prime numbers, has at least four solutions and it has been proved that at least five primes can be represented as the sum of two fourth powers of integers. We also proved that for at least one positive integer, the sum of the fourth powers of this number and its successor is a composite number. And finally, it has been shown that there are infinitely many odd numbers k greater than zero such that all numbers of the form 22n + k (n = 1, 2, . . . ) are composite. 2021-01-01T00:00:00Z http://hdl.handle.net/11320/11411 Tytuł: Functional Space Consisted by Continuous Functions on Topological Space Autorzy: Yamazaki, Hiroshi; Miyajima, Keiichi; Shidama, Yasunari Abstrakt: In this article, using the Mizar system [1], [2], first we give a definition of a functional space which is constructed from all continuous functions defined on a compact topological space [5]. We prove that this functional space is a Banach space [3]. Next, we give a definition of a function space which is constructed from all continuous functions with bounded support. We also prove that this function space is a normed space. 2021-01-01T00:00:00Z http://hdl.handle.net/11320/11410 Tytuł: Algebraic Extensions Autorzy: Schwarzweller, Christoph; Rowińska-Schwarzweller, Agnieszka Abstrakt: In this article we further develop field theory in Mizar [1], [2], [3] towards splitting fields. We deal with algebraic extensions [4], [5]: a field extension E of a field F is algebraic, if every element of E is algebraic over F. We prove amongst others that finite extensions are algebraic and that field extensions generated by a finite set of algebraic elements are finite. From this immediately follows that field extensions generated by roots of a polynomial over F are both finite and algebraic. We also define the field of algebraic elements of E over F and show that this field is an intermediate field of E|F. 2021-01-01T00:00:00Z http://hdl.handle.net/11320/11409 Tytuł: Miscellaneous Graph Preliminaries. Part I Autorzy: Koch, Sebastian Abstrakt: This article contains many auxiliary theorems which were missing in the Mizar Mathematical Library to the best of the author’s knowledge. Most of them regard graph theory as formalized in the GLIB series and are needed in upcoming articles. 2021-01-01T00:00:00Z