Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
The Divisibility of Integers and Integer Relatively Primes

Rafal Kwiatek

Warsaw University, Bialystok

Grzegorz Zwara

Nicolaus Copernicus University, Torun
Summary.

We introduce the following notions:
1) the least common multiple of two integers
($\mathop{\rm lcm}(i,j)$),
2) the greatest common divisor of two integers
($\mathop{\rm gcd}(i,j)$),
3) the relative prime integer numbers,
4) the prime numbers.
A few facts concerning the
above items, among them a socalled Fundamental Theorem
of Arithmetic, are introduced.
Supported by RPBP.III24.B5.
MML Identifier:
INT_2
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[3]
[2]
[4]
[1]
[5]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [4]
Michal J. Trybulec.
Integers.
Journal of Formalized Mathematics,
2, 1990.
 [5]
Wojciech A. Trybulec.
Groups.
Journal of Formalized Mathematics,
2, 1990.
 [6]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received July 10, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]