Euler's Theorem and Small Fermat's Theorem

Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

Euler's Theorem and Small Fermat's Theorem

Yoshinori Fujisawa: Shinshu University, Nagano
Yasushi Fuwa: Shinshu University, Nagano
Hidetaka Shimizu: Information Technology Research Institute, of Nagano Prefecture

Summary.

This article is concerned with Euler's theorem and small Fermat's theorem that play important roles in public-key cryptograms. In the first section, we present some selected theorems on integers. In the following section, we remake definitions about the finite sequence of natural, the function of natural times finite sequence of natural and $\pi$ of the finite sequence of natural. We also prove some basic theorems that concern these redefinitions. Next, we define the function of modulus for finite sequence of natural and some fundamental theorems about this function are proved. Finally, Euler's theorem and small Fermat's theorem are proved.

MML Identifier: EULER_2

The terminology and notation used in this paper have been introduced in the following articles [14] [17] [15] [1] [16] [13] [8] [2] [5] [12] [9] [11] [7] [18] [4] [6] [3] [10]

Contents (PDF format)

Preliminary
Finite Sequence of Naturals
Modulus for Finite Sequence of Naturals
Euler's Theorem and Small Fermat's Theorem

Acknowledgments

The authors wish to thank Professor A. Trybulec for all of his advice on this article.

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. Joining of decorated trees. Journal of Formalized Mathematics, 5, 1993.

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. Semigroup operations on finite subsets. Journal of Formalized Mathematics, 2, 1990.

[7] Czeslaw Bylinski. The sum and product of finite sequences of real numbers. Journal of Formalized Mathematics, 2, 1990.

[8] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[9] Yoshinori Fujisawa and Yasushi Fuwa. The Euler's function. Journal of Formalized Mathematics, 9, 1997.

[10] Andrzej Kondracki. The Chinese Remainder Theorem. Journal of Formalized Mathematics, 9, 1997.

[11] Jaroslaw Kotowicz. Functions and finite sequences of real numbers. Journal of Formalized Mathematics, 5, 1993.

[12] Rafal Kwiatek. Factorial and Newton coefficients. Journal of Formalized Mathematics, 2, 1990.

[13] Rafal Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Journal of Formalized Mathematics, 2, 1990.

[14] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[15] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[16] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[17] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[18] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received June 10, 1998

[ Download a postscript version, MML identifier index, Mizar home page]